Trivial ZMod p coefficients for continuous cohomology

This file provides the trivial representation trivialFp p G of a group G on ZMod p. When p is prime this gives the coefficient object for cohomology of pro-p groups over the field 𝔽_p. Mathlib's continuous-cohomology resolution requires coefficients in the universe of G, so its carrier is the corresponding universe lift of ZMod p. The abbreviation cohomFp p G n is continuous cohomology with these coefficients.

The coefficient object is deliberately available for an arbitrary topological group. The pro-p hypothesis belongs to the theorems which compute this cohomology, not to its definition. The restriction map is named because later rank and cup-product arguments must change groups without repeatedly transporting across the definitional equality of trivial representations.

Main definitions

• TauCeti.trivialFp: trivial ZMod p coefficients in the universe of the group.
• TauCeti.cohomFp: continuous cohomology with trivial ZMod p coefficients.
• TauCeti.trivialFpResMap: restriction on cohomFp.
• TauCeti.cohomFpMap: the map induced by a continuous group homomorphism.
• TauCeti.cohomFpLinearEquiv: invariance under topological group isomorphism.

Main results

• TauCeti.trivialFp_ρ_apply_apply, TauCeti.smul_trivialFp_V: the action is trivial.
• TauCeti.continuousSMul_trivialFp: the derived action on the carrier is continuous.
• TauCeti.natCard_trivialFp_V: the Nat.card of the carrier is p.
• TauCeti.nontrivial_cohomFp_zero: H⁰(G, ZMod p) is nontrivial.
• TauCeti.res_trivialFp: restriction preserves trivial coefficients on the nose; TauCeti.trivialFpEquiv_eqToHom_res_trivialFp: the transport along this equality is the identity on the underlying values.
• TauCeti.trivialFpQuotientToInvariantsIso: the quotient representation on the invariants of trivial coefficients is canonically the trivial coefficient object of the quotient group.
• TauCeti.zmodEquivFixedPointsOfTrivialAction: for any trivial action on ZMod p, the fixed points of a subgroup are additively equivalent to ZMod p itself.

References

• J.-P. Serre, Galois Cohomology, I §4.
• TauCeti.RepresentationTheory.Homological.ContCohomology.TrivialF2, whose coefficient API provides the formal template for this module.

noncomputable def TauCeti.trivialFp (p : ℕ) (G : Type u) [Monoid G] : TopRep (ZMod p) G

Trivial ZMod p coefficients as an object of TopRep (ZMod p) G in the universe of G.

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

Equations

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

@[simp]

theorem TauCeti.trivialFp_V (p : ℕ) (G : Type u) [Monoid G] : ↑(trivialFp p G) = ULift.{u, 0} (ZMod p)

The carrier of trivialFp p G is the universe lift of ZMod p.

noncomputable def TauCeti.trivialFpEquiv (p : ℕ) (G : Type u) [Monoid G] : ↑(trivialFp p G) ≃ₗ[ZMod p] ZMod p

The ZMod p-linear equivalence from the lifted carrier of trivialFp p G to ZMod p.

Equations

• TauCeti.trivialFpEquiv p G = ULift.moduleEquiv

@[simp]

theorem TauCeti.trivialFpEquiv_apply (p : ℕ) (G : Type u) [Monoid G] (x : ULift.{u, 0} (ZMod p)) : (trivialFpEquiv p G) (cast ⋯ x) = x.down

trivialFpEquiv sends a lifted element to its underlying value.

@[simp]

theorem TauCeti.trivialFpEquiv_symm_apply (p : ℕ) (G : Type u) [Monoid G] (x : ZMod p) : (trivialFpEquiv p G).symm x = cast ⋯ { down := x }

The inverse of trivialFpEquiv lifts a value.

instance TauCeti.instDiscreteTopologyVZModTrivialFp (p : ℕ) (G : Type u) [Monoid G] : DiscreteTopology ↑(trivialFp p G)

