The index-two graph class of the Evens norm

For an open subgroup U of index two and a continuous homomorphism α : U → Multiplicative (ZMod 2), the two-point graph cochain constructed in TauCeti.RepresentationTheory.Homological.ContCohomology.Evens.Cochain is a continuous 2-cocycle. This file takes its class in continuous cohomology.

The cochain formula uses an element s ∉ U, but its class does not. The difference between the formulas attached to two such elements is the explicit continuous coboundary proved in TauCeti.ContCohomology.evensGraphCochain_sub_evensGraphCochain. Thus graphClass only takes the index-two hypothesis, while graphClass_eq_cochainClass identifies it with the class of the graph cochain, read in Mathlib's homogeneous complex through inhomogeneousCochain2, for every possible s.

The raw formula is ZMod 2-valued. The coefficient object TauCeti.trivialF2 G uses a universe lift, so TauCeti.trivialF2Equiv crosses that lift before the explicit degree-two comparison places the class in Mathlib's canonical continuous cohomology.

Main definitions

• TauCeti.ContCohomology.evensHomCocycleAmbient: a continuous homomorphism α on a subgroup U, as a continuous 1-cocycle of U with the lifted trivial 𝔽₂ coefficients of the ambient group. It represents the class of α to which the restriction, corestriction and cup products of the ambient group apply. On the whole group the corresponding cocycle is TauCeti.ContCohomology.evensHomCocycle of TrivialF2/Character.lean.
• TauCeti.ContCohomology.evensGraphCocycle: the lifted continuous graph 2-cocycle.
• TauCeti.ContCohomology.explicitGraphClass: the choice-free class of the graph cocycle in the explicit inhomogeneous model H², which carries the explicit restriction, corestriction, cup and inflation operations.
• TauCeti.ContCohomology.evensGraphCochainClass: its canonical continuous-cohomology class for a specified s ∉ U.
• TauCeti.ContCohomology.graphClass: the choice-free graph class.

Main results

• TauCeti.ContCohomology.evensGraphCocycle_class_eq: in explicit H², the graph cocycles attached to two elements outside U have the same class. This is the choice-independence fact behind both graphClass and explicitGraphClass.
• TauCeti.ContCohomology.graphClass_eq_evensGraphCochainClass: graphClass is the class of the graph cochain, through the explicit comparison, for every element outside U.
• TauCeti.ContCohomology.graphClass_eq_cochainClass: the same class read on Mathlib's homogeneous complex, as the TopRep.cochainClass of the graph cochain placed there by inhomogeneousCochain2.
• TauCeti.ContCohomology.graphClass_eq_explicitGraphClass: the canonical class is the image of the explicit one under the degree-two comparison.

References

• L. Evens, A generalization of the transfer map in the cohomology of groups, Trans. Amer. Math. Soc. 108 (1963), 54–65.
• A. Kozlowski, The Evens–Kahn formula for the total Stiefel–Whitney class, Proc. Amer. Math. Soc. 91 (1984), 309–313.

noncomputable def TauCeti.ContCohomology.evensHomCocycleAmbient {G : Type u} [Group G] [TopologicalSpace G] (U : Subgroup G) (α : ↥U →* Multiplicative (ZMod 2)) (hα : Continuous ⇑α) : ↥(Z1 ↥U ↑(trivialF2 G))

A continuous homomorphism α : U → Multiplicative (ZMod 2) on a subgroup U, as a continuous 1-cocycle of U with coefficients in the lifted trivial 𝔽₂ object of the ambient group G. This is the representative of the class of α to which restriction, corestriction and the cup products of the ambient group apply.

Equations

• TauCeti.ContCohomology.evensHomCocycleAmbient U α hα = ⟨fun (h : ↥U) => (TauCeti.trivialF2Equiv G).symm (Multiplicative.toAdd (α h)), ⋯⟩

@[simp]

