The trivial F₂ coefficient representation

This file defines a trivial object of TopRep ℤ G whose carrier is a universe lift of ZMod 2. It is stable under restriction and is smooth discrete, as needed for continuous cohomology with trivial 𝔽₂ coefficients.

The homomorphism and isomorphism maps follow the cohomFpMap and cohomFpLinearEquiv construction in TauCeti/RepresentationTheory/Homological/ContCohomology/TrivialFp.lean, with ℤ as the scalar ring used by the all-degree cup product.

For G : Type u, Mathlib's continuous-cohomology resolution requires the coefficient module to live in Type u. The carrier of trivialF2 G is therefore ULift.{u} (ZMod 2), not ZMod 2. The action is trivial, and restriction to a subgroup is definitionally the corresponding trivial coefficient object for that subgroup.

Main definitions

• TauCeti.trivialF2: trivial 𝔽₂ coefficients over an arbitrary universe.
• TauCeti.cohomF2: continuous cohomology with trivial 𝔽₂ coefficients, with its canonical ZMod 2-module structure TauCeti.cohomF2.instModule.
• TauCeti.trivialF2ResMap: restriction on continuous cohomology with trivial 𝔽₂ coefficients.
• TauCeti.trivialF2Map: pullback along any continuous group homomorphism with trivial 𝔽₂ coefficients, and TauCeti.trivialF2Iso for a topological group isomorphism.
• TauCeti.trivialF2QuotientEquivFixedPoints: trivial 𝔽₂ coefficients on a quotient G ⧸ N, identified with the N-fixed points of the ambient trivial 𝔽₂ coefficients.

Main results

• TauCeti.trivialF2_V: the carrier is ULift (ZMod 2).
• TauCeti.trivialF2Equiv: the additive equivalence that crosses the universe lift, with TauCeti.trivialF2Equiv_cast its invariance under casts between the carriers of two groups.
• TauCeti.trivialF2_ρ_apply_apply: every monoid element acts trivially.
• TauCeti.trivialF2_two_nsmul_eq_zero, TauCeti.cohomF2.two_nsmul_eq_zero: the coefficients, and hence every cohomology class, are killed by 2.
• TauCeti.trivialF2Pairing: multiplication in 𝔽₂ as a biadditive pairing on the lifted carrier, with TauCeti.trivialF2Pairing_smul_smul its equivariance.
• TauCeti.ofDiscreteModule_trivialF2: the coefficient dictionary recovers trivialF2, with TauCeti.eqToHom_ofDiscreteModule_trivialF2_apply and TauCeti.eqToHom_ofDiscreteModule_trivialF2_symm_apply its carrier-level reading.
• TauCeti.res_trivialF2: restriction preserves the coefficient object on the nose.
• TauCeti.trivialF2Map_subgroupSubtype: the general pullback recovers subgroup restriction.
• TauCeti.trivialF2Map_id, TauCeti.trivialF2Map_comp: the functoriality laws.
• TauCeti.trivialF2Map_eq_of_conj: over a locally compact target, pullbacks along two homomorphisms that differ by an inner automorphism agree.
• TauCeti.eqToHom_comp_trivialF2Map: read in discrete models of the coefficients, the pullback is the compatible-pair map of any coefficient map that is the identity of 𝔽₂.
• TauCeti.isSmoothDiscrete_trivialF2: the coefficient object is smooth discrete.
• TauCeti.trivialF2QuotientEquivFixedPoints_smul: that identification is equivariant for the G ⧸ N-actions, with TauCeti.trivialF2Equiv_apply_trivialF2QuotientEquivFixedPoints its value rule.

noncomputable def TauCeti.trivialF2 (G : Type u) [Monoid G] : TopRep ℤ G

Trivial 𝔽₂ coefficients as an object of TopRep ℤ G in the universe of G.

The lift is forced by the universe of Mathlib's continuous-cohomology resolution.

Equations

