The mod-two cohomology algebra of a group of order two

For a discrete group of order two, cup product with its unique nonzero character is an isomorphism in every degree. Consequently its canonical graded continuous cohomology algebra is the polynomial algebra on that degree-one character.

The calculation uses the index-two restriction–corestriction exact sequence for the trivial subgroup. Positive cohomology of that subgroup vanishes, and degree-zero corestriction is multiplication by two. The resulting degreewise equivalences give the polynomial-algebra identification, with its generator and homogeneous monomials explicitly normalized. The forward equations involving DirectSum.of retain the caller's equality decision on degrees; the algebra equivalence itself is independent of that decision.

The classical polynomial-ring calculation is A. Hatcher, Algebraic Topology, Theorem 3.19, p. 220, via the classifying space ℝP∞ = BC₂. The formal proof here instead uses the index-two coefficient sequence. The cup identities are from K. S. Brown, Cohomology of Groups, Chapter V, §3.

noncomputable def TauCeti.cyclicTwoCharacterClass (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [DiscreteTopology G] (hG : Nat.card G = 2) : cohomF2 G 1

The nontrivial degree-one character class of a discrete group of order two.

theorem TauCeti.cyclicTwoCharacterClass_eq_homClass (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [DiscreteTopology G] (hG : Nat.card G = 2) : cyclicTwoCharacterClass G hG = ContCohomology.homClass G (⊥.indexTwoCharacter ⋯) ⋯

The generator is the class of the continuous character with trivial kernel.

theorem TauCeti.bijective_cup_cyclicTwoCharacterClass (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [DiscreteTopology G] (hG : Nat.card G = 2) (n : ℕ) : Function.Bijective fun (x : cohomF2 G n) => (((trivialF2TopPairing G).cup n 1) x) (cyclicTwoCharacterClass G hG)

Cup product with the character of an order-two discrete group is bijective in every nonnegative degree, including degree zero.

noncomputable def TauCeti.cyclicTwoCupLinearEquiv (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [DiscreteTopology G] (hG : Nat.card G = 2) (n : ℕ) : cohomF2 G n ≃ₗ[ZMod 2] cohomF2 G (n + 1)

Multiplication by the degree-one character, as a linear equivalence between successive mod-two continuous cohomology groups.

theorem TauCeti.cyclicTwoCupLinearEquiv_apply (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [DiscreteTopology G] (hG : Nat.card G = 2) (n : ℕ) (x : cohomF2 G n) : (cyclicTwoCupLinearEquiv G hG n) x = (((trivialF2TopPairing G).cup n 1) x) (cyclicTwoCharacterClass G hG)

The periodicity equivalence is cup product with the character.

def TauCeti.cyclicTwoCohomLinearEquiv (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [DiscreteTopology G] (hG : Nat.card G = 2) (n : ℕ) : ZMod 2 ≃ₗ[ZMod 2] cohomF2 G n

The canonical generator in every degree, obtained by iterated cup product with the nontrivial character, identifies that degree with ZMod 2.

theorem TauCeti.cyclicTwoCohomLinearEquiv_zero_one (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [DiscreteTopology G] (hG : Nat.card G = 2) : (cyclicTwoCohomLinearEquiv G hG 0) 1 = 1

The degree-zero generator is the unit class.

theorem TauCeti.cyclicTwoCohomLinearEquiv_succ (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [DiscreteTopology G] (hG : Nat.card G = 2) (n : ℕ) (r : ZMod 2) : (cyclicTwoCohomLinearEquiv G hG (n + 1)) r = (((trivialF2TopPairing G).cup n 1) ((cyclicTwoCohomLinearEquiv G hG n) r)) (cyclicTwoCharacterClass G hG)

The generators in successive degrees differ by cup product with the character.

@[simp]

theorem TauCeti.cyclicTwoCohomLinearEquiv_one_one (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [DiscreteTopology G] (hG : Nat.card G = 2) : (cyclicTwoCohomLinearEquiv G hG 1) 1 = cyclicTwoCharacterClass G hG

The normalized degree-one generator is the nontrivial character.

@[simp]

theorem TauCeti.cyclicTwoCohomLinearEquiv_symm_character (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [DiscreteTopology G] (hG : Nat.card G = 2) : (cyclicTwoCohomLinearEquiv G hG 1).symm (cyclicTwoCharacterClass G hG) = 1

The normalized degree-one coordinate of the nontrivial character is one.

noncomputable def TauCeti.cyclicTwoCohomPolynomialEquiv (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [DiscreteTopology G] (hG : Nat.card G = 2) : Polynomial (ZMod 2) ≃ₐ[ZMod 2] gradedCohomF2 G

The canonical graded mod-two cohomology algebra of an order-two discrete group is a polynomial algebra, with X sent to its nontrivial character in degree one.

@[simp]

theorem TauCeti.cyclicTwoCohomPolynomialEquiv_X (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [DiscreteTopology G] [h : DecidableEq ℕ] (hG : Nat.card G = 2) : (cyclicTwoCohomPolynomialEquiv G hG) Polynomial.X = (DirectSum.of (cohomF2 G) 1) (cyclicTwoCharacterClass G hG)

The polynomial generator is the character class in degree one.

theorem TauCeti.cyclicTwoCohomPolynomialEquiv_monomial (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [DiscreteTopology G] [h : DecidableEq ℕ] (hG : Nat.card G = 2) (n : ℕ) (r : ZMod 2) : (cyclicTwoCohomPolynomialEquiv G hG) ((Polynomial.monomial n) r) = (DirectSum.of (cohomF2 G) n) ((cyclicTwoCohomLinearEquiv G hG n) r)

A monomial is the corresponding normalized homogeneous cohomology class.

theorem TauCeti.cyclicTwoCohomPolynomialEquiv_symm_of (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [DiscreteTopology G] (hG : Nat.card G = 2) (n : ℕ) (x : cohomF2 G n) : (cyclicTwoCohomPolynomialEquiv G hG).symm ((DirectSum.of (cohomF2 G) n) x) = (Polynomial.monomial n) ((cyclicTwoCohomLinearEquiv G hG n).symm x)

The inverse sends a homogeneous class to the monomial with its normalized coefficient.

@[simp]

theorem TauCeti.cyclicTwoCohomPolynomialEquiv_symm_character (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [DiscreteTopology G] (hG : Nat.card G = 2) : (cyclicTwoCohomPolynomialEquiv G hG).symm ((DirectSum.of (cohomF2 G) 1) (cyclicTwoCharacterClass G hG)) = Polynomial.X

The inverse sends the degree-one character to the polynomial generator.

theorem TauCeti.cyclicTwoCohomPolynomialEquiv_apply_component (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [DiscreteTopology G] (hG : Nat.card G = 2) (p : Polynomial (ZMod 2)) (n : ℕ) : ((cyclicTwoCohomPolynomialEquiv G hG) p) n = (cyclicTwoCohomLinearEquiv G hG n) (p.coeff n)

The coefficient of a polynomial is the coordinate of its homogeneous cohomology class.

@[simp]

theorem TauCeti.cyclicTwoCohomPolynomialEquiv_symm_coeff (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [DiscreteTopology G] (hG : Nat.card G = 2) (z : gradedCohomF2 G) (n : ℕ) : ((cyclicTwoCohomPolynomialEquiv G hG).symm z).coeff n = (cyclicTwoCohomLinearEquiv G hG n).symm (z n)

The inverse polynomial has the coordinates supplied by the normalized degreewise equivalences.

theorem TauCeti.cyclicTwoCharacterClass_ne_zero (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [DiscreteTopology G] (hG : Nat.card G = 2) : cyclicTwoCharacterClass G hG ≠ 0

The degree-one character class of an order-two group is nonzero.