Continuous cohomology of topological groups in degrees ≤ 2

Continuous (inhomogeneous) cochain cohomology H⁰, H¹, H² of a topological group G with coefficients in a topological G-module M, following Serre, Galois Cohomology I §2.2. This is the coefficient system for the literature axioms B3 (Demushkin), B6 (local Tate duality), B7 (local Euler characteristic) and B9 (Evens/Kahn) — see docs/orchestration/formalization-plan.md (U2). Design constraints: no derived functors, no new coefficient structures (module = Mathlib classes, cf. GQ2/DiscreteModule.lean), everything explicit and human-checkable.

Definitions

Cochains are plain functions (G → M, G × G → M); continuity is carried by the subgroups:

• ContCoh.C1, C2 — continuous cochains;
• ContCoh.dZero, dOne, dTwo — the inhomogeneous differentials (δ⁰m)(g) = g•m − m, (δ¹ψ)(g,h) = g•ψ(h) − ψ(gh) + ψ(g), (δ²φ)(g,h,k) = g•φ(h,k) − φ(gh,k) + φ(g,hk) − φ(g,h) (with δ∘δ = 0 proved);
• ContCoh.Z1 = C1 ⊓ ker δ¹, Z2 = C2 ⊓ ker δ² — continuous cocycles (readable forms: mem_Z1_iff, mem_Z2_iff);
• ContCoh.B1 = δ⁰(M), B2 = δ¹(C1) — continuous coboundaries (B1_le_Z1, B2_le_Z2);
• ContCoh.H0 (invariants, an AddSubgroup M), ContCoh.H1, ContCoh.H2 (cocycles mod coboundaries, with AddCommGroup instances).

Functoriality

One general pullback along a compatible pair: a continuous hom π : G →ₜ* Q together with a continuous additive map f : N →+ M intertwining the actions (f (π g • n) = g • f n) induces H0comap, H1comap, H2comap : Hⁱ(Q,N) →+ Hⁱ(G,M). Specializations:

