The explicit models of H¹(G, 𝔽_p) and H²(G, 𝔽_p)

The cohomology cohomFp p G n with trivial ZMod p coefficients is Mathlib's continuous cohomology of an object of TopRep (ZMod p) G, while the explicit low-degree cohomology H1 G M and H2 G M of TauCeti.ContCohomology is computed from inhomogeneous cochains with values in a discrete G-module, and every rank count of a pro-p group is stated for the explicit model. This file identifies the two in degrees one and two.

The comparison for a discrete smooth representation over any scalars is TopRep.explicitH1AddEquivContinuousCohomologyOfDiscrete and its degree-two counterpart. For X = trivialFp p G the carrier is the universe lift of ZMod p, and a further change of coefficients along trivialFpEquiv p G lands in H1 G (ZMod p) and H2 G (ZMod p), for any trivial action of G on ZMod p. In degree one, the class group of a trivial action is the group of continuous characters, so H¹(G, 𝔽_p) is the continuous 𝔽_p-dual of G, as an 𝔽_p-vector space. The extensions of a profinite group by 𝔽_p are written multiplicatively, so the degree-two identification is also read on the additive type tag of Multiplicative (ZMod p) with a trivial action.

Main definitions

• TauCeti.cohomFpAddEquivH1, TauCeti.cohomFpAddEquivH2: cohomFp p G 1 and cohomFp p G 2 are the explicit H1 G (ZMod p) and H2 G (ZMod p) for a trivial action.
• TauCeti.cohomFpLinearEquivH2: the degree-two identification is 𝔽_p-linear; by TauCeti.cohomFpAddEquivH2_cohomFpMap it carries cohomFpMap to the explicit pullback, and TauCeti.natCard_H2_eq_pow_finrank_cohomFp_two counts the explicit model by the dimension.
• TauCeti.cohomFpAddEquivH2Additive: cohomFp p G 2 is the explicit H²(G, Additive 𝔽_p) of the additive type tag of a multiplicatively written 𝔽_p with trivial action.
• TauCeti.cohomFpLinearEquivContinuousZModDual: H¹(G, 𝔽_p) is the continuous 𝔽_p-dual of G, as an 𝔽_p-vector space; TauCeti.cohomFpLinearEquivContinuousZModDual_π_apply computes it on the class of a homogeneous one-cocycle.
• TauCeti.cohomFpTwoLinearEquivOfContinuousMulEquiv: a topological isomorphism G ≃ₜ* H induces H²(G, 𝔽_p) ≃ₗ[𝔽_p] H²(H, 𝔽_p), with no action of either group in its statement; on the explicit models it is the pullback along e.symm for any trivial actions (TauCeti.cohomFpTwoLinearEquivOfContinuousMulEquiv_apply), so TauCeti.finrank_cohomFp_two_congr: the dimension of H²(-, 𝔽_p) is an isomorphism invariant.

References

• J.-P. Serre, Galois Cohomology, I §2.

theorem TauCeti.trivialFpEquiv_smul (p : ℕ) (G : Type u) [Group G] [TopologicalSpace G] [DistribMulAction G (ZMod p)] (htriv : ∀ (g : G) (m : ZMod p), g • m = m) (g : G) (x : ↑(trivialFp p G)) : (trivialFpEquiv p G) ((ContinuousMulEquiv.refl G) g • x) = g • (trivialFpEquiv p G) x

The universe lift trivialFpEquiv p G is compatible with the trivial actions on both sides.

