Documentation

Mathlib.Combinatorics.SimpleGraph.Maps

Maps between graphs #

This file defines two functions and three structures relating graphs. The structures directly correspond to the classification of functions as injective, surjective and bijective, and have corresponding notation.

Main definitions #

Note that a graph embedding is a stronger notion than an injective graph homomorphism, since its image is an induced subgraph.

Implementation notes #

Morphisms of graphs are abbreviations for RelHom, RelEmbedding and RelIso. To make use of pre-existing simp lemmas, definitions involving morphisms are abbreviations as well.

Map and comap #

def SimpleGraph.map {V : Type u_1} {W : Type u_2} (f : V W) (G : SimpleGraph V) :

Given an injective function, there is a covariant induced map on graphs by pushing forward the adjacency relation.

This is injective (see SimpleGraph.map_injective).

Equations
Instances For
    instance SimpleGraph.instDecidableMapAdj {V : Type u_1} {W : Type u_2} (G : SimpleGraph V) {f : V W} {a : W} {b : W} [Decidable (Relation.Map G.Adj (⇑f) (⇑f) a b)] :
    Decidable ((SimpleGraph.map f G).Adj a b)
    Equations
    • G.instDecidableMapAdj = inst
    @[simp]
    theorem SimpleGraph.map_adj {V : Type u_1} {W : Type u_2} (f : V W) (G : SimpleGraph V) (u : W) (v : W) :
    (SimpleGraph.map f G).Adj u v ∃ (u' : V) (v' : V), G.Adj u' v' f u' = u f v' = v
    theorem SimpleGraph.map_adj_apply {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {f : V W} {a : V} {b : V} :
    (SimpleGraph.map f G).Adj (f a) (f b) G.Adj a b
    theorem SimpleGraph.map_monotone {V : Type u_1} {W : Type u_2} (f : V W) :
    @[simp]
    theorem SimpleGraph.map_map {V : Type u_1} {W : Type u_2} {X : Type u_3} (G : SimpleGraph V) (f : V W) (g : W X) :
    def SimpleGraph.comap {V : Type u_1} {W : Type u_2} (f : VW) (G : SimpleGraph W) :

    Given a function, there is a contravariant induced map on graphs by pulling back the adjacency relation. This is one of the ways of creating induced graphs. See SimpleGraph.induce for a wrapper.

    This is surjective when f is injective (see SimpleGraph.comap_surjective).

    Equations
    • SimpleGraph.comap f G = { Adj := fun (u v : V) => G.Adj (f u) (f v), symm := , loopless := }
    Instances For
      @[simp]
      theorem SimpleGraph.comap_adj {V : Type u_1} {W : Type u_2} {u : V} {v : V} {G : SimpleGraph W} {f : VW} :
      (SimpleGraph.comap f G).Adj u v G.Adj (f u) (f v)
      @[simp]
      theorem SimpleGraph.comap_id {V : Type u_1} {G : SimpleGraph V} :
      @[simp]
      theorem SimpleGraph.comap_comap {V : Type u_1} {W : Type u_2} {X : Type u_3} {G : SimpleGraph X} (f : VW) (g : WX) :
      instance SimpleGraph.instDecidableComapAdj {V : Type u_1} {W : Type u_2} (f : VW) (G : SimpleGraph W) [DecidableRel G.Adj] :
      Equations
      theorem SimpleGraph.comap_symm {V : Type u_1} {W : Type u_2} (G : SimpleGraph V) (e : V W) :
      SimpleGraph.comap (⇑e.symm.toEmbedding) G = SimpleGraph.map e.toEmbedding G
      theorem SimpleGraph.map_symm {V : Type u_1} {W : Type u_2} (G : SimpleGraph W) (e : V W) :
      SimpleGraph.map e.symm.toEmbedding G = SimpleGraph.comap (⇑e.toEmbedding) G
      theorem SimpleGraph.comap_monotone {V : Type u_1} {W : Type u_2} (f : V W) :
      @[simp]
      theorem SimpleGraph.comap_map_eq {V : Type u_1} {W : Type u_2} (f : V W) (G : SimpleGraph V) :
      theorem SimpleGraph.map_le_iff_le_comap {V : Type u_1} {W : Type u_2} (f : V W) (G : SimpleGraph V) (G' : SimpleGraph W) :
      theorem SimpleGraph.map_comap_le {V : Type u_1} {W : Type u_2} (f : V W) (G : SimpleGraph W) :
      theorem SimpleGraph.le_comap_of_subsingleton {V : Type u_1} {W : Type u_2} (G : SimpleGraph V) (G' : SimpleGraph W) (f : VW) [Subsingleton V] :
      theorem SimpleGraph.map_le_of_subsingleton {V : Type u_1} {W : Type u_2} (G : SimpleGraph V) (G' : SimpleGraph W) (f : V W) [Subsingleton V] :
      @[reducible, inline]
      abbrev SimpleGraph.completeMultipartiteGraph {ι : Type u_4} (V : ιType u_5) :
      SimpleGraph ((i : ι) × V i)

      Given a family of vertex types indexed by ι, pulling back from ⊤ : SimpleGraph ι yields the complete multipartite graph on the family. Two vertices are adjacent if and only if their indices are not equal.

      Equations
      Instances For
        @[simp]
        theorem Equiv.simpleGraph_apply {V : Type u_1} {W : Type u_2} (e : V W) (G : SimpleGraph V) :
        e.simpleGraph G = SimpleGraph.comap (⇑e.symm) G
        def Equiv.simpleGraph {V : Type u_1} {W : Type u_2} (e : V W) :

        Equivalent types have equivalent simple graphs.

        Equations
        Instances For
          @[simp]
          theorem Equiv.simpleGraph_refl {V : Type u_1} :
          (Equiv.refl V).simpleGraph = Equiv.refl (SimpleGraph V)
          @[simp]
          theorem Equiv.simpleGraph_trans {V : Type u_1} {W : Type u_2} {X : Type u_3} (e₁ : V W) (e₂ : W X) :
          (e₁.trans e₂).simpleGraph = e₁.simpleGraph.trans e₂.simpleGraph
          @[simp]
          theorem Equiv.symm_simpleGraph {V : Type u_1} {W : Type u_2} (e : V W) :
          e.simpleGraph.symm = e.symm.simpleGraph

          Induced graphs #

          @[reducible, inline]
          abbrev SimpleGraph.induce {V : Type u_1} (s : Set V) (G : SimpleGraph V) :

          Restrict a graph to the vertices in the set s, deleting all edges incident to vertices outside the set. This is a wrapper around SimpleGraph.comap.

          Equations
          Instances For
            @[simp]
            @[reducible, inline]
            abbrev SimpleGraph.spanningCoe {V : Type u_1} {s : Set V} (G : SimpleGraph s) :

            Given a graph on a set of vertices, we can make it be a SimpleGraph V by adding in the remaining vertices without adding in any additional edges. This is a wrapper around SimpleGraph.map.

            Equations
            Instances For
              theorem SimpleGraph.induce_spanningCoe {V : Type u_1} {s : Set V} {G : SimpleGraph s} :
              SimpleGraph.induce s G.spanningCoe = G
              theorem SimpleGraph.spanningCoe_induce_le {V : Type u_1} (G : SimpleGraph V) (s : Set V) :
              (SimpleGraph.induce s G).spanningCoe G

              Homomorphisms, embeddings and isomorphisms #

              @[reducible, inline]
              abbrev SimpleGraph.Hom {V : Type u_1} {W : Type u_2} (G : SimpleGraph V) (G' : SimpleGraph W) :
              Type (max u_1 u_2)

              A graph homomorphism is a map on vertex sets that respects adjacency relations.

              The notation G →g G' represents the type of graph homomorphisms.

              Equations
              Instances For
                @[reducible, inline]
                abbrev SimpleGraph.Embedding {V : Type u_1} {W : Type u_2} (G : SimpleGraph V) (G' : SimpleGraph W) :
                Type (max u_1 u_2)

                A graph embedding is an embedding f such that for vertices v w : V, G.Adj (f v) (f w) ↔ G.Adj v w. Its image is an induced subgraph of G'.

                The notation G ↪g G' represents the type of graph embeddings.

                Equations
                Instances For
                  @[reducible, inline]
                  abbrev SimpleGraph.Iso {V : Type u_1} {W : Type u_2} (G : SimpleGraph V) (G' : SimpleGraph W) :
                  Type (max u_1 u_2)

                  A graph isomorphism is a bijective map on vertex sets that respects adjacency relations.

                  The notation G ≃g G' represents the type of graph isomorphisms.

                  Equations
                  Instances For

                    A graph homomorphism is a map on vertex sets that respects adjacency relations.

                    The notation G →g G' represents the type of graph homomorphisms.

                    Equations
                    Instances For

                      A graph embedding is an embedding f such that for vertices v w : V, G.Adj (f v) (f w) ↔ G.Adj v w. Its image is an induced subgraph of G'.

                      The notation G ↪g G' represents the type of graph embeddings.

                      Equations
                      Instances For

                        A graph isomorphism is a bijective map on vertex sets that respects adjacency relations.

                        The notation G ≃g G' represents the type of graph isomorphisms.

                        Equations
                        Instances For
                          @[reducible, inline]
                          abbrev SimpleGraph.Hom.id {V : Type u_1} {G : SimpleGraph V} :
                          G →g G

                          The identity homomorphism from a graph to itself.

                          Equations
                          Instances For
                            @[simp]
                            theorem SimpleGraph.Hom.coe_id {V : Type u_1} {G : SimpleGraph V} :
                            SimpleGraph.Hom.id = id
                            instance SimpleGraph.Hom.instSubsingletonOfForall {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W} [Subsingleton (VW)] :
                            Equations
                            • =
                            instance SimpleGraph.Hom.instUniqueOfIsEmpty {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W} [IsEmpty V] :
                            Unique (G →g H)
                            Equations
                            • SimpleGraph.Hom.instUniqueOfIsEmpty = { default := { toFun := fun (a : V) => isEmptyElim a, map_rel' := }, uniq := }
                            instance SimpleGraph.Hom.instFinite {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W} [Finite V] [Finite W] :
                            Finite (G →g H)
                            Equations
                            • =
                            theorem SimpleGraph.Hom.map_adj {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G →g G') {v : V} {w : V} (h : G.Adj v w) :
                            G'.Adj (f v) (f w)
                            theorem SimpleGraph.Hom.map_mem_edgeSet {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G →g G') {e : Sym2 V} (h : e G.edgeSet) :
                            Sym2.map (⇑f) e G'.edgeSet
                            theorem SimpleGraph.Hom.apply_mem_neighborSet {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G →g G') {v : V} {w : V} (h : w G.neighborSet v) :
                            f w G'.neighborSet (f v)
                            @[simp]
                            theorem SimpleGraph.Hom.mapEdgeSet_coe {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G →g G') (e : G.edgeSet) :
                            (f.mapEdgeSet e) = Sym2.map f e
                            def SimpleGraph.Hom.mapEdgeSet {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G →g G') (e : G.edgeSet) :
                            G'.edgeSet

                            The map between edge sets induced by a homomorphism. The underlying map on edges is given by Sym2.map.

                            Equations
                            • f.mapEdgeSet e = Sym2.map f e,
                            Instances For
                              @[simp]
                              theorem SimpleGraph.Hom.mapNeighborSet_coe {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G →g G') (v : V) (w : (G.neighborSet v)) :
                              (f.mapNeighborSet v w) = f w
                              def SimpleGraph.Hom.mapNeighborSet {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G →g G') (v : V) (w : (G.neighborSet v)) :
                              (G'.neighborSet (f v))

                              The map between neighbor sets induced by a homomorphism.

                              Equations
                              • f.mapNeighborSet v w = f w,
                              Instances For
                                def SimpleGraph.Hom.mapDart {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G →g G') (d : G.Dart) :
                                G'.Dart

                                The map between darts induced by a homomorphism.

                                Equations
                                • f.mapDart d = { toProd := Prod.map (⇑f) (⇑f) d.toProd, adj := }
                                Instances For
                                  @[simp]
                                  theorem SimpleGraph.Hom.mapDart_apply {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G →g G') (d : G.Dart) :
                                  f.mapDart d = { toProd := Prod.map (⇑f) (⇑f) d.toProd, adj := }
                                  @[simp]
                                  def SimpleGraph.Hom.mapSpanningSubgraphs {V : Type u_1} {G : SimpleGraph V} {G' : SimpleGraph V} (h : G G') :
                                  G →g G'

                                  The induced map for spanning subgraphs, which is the identity on vertices.

                                  Equations
                                  Instances For
                                    theorem SimpleGraph.Hom.mapEdgeSet.injective {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G →g G') (hinj : Function.Injective f) :
                                    Function.Injective f.mapEdgeSet
                                    theorem SimpleGraph.Hom.injective_of_top_hom {V : Type u_1} {W : Type u_2} {G' : SimpleGraph W} (f : →g G') :

                                    Every graph homomorphism from a complete graph is injective.

                                    @[simp]
                                    theorem SimpleGraph.Hom.comap_apply {V : Type u_1} {W : Type u_2} (f : VW) (G : SimpleGraph W) :
                                    ∀ (a : V), (SimpleGraph.Hom.comap f G) a = f a
                                    def SimpleGraph.Hom.comap {V : Type u_1} {W : Type u_2} (f : VW) (G : SimpleGraph W) :

                                    There is a homomorphism to a graph from a comapped graph. When the function is injective, this is an embedding (see SimpleGraph.Embedding.comap).

                                    Equations
                                    Instances For
                                      @[reducible, inline]
                                      abbrev SimpleGraph.Hom.comp {V : Type u_1} {W : Type u_2} {X : Type u_3} {G : SimpleGraph V} {G' : SimpleGraph W} {G'' : SimpleGraph X} (f' : G' →g G'') (f : G →g G') :
                                      G →g G''

                                      Composition of graph homomorphisms.

                                      Equations
                                      Instances For
                                        @[simp]
                                        theorem SimpleGraph.Hom.coe_comp {V : Type u_1} {W : Type u_2} {X : Type u_3} {G : SimpleGraph V} {G' : SimpleGraph W} {G'' : SimpleGraph X} (f' : G' →g G'') (f : G →g G') :
                                        (f'.comp f) = f' f
                                        def SimpleGraph.Hom.ofLE {V : Type u_1} {G₁ : SimpleGraph V} {G₂ : SimpleGraph V} (h : G₁ G₂) :
                                        G₁ →g G₂

                                        The graph homomorphism from a smaller graph to a bigger one.

                                        Equations
                                        Instances For
                                          @[simp]
                                          theorem SimpleGraph.Hom.coe_ofLE {V : Type u_1} {G₁ : SimpleGraph V} {G₂ : SimpleGraph V} (h : G₁ G₂) :
                                          @[reducible, inline]
                                          abbrev SimpleGraph.Embedding.refl {V : Type u_1} {G : SimpleGraph V} :
                                          G ↪g G

                                          The identity embedding from a graph to itself.

                                          Equations
                                          Instances For
                                            @[reducible, inline]
                                            abbrev SimpleGraph.Embedding.toHom {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G ↪g G') :
                                            G →g G'

                                            An embedding of graphs gives rise to a homomorphism of graphs.

                                            Equations
                                            Instances For
                                              @[simp]
                                              theorem SimpleGraph.Embedding.coe_toHom {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W} (f : G ↪g H) :
                                              f.toHom = f
                                              @[simp]
                                              theorem SimpleGraph.Embedding.map_adj_iff {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G ↪g G') {v : V} {w : V} :
                                              G'.Adj (f v) (f w) G.Adj v w
                                              theorem SimpleGraph.Embedding.map_mem_edgeSet_iff {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G ↪g G') {e : Sym2 V} :
                                              Sym2.map (⇑f) e G'.edgeSet e G.edgeSet
                                              theorem SimpleGraph.Embedding.apply_mem_neighborSet_iff {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G ↪g G') {v : V} {w : V} :
                                              f w G'.neighborSet (f v) w G.neighborSet v
                                              @[simp]
                                              theorem SimpleGraph.Embedding.mapEdgeSet_apply {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G ↪g G') (e : G.edgeSet) :
                                              def SimpleGraph.Embedding.mapEdgeSet {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G ↪g G') :
                                              G.edgeSet G'.edgeSet

                                              A graph embedding induces an embedding of edge sets.

                                              Equations
                                              Instances For
                                                @[simp]
                                                theorem SimpleGraph.Embedding.mapNeighborSet_apply_coe {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G ↪g G') (v : V) (w : (G.neighborSet v)) :
                                                ((f.mapNeighborSet v) w) = f w
                                                def SimpleGraph.Embedding.mapNeighborSet {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G ↪g G') (v : V) :
                                                (G.neighborSet v) (G'.neighborSet (f v))

                                                A graph embedding induces an embedding of neighbor sets.

                                                Equations
                                                • f.mapNeighborSet v = { toFun := fun (w : (G.neighborSet v)) => f w, , inj' := }
                                                Instances For
                                                  def SimpleGraph.Embedding.comap {V : Type u_1} {W : Type u_2} (f : V W) (G : SimpleGraph W) :

                                                  Given an injective function, there is an embedding from the comapped graph into the original graph.

                                                  Equations
                                                  Instances For
                                                    @[simp]
                                                    theorem SimpleGraph.Embedding.comap_apply {V : Type u_1} {W : Type u_2} (f : V W) (G : SimpleGraph W) (v : V) :
                                                    def SimpleGraph.Embedding.map {V : Type u_1} {W : Type u_2} (f : V W) (G : SimpleGraph V) :

                                                    Given an injective function, there is an embedding from a graph into the mapped graph.

                                                    Equations
                                                    Instances For
                                                      @[simp]
                                                      theorem SimpleGraph.Embedding.map_apply {V : Type u_1} {W : Type u_2} (f : V W) (G : SimpleGraph V) (v : V) :
                                                      @[reducible, inline]

                                                      Induced graphs embed in the original graph.

                                                      Note that if G.induce s = ⊤ (i.e., if s is a clique) then this gives the embedding of a complete graph.

                                                      Equations
                                                      Instances For
                                                        @[reducible, inline]
                                                        abbrev SimpleGraph.Embedding.spanningCoe {V : Type u_1} {s : Set V} (G : SimpleGraph s) :
                                                        G ↪g G.spanningCoe

                                                        Graphs on a set of vertices embed in their spanningCoe.

                                                        Equations
                                                        Instances For
                                                          def SimpleGraph.Embedding.completeGraph {α : Type u_4} {β : Type u_5} (f : α β) :

                                                          Embeddings of types induce embeddings of complete graphs on those types.

                                                          Equations
                                                          Instances For
                                                            @[simp]
                                                            theorem SimpleGraph.Embedding.coe_completeGraph {α : Type u_4} {β : Type u_5} (f : α β) :
                                                            @[reducible, inline]
                                                            abbrev SimpleGraph.Embedding.comp {V : Type u_1} {W : Type u_2} {X : Type u_3} {G : SimpleGraph V} {G' : SimpleGraph W} {G'' : SimpleGraph X} (f' : G' ↪g G'') (f : G ↪g G') :
                                                            G ↪g G''

                                                            Composition of graph embeddings.

                                                            Equations
                                                            Instances For
                                                              @[simp]
                                                              theorem SimpleGraph.Embedding.coe_comp {V : Type u_1} {W : Type u_2} {X : Type u_3} {G : SimpleGraph V} {G' : SimpleGraph W} {G'' : SimpleGraph X} (f' : G' ↪g G'') (f : G ↪g G') :
                                                              (f'.comp f) = f' f
                                                              def SimpleGraph.induceHom {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {G' : SimpleGraph W} {s : Set V} {t : Set W} (φ : G →g G') (φst : Set.MapsTo (⇑φ) s t) :

                                                              The restriction of a morphism of graphs to induced subgraphs.

                                                              Equations
                                                              Instances For
                                                                @[simp]
                                                                theorem SimpleGraph.coe_induceHom {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {G' : SimpleGraph W} {s : Set V} {t : Set W} (φ : G →g G') (φst : Set.MapsTo (⇑φ) s t) :
                                                                (SimpleGraph.induceHom φ φst) = Set.MapsTo.restrict (⇑φ) s t φst
                                                                @[simp]
                                                                theorem SimpleGraph.induceHom_id {V : Type u_1} (G : SimpleGraph V) (s : Set V) :
                                                                SimpleGraph.induceHom SimpleGraph.Hom.id = SimpleGraph.Hom.id
                                                                @[simp]
                                                                theorem SimpleGraph.induceHom_comp {V : Type u_1} {W : Type u_2} {X : Type u_3} {G : SimpleGraph V} {G' : SimpleGraph W} {G'' : SimpleGraph X} {s : Set V} {t : Set W} {r : Set X} (φ : G →g G') (φst : Set.MapsTo (⇑φ) s t) (ψ : G' →g G'') (ψtr : Set.MapsTo (⇑ψ) t r) :
                                                                (SimpleGraph.induceHom ψ ψtr).comp (SimpleGraph.induceHom φ φst) = SimpleGraph.induceHom (ψ.comp φ)
                                                                theorem SimpleGraph.induceHom_injective {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {G' : SimpleGraph W} {s : Set V} {t : Set W} (φ : G →g G') (φst : Set.MapsTo (⇑φ) s t) (hi : Set.InjOn (⇑φ) s) :
                                                                def SimpleGraph.induceHomOfLE {V : Type u_1} (G : SimpleGraph V) {s : Set V} {s' : Set V} (h : s s') :

                                                                Given an inclusion of vertex subsets, the induced embedding on induced graphs. This is not an abbreviation for induceHom since we get an embedding in this case.

                                                                Equations
                                                                • G.induceHomOfLE h = { toEmbedding := s.embeddingOfSubset s' h, map_rel_iff' := }
                                                                Instances For
                                                                  @[simp]
                                                                  theorem SimpleGraph.induceHomOfLE_apply {V : Type u_1} (G : SimpleGraph V) {s : Set V} {s' : Set V} (h : s s') (v : s) :
                                                                  (G.induceHomOfLE h) v = Set.inclusion h v
                                                                  @[simp]
                                                                  theorem SimpleGraph.induceHomOfLE_toHom {V : Type u_1} (G : SimpleGraph V) {s : Set V} {s' : Set V} (h : s s') :
                                                                  (G.induceHomOfLE h).toHom = SimpleGraph.induceHom SimpleGraph.Hom.id
                                                                  @[reducible, inline]
                                                                  abbrev SimpleGraph.Iso.refl {V : Type u_1} {G : SimpleGraph V} :
                                                                  G ≃g G

                                                                  The identity isomorphism of a graph with itself.

                                                                  Equations
                                                                  Instances For
                                                                    @[reducible, inline]
                                                                    abbrev SimpleGraph.Iso.toEmbedding {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G ≃g G') :
                                                                    G ↪g G'

                                                                    An isomorphism of graphs gives rise to an embedding of graphs.

                                                                    Equations
                                                                    Instances For
                                                                      @[reducible, inline]
                                                                      abbrev SimpleGraph.Iso.toHom {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G ≃g G') :
                                                                      G →g G'

                                                                      An isomorphism of graphs gives rise to a homomorphism of graphs.

                                                                      Equations
                                                                      • f.toHom = f.toEmbedding.toHom
                                                                      Instances For
                                                                        @[reducible, inline]
                                                                        abbrev SimpleGraph.Iso.symm {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G ≃g G') :
                                                                        G' ≃g G

                                                                        The inverse of a graph isomorphism.

                                                                        Equations
                                                                        Instances For
                                                                          theorem SimpleGraph.Iso.map_adj_iff {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G ≃g G') {v : V} {w : V} :
                                                                          G'.Adj (f v) (f w) G.Adj v w
                                                                          theorem SimpleGraph.Iso.map_mem_edgeSet_iff {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G ≃g G') {e : Sym2 V} :
                                                                          Sym2.map (⇑f) e G'.edgeSet e G.edgeSet
                                                                          theorem SimpleGraph.Iso.apply_mem_neighborSet_iff {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G ≃g G') {v : V} {w : V} :
                                                                          f w G'.neighborSet (f v) w G.neighborSet v
                                                                          @[simp]
                                                                          theorem SimpleGraph.Iso.mapEdgeSet_symm_apply {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G ≃g G') (e : G'.edgeSet) :
                                                                          f.mapEdgeSet.symm e = SimpleGraph.Hom.mapEdgeSet (RelIso.toRelEmbedding f.symm).toRelHom e
                                                                          @[simp]
                                                                          theorem SimpleGraph.Iso.mapEdgeSet_apply {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G ≃g G') (e : G.edgeSet) :
                                                                          f.mapEdgeSet e = SimpleGraph.Hom.mapEdgeSet (RelIso.toRelEmbedding f).toRelHom e
                                                                          def SimpleGraph.Iso.mapEdgeSet {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G ≃g G') :
                                                                          G.edgeSet G'.edgeSet

                                                                          An isomorphism of graphs induces an equivalence of edge sets.

                                                                          Equations
                                                                          • One or more equations did not get rendered due to their size.
                                                                          Instances For
                                                                            @[simp]
                                                                            theorem SimpleGraph.Iso.mapNeighborSet_apply_coe {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G ≃g G') (v : V) (w : (G.neighborSet v)) :
                                                                            ((f.mapNeighborSet v) w) = f w
                                                                            @[simp]
                                                                            theorem SimpleGraph.Iso.mapNeighborSet_symm_apply_coe {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G ≃g G') (v : V) (w : (G'.neighborSet (f v))) :
                                                                            ((f.mapNeighborSet v).symm w) = f.symm w
                                                                            def SimpleGraph.Iso.mapNeighborSet {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G ≃g G') (v : V) :
                                                                            (G.neighborSet v) (G'.neighborSet (f v))

                                                                            A graph isomorphism induces an equivalence of neighbor sets.

                                                                            Equations
                                                                            • f.mapNeighborSet v = { toFun := fun (w : (G.neighborSet v)) => f w, , invFun := fun (w : (G'.neighborSet (f v))) => f.symm w, , left_inv := , right_inv := }
                                                                            Instances For
                                                                              theorem SimpleGraph.Iso.card_eq {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G ≃g G') [Fintype V] [Fintype W] :
                                                                              def SimpleGraph.Iso.comap {V : Type u_1} {W : Type u_2} (f : V W) (G : SimpleGraph W) :
                                                                              SimpleGraph.comap (⇑f.toEmbedding) G ≃g G

                                                                              Given a bijection, there is an embedding from the comapped graph into the original graph.

                                                                              Equations
                                                                              Instances For
                                                                                @[simp]
                                                                                theorem SimpleGraph.Iso.comap_apply {V : Type u_1} {W : Type u_2} (f : V W) (G : SimpleGraph W) (v : V) :
                                                                                @[simp]
                                                                                theorem SimpleGraph.Iso.comap_symm_apply {V : Type u_1} {W : Type u_2} (f : V W) (G : SimpleGraph W) (w : W) :
                                                                                (SimpleGraph.Iso.comap f G).symm w = f.symm w
                                                                                def SimpleGraph.Iso.map {V : Type u_1} {W : Type u_2} (f : V W) (G : SimpleGraph V) :
                                                                                G ≃g SimpleGraph.map f.toEmbedding G

                                                                                Given an injective function, there is an embedding from a graph into the mapped graph.

                                                                                Equations
                                                                                Instances For
                                                                                  @[simp]
                                                                                  theorem SimpleGraph.Iso.map_apply {V : Type u_1} {W : Type u_2} (f : V W) (G : SimpleGraph V) (v : V) :
                                                                                  @[simp]
                                                                                  theorem SimpleGraph.Iso.map_symm_apply {V : Type u_1} {W : Type u_2} (f : V W) (G : SimpleGraph V) (w : W) :
                                                                                  (SimpleGraph.Iso.map f G).symm w = f.symm w
                                                                                  def SimpleGraph.Iso.completeGraph {α : Type u_4} {β : Type u_5} (f : α β) :

                                                                                  Equivalences of types induce isomorphisms of complete graphs on those types.

                                                                                  Equations
                                                                                  Instances For
                                                                                    @[reducible, inline]
                                                                                    abbrev SimpleGraph.Iso.comp {V : Type u_1} {W : Type u_2} {X : Type u_3} {G : SimpleGraph V} {G' : SimpleGraph W} {G'' : SimpleGraph X} (f' : G' ≃g G'') (f : G ≃g G') :
                                                                                    G ≃g G''

                                                                                    Composition of graph isomorphisms.

                                                                                    Equations
                                                                                    Instances For
                                                                                      @[simp]
                                                                                      theorem SimpleGraph.Iso.coe_comp {V : Type u_1} {W : Type u_2} {X : Type u_3} {G : SimpleGraph V} {G' : SimpleGraph W} {G'' : SimpleGraph X} (f' : G' ≃g G'') (f : G ≃g G') :
                                                                                      (f'.comp f) = f' f
                                                                                      @[simp]
                                                                                      theorem SimpleGraph.induceUnivIso_symm_apply_coe {V : Type u_1} (G : SimpleGraph V) (a : V) :
                                                                                      ((RelIso.symm G.induceUnivIso) a) = a
                                                                                      @[simp]
                                                                                      theorem SimpleGraph.induceUnivIso_apply {V : Type u_1} (G : SimpleGraph V) (self : { x : V // x Set.univ }) :
                                                                                      G.induceUnivIso self = self

                                                                                      The graph induced on Set.univ is isomorphic to the original graph.

                                                                                      Equations
                                                                                      Instances For
                                                                                        def SimpleGraph.overFin {V : Type u_1} (G : SimpleGraph V) [Fintype V] {n : } (hc : Fintype.card V = n) :

                                                                                        Given a graph over a finite vertex type V and a proof hc that Fintype.card V = n, G.overFin n is an isomorphic (as shown in overFinIso) graph over Fin n.

                                                                                        Equations
                                                                                        Instances For
                                                                                          noncomputable def SimpleGraph.overFinIso {V : Type u_1} (G : SimpleGraph V) [Fintype V] {n : } (hc : Fintype.card V = n) :
                                                                                          G ≃g G.overFin hc

                                                                                          The isomorphism between G and G.overFin hc.

                                                                                          Equations
                                                                                          Instances For