Lax Lean Archive

Isomorphism from a multigraph to a simple graph

Lax683916.MultigraphIsomorphism · concepts/Lax683916/MultigraphIsomorphism.lean · lax-683916

definition

Loading review…

Community review

Flags

Each flag is tied to a public ORCID identity and explains why this concept may be incorrect.

No flags have been submitted.

    Community review

    Flag this concept

    State precisely what appears incorrect. This explanation will be public under your ORCID name.

    No source line selected.

    Natural Language Statement

    Definition

    A multigraph and a simple graph are isomorphic when their actual vertex and edge sets are in bijection and these bijections preserve endpoints.

    Concept map
    1 concept; 2 descendants hidden
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

    Lean source view on GitHub

    1import Mathlib.Combinatorics.Graph.Simple
    2
    3/-!
    4---
    5title: Isomorphism from a multigraph to a simple graph
    6type: definition
    7---
    8A multigraph and a simple graph are isomorphic when their actual vertex and
    9edge sets are in bijection and these bijections preserve endpoints.
    10
    11# Formalization notes
    12
    13`Graph α β` stores vertex and edge sets inside ambient types, whereas
    14`SimpleGraph V` takes the vertex type itself as its vertex set and represents
    15edges canonically as unordered pairs. The comparison therefore uses
    16equivalences between the subtypes `G.vertexSet` and `G.edgeSet`, not between
    17the ambient types `α`, `β` and the canonical carriers.
    18-/
    19
    20namespace Lax683916.MultigraphIsomorphism
    21
    22/-- An incidence-preserving vertex-and-edge isomorphism from a multigraph to a simple graph. -/
    23structure IsomorphicToSimpleGraph {α β V : Type*} (G : Graph α β) (H : SimpleGraph V) where
    24 /-- The bijection between the actual vertices of the two graphs. -/
    25 vertexEquiv : G.vertexSet ≃ V
    26 /-- The bijection between the actual edges of the two graphs. -/
    27 edgeEquiv : G.edgeSet ≃ H.edgeSet
    28 /-- The vertex and edge bijections preserve the endpoint relation. -/
    29 map_isLink : ∀ (e : G.edgeSet) (u v : G.vertexSet),
    30 G.IsLink e.1 u.1 v.1 ↔
    31 (edgeEquiv e).1 = s(vertexEquiv u, vertexEquiv v)
    32
    33end Lax683916.MultigraphIsomorphism
    34
    Formalization notes

    GraphαβGraph α β stores vertex and edge sets inside ambient types, whereas SimpleGraphVSimpleGraph V takes the vertex type itself as its vertex set and represents edges canonically as unordered pairs. The comparison therefore uses equivalences between the subtypes G.vertexSetG.vertexSet and G.edgeSetG.edgeSet, not between the ambient types αα, ββ and the canonical carriers.

    Builds on

    none

    Used by
    From Mathlib

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…