Functoriality of explicit continuous cohomology in degrees one and two

A compatible pair consists of a continuous monoid homomorphism φ : H →ₜ* G and a continuous additive homomorphism f : M →+ N satisfying f (φ h • m) = h • f m. It pulls a continuous cochain c : G → M back to h ↦ f (c (φ h)). This file proves that pullback preserves continuous cocycles and coboundaries, and descends it to the explicit groups H¹ = Z¹/B¹ and H² = Z²/B².

The resulting maps are TauCeti.ContCohomology.explicitMap1 and explicitMap2. Their identity and composition laws make the construction functorial, while the _mk theorems fix their values on cocycle classes. The named specializations explicitRes1, explicitRes2, explicitCoeff1, and explicitCoeff2 provide restriction and coefficient maps in positive degrees, and explicitRes1_eq_explicitMap1, explicitRes2_eq_explicitMap2, explicitCoeff1_eq_explicitMap1 and explicitCoeff2_eq_explicitMap2 exhibit each of them as the compatible pair it is, so that a theorem proved for a general pair specializes to all four. They are the positive-degree counterparts of explicitRes0_eq_explicitMap0 and explicitCoeff0_eq_explicitMap0. The constructions explicitCoeff1Equiv and explicitCoeff2Equiv upgrade a continuous equivariant additive equivalence of coefficient modules to additive equivalences on explicit H¹ and H², and explicitCoeff1_bijective and explicitCoeff2_bijective record that a bijective equivariant homomorphism of discrete coefficient modules induces bijections. Finally, explicitCoeff2_eq_card_nsmul records that the norm of a finite normal subgroup N, as a coefficient map, acts on H² as multiplication by #N.

This is functoriality of the explicit model: the carriers are the quotients Z¹/B¹ and Z²/B² of plain continuous cochains. Mathlib's ContinuousCohomology.map is the compatible-pair pullback on the canonical bundled carrier, and it is what the sibling file TauCeti/RepresentationTheory/Homological/ContCohomology/Functoriality.lean specialises to restriction, inflation and coefficient maps. The comparison with the canonical model lives in TauCeti/RepresentationTheory/Homological/ContCohomology/CohomologyComparison.lean.

The formulas follow Mathlib's groupCohomology.cochainsMap₁, cochainsMap₂, mapCocycles₁, and mapCocycles₂, with universe-polymorphic unbundled continuous coefficients. The coefficient maps and their equivalences apply to monoid actions; restriction to subgroups requires a group.

def TauCeti.ContCohomology.cochainsMap1 {G : Type uG} {H : Type uH} {M : Type uM} {N : Type uN} [Monoid G] [Monoid H] [AddMonoid M] [AddMonoid N] (φ : H →* G) (f : M →+ N) : (G → M) →+ H → N

Pullback of degree-one cochains along a monoid map and a coefficient map.

Equations

• TauCeti.ContCohomology.cochainsMap1 φ f = { toFun := fun (c : G → M) (h : H) => f (c (φ h)), map_zero' := ⋯, map_add' := ⋯ }

def TauCeti.ContCohomology.cochainsMap2 {G : Type uG} {H : Type uH} {M : Type uM} {N : Type uN} [Monoid G] [Monoid H] [AddMonoid M] [AddMonoid N] (φ : H →* G) (f : M →+ N) : (G × G → M) →+ H × H → N

Pullback of degree-two cochains along a monoid map and a coefficient map: the degree-one pullback along the pair φ × φ of the domain.

Equations

• TauCeti.ContCohomology.cochainsMap2 φ f = TauCeti.ContCohomology.cochainsMap1 (φ.prodMap φ) f

@[simp]

theorem TauCeti.ContCohomology.cochainsMap1_apply {G : Type uG} {H : Type uH} {M : Type uM} {N : Type uN} [Monoid G] [Monoid H] [AddMonoid M] [AddMonoid N] (φ : H →* G) (f : M →+ N) (c : G → M) (h : H) : (cochainsMap1 φ f) c h = f (c (φ h))

The defining formula for the degree-one cochain pullback.

@[simp]

theorem TauCeti.ContCohomology.cochainsMap2_apply {G : Type uG} {H : Type uH} {M : Type uM} {N : Type uN} [Monoid G] [Monoid H] [AddMonoid M] [AddMonoid N] (φ : H →* G) (f : M →+ N) (c : G × G → M) (h k : H) : (cochainsMap2 φ f) c (h, k) = f (c (φ h, φ k))

The defining formula for the degree-two cochain pullback.

theorem TauCeti.ContCohomology.cochainsMap1_injective {G : Type uG} {H : Type uH} {M : Type uM} {N : Type uN} [Monoid G] [Monoid H] [AddMonoid M] [AddMonoid N] (φ : H →* G) (f : M →+ N) (hφ : Function.Surjective ⇑φ) (hf : Function.Injective ⇑f) : Function.Injective ⇑(cochainsMap1 φ f)

Pullback of degree-one cochains is injective when the group map is surjective and the coefficient map is injective.

theorem TauCeti.ContCohomology.cochainsMap2_injective {G : Type uG} {H : Type uH} {M : Type uM} {N : Type uN} [Monoid G] [Monoid H] [AddMonoid M] [AddMonoid N] (φ : H →* G) (f : M →+ N) (hφ : Function.Surjective ⇑φ) (hf : Function.Injective ⇑f) : Function.Injective ⇑(cochainsMap2 φ f)

Pullback of degree-two cochains is injective when the group map is surjective and the coefficient map is injective.

theorem TauCeti.ContCohomology.continuous_cochainsMap1 {G : Type uG} {H : Type uH} {M : Type uM} {N : Type uN} [Monoid G] [Monoid H] [AddMonoid M] [AddMonoid N] [TopologicalSpace G] [TopologicalSpace H] [TopologicalSpace M] [TopologicalSpace N] (φ : H →ₜ* G) (f : M →+ N) (hf : Continuous ⇑f) {c : G → M} (hc : Continuous c) : Continuous ((cochainsMap1 (↑φ) f) c)

Pullback preserves continuity of degree-one cochains.

theorem TauCeti.ContCohomology.continuous_cochainsMap2 {G : Type uG} {H : Type uH} {M : Type uM} {N : Type uN} [Monoid G] [Monoid H] [AddMonoid M] [AddMonoid N] [TopologicalSpace G] [TopologicalSpace H] [TopologicalSpace M] [TopologicalSpace N] (φ : H →ₜ* G) (f : M →+ N) (hf : Continuous ⇑f) {c : G × G → M} (hc : Continuous c) : Continuous ((cochainsMap2 (↑φ) f) c)

Pullback preserves continuity of degree-two cochains.

@[simp]

theorem TauCeti.ContCohomology.cochainsMap1_id {G : Type uG} {M : Type uM} [Monoid G] [AddMonoid M] : cochainsMap1 (MonoidHom.id G) (AddMonoidHom.id M) = AddMonoidHom.id (G → M)

Pullback of degree-one cochains along the identity compatible pair is the identity.

@[simp]

theorem TauCeti.ContCohomology.cochainsMap2_id {G : Type uG} {M : Type uM} [Monoid G] [AddMonoid M] : cochainsMap2 (MonoidHom.id G) (AddMonoidHom.id M) = AddMonoidHom.id (G × G → M)

Pullback of degree-two cochains along the identity compatible pair is the identity.

@[simp]

theorem TauCeti.ContCohomology.cochainsMap1_comp {G : Type uG} {H : Type uH} {M : Type uM} {N : Type uN} [Monoid G] [Monoid H] [AddMonoid M] [AddMonoid N] {K : Type uK} {P : Type uP} [Monoid K] [AddMonoid P] (φ : H →* G) (ψ : K →* H) (f : M →+ N) (q : N →+ P) : cochainsMap1 (φ.comp ψ) (q.comp f) = (cochainsMap1 ψ q).comp (cochainsMap1 φ f)