The lifted carrier of trivialFp p G has the discrete topology.

instance TauCeti.instFiniteVZModTrivialFpOfNeZeroNat (p : ℕ) (G : Type u) [Monoid G] [NeZero p] : Finite ↑(trivialFp p G)

The lifted carrier of trivialFp p G is finite, for p ≠ 0.

theorem TauCeti.natCard_trivialFp_V (p : ℕ) (G : Type u) [Monoid G] : Nat.card ↑(trivialFp p G) = p

The Nat.card of the carrier of trivialFp p G is p. For p ≠ 0 this says that the carrier has p elements; for p = 0 the carrier is infinite, and Nat.card is 0 by convention.

@[simp]

theorem TauCeti.trivialFp_ρ_apply_apply (p : ℕ) (G : Type u) [Monoid G] (g : G) (x : ↑(trivialFp p G)) : ((trivialFp p G).ρ g) x = x

Every monoid element acts trivially on trivialFp p G.

theorem TauCeti.smul_trivialFp_V (p : ℕ) (G : Type u) [Monoid G] (g : G) (x : ↑(trivialFp p G)) : g • x = x

The derived action of G on the carrier of trivialFp p G is trivial. Not a simp lemma: simp already proves it from TopRep.distribMulAction_smul and trivialFp_ρ_apply_apply.

theorem TauCeti.isSmoothDiscrete_trivialFp (p : ℕ) (G : Type u) [Monoid G] [TopologicalSpace G] : IsSmoothDiscrete (ZMod p) (trivialFp p G)

The trivial ZMod p coefficient object is smooth discrete.

@[simp]

theorem TauCeti.res_trivialFp (p : ℕ) (G : Type u) [Group G] (S : Subgroup G) : TopRep.res S.subtype (trivialFp p G) = trivialFp p ↥S

Restriction preserves the trivial ZMod p coefficient object on the nose.

@[simp]

theorem TauCeti.trivialFpEquiv_eqToHom_res_trivialFp (p : ℕ) (G : Type u) [Group G] (S : Subgroup G) (x : ↑(TopRep.res S.subtype (trivialFp p G))) : (trivialFpEquiv p ↥S) ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.eqToHom ⋯)) x) = (trivialFpEquiv p G) x

Transport along res_trivialFp is the identity on the underlying values: the restricted coefficient object and trivialFp p S have the same lifted carrier, and trivialFpEquiv reads off the same value on both sides.

noncomputable def TauCeti.zmodEquivFixedPointsOfTrivialAction (p : ℕ) (G : Type u) [Group G] [DistribMulAction G (ZMod p)] (N : Subgroup G) (htriv : ∀ (g : G) (m : ZMod p), g • m = m) : ZMod p ≃+ ↥(FixedPoints.addSubgroup (↥N) (ZMod p))

For a trivial action, ZMod p is additively equivalent to its subgroup of N-fixed points.

Equations

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

@[simp]

theorem TauCeti.zmodEquivFixedPointsOfTrivialAction_apply (p : ℕ) (G : Type u) [Group G] [DistribMulAction G (ZMod p)] (N : Subgroup G) (htriv : ∀ (g : G) (m : ZMod p), g • m = m) (m : ZMod p) : ↑((zmodEquivFixedPointsOfTrivialAction p G N htriv) m) = m

The fixed-point equivalence for a trivial action preserves the underlying ZMod p value.

