Explicit inhomogeneous cochains with trivial 𝔽₂ coefficients

Explicit cohomological constructions with trivial 𝔽₂ coefficients, such as the two-point graph cocycle of the Evens norm or a factor set pulled back along a homomorphism, are given by formulas G → ZMod 2 and G × G → ZMod 2. Continuous cohomology with these coefficients is computed by Mathlib's homogeneous cochains of TauCeti.trivialF2 G, whose carrier is the universe lift ULift (ZMod 2). This file places continuous formulas in that complex, through the classical passage f ↦ ((g₀, g₁) ↦ f (g₀⁻¹ g₁)) and f ↦ ((g₀, g₁, g₂) ↦ f (g₀⁻¹ g₁, g₁⁻¹ g₂)) from inhomogeneous to homogeneous cochains, the action being trivial. These constructors are the only place where the universe lift is crossed.

Under this passage the canonical differential becomes the inhomogeneous one: a formula is a cocycle exactly when it satisfies the inhomogeneous cocycle identity, and the differential of the image of a 1-cochain ψ is the image of (g, h) ↦ ψ h - ψ (g h) + ψ g. Hence two continuous inhomogeneous 2-cocycles that differ by such an explicit coboundary have the same class in continuousCohomology 2 (trivialF2 G). This is how a coboundary witness written as a formula crosses to the canonical object.

No local compactness is needed: the homogeneous cochains are obtained by currying a jointly continuous function, which is always possible. For a general discrete module, the passage between the two kinds of cochains is TauCeti.ContCohomology.cochainEquiv1 and TauCeti.ContCohomology.cochainEquiv2.

The explicit low-degree model presents a class with these coefficients as the class of a continuous inhomogeneous cocycle in H¹ or H², carried to continuousCohomology n (trivialF2 G) by the comparisons TauCeti.ContCohomology.explicitH1AddEquivContinuousCohomology and TauCeti.ContCohomology.explicitH2AddEquivContinuousCohomology followed by the identification TauCeti.ofDiscreteModule_trivialF2 of the coefficients. The last section proves that this is the TopRep.cochainClass of the image of the same formula, so that a class defined in the explicit model can be computed with on homogeneous cochains, and conversely.

Main definitions

• TauCeti.ContCohomology.inhomogeneousCochain1, TauCeti.ContCohomology.inhomogeneousCochain2: a continuous ZMod 2-valued function on G, respectively G × G, as a homogeneous cochain of trivialF2 G.

Main results

• TauCeti.ContCohomology.inhomogeneousCochain1_d_eq_zero_iff: the image of f : G → ZMod 2 is a cocycle exactly when f is additive, that is, a homomorphism.
• TauCeti.ContCohomology.inhomogeneousCochain2_d_eq_zero_iff: the image of f : G × G → ZMod 2 is a cocycle exactly when f satisfies the inhomogeneous 2-cocycle identity.
• TauCeti.ContCohomology.d_inhomogeneousCochain1: the differential of the image of a 1-cochain is the image of its inhomogeneous coboundary.
• TauCeti.ContCohomology.cochainClass_inhomogeneousCochain2_eq_of_coboundary: cohomologous continuous inhomogeneous 2-cocycles have the same class.
• TauCeti.ContCohomology.trivialF2Map_cochainClass_inhomogeneousCochain1: pulling back along a continuous homomorphism φ sends the class of the image of f to the class of the image of f ∘ φ.
• TauCeti.ContCohomology.eqToHom_explicitH1AddEquivContinuousCohomology_eq_cochainClass and TauCeti.ContCohomology.eqToHom_explicitH2AddEquivContinuousCohomology_eq_cochainClass: the explicit class of a trivial-𝔽₂ cocycle in degree one, respectively two (over a locally compact group, where the explicit comparison exists), is the canonical class of its image.

References

• J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, 2nd ed., Ch. I, §2: the inhomogeneous description of continuous cochains.

noncomputable def TauCeti.ContCohomology.inhomogeneousCochain1 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (f : G → ZMod 2) (hf : Continuous f) : ↑((trivialF2 G).homogeneousCochains.X 1).toModuleCat

A continuous function f : G → ZMod 2, as the homogeneous 1-cochain (g₀, g₁) ↦ f (g₀⁻¹ * g₁) of the trivial 𝔽₂ coefficients trivialF2 G, lifted to their carrier.

Source: this constructor is close to the degree-1 constructor of Tau Ceti PR #11157; here it is stated on homogeneousCochains (trivialF2 G) directly, without local compactness, with inhomogeneousCochain2 as its degree-2 counterpart.

Equations

• TauCeti.ContCohomology.inhomogeneousCochain1 f hf = ⟨{ toFun := fun (q : G × G) => (TauCeti.trivialF2Equiv G).symm (f (q.1⁻¹ * q.2)), continuous_toFun := ⋯ }.curry, ⋯⟩