Pullback of degree-one cochains along a composite compatible pair is the composite of the pullbacks: it is contravariant in the group homomorphism and covariant in the coefficient map.

@[simp]

theorem TauCeti.ContCohomology.cochainsMap2_comp {G : Type uG} {H : Type uH} {M : Type uM} {N : Type uN} [Monoid G] [Monoid H] [AddMonoid M] [AddMonoid N] {K : Type uK} {P : Type uP} [Monoid K] [AddMonoid P] (φ : H →* G) (ψ : K →* H) (f : M →+ N) (q : N →+ P) : cochainsMap2 (φ.comp ψ) (q.comp f) = (cochainsMap2 ψ q).comp (cochainsMap2 φ f)

Pullback of degree-two cochains along a composite compatible pair is the composite of the pullbacks: it is contravariant in the group homomorphism and covariant in the coefficient map.

The naturality squares are where the differentials enter, so this is the first point at which the coefficients have to be commutative groups carrying a distributive scalar action. Commutativity is necessary because d0 and d1 are additive homomorphisms; their formulas are not additive for a general noncommutative additive group.

theorem TauCeti.ContCohomology.cochainsMap1_d0 {G : Type uG} {H : Type uH} {M : Type uM} {N : Type uN} [Monoid G] [Monoid H] [AddCommGroup M] [AddCommGroup N] [DistribSMul G M] [DistribSMul H N] (φ : H →* G) (f : M →+ N) (hequiv : ∀ (h : H) (m : M), f (φ h • m) = h • f m) (m : M) : (cochainsMap1 φ f) ((d0 G M) m) = (d0 H N) (f m)

The degree-zero differential is natural in compatible pairs.

theorem TauCeti.ContCohomology.cochainsMap2_d1 {G : Type uG} {H : Type uH} {M : Type uM} {N : Type uN} [Monoid G] [Monoid H] [AddCommGroup M] [AddCommGroup N] [DistribSMul G M] [DistribSMul H N] (φ : H →* G) (f : M →+ N) (hequiv : ∀ (h : H) (m : M), f (φ h • m) = h • f m) (c : G → M) : (cochainsMap2 φ f) ((d1 G M) c) = (d1 H N) ((cochainsMap1 φ f) c)

The degree-one differential is natural in compatible pairs.

theorem TauCeti.ContCohomology.cochainsMap1_mem_B1 {G : Type uG} {H : Type uH} {M : Type uM} {N : Type uN} [Monoid G] [Monoid H] [AddCommGroup M] [AddCommGroup N] [DistribSMul G M] [DistribSMul H N] (φ : H →* G) (f : M →+ N) (hequiv : ∀ (h : H) (m : M), f (φ h • m) = h • f m) {c : G → M} (hc : c ∈ B1 G M) : (cochainsMap1 φ f) c ∈ B1 H N

A compatible pair sends degree-one coboundaries to degree-one coboundaries.

theorem TauCeti.ContCohomology.cochainsMap2_mem_B2 {G : Type uG} {H : Type uH} {M : Type uM} {N : Type uN} [Monoid G] [Monoid H] [AddCommGroup M] [AddCommGroup N] [DistribSMul G M] [DistribSMul H N] [TopologicalSpace G] [TopologicalSpace H] [TopologicalSpace M] [TopologicalSpace N] [IsTopologicalAddGroup M] [IsTopologicalAddGroup N] (φ : H →ₜ* G) (f : M →+ N) (hf : Continuous ⇑f) (hequiv : ∀ (h : H) (m : M), f (φ h • m) = h • f m) {c : G × G → M} (hc : c ∈ B2 G M) : (cochainsMap2 (↑φ) f) c ∈ B2 H N

A compatible pair sends continuous degree-two coboundaries to continuous degree-two coboundaries.

theorem TauCeti.ContCohomology.cochainsMap1_mem_Z1 (G : Type uG) [Monoid G] [TopologicalSpace G] (M : Type uM) [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribSMul G M] (H : Type uH) [Monoid H] [TopologicalSpace H] (N : Type uN) [AddCommGroup N] [TopologicalSpace N] [IsTopologicalAddGroup N] [DistribSMul H N] (φ : H →ₜ* G) (f : M →+ N) (hf : Continuous ⇑f) (hequiv : ∀ (h : H) (m : M), f (φ h • m) = h • f m) {c : G → M} (hc : c ∈ Z1 G M) : (cochainsMap1 (↑φ) f) c ∈ Z1 H N

A compatible pair sends continuous degree-one cocycles to continuous degree-one cocycles.

theorem TauCeti.ContCohomology.cochainsMap2_mem_Z2 (G : Type uG) [Monoid G] [TopologicalSpace G] (M : Type uM) [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribSMul G M] (H : Type uH) [Monoid H] [TopologicalSpace H] (N : Type uN) [AddCommGroup N] [TopologicalSpace N] [IsTopologicalAddGroup N] [DistribSMul H N] (φ : H →ₜ* G) (f : M →+ N) (hf : Continuous ⇑f) (hequiv : ∀ (h : H) (m : M), f (φ h • m) = h • f m) {c : G × G → M} (hc : c ∈ Z2 G M) : (cochainsMap2 (↑φ) f) c ∈ Z2 H N

A compatible pair sends continuous degree-two cocycles to continuous degree-two cocycles.

def TauCeti.ContCohomology.cocyclesMap1 (G : Type uG) [Monoid G] [TopologicalSpace G] (M : Type uM) [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribSMul G M] (H : Type uH) [Monoid H] [TopologicalSpace H] (N : Type uN) [AddCommGroup N] [TopologicalSpace N] [IsTopologicalAddGroup N] [DistribSMul H N] (φ : H →ₜ* G) (f : M →+ N) (hf : Continuous ⇑f) (hequiv : ∀ (h : H) (m : M), f (φ h • m) = h • f m) : ↥(Z1 G M) →+ ↥(Z1 H N)

The pullback of continuous degree-one cocycles along a compatible pair, sending a cocycle c to h ↦ f (c (φ h)).

Equations

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

@[simp]

theorem TauCeti.ContCohomology.cocyclesMap1_coe (G : Type uG) [Monoid G] [TopologicalSpace G] (M : Type uM) [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribSMul G M] (H : Type uH) [Monoid H] [TopologicalSpace H] (N : Type uN) [AddCommGroup N] [TopologicalSpace N] [IsTopologicalAddGroup N] [DistribSMul H N] (φ : H →ₜ* G) (f : M →+ N) (hf : Continuous ⇑f) (hequiv : ∀ (h : H) (m : M), f (φ h • m) = h • f m) (c : ↥(Z1 G M)) : ↑((cocyclesMap1 G M H N φ f hf hequiv) c) = (cochainsMap1 (↑φ) f) ↑c

The underlying cochain of cocyclesMap1 is the degree-one cochain pullback.

theorem TauCeti.ContCohomology.cocyclesMap1_apply (G : Type uG) [Monoid G] [TopologicalSpace G] (M : Type uM) [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribSMul G M] (H : Type uH) [Monoid H] [TopologicalSpace H] (N : Type uN) [AddCommGroup N] [TopologicalSpace N] [IsTopologicalAddGroup N] [DistribSMul H N] (φ : H →ₜ* G) (f : M →+ N) (hf : Continuous ⇑f) (hequiv : ∀ (h : H) (m : M), f (φ h • m) = h • f m) (c : ↥(Z1 G M)) (h : H) : ↑((cocyclesMap1 G M H N φ f hf hequiv) c) h = f (↑c (φ h))

The defining formula for the degree-one cocycle pullback, the pointwise form of cocyclesMap1_coe.

@[simp]