• TauCeti.trivialF2 G = TopRep.of (ContRepresentation.trivial ℤ G (ULift.{?u.1, 0} (ZMod 2)))

@[simp]

theorem TauCeti.trivialF2_V (G : Type u) [Monoid G] : ↑(trivialF2 G) = ULift.{u, 0} (ZMod 2)

The carrier of trivialF2 G is the universe lift of ZMod 2.

noncomputable def TauCeti.trivialF2Equiv (G : Type u) [Monoid G] : ↑(trivialF2 G) ≃+ ZMod 2

The additive equivalence from the lifted carrier of trivialF2 G to ZMod 2.

Equations

• TauCeti.trivialF2Equiv G = AddEquiv.ulift

@[simp]

theorem TauCeti.trivialF2Equiv_apply (G : Type u) [Monoid G] (x : ULift.{u, 0} (ZMod 2)) : (trivialF2Equiv G) (cast ⋯ x) = x.down

trivialF2Equiv sends a lifted element to its underlying value.

@[simp]

theorem TauCeti.trivialF2Equiv_symm_apply (G : Type u) [Monoid G] (x : ZMod 2) : (trivialF2Equiv G).symm x = cast ⋯ { down := x }

The inverse of trivialF2Equiv lifts a value.

theorem TauCeti.trivialF2Equiv_cast (G : Type u) [Monoid G] {H : Type u} [Monoid H] (h : ↑(trivialF2 G) = ↑(trivialF2 H)) (x : ↑(trivialF2 G)) : (trivialF2Equiv H) (cast h x) = (trivialF2Equiv G) x

The carriers of the trivial 𝔽₂ objects of two monoids are the same lifted ZMod 2, and a cast between them does not change the underlying value. This is how an element transported along an equality of coefficient objects, such as CategoryTheory.eqToHom in TopRep, is read back.

instance TauCeti.instDiscreteTopologyVIntTrivialF2 (G : Type u) [Monoid G] : DiscreteTopology ↑(trivialF2 G)

The lifted carrier of trivialF2 G has the discrete topology.

@[simp]

theorem TauCeti.ofDiscreteModule_trivialF2 (G : Type u) [Monoid G] : ofDiscreteModule ℤ G ↑(trivialF2 G) = trivialF2 G

Applying the discrete coefficient dictionary to the carrier of trivialF2 recovers the coefficient object itself.

Comparisons between explicit cocycle groups and continuous cohomology are stated for the coefficient object ofDiscreteModule ℤ G M attached to a discrete module M. Taking M := (trivialF2 G).V, this equality identifies that object with trivialF2 G, so such a comparison carries a class computed from explicit cochains into continuous cohomology with trivial 𝔽₂ coefficients.

@[simp]

theorem TauCeti.eqToHom_ofDiscreteModule_trivialF2_apply (G : Type u) [Monoid G] (x : ↑(trivialF2 G)) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.eqToHom ⋯)) x = x

The transported identity of TauCeti.ofDiscreteModule_trivialF2 acts as the identity on carriers: TauCeti.eqToHom (ofDiscreteModule_trivialF2 G) is the morphism TauCeti.eqToIso (ofDiscreteModule_trivialF2 G) read by TauCeti.eqToIso.hom, so it is the identity on the carrier of trivialF2 G.

theorem TauCeti.eqToHom_ofDiscreteModule_trivialF2_symm_apply (G : Type u) [Monoid G] (x : ↑(trivialF2 G)) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.eqToHom ⋯)) x = x

The transported inverse of TauCeti.ofDiscreteModule_trivialF2 acts as the identity on carriers: TauCeti.eqToHom (ofDiscreteModule_trivialF2 G).symm is the inverse morphism TauCeti.eqToIso (ofDiscreteModule_trivialF2 G) read by TauCeti.eqToIso.inv, so it too is the identity on the carrier of trivialF2 G.

@[simp]

theorem TauCeti.trivialF2_ρ_apply_apply (G : Type u) [Monoid G] (g : G) (x : ↑(trivialF2 G)) : ((trivialF2 G).ρ g) x = x