@[simp]

theorem TauCeti.ContCohomology.inhomogeneousCochain1_apply {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (f : G → ZMod 2) (hf : Continuous f) (g₀ g₁ : G) : (↑(inhomogeneousCochain1 f hf) g₀) g₁ = (trivialF2Equiv G).symm (f (g₀⁻¹ * g₁))

The value of inhomogeneousCochain1 f hf at (g₀, g₁) is f (g₀⁻¹ * g₁), lifted to the carrier of trivialF2 G.

noncomputable def TauCeti.ContCohomology.inhomogeneousCochain2 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (f : G × G → ZMod 2) (hf : Continuous f) : ↑((trivialF2 G).homogeneousCochains.X 2).toModuleCat

A continuous function f : G × G → ZMod 2, as the homogeneous 2-cochain (g₀, g₁, g₂) ↦ f (g₀⁻¹ * g₁, g₁⁻¹ * g₂) of the trivial 𝔽₂ coefficients trivialF2 G, lifted to their carrier.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.ContCohomology.inhomogeneousCochain2_apply {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (f : G × G → ZMod 2) (hf : Continuous f) (g₀ g₁ g₂ : G) : ((↑(inhomogeneousCochain2 f hf) g₀) g₁) g₂ = (trivialF2Equiv G).symm (f (g₀⁻¹ * g₁, g₁⁻¹ * g₂))

The value of inhomogeneousCochain2 f hf at (g₀, g₁, g₂) is f (g₀⁻¹ * g₁, g₁⁻¹ * g₂), lifted to the carrier of trivialF2 G.

theorem TauCeti.ContCohomology.d_inhomogeneousCochain1 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (ψ : G → ZMod 2) (hψ : Continuous ψ) : (TopModuleCat.Hom.hom ((trivialF2 G).homogeneousCochains.d 1 2)) (inhomogeneousCochain1 ψ hψ) = inhomogeneousCochain2 (fun (p : G × G) => ψ p.2 - ψ (p.1 * p.2) + ψ p.1) ⋯

The canonical differential of an inhomogeneous 1-cochain is its inhomogeneous coboundary: the differential of the image of ψ is the image of (g, h) ↦ ψ h - ψ (g * h) + ψ g.

theorem TauCeti.ContCohomology.inhomogeneousCochain1_d_eq_zero_iff {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (f : G → ZMod 2) (hf : Continuous f) : (TopModuleCat.Hom.hom ((trivialF2 G).homogeneousCochains.d 1 2)) (inhomogeneousCochain1 f hf) = 0 ↔ ∀ (g h : G), f (g * h) = f g + f h

The image of f : G → ZMod 2 is a cocycle exactly when f is additive. With trivial coefficients the inhomogeneous 1-cocycles are the homomorphisms.

theorem TauCeti.ContCohomology.inhomogeneousCochain1_d_eq_zero {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (f : G → ZMod 2) (hf : Continuous f) (hcocycle : ∀ (g h : G), f (g * h) = f g + f h) : (TopModuleCat.Hom.hom ((trivialF2 G).homogeneousCochains.d 1 2)) (inhomogeneousCochain1 f hf) = 0

The image of a homomorphism is a cocycle.

theorem TauCeti.ContCohomology.inhomogeneousCochain2_d_eq_zero_iff {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (f : G × G → ZMod 2) (hf : Continuous f) : (TopModuleCat.Hom.hom ((trivialF2 G).homogeneousCochains.d 2 3)) (inhomogeneousCochain2 f hf) = 0 ↔ ∀ (g h j : G), f (g * h, j) + f (g, h) = f (h, j) + f (g, h * j)

The image of f : G × G → ZMod 2 is a cocycle exactly when f satisfies the inhomogeneous 2-cocycle identity f (g * h, j) + f (g, h) = f (h, j) + f (g, h * j).

theorem TauCeti.ContCohomology.inhomogeneousCochain2_d_eq_zero {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (f : G × G → ZMod 2) (hf : Continuous f) (hcocycle : ∀ (g h j : G), f (g * h, j) + f (g, h) = f (h, j) + f (g, h * j)) : (TopModuleCat.Hom.hom ((trivialF2 G).homogeneousCochains.d 2 3)) (inhomogeneousCochain2 f hf) = 0

The image of an inhomogeneous 2-cocycle is a cocycle.

theorem TauCeti.ContCohomology.cochainClass_inhomogeneousCochain2_eq_of_coboundary {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (f f' : G × G → ZMod 2) (hf : Continuous f) (hf' : Continuous f') (ψ : G → ZMod 2) (hψ : Continuous ψ) (hfψ : ∀ (g h : G), f (g, h) = f' (g, h) + (ψ h - ψ (g * h) + ψ g)) (ha : (TopModuleCat.Hom.hom ((trivialF2 G).homogeneousCochains.d 2 3)) (inhomogeneousCochain2 f hf) = 0) (hb : (TopModuleCat.Hom.hom ((trivialF2 G).homogeneousCochains.d 2 3)) (inhomogeneousCochain2 f' hf') = 0) : (trivialF2 G).cochainClass 2 (inhomogeneousCochain2 f hf) ha = (trivialF2 G).cochainClass 2 (inhomogeneousCochain2 f' hf') hb

Cohomologous inhomogeneous 2-cocycles have the same class. If two continuous functions f f' : G × G → ZMod 2 whose images are cocycles differ by the inhomogeneous coboundary (g, h) ↦ ψ h - ψ (g * h) + ψ g of a continuous ψ : G → ZMod 2, their images have the same class in continuousCohomology 2 (trivialF2 G). The cocycle hypotheses are typically inhomogeneousCochain2_d_eq_zero f hf hcf and its counterpart for f'.

Pullback along a continuous homomorphism

theorem TauCeti.ContCohomology.trivialF2Map_cochainClass_inhomogeneousCochain1 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] (φ : H →ₜ* G) (f : G → ZMod 2) (hf : Continuous f) (hd : (TopModuleCat.Hom.hom ((trivialF2 G).homogeneousCochains.d 1 2)) (inhomogeneousCochain1 f hf) = 0) (hd' : (TopModuleCat.Hom.hom ((trivialF2 H).homogeneousCochains.d 1 2)) (inhomogeneousCochain1 (f ∘ ⇑φ) ⋯) = 0) : (CategoryTheory.ConcreteCategory.hom (trivialF2Map φ 1)) ((trivialF2 G).cochainClass 1 (inhomogeneousCochain1 f hf) hd) = (trivialF2 H).cochainClass 1 (inhomogeneousCochain1 (f ∘ ⇑φ) ⋯) hd'

Pullback of the class of an inhomogeneous 1-cocycle. Along a continuous homomorphism φ : H → G, the map TauCeti.trivialF2Map φ 1 sends the class of the image of a continuous f : G → ZMod 2 to the class of the image of f ∘ φ. The two cocycle hypotheses are typically inhomogeneousCochain1_d_eq_zero for f and for f ∘ φ.

Explicit classes as canonical cochain classes

theorem TauCeti.ContCohomology.instContinuousSMulVIntTrivialF2 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : ContinuousSMul G ↑(trivialF2 G)

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

theorem TauCeti.ContCohomology.eqToHom_explicitH1AddEquivContinuousCohomology_eq_cochainClass {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (c : ↥(Z1 G ↑(trivialF2 G))) (f : G → ZMod 2) (hf : Continuous f) (hcf : ∀ (g : G), ↑c g = (trivialF2Equiv G).symm (f g)) (hd : (TopModuleCat.Hom.hom ((trivialF2 G).homogeneousCochains.d 1 2)) (inhomogeneousCochain1 f hf) = 0) : (TopModuleCat.Hom.hom (CategoryTheory.eqToHom ⋯)) ((explicitH1AddEquivContinuousCohomology G ↑(trivialF2 G)) ↑c) = (trivialF2 G).cochainClass 1 (inhomogeneousCochain1 f hf) hd

The explicit degree-one class of a trivial-𝔽₂ cocycle is its canonical cochain class. If the continuous cocycle c is the formula f : G → ZMod 2 lifted to the carrier of trivialF2 G, the degree-one comparison sends its class to the TopRep.cochainClass of inhomogeneousCochain1 f.

theorem TauCeti.ContCohomology.eqToHom_explicitH2AddEquivContinuousCohomology_eq_cochainClass {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [LocallyCompactSpace G] (c : ↥(Z2 G ↑(trivialF2 G))) (f : G × G → ZMod 2) (hf : Continuous f) (hcf : ∀ (p : G × G), ↑c p = (trivialF2Equiv G).symm (f p)) (hd : (TopModuleCat.Hom.hom ((trivialF2 G).homogeneousCochains.d 2 3)) (inhomogeneousCochain2 f hf) = 0) : (TopModuleCat.Hom.hom (CategoryTheory.eqToHom ⋯)) ((explicitH2AddEquivContinuousCohomology G ↑(trivialF2 G)) ↑c) = (trivialF2 G).cochainClass 2 (inhomogeneousCochain2 f hf) hd

The explicit degree-two class of a trivial-𝔽₂ cocycle is its canonical cochain class. If the continuous cocycle c is the formula f : G × G → ZMod 2 lifted to the carrier of trivialF2 G, the degree-two comparison sends its class to the TopRep.cochainClass of inhomogeneousCochain2 f.