theorem TauCeti.ContCohomology.cocyclesMap1_id (G : Type uG) [Monoid G] [TopologicalSpace G] (M : Type uM) [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribSMul G M] (hid : ∀ (g : G) (m : M), (AddMonoidHom.id M) ((ContinuousMonoidHom.id G) g • m) = g • (AddMonoidHom.id M) m := ⋯) : cocyclesMap1 G M G M (ContinuousMonoidHom.id G) (AddMonoidHom.id M) ⋯ hid = AddMonoidHom.id ↥(Z1 G M)

Pullback of continuous cocycles along the identity compatible pair is the identity.

theorem TauCeti.ContCohomology.cocyclesMap1_comp (G : Type uG) [Monoid G] [TopologicalSpace G] (M : Type uM) [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribSMul G M] (H : Type uH) [Monoid H] [TopologicalSpace H] (N : Type uN) [AddCommGroup N] [TopologicalSpace N] [IsTopologicalAddGroup N] [DistribSMul H N] (φ : H →ₜ* G) (f : M →+ N) (hf : Continuous ⇑f) (hequiv : ∀ (h : H) (m : M), f (φ h • m) = h • f m) (K : Type uK) [Monoid K] [TopologicalSpace K] (P : Type uP) [AddCommGroup P] [TopologicalSpace P] [IsTopologicalAddGroup P] [DistribSMul K P] (ψ : K →ₜ* H) (q : N →+ P) (hq : Continuous ⇑q) (hequivq : ∀ (k : K) (n : N), q (ψ k • n) = k • q n) (hcomp : ∀ (k : K) (m : M), (q.comp f) ((φ.comp ψ) k • m) = k • (q.comp f) m := ⋯) : cocyclesMap1 G M K P (φ.comp ψ) (q.comp f) ⋯ hcomp = (cocyclesMap1 H N K P ψ q hq hequivq).comp (cocyclesMap1 G M H N φ f hf hequiv)

Pullback of continuous cocycles along a composite compatible pair is the composite of the pullbacks: it is contravariant in the group homomorphism and covariant in the coefficient map. The compatibility of the composite pair follows from ContinuousMonoidHom.comp_map_smul.

def TauCeti.ContCohomology.cocyclesMap2 (G : Type uG) [Monoid G] [TopologicalSpace G] (M : Type uM) [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribSMul G M] (H : Type uH) [Monoid H] [TopologicalSpace H] (N : Type uN) [AddCommGroup N] [TopologicalSpace N] [IsTopologicalAddGroup N] [DistribSMul H N] (φ : H →ₜ* G) (f : M →+ N) (hf : Continuous ⇑f) (hequiv : ∀ (h : H) (m : M), f (φ h • m) = h • f m) : ↥(Z2 G M) →+ ↥(Z2 H N)

The pullback of continuous degree-two cocycles along a compatible pair.

Equations

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

@[simp]

theorem TauCeti.ContCohomology.cocyclesMap2_coe (G : Type uG) [Monoid G] [TopologicalSpace G] (M : Type uM) [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribSMul G M] (H : Type uH) [Monoid H] [TopologicalSpace H] (N : Type uN) [AddCommGroup N] [TopologicalSpace N] [IsTopologicalAddGroup N] [DistribSMul H N] (φ : H →ₜ* G) (f : M →+ N) (hf : Continuous ⇑f) (hequiv : ∀ (h : H) (m : M), f (φ h • m) = h • f m) (c : ↥(Z2 G M)) : ↑((cocyclesMap2 G M H N φ f hf hequiv) c) = (cochainsMap2 (↑φ) f) ↑c

The underlying cochain of cocyclesMap2 is the degree-two cochain pullback.

theorem TauCeti.ContCohomology.cocyclesMap2_apply (G : Type uG) [Monoid G] [TopologicalSpace G] (M : Type uM) [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribSMul G M] (H : Type uH) [Monoid H] [TopologicalSpace H] (N : Type uN) [AddCommGroup N] [TopologicalSpace N] [IsTopologicalAddGroup N] [DistribSMul H N] (φ : H →ₜ* G) (f : M →+ N) (hf : Continuous ⇑f) (hequiv : ∀ (h : H) (m : M), f (φ h • m) = h • f m) (c : ↥(Z2 G M)) (h k : H) : ↑((cocyclesMap2 G M H N φ f hf hequiv) c) (h, k) = f (↑c (φ h, φ k))

The defining formula for the degree-two cocycle pullback.

@[simp]

theorem TauCeti.ContCohomology.cocyclesMap2_id (G : Type uG) [Monoid G] [TopologicalSpace G] (M : Type uM) [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribSMul G M] (hid : ∀ (g : G) (m : M), (AddMonoidHom.id M) ((ContinuousMonoidHom.id G) g • m) = g • (AddMonoidHom.id M) m := ⋯) : cocyclesMap2 G M G M (ContinuousMonoidHom.id G) (AddMonoidHom.id M) ⋯ hid = AddMonoidHom.id ↥(Z2 G M)

Pullback of continuous degree-two cocycles along the identity compatible pair is the identity.

theorem TauCeti.ContCohomology.cocyclesMap2_comp (G : Type uG) [Monoid G] [TopologicalSpace G] (M : Type uM) [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribSMul G M] (H : Type uH) [Monoid H] [TopologicalSpace H] (N : Type uN) [AddCommGroup N] [TopologicalSpace N] [IsTopologicalAddGroup N] [DistribSMul H N] (φ : H →ₜ* G) (f : M →+ N) (hf : Continuous ⇑f) (hequiv : ∀ (h : H) (m : M), f (φ h • m) = h • f m) (K : Type uK) [Monoid K] [TopologicalSpace K] (P : Type uP) [AddCommGroup P] [TopologicalSpace P] [IsTopologicalAddGroup P] [DistribSMul K P] (ψ : K →ₜ* H) (q : N →+ P) (hq : Continuous ⇑q) (hequivq : ∀ (k : K) (n : N), q (ψ k • n) = k • q n) (hcomp : ∀ (k : K) (m : M), (q.comp f) ((φ.comp ψ) k • m) = k • (q.comp f) m := ⋯) : cocyclesMap2 G M K P (φ.comp ψ) (q.comp f) ⋯ hcomp = (cocyclesMap2 H N K P ψ q hq hequivq).comp (cocyclesMap2 G M H N φ f hf hequiv)

Pullback of continuous degree-two cocycles respects composition of compatible pairs.

noncomputable def TauCeti.ContCohomology.explicitMap1 (G : Type uG) [Monoid G] [TopologicalSpace G] (M : Type uM) [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribMulAction G M] [ContinuousSMul G M] (H : Type uH) [Monoid H] [TopologicalSpace H] (N : Type uN) [AddCommGroup N] [TopologicalSpace N] [IsTopologicalAddGroup N] [DistribMulAction H N] [ContinuousSMul H N] (φ : H →ₜ* G) (f : M →+ N) (hf : Continuous ⇑f) (hequiv : ∀ (h : H) (m : M), f (φ h • m) = h • f m) : H1 G M →+ H1 H N

Pullback on the explicit first continuous cohomology group along a compatible pair.

Equations

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

@[simp]

theorem TauCeti.ContCohomology.explicitMap1_mk (G : Type uG) [Monoid G] [TopologicalSpace G] (M : Type uM) [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribMulAction G M] [ContinuousSMul G M] (H : Type uH) [Monoid H] [TopologicalSpace H] (N : Type uN) [AddCommGroup N] [TopologicalSpace N] [IsTopologicalAddGroup N] [DistribMulAction H N] [ContinuousSMul H N] (φ : H →ₜ* G) (f : M →+ N) (hf : Continuous ⇑f) (hequiv : ∀ (h : H) (m : M), f (φ h • m) = h • f m) (c : ↥(Z1 G M)) : (explicitMap1 G M H N φ f hf hequiv) ↑c = ↑((cocyclesMap1 G M H N φ f hf hequiv) c)