Every monoid element acts trivially on trivialF2 G.

This is the public action rule of the object, in the same role as TauCeti.ofDiscreteModule_ρ_apply_apply: the body of trivialF2 is not exposed, so a consumer cannot reach ContRepresentation.trivial_apply through it.

noncomputable def TauCeti.trivialF2Pairing (G : Type u) [Monoid G] : ↑(trivialF2 G) →+ ↑(trivialF2 G) →+ ↑(trivialF2 G)

Multiplication in 𝔽₂, transported along trivialF2Equiv to a biadditive pairing on the lifted carrier of trivialF2 G. It is the coefficient pairing of the 𝔽₂-valued cup products and of the identities of the Evens norm.

Equations

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

@[simp]

theorem TauCeti.trivialF2Pairing_apply (G : Type u) [Monoid G] (x y : ↑(trivialF2 G)) : ((trivialF2Pairing G) x) y = (trivialF2Equiv G).symm ((trivialF2Equiv G) x * (trivialF2Equiv G) y)

The pairing multiplies the underlying values in ZMod 2.

theorem TauCeti.trivialF2Pairing_smul_smul (G : Type u) [Monoid G] (g : G) (x y : ↑(trivialF2 G)) : ((trivialF2Pairing G) (g • x)) (g • y) = g • ((trivialF2Pairing G) x) y

The pairing is G-equivariant, the action being trivial.

theorem TauCeti.trivialF2_two_nsmul_eq_zero (G : Type u) [Monoid G] (x : ↑(trivialF2 G)) : 2 • x = 0

Every element of the trivial 𝔽₂ coefficient object is killed by 2.

theorem TauCeti.isSmoothDiscrete_trivialF2 (G : Type u) [Monoid G] [TopologicalSpace G] : IsSmoothDiscrete ℤ (trivialF2 G)

The trivial 𝔽₂ coefficient object is smooth discrete.

@[simp]

theorem TauCeti.res_trivialF2 (G : Type u) [Group G] (S : Subgroup G) : TopRep.res S.subtype (trivialF2 G) = trivialF2 ↥S

Restriction preserves the trivial 𝔽₂ coefficient object on the nose.

