Documentation

TauCeti.RepresentationTheory.Homological.ContCohomology.TrivialF2.Character

The degree-one class of a continuous homomorphism to 𝔽₂ #

With trivial 𝔽₂ coefficients, continuous first cohomology is the group of continuous homomorphisms to 𝔽₂: a continuous 1-cocycle for the trivial action is a homomorphism, and there are no nonzero coboundaries. This file names the class homClass H α of a continuous homomorphism α : H → 𝔽₂ in Mathlib's continuousCohomology 1 (trivialF2 H), identifies it with the TopRep.cochainClass of the homogeneous cochain of α, and shows that homClass is a bijection from continuous homomorphisms onto degree-one classes that turns multiplication of homomorphisms into addition of classes.

Main definitions #

Main results #

References #

Source note #

The definition of homClass in the explicit model and its injectivity follow the earlier Tau Ceti formalization in TauCeti PR #11157 by @mccorvie-agent ("feat: descend the index-two Evens norm").

source
noncomputable def TauCeti.ContCohomology.evensHomCocycle {G : Type u} [Group G] [TopologicalSpace G] (y : G →* Multiplicative (ZMod 2)) (hy : Continuous ⇑y) :
↥(Z1 G ↑(trivialF2 G))

A continuous homomorphism y : G →* Multiplicative (ZMod 2), as a continuous 1-cocycle of G with coefficients in the lifted trivial 𝔽₂ object trivialF2 G. Its restriction to a subgroup U is evensHomCocycleAmbient U (y.comp U.subtype).

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem TauCeti.ContCohomology.coe_evensHomCocycle {G : Type u} [Group G] [TopologicalSpace G] (y : G →* Multiplicative (ZMod 2)) (hy : Continuous ⇑y) :
    ↑(evensHomCocycle y hy) = fun (g : G) => (trivialF2Equiv G).symm (Multiplicative.toAdd (y g))

    The underlying cochain of evensHomCocycle.

    source
    theorem TauCeti.ContCohomology.continuousSMul_trivialF2_homClass (H : Type u) [Group H] [TopologicalSpace H] [IsTopologicalGroup H] :
    ContinuousSMul H ↑(trivialF2 H)

    H acts continuously on the trivial coefficients 𝔽₂, which are smooth discrete.

    source
    noncomputable def TauCeti.ContCohomology.homClass (H : Type u) [Group H] [TopologicalSpace H] [IsTopologicalGroup H] (α : H →* Multiplicative (ZMod 2)) (hα : Continuous ⇑α) :
    ↑(continuousCohomology 1 (trivialF2 H)).toModuleCat

    The class of a continuous homomorphism α : H → 𝔽₂ in continuousCohomology 1 (trivialF2 H): the explicit class of α, read as a continuous 1-cocycle for the trivial action, carried to the canonical object by the degree-one comparison. homClass_eq_cochainClass identifies it with the class of the homogeneous cochain of α.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem TauCeti.ContCohomology.homClass_def (H : Type u) [Group H] [TopologicalSpace H] [IsTopologicalGroup H] (α : H →* Multiplicative (ZMod 2)) (hα : Continuous ⇑α) :
      homClass H α hα = (TopModuleCat.Hom.hom (CategoryTheory.eqToHom ⋯)) ((explicitH1AddEquivContinuousCohomology H ↑(trivialF2 H)) ↑(evensHomCocycle α hα))

      homClass is the degree-one comparison applied to the explicit class of the homomorphism.

      source
      theorem TauCeti.ContCohomology.homClass_eq_cochainClass (H : Type u) [Group H] [TopologicalSpace H] [IsTopologicalGroup H] (α : H →* Multiplicative (ZMod 2)) (hα : Continuous ⇑α) :
      homClass H α hα = (trivialF2 H).cochainClass 1 (inhomogeneousCochain1 (fun (h : H) => Multiplicative.toAdd (α h)) ⋯) ⋯

      The class of a continuous homomorphism is the class of its cochain: homClass H α is the TopRep.cochainClass of the homogeneous cochain (h₀, h₁) ↦ α (h₀⁻¹ * h₁), read additively.

      source
      @[simp]
      theorem TauCeti.ContCohomology.homClass_one (H : Type u) [Group H] [TopologicalSpace H] [IsTopologicalGroup H] :
      homClass H 1 ⋯ = 0

      The trivial homomorphism has the zero class.

      source
      @[simp]
      theorem TauCeti.ContCohomology.homClass_mul (H : Type u) [Group H] [TopologicalSpace H] [IsTopologicalGroup H] (α β : H →* Multiplicative (ZMod 2)) (hα : Continuous ⇑α) (hβ : Continuous ⇑β) :
      homClass H (α * β) ⋯ = homClass H α hα + homClass H β hβ

      homClass turns products into sums: the class of α * β is the sum of the classes.

      source
      theorem TauCeti.ContCohomology.homClass_surjective (H : Type u) [Group H] [TopologicalSpace H] [IsTopologicalGroup H] (x : ↑(continuousCohomology 1 (trivialF2 H)).toModuleCat) :
      ∃ (α : H →* Multiplicative (ZMod 2)) (hα : Continuous ⇑α), homClass H α hα = x

      Every degree-one class is the class of a continuous homomorphism. With trivial 𝔽₂ coefficients the continuous 1-cocycles are the continuous homomorphisms and there are no nonzero coboundaries, so H¹(H, 𝔽₂) is the group of continuous homomorphisms H → 𝔽₂.

      source
      @[simp]
      theorem TauCeti.ContCohomology.homClass_inj (H : Type u) [Group H] [TopologicalSpace H] [IsTopologicalGroup H] {α β : H →* Multiplicative (ZMod 2)} (hα : Continuous ⇑α) (hβ : Continuous ⇑β) :
      homClass H α hα = homClass H β hβ ↔ α = β

      Two continuous homomorphisms have the same class exactly when they are equal. With trivial 𝔽₂ coefficients there are no nonzero degree-one coboundaries.

      source
      theorem TauCeti.ContCohomology.continuousSMul_trivialF2_homClass_naturality (K : Type u) [Group K] [TopologicalSpace K] [IsTopologicalGroup K] :
      ContinuousSMul K ↑(trivialF2 K)

      A group acts continuously on its trivial coefficients 𝔽₂, which are smooth discrete.

      source
      theorem TauCeti.ContCohomology.trivialF2Map_homClass {G H : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [Group H] [TopologicalSpace H] [IsTopologicalGroup H] (φ : H →ₜ* G) (α : G →* Multiplicative (ZMod 2)) (hα : Continuous ⇑α) :
      (CategoryTheory.ConcreteCategory.hom (trivialF2Map φ 1)) (homClass G α hα) = homClass H (α.comp ↑φ) ⋯

      Naturality of the class of a homomorphism. For a continuous homomorphism φ : H → G, pulling the class of a continuous α : G → 𝔽₂ back along φ gives the class of α ∘ φ.