noncomputable def TauCeti.cohomFpAddEquivH1 (p : ℕ) (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [DistribMulAction G (ZMod p)] [ContinuousSMul G (ZMod p)] (htriv : ∀ (g : G) (m : ZMod p), g • m = m) : ↑(cohomFp p G 1).toModuleCat ≃+ ContCohomology.H1 G (ZMod p)

H¹(G, 𝔽_p) is the explicit H1 G (ZMod p), for any trivial action of G on ZMod p.

Equations

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

theorem TauCeti.cohomFpAddEquivH1_explicitH1AddEquivContinuousCohomologyOfDiscrete (p : ℕ) (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [DistribMulAction G (ZMod p)] [ContinuousSMul G (ZMod p)] (htriv : ∀ (g : G) (m : ZMod p), g • m = m) (x : ContCohomology.H1 G ↑(trivialFp p G)) : (cohomFpAddEquivH1 p G htriv) ((trivialFp p G).explicitH1AddEquivContinuousCohomologyOfDiscrete x) = (ContCohomology.explicitMap1Equiv G (↑(trivialFp p G)) G (ZMod p) (ContinuousMulEquiv.refl G) (trivialFpEquiv p G).toAddEquiv ⋯ ⋯ ⋯) x

On the comparison of the carrier of trivialFp p G, the identification cohomFpAddEquivH1 is the change of coefficients along the universe lift trivialFpEquiv p G.

noncomputable def TauCeti.cohomFpAddEquivH2 (p : ℕ) (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [DistribMulAction G (ZMod p)] [ContinuousSMul G (ZMod p)] (htriv : ∀ (g : G) (m : ZMod p), g • m = m) [LocallyCompactSpace G] : ↑(cohomFp p G 2).toModuleCat ≃+ ContCohomology.H2 G (ZMod p)

H²(G, 𝔽_p) is the explicit H2 G (ZMod p), for any trivial action of G on ZMod p.

Equations

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

theorem TauCeti.cohomFpAddEquivH2_explicitH2AddEquivContinuousCohomologyOfDiscrete (p : ℕ) (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [DistribMulAction G (ZMod p)] [ContinuousSMul G (ZMod p)] (htriv : ∀ (g : G) (m : ZMod p), g • m = m) [LocallyCompactSpace G] (x : ContCohomology.H2 G ↑(trivialFp p G)) : (cohomFpAddEquivH2 p G htriv) ((trivialFp p G).explicitH2AddEquivContinuousCohomologyOfDiscrete x) = (ContCohomology.explicitMap2Equiv G (↑(trivialFp p G)) G (ZMod p) (ContinuousMulEquiv.refl G) (trivialFpEquiv p G).toAddEquiv ⋯ ⋯ ⋯) x

On the comparison of the carrier of trivialFp p G, the identification cohomFpAddEquivH2 is the change of coefficients along the universe lift trivialFpEquiv p G.

theorem TauCeti.cohomFpAddEquivH2_cohomFpMap (p : ℕ) (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [DistribMulAction G (ZMod p)] [ContinuousSMul G (ZMod p)] (htriv : ∀ (g : G) (m : ZMod p), g • m = m) [LocallyCompactSpace G] {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] [LocallyCompactSpace H] [DistribMulAction H (ZMod p)] [ContinuousSMul H (ZMod p)] (htH : ∀ (h : H) (m : ZMod p), h • m = m) (φ : H →ₜ* G) (x : ↑(cohomFp p G 2).toModuleCat) : (cohomFpAddEquivH2 p H htH) ((CategoryTheory.ConcreteCategory.hom (cohomFpMap p φ 2)) x) = (ContCohomology.explicitMap2 G (ZMod p) H (ZMod p) φ (AddMonoidHom.id (ZMod p)) ⋯ ⋯) ((cohomFpAddEquivH2 p G htriv) x)

The degree-two identification is natural. Under cohomFpAddEquivH2, the cohomology map cohomFpMap p φ 2 along a continuous homomorphism φ : H →ₜ* G is the explicit pullback of two-cocycles along φ, for any trivial actions of G and H on ZMod p.

noncomputable def TauCeti.cohomFpLinearEquivH2 (p : ℕ) (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [DistribMulAction G (ZMod p)] [ContinuousSMul G (ZMod p)] (htriv : ∀ (g : G) (m : ZMod p), g • m = m) [LocallyCompactSpace G] : ↑(cohomFp p G 2).toModuleCat ≃ₗ[ZMod p] ContCohomology.H2 G (ZMod p)

H²(G, 𝔽_p) is the explicit H2 G (ZMod p) as an 𝔽_p-vector space, for any trivial action of G on ZMod p.

Equations

• TauCeti.cohomFpLinearEquivH2 p G htriv = LinearEquiv.ofBijective (AddMonoidHom.toZModLinearMap p (TauCeti.cohomFpAddEquivH2 p G htriv).toAddMonoidHom) ⋯

@[simp]

theorem TauCeti.cohomFpLinearEquivH2_apply (p : ℕ) (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [DistribMulAction G (ZMod p)] [ContinuousSMul G (ZMod p)] (htriv : ∀ (g : G) (m : ZMod p), g • m = m) [LocallyCompactSpace G] (x : ↑(cohomFp p G 2).toModuleCat) : (cohomFpLinearEquivH2 p G htriv) x = (cohomFpAddEquivH2 p G htriv) x

The linear identification of H²(G, 𝔽_p) with its explicit model is the additive one.

theorem TauCeti.natCard_H2_eq_pow_finrank_cohomFp_two (p : ℕ) (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [DistribMulAction G (ZMod p)] [ContinuousSMul G (ZMod p)] (htriv : ∀ (g : G) (m : ZMod p), g • m = m) [Fact (Nat.Prime p)] [LocallyCompactSpace G] [Module.Finite (ZMod p) ↑(cohomFp p G 2).toModuleCat] : Nat.card (ContCohomology.H2 G (ZMod p)) = p ^ Module.finrank (ZMod p) ↑(cohomFp p G 2).toModuleCat

The order of H²(G, 𝔽_p): a finite-dimensional H²(G, 𝔽_p) makes the explicit model H2 G (ZMod p) of order p ^ dim H²(G, 𝔽_p), for any trivial action of G on ZMod p.

noncomputable def TauCeti.cohomFpLinearEquivContinuousZModDual (p : ℕ) (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : ↑(cohomFp p G 1).toModuleCat ≃ₗ[ZMod p] continuousZModDual p G

H¹(G, 𝔽_p) is the continuous 𝔽_p-dual of G, as an 𝔽_p-vector space: the classes of continuous 1-cocycles for the trivial action are the continuous characters G → 𝔽_p.

Equations

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

theorem TauCeti.cohomFpLinearEquivContinuousZModDual_apply (p : ℕ) (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (x : ↑(cohomFp p G 1).toModuleCat) : (cohomFpLinearEquivContinuousZModDual p G) x = (ContCohomology.H1EquivOfSmulEqSelf ⋯) ((cohomFpAddEquivH1 p G ⋯) x)

The defining equation of cohomFpLinearEquivContinuousZModDual: for the trivial action trivialZModAction p G, it is the identification cohomFpAddEquivH1 of H¹(G, 𝔽_p) with the explicit model followed by the identification H1EquivOfSmulEqSelf of the explicit classes with the continuous characters.

theorem TauCeti.cohomFpLinearEquivContinuousZModDual_π_apply (p : ℕ) (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (z : ↑(ContinuousCohomology.cocycles (trivialFp p G) 1).toModuleCat) (g : G) : Multiplicative.toAdd ((Additive.toMul ((cohomFpLinearEquivContinuousZModDual p G) ((CategoryTheory.ConcreteCategory.hom (ContinuousCohomology.π (trivialFp p G) 1)) z))) g) = (trivialFpEquiv p G) ((↑((CategoryTheory.ConcreteCategory.hom (HomologicalComplex.iCycles (trivialFp p G).homogeneousCochains 1)) z) 1) g)

The character attached by cohomFpLinearEquivContinuousZModDual to the class of a homogeneous one-cocycle z reads z at (1, g).

theorem TauCeti.additiveMultiplicative_smul (p : ℕ) (G : Type u) [Group G] [MulDistribMulAction G (Multiplicative (ZMod p))] (htriv : ∀ (g : G) (m : Multiplicative (ZMod p)), g • m = m) (g : G) (m : Additive (Multiplicative (ZMod p))) : (AddEquiv.additiveMultiplicative (ZMod p)) (g • m) = g • (AddEquiv.additiveMultiplicative (ZMod p)) m

The identification Additive (Multiplicative (ZMod p)) ≃+ ZMod p carries a trivial action of G on the source to the trivial action TauCeti.trivialZModAction on the target.

noncomputable def TauCeti.cohomFpAddEquivH2Additive (p : ℕ) (G : Type u) [Group G] [MulDistribMulAction G (Multiplicative (ZMod p))] (htriv : ∀ (g : G) (m : Multiplicative (ZMod p)), g • m = m) [TopologicalSpace G] [IsTopologicalGroup G] [LocallyCompactSpace G] [hcont : ContinuousSMul G (Multiplicative (ZMod p))] : ↑(cohomFp p G 2).toModuleCat ≃+ ContCohomology.H2 G (Additive (Multiplicative (ZMod p)))

H²(G, 𝔽_p) is the explicit H²(G, Additive 𝔽_p) of the multiplicatively written 𝔽_p with a trivial action of G, read additively: the identification TauCeti.cohomFpAddEquivH2 with the explicit H²(G, ZMod p) for the trivial action, followed by the change of coefficients along Additive (Multiplicative (ZMod p)) ≃+ ZMod p.

Equations

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

theorem TauCeti.cohomFpAddEquivH2Additive_apply (p : ℕ) (G : Type u) [Group G] [MulDistribMulAction G (Multiplicative (ZMod p))] (htriv : ∀ (g : G) (m : Multiplicative (ZMod p)), g • m = m) [TopologicalSpace G] [IsTopologicalGroup G] [LocallyCompactSpace G] [hcont : ContinuousSMul G (Multiplicative (ZMod p))] (x : ↑(cohomFp p G 2).toModuleCat) : (cohomFpAddEquivH2Additive p G htriv) x = (ContCohomology.explicitMap2Equiv G (Additive (Multiplicative (ZMod p))) G (ZMod p) (ContinuousMulEquiv.refl G) (AddEquiv.additiveMultiplicative (ZMod p)) ⋯ ⋯ ⋯).symm ((cohomFpAddEquivH2 p G ⋯) x)

The identification TauCeti.cohomFpAddEquivH2Additive is TauCeti.cohomFpAddEquivH2 for the trivial action TauCeti.trivialZModAction, followed by the change of coefficients along Additive (Multiplicative (ZMod p)) ≃+ ZMod p.

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

H²(-, 𝔽_p) is invariant under topological isomorphism: a topological isomorphism G ≃ₜ* H induces an 𝔽_p-linear isomorphism H²(G, 𝔽_p) ≃ₗ[𝔽_p] H²(H, 𝔽_p). On the explicit models H2 G (ZMod p) and H2 H (ZMod p), for any trivial actions of G and H on ZMod p, it is the pullback along e.symm (TauCeti.cohomFpTwoLinearEquivOfContinuousMulEquiv_apply).

Equations

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

@[simp]

theorem TauCeti.cohomFpTwoLinearEquivOfContinuousMulEquiv_apply (p : ℕ) {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [LocallyCompactSpace G] {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] [LocallyCompactSpace H] [DistribMulAction G (ZMod p)] [ContinuousSMul G (ZMod p)] [DistribMulAction H (ZMod p)] [ContinuousSMul H (ZMod p)] (e : G ≃ₜ* H) (htG : ∀ (g : G) (m : ZMod p), g • m = m) (htH : ∀ (h : H) (m : ZMod p), h • m = m) (x : ↑(cohomFp p G 2).toModuleCat) : (cohomFpTwoLinearEquivOfContinuousMulEquiv p e) x = (cohomFpLinearEquivH2 p H htH).symm ((ContCohomology.explicitMap2 G (ZMod p) H (ZMod p) (↑e.symm) (AddMonoidHom.id (ZMod p)) ⋯ ⋯) ((cohomFpLinearEquivH2 p G htG) x))

On the explicit models, for any trivial actions of G and H on ZMod p, the transport of H²(-, 𝔽_p) along e : G ≃ₜ* H is the pullback along e.symm.

theorem TauCeti.finrank_cohomFp_two_congr (p : ℕ) {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [LocallyCompactSpace G] {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] (e : G ≃ₜ* H) : Module.finrank (ZMod p) ↑(cohomFp p G 2).toModuleCat = Module.finrank (ZMod p) ↑(cohomFp p H 2).toModuleCat

The dimension of H²(-, 𝔽_p) is invariant under topological isomorphism.