• restriction res0/res1/res2 : Hⁱ(G,M) →+ Hⁱ(U,M) for U : Subgroup G (π = inclusion, f = id — Mathlib's subgroup action instances make this definitional);
• inflation: for π : G ↠ Q and a Q-module N, instantiate the G-module as N with the composed action letI := DistribMulAction.compHom N π.toMonoidHom; then hcompat is rfl and H1comap π (AddMonoidHom.id N) … is inflation. (Kept as a recipe rather than a def to avoid carrying two actions on one type; finite-level comparison lemmas live in the downstream cohomology layer.)

Corestriction (degree 1, open finite-index U) is given by the Evens–Kahn explicit coset formula; cup products relative to a pairing M →+ N →+ P are defined in GQ2/CupProduct.lean. Both build on the Z-level API here.

Stress tests

dOne_comp_dZero = 0, dTwo_comp_dOne = 0; for the trivial action: B1 = ⊥, mem_Z1_iff_of_trivial (1-cocycles = continuous additive-style homs), H1equivZ1OfTrivial (H¹ ≃+ Z¹), H0_eq_top_of_trivial; Z1_apply_one (cocycles vanish at 1).

Degree 0

def GQ2.ContCoh.H0 (G : Type u_1) [Group G] (M : Type u_2) [AddCommGroup M] [DistribMulAction G M] : AddSubgroup M

H⁰(G, M): the invariants M^G, as an additive subgroup of M.

Equations

• GQ2.ContCoh.H0 G M = { carrier := {m : M | ∀ (g : G), g • m = m}, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯ }

Cochains and differentials

def GQ2.ContCoh.C1 (G : Type u_1) [TopologicalSpace G] (M : Type u_2) [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] : AddSubgroup (G → M)

Continuous 1-cochains C¹(G, M).

Equations

• GQ2.ContCoh.C1 G M = { carrier := {φ : G → M | Continuous φ}, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯ }

def GQ2.ContCoh.C2 (G : Type u_1) [TopologicalSpace G] (M : Type u_2) [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] : AddSubgroup (G × G → M)

Continuous 2-cochains C²(G, M).

Equations

• GQ2.ContCoh.C2 G M = { carrier := {φ : G × G → M | Continuous φ}, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯ }

def GQ2.ContCoh.dZero (G : Type u_1) [Group G] (M : Type u_2) [AddCommGroup M] [DistribMulAction G M] : M →+ G → M

The differential δ⁰ : M → C¹, (δ⁰m)(g) = g•m − m.

Equations

• GQ2.ContCoh.dZero G M = { toFun := fun (m : M) (g : G) => g • m - m, map_zero' := ⋯, map_add' := ⋯ }

def GQ2.ContCoh.dOne (G : Type u_1) [Group G] (M : Type u_2) [AddCommGroup M] [DistribMulAction G M] : (G → M) →+ G × G → M

The differential δ¹ : C¹ → C², (δ¹ψ)(g,h) = g•ψ(h) − ψ(gh) + ψ(g).

Equations

• GQ2.ContCoh.dOne G M = { toFun := fun (ψ : G → M) (p : G × G) => p.1 • ψ p.2 - ψ (p.1 * p.2) + ψ p.1, map_zero' := ⋯, map_add' := ⋯ }

def GQ2.ContCoh.dTwo (G : Type u_1) [Group G] (M : Type u_2) [AddCommGroup M] [DistribMulAction G M] : (G × G → M) →+ G × G × G → M

The differential δ² : C² → C³, (δ²φ)(g,h,k) = g•φ(h,k) − φ(gh,k) + φ(g,hk) − φ(g,h).

Equations

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

Cocycles, coboundaries, cohomology

def GQ2.ContCoh.Z1 (G : Type u_1) [Group G] [TopologicalSpace G] (M : Type u_2) [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribMulAction G M] : AddSubgroup (G → M)

Continuous 1-cocycles: continuous cochains killed by δ¹.

Equations

• GQ2.ContCoh.Z1 G M = GQ2.ContCoh.C1 G M ⊓ (GQ2.ContCoh.dOne G M).ker

def GQ2.ContCoh.Z2 (G : Type u_1) [Group G] [TopologicalSpace G] (M : Type u_2) [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribMulAction G M] : AddSubgroup (G × G → M)

Continuous 2-cocycles: continuous cochains killed by δ².

Equations

• GQ2.ContCoh.Z2 G M = GQ2.ContCoh.C2 G M ⊓ (GQ2.ContCoh.dTwo G M).ker

def GQ2.ContCoh.B1 (G : Type u_1) [Group G] (M : Type u_2) [AddCommGroup M] [DistribMulAction G M] : AddSubgroup (G → M)

1-coboundaries δ⁰(M) (automatically continuous).

Equations

• GQ2.ContCoh.B1 G M = (GQ2.ContCoh.dZero G M).range

def GQ2.ContCoh.B2 (G : Type u_1) [Group G] [TopologicalSpace G] (M : Type u_2) [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribMulAction G M] : AddSubgroup (G × G → M)

2-coboundaries δ¹(C¹) — the image of the continuous 1-cochains.

Equations

• GQ2.ContCoh.B2 G M = AddSubgroup.map (GQ2.ContCoh.dOne G M) (GQ2.ContCoh.C1 G M)

def GQ2.ContCoh.H1 (G : Type u_1) [Group G] [TopologicalSpace G] (M : Type u_2) [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribMulAction G M] : Type (max u_1 u_2)

H¹(G, M): continuous 1-cocycles modulo 1-coboundaries.

Equations

• GQ2.ContCoh.H1 G M = (↥(GQ2.ContCoh.Z1 G M) ⧸ (GQ2.ContCoh.B1 G M).addSubgroupOf (GQ2.ContCoh.Z1 G M))

@[implicit_reducible]

instance GQ2.ContCoh.instAddCommGroupH1 (G : Type u_1) [Group G] [TopologicalSpace G] (M : Type u_2) [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribMulAction G M] : AddCommGroup (H1 G M)

Equations

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

def GQ2.ContCoh.H1mk (G : Type u_1) [Group G] [TopologicalSpace G] (M : Type u_2) [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribMulAction G M] : ↥(Z1 G M) →+ H1 G M

The class map Z¹ → H¹.

Equations

• GQ2.ContCoh.H1mk G M = QuotientAddGroup.mk' ((GQ2.ContCoh.B1 G M).addSubgroupOf (GQ2.ContCoh.Z1 G M))

def GQ2.ContCoh.H2 (G : Type u_1) [Group G] [TopologicalSpace G] (M : Type u_2) [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribMulAction G M] : Type (max u_1 u_2)

H²(G, M): continuous 2-cocycles modulo coboundaries of continuous 1-cochains.

Equations

• GQ2.ContCoh.H2 G M = (↥(GQ2.ContCoh.Z2 G M) ⧸ (GQ2.ContCoh.B2 G M).addSubgroupOf (GQ2.ContCoh.Z2 G M))

@[implicit_reducible]

instance GQ2.ContCoh.instAddCommGroupH2 (G : Type u_1) [Group G] [TopologicalSpace G] (M : Type u_2) [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribMulAction G M] : AddCommGroup (H2 G M)

Equations

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

def GQ2.ContCoh.H2mk (G : Type u_1) [Group G] [TopologicalSpace G] (M : Type u_2) [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribMulAction G M] : ↥(Z2 G M) →+ H2 G M

The class map Z² → H².

Equations

• GQ2.ContCoh.H2mk G M = QuotientAddGroup.mk' ((GQ2.ContCoh.B2 G M).addSubgroupOf (GQ2.ContCoh.Z2 G M))

Basic API

@[simp]

theorem GQ2.ContCoh.mem_C1_iff {G : Type u_1} [TopologicalSpace G] {M : Type u_2} [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] {φ : G → M} : φ ∈ C1 G M ↔ Continuous φ

theorem GQ2.ContCoh.dOne_comp_dZero {G : Type u_1} [Group G] {M : Type u_2} [AddCommGroup M] [DistribMulAction G M] : (dOne G M).comp (dZero G M) = 0

δ¹ ∘ δ⁰ = 0: coboundaries are cocycles (chain-complex sanity).

theorem GQ2.ContCoh.dTwo_comp_dOne {G : Type u_1} [Group G] {M : Type u_2} [AddCommGroup M] [DistribMulAction G M] : (dTwo G M).comp (dOne G M) = 0

δ² ∘ δ¹ = 0 (chain-complex sanity).

theorem GQ2.ContCoh.mem_Z1_iff {G : Type u_1} [Group G] [TopologicalSpace G] {M : Type u_2} [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribMulAction G M] {φ : G → M} : φ ∈ Z1 G M ↔ Continuous φ ∧ ∀ (g h : G), φ (g * h) = φ g + g • φ h

Membership in Z¹, in cocycle-identity form: continuous crossed homomorphisms.

theorem GQ2.ContCoh.mem_Z2_iff {G : Type u_1} [Group G] [TopologicalSpace G] {M : Type u_2} [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribMulAction G M] {φ : G × G → M} : φ ∈ Z2 G M ↔ Continuous φ ∧ ∀ (g h k : G), g • φ (h, k) + φ (g, h * k) = φ (g * h, k) + φ (g, h)

Membership in Z², in Serre's cocycle-identity form g•φ(h,k) + φ(g,hk) = φ(gh,k) + φ(g,h).

theorem GQ2.ContCoh.B1_le_Z1 {G : Type u_1} [Group G] [TopologicalSpace G] {M : Type u_2} [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribMulAction G M] [ContinuousSMul G M] : B1 G M ≤ Z1 G M

theorem GQ2.ContCoh.B2_le_Z2 {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {M : Type u_2} [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribMulAction G M] [ContinuousSMul G M] : B2 G M ≤ Z2 G M

theorem GQ2.ContCoh.H1mk_surjective {G : Type u_1} [Group G] [TopologicalSpace G] {M : Type u_2} [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribMulAction G M] : Function.Surjective ⇑(H1mk G M)

theorem GQ2.ContCoh.H2mk_surjective {G : Type u_1} [Group G] [TopologicalSpace G] {M : Type u_2} [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribMulAction G M] : Function.Surjective ⇑(H2mk G M)

theorem GQ2.ContCoh.Z1_apply_one {G : Type u_1} [Group G] [TopologicalSpace G] {M : Type u_2} [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribMulAction G M] (φ : ↥(Z1 G M)) : ↑φ 1 = 0

A 1-cocycle vanishes at 1.

Functoriality: pullback along a compatible pair

Given π : G →ₜ* Q continuous and f : N →+ M continuous with f (π g • n) = g • f n, cochains pull back by φ ↦ f ∘ φ ∘ π (in each degree), inducing Hⁱ(Q,N) →+ Hⁱ(G,M). Restriction and inflation are instances of this single construction (see module docstring).

def GQ2.ContCoh.H0comap {G : Type u_1} [Group G] [TopologicalSpace G] {M : Type u_2} [AddCommGroup M] [DistribMulAction G M] {Q : Type u_3} [Group Q] [TopologicalSpace Q] {N : Type u_4} [AddCommGroup N] [DistribMulAction Q N] (π : G →ₜ* Q) (f : N →+ M) (hcompat : ∀ (g : G) (n : N), f (π g • n) = g • f n) : ↥(H0 Q N) →+ ↥(H0 G M)

Degree-0 pullback: invariants map to invariants (no continuity of f needed).

Equations

• GQ2.ContCoh.H0comap π f hcompat = { toFun := fun (n : ↥(GQ2.ContCoh.H0 Q N)) => ⟨f ↑n, ⋯⟩, map_zero' := ⋯, map_add' := ⋯ }

def GQ2.ContCoh.Z1comap {G : Type u_1} [Group G] [TopologicalSpace G] {M : Type u_2} [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribMulAction G M] {Q : Type u_3} [Group Q] [TopologicalSpace Q] {N : Type u_4} [AddCommGroup N] [TopologicalSpace N] [IsTopologicalAddGroup N] [DistribMulAction Q N] (π : G →ₜ* Q) (f : N →+ M) (hf : Continuous ⇑f) (hcompat : ∀ (g : G) (n : N), f (π g • n) = g • f n) : ↥(Z1 Q N) →+ ↥(Z1 G M)

Degree-1 pullback on cocycles: φ ↦ f ∘ φ ∘ π.

Equations

• GQ2.ContCoh.Z1comap π f hf hcompat = { toFun := fun (φ : ↥(GQ2.ContCoh.Z1 Q N)) => ⟨fun (g : G) => f (↑φ (π g)), ⋯⟩, map_zero' := ⋯, map_add' := ⋯ }

def GQ2.ContCoh.Z2comap {G : Type u_1} [Group G] [TopologicalSpace G] {M : Type u_2} [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribMulAction G M] {Q : Type u_3} [Group Q] [TopologicalSpace Q] {N : Type u_4} [AddCommGroup N] [TopologicalSpace N] [IsTopologicalAddGroup N] [DistribMulAction Q N] (π : G →ₜ* Q) (f : N →+ M) (hf : Continuous ⇑f) (hcompat : ∀ (g : G) (n : N), f (π g • n) = g • f n) : ↥(Z2 Q N) →+ ↥(Z2 G M)

Degree-2 pullback on cocycles: φ ↦ f ∘ φ ∘ (π × π).

Equations

• GQ2.ContCoh.Z2comap π f hf hcompat = { toFun := fun (φ : ↥(GQ2.ContCoh.Z2 Q N)) => ⟨fun (p : G × G) => f (↑φ (π p.1, π p.2)), ⋯⟩, map_zero' := ⋯, map_add' := ⋯ }

def GQ2.ContCoh.H1comap {G : Type u_1} [Group G] [TopologicalSpace G] {M : Type u_2} [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribMulAction G M] {Q : Type u_3} [Group Q] [TopologicalSpace Q] {N : Type u_4} [AddCommGroup N] [TopologicalSpace N] [IsTopologicalAddGroup N] [DistribMulAction Q N] (π : G →ₜ* Q) (f : N →+ M) (hf : Continuous ⇑f) (hcompat : ∀ (g : G) (n : N), f (π g • n) = g • f n) : H1 Q N →+ H1 G M

Degree-1 pullback on cohomology.

Equations

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

def GQ2.ContCoh.H2comap {G : Type u_1} [Group G] [TopologicalSpace G] {M : Type u_2} [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribMulAction G M] {Q : Type u_3} [Group Q] [TopologicalSpace Q] {N : Type u_4} [AddCommGroup N] [TopologicalSpace N] [IsTopologicalAddGroup N] [DistribMulAction Q N] (π : G →ₜ* Q) (f : N →+ M) (hf : Continuous ⇑f) (hcompat : ∀ (g : G) (n : N), f (π g • n) = g • f n) : H2 Q N →+ H2 G M

Degree-2 pullback on cohomology.

Equations

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

Restriction to a subgroup

def GQ2.ContCoh.subgroupIncl (G : Type u_1) [Group G] [TopologicalSpace G] (U : Subgroup G) : ↥U →ₜ* G

The inclusion of a subgroup as a continuous monoid hom.

Equations

• GQ2.ContCoh.subgroupIncl G U = { toMonoidHom := U.subtype, continuous_toFun := ⋯ }

def GQ2.ContCoh.res0 (G : Type u_1) [Group G] [TopologicalSpace G] (M : Type u_2) [AddCommGroup M] [DistribMulAction G M] (U : Subgroup G) : ↥(H0 G M) →+ ↥(H0 (↥U) M)

Restriction H⁰(G,M) → H⁰(U,M).

Equations

• GQ2.ContCoh.res0 G M U = GQ2.ContCoh.H0comap (GQ2.ContCoh.subgroupIncl G U) (AddMonoidHom.id M) ⋯

def GQ2.ContCoh.res1 (G : Type u_1) [Group G] [TopologicalSpace G] (M : Type u_2) [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribMulAction G M] (U : Subgroup G) : H1 G M →+ H1 (↥U) M

Restriction H¹(G,M) → H¹(U,M).

Equations

• GQ2.ContCoh.res1 G M U = GQ2.ContCoh.H1comap (GQ2.ContCoh.subgroupIncl G U) (AddMonoidHom.id M) ⋯ ⋯

def GQ2.ContCoh.res2 (G : Type u_1) [Group G] [TopologicalSpace G] (M : Type u_2) [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribMulAction G M] (U : Subgroup G) : H2 G M →+ H2 (↥U) M

Restriction H²(G,M) → H²(U,M).

Equations

• GQ2.ContCoh.res2 G M U = GQ2.ContCoh.H2comap (GQ2.ContCoh.subgroupIncl G U) (AddMonoidHom.id M) ⋯ ⋯

The trivial-action stress tests

theorem GQ2.ContCoh.mem_Z1_iff_of_trivial {G : Type u_1} [Group G] [TopologicalSpace G] {M : Type u_2} [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribMulAction G M] (htriv : ∀ (g : G) (m : M), g • m = m) {φ : G → M} : φ ∈ Z1 G M ↔ Continuous φ ∧ ∀ (g h : G), φ (g * h) = φ g + φ h

With trivial action, Z¹ is exactly the continuous additive-style homs (φ(gh) = φ(g) + φ(h)).

theorem GQ2.ContCoh.B1_eq_bot_of_trivial {G : Type u_1} [Group G] {M : Type u_2} [AddCommGroup M] [DistribMulAction G M] (htriv : ∀ (g : G) (m : M), g • m = m) : B1 G M = ⊥

With trivial action there are no nonzero 1-coboundaries.

noncomputable def GQ2.ContCoh.H1equivZ1OfTrivial {G : Type u_1} [Group G] [TopologicalSpace G] {M : Type u_2} [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribMulAction G M] (htriv : ∀ (g : G) (m : M), g • m = m) : H1 G M ≃+ ↥(Z1 G M)

With trivial action, H¹ ≃+ Z¹ (nothing is killed).

Equations

• GQ2.ContCoh.H1equivZ1OfTrivial htriv = (QuotientAddGroup.quotientAddEquivOfEq ⋯).trans QuotientAddGroup.quotientBot

theorem GQ2.ContCoh.H0_eq_top_of_trivial {G : Type u_1} [Group G] {M : Type u_2} [AddCommGroup M] [DistribMulAction G M] (htriv : ∀ (g : G) (m : M), g • m = m) : H0 G M = ⊤

With trivial action, everything is invariant.

Cocycle algebra

A few more identities for continuous 1-cocycles, beyond Z1_apply_one.

theorem GQ2.ContCoh.Z1_apply_inv {G : Type u_1} [Group G] [TopologicalSpace G] {M : Type u_2} [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribMulAction G M] (φ : ↥(Z1 G M)) (g : G) : ↑φ g⁻¹ = -(g⁻¹ • ↑φ g)

The value of a 1-cocycle at an inverse: φ(g⁻¹) = −g⁻¹ • φ(g).

Coefficient functoriality

The π = id special case of Hicomap: a continuous G-equivariant additive map f : N →+ M (same group G) induces Hⁱ(G,N) →+ Hⁱ(G,M). Needed by B6/B9 (pairing- and connecting-maps on coefficients).

def GQ2.ContCoh.mapCoeff0 {G : Type u_1} [Group G] [TopologicalSpace G] {M : Type u_2} [AddCommGroup M] [DistribMulAction G M] {N : Type u_3} [AddCommGroup N] [DistribMulAction G N] (f : N →+ M) (hcompat : ∀ (g : G) (n : N), f (g • n) = g • f n) : ↥(H0 G N) →+ ↥(H0 G M)

Coefficient functoriality in degree 0.

Equations

• GQ2.ContCoh.mapCoeff0 f hcompat = GQ2.ContCoh.H0comap (ContinuousMonoidHom.id G) f ⋯

def GQ2.ContCoh.mapCoeff1 {G : Type u_1} [Group G] [TopologicalSpace G] {M : Type u_2} [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribMulAction G M] {N : Type u_3} [AddCommGroup N] [TopologicalSpace N] [IsTopologicalAddGroup N] [DistribMulAction G N] (f : N →+ M) (hf : Continuous ⇑f) (hcompat : ∀ (g : G) (n : N), f (g • n) = g • f n) : H1 G N →+ H1 G M

Coefficient functoriality in degree 1.

Equations

• GQ2.ContCoh.mapCoeff1 f hf hcompat = GQ2.ContCoh.H1comap (ContinuousMonoidHom.id G) f hf ⋯

theorem GQ2.ContCoh.mapCoeff1_H1mk {G : Type u_1} [Group G] [TopologicalSpace G] {M : Type u_2} [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribMulAction G M] {N : Type u_3} [AddCommGroup N] [TopologicalSpace N] [IsTopologicalAddGroup N] [DistribMulAction G N] (f : N →+ M) (hf : Continuous ⇑f) (hcompat : ∀ (g : G) (n : N), f (g • n) = g • f n) (z : ↥(Z1 G N)) : (mapCoeff1 f hf hcompat) ((H1mk G N) z) = (H1mk G M) ((Z1comap (ContinuousMonoidHom.id G) f hf ⋯) z)

mapCoeff1 computes on classes: the image of H1mk z is H1mk of the pushed-forward cocycle (definitional).

def GQ2.ContCoh.mapCoeff2 {G : Type u_1} [Group G] [TopologicalSpace G] {M : Type u_2} [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribMulAction G M] {N : Type u_3} [AddCommGroup N] [TopologicalSpace N] [IsTopologicalAddGroup N] [DistribMulAction G N] (f : N →+ M) (hf : Continuous ⇑f) (hcompat : ∀ (g : G) (n : N), f (g • n) = g • f n) : H2 G N →+ H2 G M

Coefficient functoriality in degree 2.

Equations

• GQ2.ContCoh.mapCoeff2 f hf hcompat = GQ2.ContCoh.H2comap (ContinuousMonoidHom.id G) f hf ⋯

Inflation

The f = id special case of Hicomap along a continuous hom π : G →ₜ* Q whose associated Q-action on M agrees, through π, with a given G-action (hπ : π g • m = g • m). For a continuous surjection π : G ↠ Q this is inflation Hⁱ(Q,M) →+ Hⁱ(G,M) from a quotient.

def GQ2.ContCoh.inf0 {G : Type u_1} [Group G] [TopologicalSpace G] {Q : Type u_2} [Group Q] [TopologicalSpace Q] {M : Type u_3} [AddCommGroup M] [DistribMulAction G M] [DistribMulAction Q M] (π : G →ₜ* Q) (hπ : ∀ (g : G) (m : M), π g • m = g • m) : ↥(H0 Q M) →+ ↥(H0 G M)

Inflation in degree 0.

Equations

• GQ2.ContCoh.inf0 π hπ = GQ2.ContCoh.H0comap π (AddMonoidHom.id M) ⋯

def GQ2.ContCoh.inf1 {G : Type u_1} [Group G] [TopologicalSpace G] {Q : Type u_2} [Group Q] [TopologicalSpace Q] {M : Type u_3} [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribMulAction G M] [DistribMulAction Q M] (π : G →ₜ* Q) (hπ : ∀ (g : G) (m : M), π g • m = g • m) : H1 Q M →+ H1 G M

Inflation in degree 1.

Equations

• GQ2.ContCoh.inf1 π hπ = GQ2.ContCoh.H1comap π (AddMonoidHom.id M) ⋯ ⋯

def GQ2.ContCoh.inf2 {G : Type u_1} [Group G] [TopologicalSpace G] {Q : Type u_2} [Group Q] [TopologicalSpace Q] {M : Type u_3} [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribMulAction G M] [DistribMulAction Q M] (π : G →ₜ* Q) (hπ : ∀ (g : G) (m : M), π g • m = g • m) : H2 Q M →+ H2 G M

Inflation in degree 2.

Equations

• GQ2.ContCoh.inf2 π hπ = GQ2.ContCoh.H2comap π (AddMonoidHom.id M) ⋯ ⋯

Note: comparison with Mathlib's finite group cohomology (deferred)

The plan lists a stress test that for finite G these definitions agree with Mathlib's groupCohomology.H1/H2. We deliberately defer it: Mathlib's group cohomology is built over Rep k G (k-linear representations, ModuleCat-based, no topology), so a comparison needs a bridge Rep ℤ G ↝ (our DistribMulAction-modules) matching the inhomogeneous-cochain conventions of cocycles₁/cocycles₂ (for finite G continuity is automatic, so the underlying groups do coincide). That bridge is a verification task (step 3), not needed to state any of B3/B6/B7/B9 — those are phrased entirely in terms of the ContCoh API here. The human-checkability of the definitions is already secured by the explicit cocycle-identity forms mem_Z1_iff/mem_Z2_iff (Serre GC I §2.2) and the trivial-action characterization H1equivZ1OfTrivial.