theorem TauCeti.continuousSMul_trivialFp (p : ℕ) (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : ContinuousSMul G ↑(trivialFp p G)

The derived action of G on the carrier of trivialFp p G is continuous, the carrier being discrete and the action trivial.

noncomputable def TauCeti.trivialFpQuotientToInvariantsContinuousLinearEquiv (p : ℕ) (G : Type u) [Group G] (N : Subgroup G) [N.Normal] : ↑(trivialFp p (G ⧸ N)) ≃L[ZMod p] ↥((trivialFp p G).ρ.restrict N.subtype).invariants

The carrier of trivial coefficients for G ⧸ N is continuously linearly equivalent to the N-invariants of trivial coefficients for G, by preserving the underlying ZMod p value.

Equations

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

noncomputable def TauCeti.trivialFpQuotientToInvariantsIso (p : ℕ) (G : Type u) [Group G] (N : Subgroup G) [N.Normal] : trivialFp p (G ⧸ N) ≅ (trivialFp p G).quotientToInvariants N

Trivial coefficients for G ⧸ N are the quotient representation on the N-invariants of trivial coefficients for G. This is the coefficient adapter used by inflation.

Equations

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

@[simp]

theorem TauCeti.trivialFpEquiv_trivialFpQuotientToInvariantsIso_hom_apply (p : ℕ) (G : Type u) [Group G] (N : Subgroup G) [N.Normal] (x : ↑(trivialFp p (G ⧸ N))) : (trivialFpEquiv p G) ↑((CategoryTheory.ConcreteCategory.hom (trivialFpQuotientToInvariantsIso p G N).hom) x) = (trivialFpEquiv p (G ⧸ N)) x

The coefficient adapter preserves the underlying ZMod p value.

@[reducible, inline]

noncomputable abbrev TauCeti.cohomFp (p : ℕ) (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (n : ℕ) : TopModuleCat (ZMod p)

Continuous cohomology with trivial ZMod p coefficients.

Equations

• TauCeti.cohomFp p G n = continuousCohomology n (TauCeti.trivialFp p G)

theorem TauCeti.nontrivial_cohomFp_zero (p : ℕ) (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [Nontrivial (ZMod p)] : Nontrivial ↑(cohomFp p G 0).toModuleCat

H⁰(G, ZMod p) is nontrivial: it is the invariants of the trivial representation, that is the whole of ZMod p.

noncomputable def TauCeti.trivialFpResMap (p : ℕ) (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (S : Subgroup G) (n : ℕ) : cohomFp p G n ⟶ cohomFp p (↥S) n

Restriction on cohomology with trivial ZMod p coefficients.

Equations

• TauCeti.trivialFpResMap p G S n = CategoryTheory.CategoryStruct.comp (TauCeti.ContinuousCohomology.res S (TauCeti.trivialFp p G) n) (CategoryTheory.eqToHom ⋯)

theorem TauCeti.trivialFpResMap_def (p : ℕ) (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (S : Subgroup G) (n : ℕ) : trivialFpResMap p G S n = CategoryTheory.CategoryStruct.comp (ContinuousCohomology.res S (trivialFp p G) n) (CategoryTheory.eqToHom ⋯)

The defining equation of restriction with trivial ZMod p coefficients.

@[simp]

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

Restriction along a continuous group homomorphism preserves trivial coefficients.

@[simp]

theorem TauCeti.trivialFpEquiv_eqToHom_res_trivialFp_hom (p : ℕ) {G H : Type u} [Group G] [TopologicalSpace G] [Group H] [TopologicalSpace H] (φ : H →ₜ* G) (x : ↑(TopRep.res (↑φ) (trivialFp p G))) : (trivialFpEquiv p H) ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.eqToHom ⋯)) x) = (trivialFpEquiv p G) x

The transport to trivial coefficients along a homomorphism leaves coefficient values unchanged.

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

The contravariant map on cohomology with trivial ZMod p coefficients.

Equations

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

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

The cohomology map is the general map with identity transport on trivial coefficients.

theorem TauCeti.trivialFpQuotientToInvariantsIso_hom_comp_quotientToInvariantsι (p : ℕ) {G : Type u} [Group G] [TopologicalSpace G] (N : Subgroup G) [N.Normal] : CategoryTheory.CategoryStruct.comp ((TopRep.resFunctor ↑(ContinuousMonoidHom.quotientMk N)).map (trivialFpQuotientToInvariantsIso p G N).hom) ((trivialFp p G).quotientToInvariantsι N) = CategoryTheory.eqToHom ⋯

After the trivial-coefficient adapter, the inclusion of quotient invariants is the identity coefficient morphism along the quotient map. This pins the coefficient identification used by inflation.

theorem TauCeti.coeffMap_trivialFpQuotientToInvariantsIso_hom_comp_infl (p : ℕ) {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (N : Subgroup G) [N.Normal] (n : ℕ) : CategoryTheory.CategoryStruct.comp (ContinuousCohomology.coeffMap (trivialFpQuotientToInvariantsIso p G N).hom n) (ContinuousCohomology.infl N (trivialFp p G) n) = cohomFpMap p (ContinuousMonoidHom.quotientMk N) n

With the quotient-invariants coefficient object identified with trivial coefficients, canonical inflation is the usual contravariant map along the quotient homomorphism.

@[simp]

theorem TauCeti.cohomFpMap_subgroupSubtype (p : ℕ) {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (S : Subgroup G) (n : ℕ) : cohomFpMap p (ContinuousMonoidHom.subgroupSubtype S) n = trivialFpResMap p G S n

The general cohomology map along a subgroup inclusion is the named restriction map.

@[simp]

theorem TauCeti.cohomFpMap_id (p : ℕ) {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (n : ℕ) : cohomFpMap p (ContinuousMonoidHom.id G) n = CategoryTheory.CategoryStruct.id (cohomFp p G n)

The identity homomorphism induces the identity on cohomology.

theorem TauCeti.res_trivialFp_hom_comp (p : ℕ) {G H K : Type u} [Group G] [TopologicalSpace G] [Group H] [TopologicalSpace H] [Group K] [TopologicalSpace K] (φ : H →ₜ* G) (ψ : K →ₜ* H) : CategoryTheory.CategoryStruct.comp ((TopRep.resFunctor ↑ψ).map (CategoryTheory.eqToHom ⋯)) (CategoryTheory.eqToHom ⋯) = CategoryTheory.eqToHom ⋯

The transports of trivial coefficients compose along continuous group homomorphisms.

@[simp]

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

Cohomology maps with trivial coefficients compose contravariantly.

noncomputable def TauCeti.cohomFpLinearEquiv (p : ℕ) {G H : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [Group H] [TopologicalSpace H] [IsTopologicalGroup H] (e : G ≃ₜ* H) (n : ℕ) : ↑(cohomFp p G n).toModuleCat ≃ₗ[ZMod p] ↑(cohomFp p H n).toModuleCat

The cohomology map induced by a topological group isomorphism is a linear equivalence, with the inverse induced by the inverse group isomorphism.

Equations

• TauCeti.cohomFpLinearEquiv p e n = ↑{ hom := TauCeti.cohomFpMap p (↑e.symm) n, inv := TauCeti.cohomFpMap p (↑e) n, hom_inv_id := ⋯, inv_hom_id := ⋯ }.toContinuousLinearEquiv

@[simp]

theorem TauCeti.cohomFpLinearEquiv_apply (p : ℕ) {G H : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [Group H] [TopologicalSpace H] [IsTopologicalGroup H] (e : G ≃ₜ* H) (n : ℕ) (x : ↑(cohomFp p G n).toModuleCat) : (cohomFpLinearEquiv p e n) x = (CategoryTheory.ConcreteCategory.hom (cohomFpMap p (↑e.symm) n)) x

The cohomology equivalence acts by the map induced by the inverse group isomorphism.

@[simp]

theorem TauCeti.cohomFpLinearEquiv_symm_apply (p : ℕ) {G H : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [Group H] [TopologicalSpace H] [IsTopologicalGroup H] (e : G ≃ₜ* H) (n : ℕ) (x : ↑(cohomFp p H n).toModuleCat) : (cohomFpLinearEquiv p e n).symm x = (CategoryTheory.ConcreteCategory.hom (cohomFpMap p (↑e) n)) x

The inverse cohomology equivalence acts by the map induced by the forward group isomorphism.