theorem TauCeti.ContCohomology.coe_evensHomCocycleAmbient {G : Type u} [Group G] [TopologicalSpace G] (U : Subgroup G) (α : ↥U →* Multiplicative (ZMod 2)) (hα : Continuous ⇑α) : ↑(evensHomCocycleAmbient U α hα) = fun (h : ↥U) => (trivialF2Equiv G).symm (Multiplicative.toAdd (α h))

The underlying cochain of evensHomCocycleAmbient.

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

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

noncomputable def TauCeti.ContCohomology.evensGraphCocycle {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (U : OpenSubgroup G) (s : G) (α : ↥↑U →* Multiplicative (ZMod 2)) (hU : (↑U).index = 2) (hs : s ∉ U) (hα : Continuous ⇑α) : ↥(Z2 G ↑(trivialF2 G))

The two-point graph cochain as a continuous 2-cocycle with coefficients in trivialF2 G.

The inverse of trivialF2Equiv is applied pointwise because the canonical coefficient object has carrier ULift (ZMod 2), while the explicit formula naturally takes values in ZMod 2.

Equations

• TauCeti.ContCohomology.evensGraphCocycle U s α hU hs hα = ⟨fun (p : G × G) => (TauCeti.trivialF2Equiv G).symm (TauCeti.ContCohomology.evensGraphCochain (↑U) s α p), ⋯⟩

@[simp]

theorem TauCeti.ContCohomology.coe_evensGraphCocycle {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (U : OpenSubgroup G) (s : G) (α : ↥↑U →* Multiplicative (ZMod 2)) (hU : (↑U).index = 2) (hs : s ∉ U) (hα : Continuous ⇑α) : ↑(evensGraphCocycle U s α hU hs hα) = fun (p : G × G) => (trivialF2Equiv G).symm (evensGraphCochain (↑U) s α p)

The underlying function of evensGraphCocycle is the graph cochain, transported across the universe lift in trivialF2.

theorem TauCeti.ContCohomology.evensGraphCocycle_class_eq {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (U : OpenSubgroup G) (s s' : G) (α : ↥↑U →* Multiplicative (ZMod 2)) (hU : (↑U).index = 2) (hs : s ∉ U) (hs' : s' ∉ U) (hα : Continuous ⇑α) : ↑(evensGraphCocycle U s' α hU hs' hα) = ↑(evensGraphCocycle U s α hU hs hα)

The class of the graph cocycle does not depend on the element chosen outside U. The two cochain formulas differ by the explicit continuous coboundary computed in TauCeti.ContCohomology.evensGraphCochain_sub_evensGraphCochain.

noncomputable def TauCeti.ContCohomology.explicitGraphClass {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (U : OpenSubgroup G) (hU : (↑U).index = 2) (α : ↥↑U →* Multiplicative (ZMod 2)) (hα : Continuous ⇑α) : H2 G ↑(trivialF2 G)

The choice-free class of the two-point graph cocycle in the explicit inhomogeneous model H²(G, 𝔽₂).

An element outside U is chosen only in the body. The theorem explicitGraphClass_eq_evensGraphCocycle identifies the result with the graph cocycle formed from every possible such element, so no choice occurs in the public interface. Unlike graphClass, this class lives in the model that carries the explicit low-degree restriction, corestriction, cup and inflation operations; graphClass_eq_explicitGraphClass compares the two.

Equations

• TauCeti.ContCohomology.explicitGraphClass U hU α hα = ↑(TauCeti.ContCohomology.evensGraphCocycle U (TauCeti.ContCohomology.graphElement✝ U hU) α hU ⋯ hα)

theorem TauCeti.ContCohomology.explicitGraphClass_eq_evensGraphCocycle {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (U : OpenSubgroup G) (hU : (↑U).index = 2) (s : G) (hs : s ∉ U) (α : ↥↑U →* Multiplicative (ZMod 2)) (hα : Continuous ⇑α) : explicitGraphClass U hU α hα = ↑(evensGraphCocycle U s α hU hs hα)

The choice-free explicit graph class is represented by the graph cocycle formed using every element outside U.

noncomputable def TauCeti.ContCohomology.evensGraphCochainClass {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [LocallyCompactSpace G] (U : OpenSubgroup G) (s : G) (α : ↥↑U →* Multiplicative (ZMod 2)) (hU : (↑U).index = 2) (hs : s ∉ U) (hα : Continuous ⇑α) : ↑(continuousCohomology 2 (trivialF2 G)).toModuleCat

The canonical continuous-cohomology class of the graph cochain attached to a specified element s ∉ U.

This named intermediate is the right-hand side of graphClass_eq_evensGraphCochainClass; unlike graphClass, it records the cochain representative used to present the class.

Equations

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

theorem TauCeti.ContCohomology.evensGraphCochainClass_def {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [LocallyCompactSpace G] (U : OpenSubgroup G) (s : G) (α : ↥↑U →* Multiplicative (ZMod 2)) (hU : (↑U).index = 2) (hs : s ∉ U) (hα : Continuous ⇑α) : evensGraphCochainClass U s α hU hs hα = (TopModuleCat.Hom.hom (CategoryTheory.eqToHom ⋯)) ((explicitH2AddEquivContinuousCohomology G ↑(trivialF2 G)) ↑(evensGraphCocycle U s α hU hs hα))

The class of the graph cochain is obtained by applying the explicit degree-two comparison, then identifying its discrete coefficient object with trivialF2 G.

noncomputable def TauCeti.ContCohomology.graphClass {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [LocallyCompactSpace G] (U : OpenSubgroup G) (hU : (↑U).index = 2) (α : ↥↑U →* Multiplicative (ZMod 2)) (hα : Continuous ⇑α) : ↑(continuousCohomology 2 (trivialF2 G)).toModuleCat

The choice-free class of the two-point graph cocycle at an index-two open subgroup.

An element outside U is chosen internally. The theorems graphClass_eq_evensGraphCochainClass and graphClass_eq_cochainClass prove that the result is the class of the graph cochain for every such element, so no choice occurs in the public signature.

Equations

• TauCeti.ContCohomology.graphClass U hU α hα = TauCeti.ContCohomology.evensGraphCochainClass U (TauCeti.ContCohomology.graphElement✝ U hU) α hU ⋯ hα

theorem TauCeti.ContCohomology.graphClass_eq_evensGraphCochainClass {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [LocallyCompactSpace G] (U : OpenSubgroup G) (hU : (↑U).index = 2) (s : G) (hs : s ∉ U) (α : ↥↑U →* Multiplicative (ZMod 2)) (hα : Continuous ⇑α) : graphClass U hU α hα = evensGraphCochainClass U s α hU hs hα

The choice-free graph class is the class of the graph cochain formed using every element outside U, through the explicit degree-two comparison.

theorem TauCeti.ContCohomology.graphClass_eq_explicitGraphClass {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [LocallyCompactSpace G] (U : OpenSubgroup G) (hU : (↑U).index = 2) (α : ↥↑U →* Multiplicative (ZMod 2)) (hα : Continuous ⇑α) : graphClass U hU α hα = (TopModuleCat.Hom.hom (CategoryTheory.eqToHom ⋯)) ((explicitH2AddEquivContinuousCohomology G ↑(trivialF2 G)) (explicitGraphClass U hU α hα))

The canonical graph class is the image of the choice-free explicit graph class under the degree-two comparison.

theorem TauCeti.ContCohomology.graphClass_eq_cochainClass {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [LocallyCompactSpace G] (U : OpenSubgroup G) (hU : (↑U).index = 2) (s : G) (hs : s ∉ U) (α : ↥↑U →* Multiplicative (ZMod 2)) (hα : Continuous ⇑α) : graphClass U hU α hα = (trivialF2 G).cochainClass 2 (inhomogeneousCochain2 (evensGraphCochain (↑U) s α) ⋯) ⋯

The graph class is the class of the graph cochain, at every element s ∉ U, read on Mathlib's homogeneous complex: the graph cochain enters it through inhomogeneousCochain2, and TopRep.cochainClass takes its class.