explicitMap1 sends the class of a cocycle to the class of its pullback.

theorem TauCeti.ContCohomology.explicitMap1_congr_of_eq (G : Type uG) [Monoid G] [TopologicalSpace G] (M : Type uM) [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribMulAction G M] [ContinuousSMul G M] (H : Type uH) [Monoid H] [TopologicalSpace H] (N : Type uN) [AddCommGroup N] [TopologicalSpace N] [IsTopologicalAddGroup N] [DistribMulAction H N] [ContinuousSMul H N] (φ ψ : H →ₜ* G) (f q : M →+ N) {hf : Continuous ⇑f} {hq : Continuous ⇑q} {hφ : ∀ (h : H) (m : M), f (φ h • m) = h • f m} {hψ : ∀ (h : H) (m : M), q (ψ h • m) = h • q m} (hφeq : φ = ψ) (hfeq : f = q) : explicitMap1 G M H N φ f hf hφ = explicitMap1 G M H N ψ q hq hψ

Equality of compatible pairs gives equality of the induced maps on explicit H¹.

@[simp]

theorem TauCeti.ContCohomology.explicitMap1_id (G : Type uG) [Monoid G] [TopologicalSpace G] (M : Type uM) [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribMulAction G M] [ContinuousSMul G M] (hid : ∀ (g : G) (m : M), (AddMonoidHom.id M) ((ContinuousMonoidHom.id G) g • m) = g • (AddMonoidHom.id M) m := ⋯) : explicitMap1 G M G M (ContinuousMonoidHom.id G) (AddMonoidHom.id M) ⋯ hid = AddMonoidHom.id (H1 G M)

Pullback by the identity compatible pair is the identity on explicit H¹.

theorem TauCeti.ContCohomology.explicitMap1_comp (G : Type uG) [Monoid G] [TopologicalSpace G] (M : Type uM) [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribMulAction G M] [ContinuousSMul G M] (H : Type uH) [Monoid H] [TopologicalSpace H] (N : Type uN) [AddCommGroup N] [TopologicalSpace N] [IsTopologicalAddGroup N] [DistribMulAction H N] [ContinuousSMul H N] (φ : H →ₜ* G) (f : M →+ N) (hf : Continuous ⇑f) (hequiv : ∀ (h : H) (m : M), f (φ h • m) = h • f m) (K : Type uK) [Monoid K] [TopologicalSpace K] (P : Type uP) [AddCommGroup P] [TopologicalSpace P] [IsTopologicalAddGroup P] [DistribMulAction K P] [ContinuousSMul K P] (ψ : K →ₜ* H) (q : N →+ P) (hq : Continuous ⇑q) (hequivq : ∀ (k : K) (n : N), q (ψ k • n) = k • q n) (hcomp : ∀ (k : K) (m : M), (q.comp f) ((φ.comp ψ) k • m) = k • (q.comp f) m := ⋯) : explicitMap1 G M K P (φ.comp ψ) (q.comp f) ⋯ hcomp = (explicitMap1 H N K P ψ q hq hequivq).comp (explicitMap1 G M H N φ f hf hequiv)

Pullback on explicit H¹ respects composition of compatible pairs: it is contravariant in the group homomorphism and covariant in the coefficient map. The compatibility of the composite pair follows from ContinuousMonoidHom.comp_map_smul.

