Documentation

TauCeti.Combinatorics.SimpleGraph.Cohomology.Relabel

Relabelling graph cohomology #

A graph isomorphism transports one-cochains by evaluating at inverse-image darts. This transport sends vertex coboundaries to vertex coboundaries and therefore induces an isomorphism on first cohomology. The construction is useful when graph-indexed algebraic parameters are classified by their cohomology classes.

source
def SimpleGraph.oneCochainsRelabel {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W} (A : Type u_3) [CommGroup A] (e : G ≃g H) :
↥(G.oneCochains A) ≃* ↥(H.oneCochains A)

Relabel a graph one-cochain along an isomorphism of graphs.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem SimpleGraph.oneCochainsRelabel_apply {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W} (A : Type u_3) [CommGroup A] (e : G ≃g H) (σ : ↥(G.oneCochains A)) (d : H.Dart) :
    ↑((oneCochainsRelabel A e) σ) d = ↑σ (e.symm.toHom.mapDart d)

    Relabelling a one-cochain evaluates it on the inverse-image dart.

    source
    @[simp]
    theorem SimpleGraph.oneCochainsRelabel_refl {V : Type u_1} {G : SimpleGraph V} (A : Type u_3) [CommGroup A] :
    oneCochainsRelabel A Iso.refl = MulEquiv.refl ↥(G.oneCochains A)

    Relabelling by the identity graph isomorphism fixes every one-cochain.

    source
    theorem SimpleGraph.oneCochainsRelabel_comp {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W} (A : Type u_3) [CommGroup A] {X : Type u_4} {I : SimpleGraph X} (e : G ≃g H) (f : H ≃g I) :
    oneCochainsRelabel A (f.comp e) = (oneCochainsRelabel A e).trans (oneCochainsRelabel A f)

    Successive graph relabellings compose on one-cochains.

    source
    @[simp]
    theorem SimpleGraph.oneCochainsRelabel_coboundary {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W} (A : Type u_3) [CommGroup A] (e : G ≃g H) (φ : V → A) :
    (oneCochainsRelabel A e) ((G.coboundary A) φ) = (H.coboundary A) (φ ∘ ⇑e.symm)

    Relabelling carries the coboundary of a vertex function to the coboundary of its inverse-image relabelling.

    source
    def SimpleGraph.firstCohomologyRelabel {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W} (A : Type u_3) [CommGroup A] (e : G ≃g H) :
    G.FirstCohomology A ≃* H.FirstCohomology A

    A graph isomorphism identifies the first cohomology groups of its two graphs.

    Equations
    Instances For
      source
      @[simp]
      theorem SimpleGraph.firstCohomologyRelabel_mk {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W} (A : Type u_3) [CommGroup A] (e : G ≃g H) (σ : ↥(G.oneCochains A)) :
      (firstCohomologyRelabel A e) ((FirstCohomology.mk G A) σ) = (FirstCohomology.mk H A) ((oneCochainsRelabel A e) σ)

      The relabelling isomorphism takes the class of a cochain to the class of its relabelling.

      source
      @[simp]
      theorem SimpleGraph.firstCohomologyRelabel_refl {V : Type u_1} {G : SimpleGraph V} (A : Type u_3) [CommGroup A] :
      firstCohomologyRelabel A Iso.refl = MulEquiv.refl (G.FirstCohomology A)

      Relabelling by the identity graph isomorphism fixes every cohomology class.

      source
      theorem SimpleGraph.firstCohomologyRelabel_comp {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W} (A : Type u_3) [CommGroup A] {X : Type u_4} {I : SimpleGraph X} (e : G ≃g H) (f : H ≃g I) :
      firstCohomologyRelabel A (f.comp e) = (firstCohomologyRelabel A e).trans (firstCohomologyRelabel A f)

      Successive graph relabellings compose on first cohomology.