noncomputable def TauCeti.trivialF2ResMap (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (S : Subgroup G) (n : ℕ) : continuousCohomology n (trivialF2 G) ⟶ continuousCohomology n (trivialF2 ↥S)

Restriction on continuous cohomology with trivial 𝔽₂ coefficients. This is the generic restriction map followed by the on-the-nose identification res_trivialF2.

Equations

• TauCeti.trivialF2ResMap G S n = CategoryTheory.CategoryStruct.comp (TauCeti.ContinuousCohomology.res S (TauCeti.trivialF2 G) n) (CategoryTheory.eqToHom ⋯)

theorem TauCeti.trivialF2ResMap_def (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (S : Subgroup G) (n : ℕ) : trivialF2ResMap G S n = CategoryTheory.CategoryStruct.comp (ContinuousCohomology.res S (trivialF2 G) n) (CategoryTheory.eqToHom ⋯)

The defining equation of restriction with trivial 𝔽₂ coefficients.

@[reducible, inline]

noncomputable abbrev TauCeti.cohomF2 (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (n : ℕ) : Type u

Continuous cohomology with trivial 𝔽₂ coefficients, indexed by its degree. It is the ℤ-coefficient counterpart of TauCeti.cohomFp.

Equations

• TauCeti.cohomF2 G n = ↑(continuousCohomology n (TauCeti.trivialF2 G)).toModuleCat

theorem TauCeti.cohomF2.two_nsmul_eq_zero (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (n : ℕ) (x : cohomF2 G n) : 2 • x = 0

Every class of continuous cohomology with trivial 𝔽₂ coefficients is killed by 2.

@[instance_reducible]

noncomputable instance TauCeti.cohomF2.instModule (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (n : ℕ) : Module (ZMod 2) (cohomF2 G n)

The canonical ZMod 2-module structure on continuous cohomology with trivial 𝔽₂ coefficients, which is killed by 2 (TauCeti.cohomF2.two_nsmul_eq_zero).

Equations

• TauCeti.cohomF2.instModule G n = AddCommGroup.zmodModule ⋯

@[simp]

theorem TauCeti.res_trivialF2_hom {G H : Type u} [Group G] [TopologicalSpace G] [Group H] [TopologicalSpace H] (φ : H →ₜ* G) : TopRep.res (↑φ) (trivialF2 G) = trivialF2 H

Pulling trivial 𝔽₂ coefficients back along a continuous group homomorphism gives the trivial coefficient object on its source.

noncomputable def TauCeti.trivialF2Map {G H : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [Group H] [TopologicalSpace H] [IsTopologicalGroup H] (φ : H →ₜ* G) (n : ℕ) : continuousCohomology n (trivialF2 G) ⟶ continuousCohomology n (trivialF2 H)

Contravariant continuous cohomology with trivial 𝔽₂ coefficients along a continuous group homomorphism.

Equations

• TauCeti.trivialF2Map φ n = ContinuousCohomology.map φ (CategoryTheory.eqToHom ⋯) n

theorem TauCeti.trivialF2Map_def {G H : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [Group H] [TopologicalSpace H] [IsTopologicalGroup H] (φ : H →ₜ* G) (n : ℕ) : trivialF2Map φ n = ContinuousCohomology.map φ (CategoryTheory.eqToHom ⋯) n

The trivial-coefficient map is Mathlib's compatible-pair map with the canonical coefficient identification.

@[simp]

theorem TauCeti.trivialF2Map_subgroupSubtype (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (S : Subgroup G) (n : ℕ) : trivialF2Map (ContinuousMonoidHom.subgroupSubtype S) n = trivialF2ResMap G S n

Pullback along a subgroup inclusion is the named restriction map.

@[simp]

theorem TauCeti.trivialF2Map_id {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (n : ℕ) : trivialF2Map (ContinuousMonoidHom.id G) n = CategoryTheory.CategoryStruct.id (continuousCohomology n (trivialF2 G))

The map induced by the identity group homomorphism is the identity.

@[simp]

theorem TauCeti.trivialF2Map_comp {G H J : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [Group H] [TopologicalSpace H] [IsTopologicalGroup H] [Group J] [TopologicalSpace J] [IsTopologicalGroup J] (φ : H →ₜ* G) (ψ : J →ₜ* H) (n : ℕ) : trivialF2Map (φ.comp ψ) n = CategoryTheory.CategoryStruct.comp (trivialF2Map φ n) (trivialF2Map ψ n)

Trivial-coefficient maps compose contravariantly.

theorem TauCeti.trivialF2Map_eq_of_conj {G H : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [Group H] [TopologicalSpace H] [IsTopologicalGroup H] [LocallyCompactSpace G] (φ ψ : H →ₜ* G) (g : G) (h : ∀ (x : H), ψ x = g * φ x * g⁻¹) (n : ℕ) : trivialF2Map ψ n = trivialF2Map φ n

Pullback is invariant under inner automorphisms of the target: if two continuous homomorphisms φ ψ : H →ₜ* G differ by conjugation by g : G, they induce the same map on continuous cohomology with trivial 𝔽₂ coefficients, in every degree: inner automorphisms act trivially on Hⁿ(G, 𝔽₂) (TauCeti.ContinuousCohomology.map_eq_id_of_inner).

noncomputable def TauCeti.trivialF2Iso {G H : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [Group H] [TopologicalSpace H] [IsTopologicalGroup H] (e : G ≃ₜ* H) (n : ℕ) : continuousCohomology n (trivialF2 G) ≅ continuousCohomology n (trivialF2 H)

A topological group isomorphism induces an equivalence on continuous cohomology with trivial 𝔽₂ coefficients. The cohomology map runs along the inverse group isomorphism.

Equations

• TauCeti.trivialF2Iso e n = { hom := TauCeti.trivialF2Map (↑e.symm) n, inv := TauCeti.trivialF2Map (↑e) n, hom_inv_id := ⋯, inv_hom_id := ⋯ }

@[simp]

theorem TauCeti.trivialF2Iso_hom {G H : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [Group H] [TopologicalSpace H] [IsTopologicalGroup H] (e : G ≃ₜ* H) (n : ℕ) : (trivialF2Iso e n).hom = trivialF2Map (↑e.symm) n

The forward cohomology transport is pullback along the inverse group isomorphism.

@[simp]

theorem TauCeti.trivialF2Iso_inv {G H : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [Group H] [TopologicalSpace H] [IsTopologicalGroup H] (e : G ≃ₜ* H) (n : ℕ) : (trivialF2Iso e n).inv = trivialF2Map (↑e) n

The inverse cohomology transport is pullback along the group isomorphism.

theorem TauCeti.eqToHom_comp_trivialF2Map {G H : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [Group H] [TopologicalSpace H] [IsTopologicalGroup H] {M : Type u} [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] {N : Type u} [AddCommGroup N] [TopologicalSpace N] [DiscreteTopology N] [DistribMulAction H N] (φ : H →ₜ* G) (hM : ofDiscreteModule ℤ G M = trivialF2 G) (hN : ofDiscreteModule ℤ H N = trivialF2 H) (f : M →+ N) (hf : ∀ (h : H) (m : M), f (φ h • m) = h • f m) (hfM : ∀ (m : M), (trivialF2Equiv H) ((TopRep.Hom.hom (CategoryTheory.eqToHom hN)) (f m)) = (trivialF2Equiv G) ((TopRep.Hom.hom (CategoryTheory.eqToHom hM)) m)) (n : ℕ) : CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (trivialF2Map φ n) = CategoryTheory.CategoryStruct.comp (ContinuousCohomology.map φ (ofDiscreteModulePair (↑φ) f.toIntLinearMap hf) n) (CategoryTheory.eqToHom ⋯)

trivialF2Map in a discrete model of the coefficients. Suppose the discrete G-module M and the discrete H-module N are models of the trivial 𝔽₂ objects, hM and hN, and f : M →+ N is compatible with φ : H →ₜ* G and is the identity of 𝔽₂ read in the two models. Then pullback trivialF2Map φ n, read in the models, is the compatible-pair map of φ and f. This is what lets pullback on trivial 𝔽₂ coefficients be computed on explicit cocycles valued in M.

noncomputable def TauCeti.trivialF2QuotientEquivFixedPoints {G : Type u} [Group G] (N : Subgroup G) [N.Normal] : ↑(trivialF2 (G ⧸ N)) ≃+ ↥(FixedPoints.addSubgroup ↥N ↑(trivialF2 G))

Trivial 𝔽₂ coefficients on G / N are additively equivalent to the N-fixed points of the ambient trivial coefficients.

Equations

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

@[simp]

theorem TauCeti.trivialF2Equiv_apply_trivialF2QuotientEquivFixedPoints {G : Type u} [Group G] (N : Subgroup G) [N.Normal] (x : ↑(trivialF2 (G ⧸ N))) : (trivialF2Equiv G) ↑((trivialF2QuotientEquivFixedPoints N) x) = (trivialF2Equiv (G ⧸ N)) x

The coefficient equivalence does not change the underlying ZMod 2 value.

theorem TauCeti.trivialF2QuotientEquivFixedPoints_smul {G : Type u} [Group G] (N : Subgroup G) [N.Normal] (q : G ⧸ N) (x : ↑(trivialF2 (G ⧸ N))) : (trivialF2QuotientEquivFixedPoints N) (q • x) = q • (trivialF2QuotientEquivFixedPoints N) x

The coefficient equivalence is equivariant for the quotient actions.