theorem TauCeti.ContCohomology.explicitMap1_explicitMap1_of_comp_eq (G : Type uG) [Monoid G] [TopologicalSpace G] (M : Type uM) [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribMulAction G M] [ContinuousSMul G M] (H : Type uH) [Monoid H] [TopologicalSpace H] (N : Type uN) [AddCommGroup N] [TopologicalSpace N] [IsTopologicalAddGroup N] [DistribMulAction H N] [ContinuousSMul H N] (φ : H →ₜ* G) (f : M →+ N) (hf : Continuous ⇑f) (hequiv : ∀ (h : H) (m : M), f (φ h • m) = h • f m) (K : Type uK) [Monoid K] [TopologicalSpace K] (P : Type uP) [AddCommGroup P] [TopologicalSpace P] [IsTopologicalAddGroup P] [DistribMulAction K P] [ContinuousSMul K P] (ψ : K →ₜ* H) (q : N →+ P) (hq : Continuous ⇑q) (hequivq : ∀ (k : K) (n : N), q (ψ k • n) = k • q n) {H' : Type u_1} [Monoid H'] [TopologicalSpace H'] {N' : Type u_2} [AddCommGroup N'] [TopologicalSpace N'] [IsTopologicalAddGroup N'] [DistribMulAction H' N'] [ContinuousSMul H' N'] (φ' : H' →ₜ* G) (f' : M →+ N') (hf' : Continuous ⇑f') (hequiv' : ∀ (h : H') (m : M), f' (φ' h • m) = h • f' m) (ψ' : K →ₜ* H') (q' : N' →+ P) (hq' : Continuous ⇑q') (hequivq' : ∀ (k : K) (n : N'), q' (ψ' k • n) = k • q' n) (hφ : φ.comp ψ = φ'.comp ψ') (hqf : q.comp f = q'.comp f') (x : H1 G M) : (explicitMap1 H N K P ψ q hq hequivq) ((explicitMap1 G M H N φ f hf hequiv) x) = (explicitMap1 H' N' K P ψ' q' hq' hequivq') ((explicitMap1 G M H' N' φ' f' hf' hequiv') x)

Commuting squares of compatible pairs commute on explicit H¹: if the composites φ ∘ ψ = φ' ∘ ψ' of the group homomorphisms and q ∘ f = q' ∘ f' of the coefficient maps agree, then pulling back along (φ, f) and then (ψ, q) agrees with pulling back along (φ', f') and then (ψ', q'). This combines explicitMap1_comp and explicitMap1_congr_of_eq without asking for the compatibility hypotheses of the composite pairs.

noncomputable def TauCeti.ContCohomology.explicitMap1Equiv (G : Type uG) [Monoid G] [TopologicalSpace G] (M : Type uM) [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribMulAction G M] [ContinuousSMul G M] (H : Type uH) [Monoid H] [TopologicalSpace H] (N : Type uN) [AddCommGroup N] [TopologicalSpace N] [IsTopologicalAddGroup N] [DistribMulAction H N] [ContinuousSMul H N] (φ : H ≃ₜ* G) (e : M ≃+ N) (he : Continuous ⇑e) (he' : Continuous ⇑e.symm) (hequiv : ∀ (h : H) (m : M), e (φ h • m) = h • e m) : H1 G M ≃+ H1 H N

Pullback along a compatible pair made of a continuous multiplicative equivalence and an additive equivalence of coefficients is an additive equivalence on explicit first continuous cohomology. Both directions of the coefficient equivalence are required to be continuous; for discrete coefficient modules this follows automatically from discreteness.

Equations

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

@[simp]

theorem TauCeti.ContCohomology.explicitMap1Equiv_apply (G : Type uG) [Monoid G] [TopologicalSpace G] (M : Type uM) [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribMulAction G M] [ContinuousSMul G M] (H : Type uH) [Monoid H] [TopologicalSpace H] (N : Type uN) [AddCommGroup N] [TopologicalSpace N] [IsTopologicalAddGroup N] [DistribMulAction H N] [ContinuousSMul H N] (φ : H ≃ₜ* G) (e : M ≃+ N) (he : Continuous ⇑e) (he' : Continuous ⇑e.symm) (hequiv : ∀ (h : H) (m : M), e (φ h • m) = h • e m) (x : H1 G M) : (explicitMap1Equiv G M H N φ e he he' hequiv) x = (explicitMap1 G M H N (↑φ) e.toAddMonoidHom he hequiv) x

The equivalence on explicit H¹ is the pullback along its forward compatible pair.

@[simp]

theorem TauCeti.ContCohomology.explicitMap1Equiv_symm_apply (G : Type uG) [Monoid G] [TopologicalSpace G] (M : Type uM) [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribMulAction G M] [ContinuousSMul G M] (H : Type uH) [Monoid H] [TopologicalSpace H] (N : Type uN) [AddCommGroup N] [TopologicalSpace N] [IsTopologicalAddGroup N] [DistribMulAction H N] [ContinuousSMul H N] (φ : H ≃ₜ* G) (e : M ≃+ N) (he : Continuous ⇑e) (he' : Continuous ⇑e.symm) (hequiv : ∀ (h : H) (m : M), e (φ h • m) = h • e m) (x : H1 H N) : (explicitMap1Equiv G M H N φ e he he' hequiv).symm x = (explicitMap1 H N G M (↑φ.symm) e.symm.toAddMonoidHom he' ⋯) x

The inverse of the equivalence on explicit H¹ is the pullback along the inverse compatible pair.

noncomputable def TauCeti.ContCohomology.explicitMap2 (G : Type uG) [Monoid G] [TopologicalSpace G] (M : Type uM) [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribMulAction G M] [ContinuousSMul G M] (H : Type uH) [Monoid H] [TopologicalSpace H] (N : Type uN) [AddCommGroup N] [TopologicalSpace N] [IsTopologicalAddGroup N] [DistribMulAction H N] [ContinuousSMul H N] [ContinuousMul G] [ContinuousMul H] (φ : H →ₜ* G) (f : M →+ N) (hf : Continuous ⇑f) (hequiv : ∀ (h : H) (m : M), f (φ h • m) = h • f m) : H2 G M →+ H2 H N

Pullback on the explicit second continuous cohomology group along a compatible pair.

Equations

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

@[simp]

theorem TauCeti.ContCohomology.explicitMap2_mk (G : Type uG) [Monoid G] [TopologicalSpace G] (M : Type uM) [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribMulAction G M] [ContinuousSMul G M] (H : Type uH) [Monoid H] [TopologicalSpace H] (N : Type uN) [AddCommGroup N] [TopologicalSpace N] [IsTopologicalAddGroup N] [DistribMulAction H N] [ContinuousSMul H N] [ContinuousMul G] [ContinuousMul H] (φ : H →ₜ* G) (f : M →+ N) (hf : Continuous ⇑f) (hequiv : ∀ (h : H) (m : M), f (φ h • m) = h • f m) (c : ↥(Z2 G M)) : (explicitMap2 G M H N φ f hf hequiv) ↑c = ↑((cocyclesMap2 G M H N φ f hf hequiv) c)

explicitMap2 sends the class of a cocycle to the class of its pullback.

theorem TauCeti.ContCohomology.explicitMap2_congr_of_eq (G : Type uG) [Monoid G] [TopologicalSpace G] (M : Type uM) [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribMulAction G M] [ContinuousSMul G M] (H : Type uH) [Monoid H] [TopologicalSpace H] (N : Type uN) [AddCommGroup N] [TopologicalSpace N] [IsTopologicalAddGroup N] [DistribMulAction H N] [ContinuousSMul H N] [ContinuousMul G] [ContinuousMul H] (φ ψ : H →ₜ* G) (f q : M →+ N) {hf : Continuous ⇑f} {hq : Continuous ⇑q} {hφ : ∀ (h : H) (m : M), f (φ h • m) = h • f m} {hψ : ∀ (h : H) (m : M), q (ψ h • m) = h • q m} (hφeq : φ = ψ) (hfeq : f = q) : explicitMap2 G M H N φ f hf hφ = explicitMap2 G M H N ψ q hq hψ

Equality of compatible pairs gives equality of the induced maps on explicit H².

@[simp]

theorem TauCeti.ContCohomology.explicitMap2_id (G : Type uG) [Monoid G] [TopologicalSpace G] (M : Type uM) [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribMulAction G M] [ContinuousSMul G M] [ContinuousMul G] (hid : ∀ (g : G) (m : M), (AddMonoidHom.id M) ((ContinuousMonoidHom.id G) g • m) = g • (AddMonoidHom.id M) m := ⋯) : explicitMap2 G M G M (ContinuousMonoidHom.id G) (AddMonoidHom.id M) ⋯ hid = AddMonoidHom.id (H2 G M)

Pullback by the identity compatible pair is the identity on explicit H².

theorem TauCeti.ContCohomology.explicitMap2_comp (G : Type uG) [Monoid G] [TopologicalSpace G] (M : Type uM) [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribMulAction G M] [ContinuousSMul G M] (H : Type uH) [Monoid H] [TopologicalSpace H] (N : Type uN) [AddCommGroup N] [TopologicalSpace N] [IsTopologicalAddGroup N] [DistribMulAction H N] [ContinuousSMul H N] [ContinuousMul G] [ContinuousMul H] (φ : H →ₜ* G) (f : M →+ N) (hf : Continuous ⇑f) (hequiv : ∀ (h : H) (m : M), f (φ h • m) = h • f m) (K : Type uK) [Monoid K] [TopologicalSpace K] [ContinuousMul K] (P : Type uP) [AddCommGroup P] [TopologicalSpace P] [IsTopologicalAddGroup P] [DistribMulAction K P] [ContinuousSMul K P] (ψ : K →ₜ* H) (q : N →+ P) (hq : Continuous ⇑q) (hequivq : ∀ (k : K) (n : N), q (ψ k • n) = k • q n) (hcomp : ∀ (k : K) (m : M), (q.comp f) ((φ.comp ψ) k • m) = k • (q.comp f) m := ⋯) : explicitMap2 G M K P (φ.comp ψ) (q.comp f) ⋯ hcomp = (explicitMap2 H N K P ψ q hq hequivq).comp (explicitMap2 G M H N φ f hf hequiv)

Pullback on explicit H² respects composition of compatible pairs.

noncomputable def TauCeti.ContCohomology.explicitMap2Equiv (G : Type uG) [Monoid G] [TopologicalSpace G] (M : Type uM) [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribMulAction G M] [ContinuousSMul G M] (H : Type uH) [Monoid H] [TopologicalSpace H] (N : Type uN) [AddCommGroup N] [TopologicalSpace N] [IsTopologicalAddGroup N] [DistribMulAction H N] [ContinuousSMul H N] [ContinuousMul G] [ContinuousMul H] (φ : H ≃ₜ* G) (e : M ≃+ N) (he : Continuous ⇑e) (he' : Continuous ⇑e.symm) (hequiv : ∀ (h : H) (m : M), e (φ h • m) = h • e m) : H2 G M ≃+ H2 H N

Pullback along a compatible pair made of a continuous multiplicative equivalence and an additive equivalence of coefficients is an additive equivalence on explicit second continuous cohomology. Both directions of the coefficient equivalence are required to be continuous; for discrete coefficient modules this follows automatically from discreteness.

Equations

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

@[simp]

theorem TauCeti.ContCohomology.explicitMap2Equiv_apply (G : Type uG) [Monoid G] [TopologicalSpace G] (M : Type uM) [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribMulAction G M] [ContinuousSMul G M] (H : Type uH) [Monoid H] [TopologicalSpace H] (N : Type uN) [AddCommGroup N] [TopologicalSpace N] [IsTopologicalAddGroup N] [DistribMulAction H N] [ContinuousSMul H N] [ContinuousMul G] [ContinuousMul H] (φ : H ≃ₜ* G) (e : M ≃+ N) (he : Continuous ⇑e) (he' : Continuous ⇑e.symm) (hequiv : ∀ (h : H) (m : M), e (φ h • m) = h • e m) (x : H2 G M) : (explicitMap2Equiv G M H N φ e he he' hequiv) x = (explicitMap2 G M H N (↑φ) e.toAddMonoidHom he hequiv) x

The equivalence on explicit H² is the pullback along its forward compatible pair.

@[simp]

theorem TauCeti.ContCohomology.explicitMap2Equiv_symm_apply (G : Type uG) [Monoid G] [TopologicalSpace G] (M : Type uM) [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribMulAction G M] [ContinuousSMul G M] (H : Type uH) [Monoid H] [TopologicalSpace H] (N : Type uN) [AddCommGroup N] [TopologicalSpace N] [IsTopologicalAddGroup N] [DistribMulAction H N] [ContinuousSMul H N] [ContinuousMul G] [ContinuousMul H] (φ : H ≃ₜ* G) (e : M ≃+ N) (he : Continuous ⇑e) (he' : Continuous ⇑e.symm) (hequiv : ∀ (h : H) (m : M), e (φ h • m) = h • e m) (x : H2 H N) : (explicitMap2Equiv G M H N φ e he he' hequiv).symm x = (explicitMap2 H N G M (↑φ.symm) e.symm.toAddMonoidHom he' ⋯) x

The inverse of the equivalence on explicit H² is the pullback along the inverse compatible pair.

noncomputable def TauCeti.ContCohomology.explicitRes1 (G : Type uG) [Group G] [TopologicalSpace G] (M : Type uM) [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribMulAction G M] [ContinuousSMul G M] (S : Subgroup G) : H1 G M →+ H1 (↥S) M

Restriction on explicit H¹, induced by the subgroup inclusion and the identity coefficient map.

Equations

• TauCeti.ContCohomology.explicitRes1 G M S = TauCeti.ContCohomology.explicitMap1 G M (↥S) M (TauCeti.ContinuousMonoidHom.subgroupSubtype S) (AddMonoidHom.id M) ⋯ ⋯

@[simp]

theorem TauCeti.ContCohomology.explicitRes1_mk (G : Type uG) [Group G] [TopologicalSpace G] (M : Type uM) [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribMulAction G M] [ContinuousSMul G M] (S : Subgroup G) (c : ↥(Z1 G M)) : (explicitRes1 G M S) ↑c = ↑((cocyclesMap1 G M (↥S) M (ContinuousMonoidHom.subgroupSubtype S) (AddMonoidHom.id M) ⋯ ⋯) c)

Restriction sends the class of a continuous 1-cocycle to the class of its restriction.

theorem TauCeti.ContCohomology.explicitRes1_eq_explicitMap1 (G : Type uG) [Group G] [TopologicalSpace G] (M : Type uM) [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribMulAction G M] [ContinuousSMul G M] (S : Subgroup G) : explicitRes1 G M S = explicitMap1 G M (↥S) M (ContinuousMonoidHom.subgroupSubtype S) (AddMonoidHom.id M) ⋯ ⋯

Restriction on explicit H¹ is the compatible-pair pullback along the inclusion of the subgroup with the identity on the coefficients, the degree-one counterpart of TauCeti.ContCohomology.explicitRes0_eq_explicitMap0.

theorem TauCeti.ContCohomology.explicitRes1_comp (G : Type uG) [Group G] [TopologicalSpace G] (M : Type uM) [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribMulAction G M] [ContinuousSMul G M] (S : Subgroup G) (T : Subgroup ↥S) : (explicitRes1 (↥S) M T).comp (explicitRes1 G M S) = explicitMap1 G M (↥T) M ((ContinuousMonoidHom.subgroupSubtype S).comp (ContinuousMonoidHom.subgroupSubtype T)) (AddMonoidHom.id M) ⋯ ⋯

Restricting explicit H¹ first to S and then to a subgroup T of S is restriction along the composite inclusion.

noncomputable def TauCeti.ContCohomology.explicitRes2 (G : Type uG) [Group G] [TopologicalSpace G] (M : Type uM) [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribMulAction G M] [ContinuousSMul G M] (S : Subgroup G) [ContinuousMul G] [ContinuousMul ↥S] : H2 G M →+ H2 (↥S) M

Restriction on explicit H², induced by the subgroup inclusion and the identity coefficient map.

Equations

• TauCeti.ContCohomology.explicitRes2 G M S = TauCeti.ContCohomology.explicitMap2 G M (↥S) M (TauCeti.ContinuousMonoidHom.subgroupSubtype S) (AddMonoidHom.id M) ⋯ ⋯

@[simp]

theorem TauCeti.ContCohomology.explicitRes2_mk (G : Type uG) [Group G] [TopologicalSpace G] (M : Type uM) [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribMulAction G M] [ContinuousSMul G M] (S : Subgroup G) [ContinuousMul G] [ContinuousMul ↥S] (c : ↥(Z2 G M)) : (explicitRes2 G M S) ↑c = ↑((cocyclesMap2 G M (↥S) M (ContinuousMonoidHom.subgroupSubtype S) (AddMonoidHom.id M) ⋯ ⋯) c)

Restriction sends the class of a continuous 2-cocycle to the class of its restriction.

theorem TauCeti.ContCohomology.explicitRes2_eq_explicitMap2 (G : Type uG) [Group G] [TopologicalSpace G] (M : Type uM) [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribMulAction G M] [ContinuousSMul G M] (S : Subgroup G) [ContinuousMul G] [ContinuousMul ↥S] : explicitRes2 G M S = explicitMap2 G M (↥S) M (ContinuousMonoidHom.subgroupSubtype S) (AddMonoidHom.id M) ⋯ ⋯

Restriction on explicit H² is the compatible-pair pullback along the inclusion of the subgroup with the identity on the coefficients.

theorem TauCeti.ContCohomology.explicitRes2_comp (G : Type uG) [Group G] [TopologicalSpace G] (M : Type uM) [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribMulAction G M] [ContinuousSMul G M] (S : Subgroup G) (T : Subgroup ↥S) [ContinuousMul G] [ContinuousMul ↥S] [ContinuousMul ↥T] : (explicitRes2 (↥S) M T).comp (explicitRes2 G M S) = explicitMap2 G M (↥T) M ((ContinuousMonoidHom.subgroupSubtype S).comp (ContinuousMonoidHom.subgroupSubtype T)) (AddMonoidHom.id M) ⋯ ⋯

Restricting explicit H² first to S and then to a subgroup T of S is restriction along the composite inclusion.

noncomputable def TauCeti.ContCohomology.explicitCoeff1 (G : Type uG) [Monoid G] [TopologicalSpace G] (M : Type uM) [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribMulAction G M] [ContinuousSMul G M] {N : Type uN} [AddCommGroup N] [TopologicalSpace N] [IsTopologicalAddGroup N] [DistribMulAction G N] [ContinuousSMul G N] (f : M →+[G] N) (hf : Continuous ⇑f) : H1 G M →+ H1 G N

The coefficient map on explicit H¹ induced by a continuous equivariant additive homomorphism.

Equations

• TauCeti.ContCohomology.explicitCoeff1 G M f hf = TauCeti.ContCohomology.explicitMap1 G M G N (ContinuousMonoidHom.id G) (↑f) hf ⋯

@[simp]

theorem TauCeti.ContCohomology.explicitCoeff1_mk (G : Type uG) [Monoid G] [TopologicalSpace G] (M : Type uM) [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribMulAction G M] [ContinuousSMul G M] {N : Type uN} [AddCommGroup N] [TopologicalSpace N] [IsTopologicalAddGroup N] [DistribMulAction G N] [ContinuousSMul G N] (f : M →+[G] N) (hf : Continuous ⇑f) (c : ↥(Z1 G M)) : (explicitCoeff1 G M f hf) ↑c = ↑((cocyclesMap1 G M G N (ContinuousMonoidHom.id G) (↑f) hf ⋯) c)

A coefficient map sends a 1-cocycle class to the class obtained by postcomposition.

theorem TauCeti.ContCohomology.explicitCoeff1_eq_explicitMap1 (G : Type uG) [Monoid G] [TopologicalSpace G] (M : Type uM) [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribMulAction G M] [ContinuousSMul G M] {N : Type uN} [AddCommGroup N] [TopologicalSpace N] [IsTopologicalAddGroup N] [DistribMulAction G N] [ContinuousSMul G N] (f : M →+[G] N) (hf : Continuous ⇑f) : explicitCoeff1 G M f hf = explicitMap1 G M G N (ContinuousMonoidHom.id G) (↑f) hf ⋯

A coefficient map on explicit H¹ is the compatible-pair pullback along the identity of the group, the degree-one counterpart of TauCeti.ContCohomology.explicitCoeff0_eq_explicitMap0.

@[simp]

theorem TauCeti.ContCohomology.explicitCoeff1_id (G : Type uG) [Monoid G] [TopologicalSpace G] (M : Type uM) [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribMulAction G M] [ContinuousSMul G M] : explicitCoeff1 G M (DistribMulActionHom.id G) ⋯ = AddMonoidHom.id (H1 G M)

The identity coefficient map induces the identity on explicit H¹.

theorem TauCeti.ContCohomology.explicitCoeff1_comp (G : Type uG) [Monoid G] [TopologicalSpace G] (M : Type uM) [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribMulAction G M] [ContinuousSMul G M] {N : Type uN} [AddCommGroup N] [TopologicalSpace N] [IsTopologicalAddGroup N] [DistribMulAction G N] [ContinuousSMul G N] {P : Type uP} [AddCommGroup P] [TopologicalSpace P] [IsTopologicalAddGroup P] [DistribMulAction G P] [ContinuousSMul G P] (f : M →+[G] N) (q : N →+[G] P) (hf : Continuous ⇑f) (hq : Continuous ⇑q) : explicitCoeff1 G M (q.comp f) ⋯ = (explicitCoeff1 G N q hq).comp (explicitCoeff1 G M f hf)

Coefficient maps on explicit H¹ respect composition.

noncomputable def TauCeti.ContCohomology.explicitCoeff1Equiv (G : Type uG) [Monoid G] [TopologicalSpace G] (M : Type uM) [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribMulAction G M] [ContinuousSMul G M] {N : Type uN} [AddCommGroup N] [TopologicalSpace N] [IsTopologicalAddGroup N] [DistribMulAction G N] [ContinuousSMul G N] (e : M ≃+ N) (he : Continuous ⇑e) (he' : Continuous ⇑e.symm) (hequiv : ∀ (g : G) (m : M), e (g • m) = g • e m) : H1 G M ≃+ H1 G N

An equivariant additive equivalence of topological coefficient modules induces an additive equivalence on explicit first continuous cohomology. Both directions are required to be continuous; for discrete coefficient modules this follows automatically from discreteness.

Equations

• TauCeti.ContCohomology.explicitCoeff1Equiv G M e he he' hequiv = TauCeti.ContCohomology.explicitMap1Equiv G M G N (ContinuousMulEquiv.refl G) e he he' hequiv

@[simp]

theorem TauCeti.ContCohomology.explicitCoeff1Equiv_apply (G : Type uG) [Monoid G] [TopologicalSpace G] (M : Type uM) [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribMulAction G M] [ContinuousSMul G M] {N : Type uN} [AddCommGroup N] [TopologicalSpace N] [IsTopologicalAddGroup N] [DistribMulAction G N] [ContinuousSMul G N] (e : M ≃+ N) (he : Continuous ⇑e) (he' : Continuous ⇑e.symm) (hequiv : ∀ (g : G) (m : M), e (g • m) = g • e m) (x : H1 G M) : (explicitCoeff1Equiv G M e he he' hequiv) x = (explicitCoeff1 G M (let __src := e.toAddMonoidHom; { toFun := (↑__src).toFun, map_smul' := hequiv, map_zero' := ⋯, map_add' := ⋯ }) he) x

The coefficient equivalence on H¹ is the coefficient map induced by its forward equivariant additive homomorphism.

@[simp]

theorem TauCeti.ContCohomology.explicitCoeff1Equiv_symm_apply (G : Type uG) [Monoid G] [TopologicalSpace G] (M : Type uM) [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribMulAction G M] [ContinuousSMul G M] {N : Type uN} [AddCommGroup N] [TopologicalSpace N] [IsTopologicalAddGroup N] [DistribMulAction G N] [ContinuousSMul G N] (e : M ≃+ N) (he : Continuous ⇑e) (he' : Continuous ⇑e.symm) (hequiv : ∀ (g : G) (m : M), e (g • m) = g • e m) (x : H1 G N) : (explicitCoeff1Equiv G M e he he' hequiv).symm x = (explicitCoeff1 G N (let __src := e.symm.toAddMonoidHom; { toFun := (↑__src).toFun, map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }) he') x

The inverse coefficient equivalence on H¹ is the coefficient map induced by the inverse equivariant additive homomorphism.

theorem TauCeti.ContCohomology.explicitCoeff1Equiv_mk (G : Type uG) [Monoid G] [TopologicalSpace G] (M : Type uM) [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribMulAction G M] [ContinuousSMul G M] {N : Type uN} [AddCommGroup N] [TopologicalSpace N] [IsTopologicalAddGroup N] [DistribMulAction G N] [ContinuousSMul G N] (e : M ≃+ N) (he : Continuous ⇑e) (he' : Continuous ⇑e.symm) (hequiv : ∀ (g : G) (m : M), e (g • m) = g • e m) (c : ↥(Z1 G M)) : (explicitCoeff1Equiv G M e he he' hequiv) ↑c = ↑((cocyclesMap1 G M G N (ContinuousMonoidHom.id G) (↑(let __src := e.toAddMonoidHom; { toFun := (↑__src).toFun, map_smul' := hequiv, map_zero' := ⋯, map_add' := ⋯ })) he ⋯) c)

On cocycle classes, the coefficient equivalence postcomposes the cocycle with the given equivalence of coefficients.

noncomputable def TauCeti.ContCohomology.explicitCoeff2 (G : Type uG) [Monoid G] [TopologicalSpace G] (M : Type uM) [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribMulAction G M] [ContinuousSMul G M] [ContinuousMul G] {N : Type uN} [AddCommGroup N] [TopologicalSpace N] [IsTopologicalAddGroup N] [DistribMulAction G N] [ContinuousSMul G N] (f : M →+[G] N) (hf : Continuous ⇑f) : H2 G M →+ H2 G N

The coefficient map on explicit H² induced by a continuous equivariant additive homomorphism.

Equations

• TauCeti.ContCohomology.explicitCoeff2 G M f hf = TauCeti.ContCohomology.explicitMap2 G M G N (ContinuousMonoidHom.id G) (↑f) hf ⋯

@[simp]

theorem TauCeti.ContCohomology.explicitCoeff2_mk (G : Type uG) [Monoid G] [TopologicalSpace G] (M : Type uM) [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribMulAction G M] [ContinuousSMul G M] [ContinuousMul G] {N : Type uN} [AddCommGroup N] [TopologicalSpace N] [IsTopologicalAddGroup N] [DistribMulAction G N] [ContinuousSMul G N] (f : M →+[G] N) (hf : Continuous ⇑f) (c : ↥(Z2 G M)) : (explicitCoeff2 G M f hf) ↑c = ↑((cocyclesMap2 G M G N (ContinuousMonoidHom.id G) (↑f) hf ⋯) c)

A coefficient map sends a 2-cocycle class to the class obtained by postcomposition.

theorem TauCeti.ContCohomology.explicitCoeff2_eq_explicitMap2 (G : Type uG) [Monoid G] [TopologicalSpace G] (M : Type uM) [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribMulAction G M] [ContinuousSMul G M] [ContinuousMul G] {N : Type uN} [AddCommGroup N] [TopologicalSpace N] [IsTopologicalAddGroup N] [DistribMulAction G N] [ContinuousSMul G N] (f : M →+[G] N) (hf : Continuous ⇑f) : explicitCoeff2 G M f hf = explicitMap2 G M G N (ContinuousMonoidHom.id G) (↑f) hf ⋯

A coefficient map on explicit H² is the compatible-pair pullback along the identity of the group.

@[simp]

theorem TauCeti.ContCohomology.explicitCoeff2_id (G : Type uG) [Monoid G] [TopologicalSpace G] (M : Type uM) [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribMulAction G M] [ContinuousSMul G M] [ContinuousMul G] : explicitCoeff2 G M (DistribMulActionHom.id G) ⋯ = AddMonoidHom.id (H2 G M)

The identity coefficient map induces the identity on explicit H².

theorem TauCeti.ContCohomology.explicitCoeff2_eq_nsmul (G : Type uG) [Monoid G] [TopologicalSpace G] (M : Type uM) [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribMulAction G M] [ContinuousSMul G M] [ContinuousMul G] (f : M →+[G] M) (hf : Continuous ⇑f) {k : ℕ} (hk : ∀ (m : M), f m = k • m) (x : H2 G M) : (explicitCoeff2 G M f hf) x = k • x

A coefficient map which is multiplication by k on M induces multiplication by k on explicit H²: the class of a 2-cocycle c goes to the class of k • c.

theorem TauCeti.ContCohomology.explicitCoeff2_comp (G : Type uG) [Monoid G] [TopologicalSpace G] (M : Type uM) [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribMulAction G M] [ContinuousSMul G M] [ContinuousMul G] {N : Type uN} [AddCommGroup N] [TopologicalSpace N] [IsTopologicalAddGroup N] [DistribMulAction G N] [ContinuousSMul G N] {P : Type uP} [AddCommGroup P] [TopologicalSpace P] [IsTopologicalAddGroup P] [DistribMulAction G P] [ContinuousSMul G P] (f : M →+[G] N) (q : N →+[G] P) (hf : Continuous ⇑f) (hq : Continuous ⇑q) : explicitCoeff2 G M (q.comp f) ⋯ = (explicitCoeff2 G N q hq).comp (explicitCoeff2 G M f hf)

Coefficient maps on explicit H² respect composition.

noncomputable def TauCeti.ContCohomology.explicitCoeff2Equiv (G : Type uG) [Monoid G] [TopologicalSpace G] (M : Type uM) [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribMulAction G M] [ContinuousSMul G M] [ContinuousMul G] {N : Type uN} [AddCommGroup N] [TopologicalSpace N] [IsTopologicalAddGroup N] [DistribMulAction G N] [ContinuousSMul G N] (e : M ≃+ N) (he : Continuous ⇑e) (he' : Continuous ⇑e.symm) (hequiv : ∀ (g : G) (m : M), e (g • m) = g • e m) : H2 G M ≃+ H2 G N

An equivariant additive equivalence of topological coefficient modules induces an additive equivalence on explicit second continuous cohomology. Both directions are required to be continuous; for discrete coefficient modules this follows automatically from discreteness.

Equations

• TauCeti.ContCohomology.explicitCoeff2Equiv G M e he he' hequiv = TauCeti.ContCohomology.explicitMap2Equiv G M G N (ContinuousMulEquiv.refl G) e he he' hequiv

@[simp]

theorem TauCeti.ContCohomology.explicitCoeff2Equiv_apply (G : Type uG) [Monoid G] [TopologicalSpace G] (M : Type uM) [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribMulAction G M] [ContinuousSMul G M] [ContinuousMul G] {N : Type uN} [AddCommGroup N] [TopologicalSpace N] [IsTopologicalAddGroup N] [DistribMulAction G N] [ContinuousSMul G N] (e : M ≃+ N) (he : Continuous ⇑e) (he' : Continuous ⇑e.symm) (hequiv : ∀ (g : G) (m : M), e (g • m) = g • e m) (x : H2 G M) : (explicitCoeff2Equiv G M e he he' hequiv) x = (explicitCoeff2 G M (let __src := e.toAddMonoidHom; { toFun := (↑__src).toFun, map_smul' := hequiv, map_zero' := ⋯, map_add' := ⋯ }) he) x

The coefficient equivalence on H² is the coefficient map induced by its forward equivariant additive homomorphism.

@[simp]

theorem TauCeti.ContCohomology.explicitCoeff2Equiv_symm_apply (G : Type uG) [Monoid G] [TopologicalSpace G] (M : Type uM) [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribMulAction G M] [ContinuousSMul G M] [ContinuousMul G] {N : Type uN} [AddCommGroup N] [TopologicalSpace N] [IsTopologicalAddGroup N] [DistribMulAction G N] [ContinuousSMul G N] (e : M ≃+ N) (he : Continuous ⇑e) (he' : Continuous ⇑e.symm) (hequiv : ∀ (g : G) (m : M), e (g • m) = g • e m) (x : H2 G N) : (explicitCoeff2Equiv G M e he he' hequiv).symm x = (explicitCoeff2 G N (let __src := e.symm.toAddMonoidHom; { toFun := (↑__src).toFun, map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }) he') x

The inverse coefficient equivalence on H² is the coefficient map induced by the inverse equivariant additive homomorphism.

theorem TauCeti.ContCohomology.explicitCoeff1_bijective (G : Type uG) [Monoid G] [TopologicalSpace G] (M : Type uM) [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribMulAction G M] [ContinuousSMul G M] [DiscreteTopology M] {N : Type uN} [AddCommGroup N] [TopologicalSpace N] [IsTopologicalAddGroup N] [DiscreteTopology N] [DistribMulAction G N] [ContinuousSMul G N] {f : M →+[G] N} (hf : Function.Bijective ⇑f) : Function.Bijective ⇑(explicitCoeff1 G M f ⋯)

A bijective equivariant homomorphism of discrete coefficient modules induces a bijection on explicit first cohomology.

theorem TauCeti.ContCohomology.explicitCoeff2_bijective (G : Type uG) [Monoid G] [TopologicalSpace G] (M : Type uM) [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribMulAction G M] [ContinuousSMul G M] [ContinuousMul G] [DiscreteTopology M] {N : Type uN} [AddCommGroup N] [TopologicalSpace N] [IsTopologicalAddGroup N] [DiscreteTopology N] [DistribMulAction G N] [ContinuousSMul G N] {f : M →+[G] N} (hf : Function.Bijective ⇑f) : Function.Bijective ⇑(explicitCoeff2 G M f ⋯)

A bijective equivariant homomorphism of discrete coefficient modules induces a bijection on explicit second cohomology.

theorem TauCeti.ContCohomology.explicitCoeff2_eq_card_nsmul (G : Type uG) [Group G] [TopologicalSpace G] [ContinuousMul G] (M : Type uM) [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribMulAction G M] [ContinuousSMul G M] (N : Subgroup G) [N.Normal] [Fintype ↥N] (x : H2 G M) : (explicitCoeff2 G M (groupNormHom N M) ⋯) x = Nat.card ↥N • x

The norm of a finite normal subgroup acts on explicit H² as multiplication by its order. The norm m ↦ ∑ n : N, n • m of a finite normal subgroup N of G, as a coefficient map, induces multiplication by #N on H²(G, M). The norm is G-equivariant because N is normal, and it is multiplication by #N on the invariants, but not in general on M.