Canonical second continuous cohomology along compatible pairs in independent universes

Mathlib's ContinuousCohomology.map pulls continuous cohomology back along a compatible pair (φ : H →ₜ* G, f : res φ X ⟶ Y), but it is a morphism in a single category of topological modules, so it binds both groups to one universe and both coefficient objects to one universe. For discrete coefficient modules and locally compact groups this file constructs the same pullback on Mathlib's continuousCohomology 2 with the universes of G and M independent of those of H and N. This is what a field isomorphism K ≃+* L between fields in different universes, such as K ≃+* ULift K, induces on the canonical second Galois cohomology groups.

On canonical homogeneous cocycles the construction is the expected cochain pullback: a cocycle σ of G goes to the cocycle (h₀, h₁, h₂) ↦ f (σ (φ h₀) (φ h₁) (φ h₂)) of H (TauCeti.ContCohomology.iCycles_homogeneousCocyclesMap2_apply), and classes go to classes (TauCeti.ContCohomology.continuousCohomologyMap2_homologyπ). Since the pullback of a canonical cocycle lives in a category of a different universe, it is constructed through the explicit inhomogeneous model, in which cochains are plain functions and pullback needs no common universe. When all four types share one universe it is Mathlib's map (TauCeti.ContCohomology.continuousCohomologyMap2_eq_map).

Main definitions

• TauCeti.ContCohomology.homogeneousCocyclesMap2: pullback of canonical continuous two-cocycles along a compatible pair.
• TauCeti.ContCohomology.continuousCohomologyMap2: the induced map on continuousCohomology 2.
• TauCeti.ContCohomology.continuousCohomologyMap2Equiv: the additive equivalence induced by a compatible pair of equivalences.

Main results

• TauCeti.ContCohomology.iCycles_homogeneousCocyclesMap2_apply: the value of a pulled-back canonical cocycle.
• TauCeti.ContCohomology.continuousCohomologyMap2_homologyπ: the map on classes is induced by the map on cocycles.
• TauCeti.ContCohomology.explicitH2AddEquivContinuousCohomology_continuousCohomologyMap2: the comparison with the explicit model carries explicitMap2 to continuousCohomologyMap2.
• TauCeti.ContCohomology.homogeneousCocyclesMap2_eq_cocyclesMap and TauCeti.ContCohomology.continuousCohomologyMap2_eq_map: in a single universe these are Mathlib's ContinuousCohomology.cocyclesMap and ContinuousCohomology.map.
• TauCeti.ContCohomology.continuousCohomologyMap2_id and TauCeti.ContCohomology.continuousCohomologyMap2_comp: functoriality, with the three groups in independent universes.

References

• J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, 2nd ed., Ch. I, §2 and §5: compatible pairs and the induced maps on homogeneous and inhomogeneous cochains.

noncomputable def TauCeti.ContCohomology.homogeneousCocyclesMap2 (G M : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [LocallyCompactSpace G] [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] [ContinuousSMul G M] (H N : Type v) [Group H] [TopologicalSpace H] [IsTopologicalGroup H] [LocallyCompactSpace H] [AddCommGroup N] [TopologicalSpace N] [DiscreteTopology N] [DistribMulAction H N] [ContinuousSMul H N] (φ : H →ₜ* G) (f : M →+ N) (hf : ∀ (h : H) (m : M), f (φ h • m) = h • f m) : ↑(ContinuousCohomology.cocycles (ofDiscreteModule ℤ G M) 2).toModuleCat →+ ↑(ContinuousCohomology.cocycles (ofDiscreteModule ℤ H N) 2).toModuleCat

Pullback of canonical continuous two-cocycles along a compatible pair (φ, f), with the universes of G and M independent of those of H and N. Its value is computed by TauCeti.ContCohomology.iCycles_homogeneousCocyclesMap2_apply.

@[simp]

theorem TauCeti.ContCohomology.homogeneousCocyclesMap2_cocycleEquiv2 (G M : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [LocallyCompactSpace G] [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] [ContinuousSMul G M] (H N : Type v) [Group H] [TopologicalSpace H] [IsTopologicalGroup H] [LocallyCompactSpace H] [AddCommGroup N] [TopologicalSpace N] [DiscreteTopology N] [DistribMulAction H N] [ContinuousSMul H N] (φ : H →ₜ* G) (f : M →+ N) (hf : ∀ (h : H) (m : M), f (φ h • m) = h • f m) (c : ↥(Z2 G M)) : (homogeneousCocyclesMap2 G M H N φ f hf) ((cocycleEquiv2 G M) c) = (cocycleEquiv2 H N) ((cocyclesMap2 G M H N φ f ⋯ hf) c)

On explicit cocycles, pullback of canonical cocycles is the explicit pullback.

theorem TauCeti.ContCohomology.iCycles_homogeneousCocyclesMap2_apply (G M : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [LocallyCompactSpace G] [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] [ContinuousSMul G M] (H N : Type v) [Group H] [TopologicalSpace H] [IsTopologicalGroup H] [LocallyCompactSpace H] [AddCommGroup N] [TopologicalSpace N] [DiscreteTopology N] [DistribMulAction H N] [ContinuousSMul H N] (φ : H →ₜ* G) (f : M →+ N) (hf : ∀ (h : H) (m : M), f (φ h • m) = h • f m) (σ : ↑(ContinuousCohomology.cocycles (ofDiscreteModule ℤ G M) 2).toModuleCat) (h₀ h₁ h₂ : H) : ((↑((CategoryTheory.ConcreteCategory.hom (HomologicalComplex.iCycles (ofDiscreteModule ℤ H N).homogeneousCochains 2)) ((homogeneousCocyclesMap2 G M H N φ f hf) σ)) h₀) h₁) h₂ = f (((↑((CategoryTheory.ConcreteCategory.hom (HomologicalComplex.iCycles (ofDiscreteModule ℤ G M).homogeneousCochains 2)) σ) (φ h₀)) (φ h₁)) (φ h₂))

The pulled-back canonical cocycle. The homogeneous cocycle σ of G goes to the homogeneous cocycle (h₀, h₁, h₂) ↦ f (σ (φ h₀) (φ h₁) (φ h₂)) of H.

noncomputable def TauCeti.ContCohomology.continuousCohomologyMap2 (G M : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [LocallyCompactSpace G] [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] [ContinuousSMul G M] (H N : Type v) [Group H] [TopologicalSpace H] [IsTopologicalGroup H] [LocallyCompactSpace H] [AddCommGroup N] [TopologicalSpace N] [DiscreteTopology N] [DistribMulAction H N] [ContinuousSMul H N] (φ : H →ₜ* G) (f : M →+ N) (hf : ∀ (h : H) (m : M), f (φ h • m) = h • f m) : ↑(continuousCohomology 2 (ofDiscreteModule ℤ G M)).toModuleCat →+ ↑(continuousCohomology 2 (ofDiscreteModule ℤ H N)).toModuleCat

Pullback along a compatible pair on Mathlib's continuousCohomology 2, with the universes of G and M independent of those of H and N. It is induced by TauCeti.ContCohomology.homogeneousCocyclesMap2 (continuousCohomologyMap2_homologyπ), and in a single universe it is Mathlib's ContinuousCohomology.map (continuousCohomologyMap2_eq_map).

@[simp]

theorem TauCeti.ContCohomology.explicitH2AddEquivContinuousCohomology_continuousCohomologyMap2 (G M : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [LocallyCompactSpace G] [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] [ContinuousSMul G M] (H N : Type v) [Group H] [TopologicalSpace H] [IsTopologicalGroup H] [LocallyCompactSpace H] [AddCommGroup N] [TopologicalSpace N] [DiscreteTopology N] [DistribMulAction H N] [ContinuousSMul H N] (φ : H →ₜ* G) (f : M →+ N) (hf : ∀ (h : H) (m : M), f (φ h • m) = h • f m) (x : H2 G M) : (continuousCohomologyMap2 G M H N φ f hf) ((explicitH2AddEquivContinuousCohomology G M) x) = (explicitH2AddEquivContinuousCohomology H N) ((explicitMap2 G M H N φ f ⋯ hf) x)

The comparison with the explicit model carries the explicit pullback explicitMap2 to continuousCohomologyMap2.

@[simp]

theorem TauCeti.ContCohomology.continuousCohomologyMap2_homologyπ (G M : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [LocallyCompactSpace G] [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] [ContinuousSMul G M] (H N : Type v) [Group H] [TopologicalSpace H] [IsTopologicalGroup H] [LocallyCompactSpace H] [AddCommGroup N] [TopologicalSpace N] [DiscreteTopology N] [DistribMulAction H N] [ContinuousSMul H N] (φ : H →ₜ* G) (f : M →+ N) (hf : ∀ (h : H) (m : M), f (φ h • m) = h • f m) (σ : ↑(ContinuousCohomology.cocycles (ofDiscreteModule ℤ G M) 2).toModuleCat) : (continuousCohomologyMap2 G M H N φ f hf) ((CategoryTheory.ConcreteCategory.hom (HomologicalComplex.homologyπ (ofDiscreteModule ℤ G M).homogeneousCochains 2)) σ) = (CategoryTheory.ConcreteCategory.hom (HomologicalComplex.homologyπ (ofDiscreteModule ℤ H N).homogeneousCochains 2)) ((homogeneousCocyclesMap2 G M H N φ f hf) σ)

The map on classes is induced by the map on cocycles. The class of a canonical cocycle goes to the class of its pullback.

theorem TauCeti.ContCohomology.homogeneousCocyclesMap2_eq_cocyclesMap (G M : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [LocallyCompactSpace G] [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] [ContinuousSMul G M] (H N : Type u) [Group H] [TopologicalSpace H] [IsTopologicalGroup H] [LocallyCompactSpace H] [AddCommGroup N] [TopologicalSpace N] [DiscreteTopology N] [DistribMulAction H N] [ContinuousSMul H N] (φ : H →ₜ* G) (f : M →+ N) (hf : ∀ (h : H) (m : M), f (φ h • m) = h • f m) (σ : ↑(ContinuousCohomology.cocycles (ofDiscreteModule ℤ G M) 2).toModuleCat) : (homogeneousCocyclesMap2 G M H N φ f hf) σ = (CategoryTheory.ConcreteCategory.hom (ContinuousCohomology.cocyclesMap φ (ofDiscreteModulePair (↑φ) f.toIntLinearMap ⋯) 2)) σ

In a single universe, pullback of canonical cocycles is Mathlib's ContinuousCohomology.cocyclesMap along the same compatible pair.

theorem TauCeti.ContCohomology.continuousCohomologyMap2_eq_map (G M : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [LocallyCompactSpace G] [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] [ContinuousSMul G M] (H N : Type u) [Group H] [TopologicalSpace H] [IsTopologicalGroup H] [LocallyCompactSpace H] [AddCommGroup N] [TopologicalSpace N] [DiscreteTopology N] [DistribMulAction H N] [ContinuousSMul H N] (φ : H →ₜ* G) (f : M →+ N) (hf : ∀ (h : H) (m : M), f (φ h • m) = h • f m) (x : ↑(continuousCohomology 2 (ofDiscreteModule ℤ G M)).toModuleCat) : (continuousCohomologyMap2 G M H N φ f hf) x = (CategoryTheory.ConcreteCategory.hom (ContinuousCohomology.map φ (ofDiscreteModulePair (↑φ) f.toIntLinearMap ⋯) 2)) x

In a single universe, continuousCohomologyMap2 is Mathlib's ContinuousCohomology.map along the same compatible pair.

@[simp]

theorem TauCeti.ContCohomology.continuousCohomologyMap2_id (G M : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [LocallyCompactSpace G] [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology 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 := ⋯) : continuousCohomologyMap2 G M G M (ContinuousMonoidHom.id G) (AddMonoidHom.id M) hid = AddMonoidHom.id ↑(continuousCohomology 2 (ofDiscreteModule ℤ G M)).toModuleCat

Pullback along the identity compatible pair is the identity.

theorem TauCeti.ContCohomology.continuousCohomologyMap2_comp (G M : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [LocallyCompactSpace G] [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] [ContinuousSMul G M] (H N : Type v) [Group H] [TopologicalSpace H] [IsTopologicalGroup H] [LocallyCompactSpace H] [AddCommGroup N] [TopologicalSpace N] [DiscreteTopology N] [DistribMulAction H N] [ContinuousSMul H N] (φ : H →ₜ* G) (f : M →+ N) (hf : ∀ (h : H) (m : M), f (φ h • m) = h • f m) (K P : Type w) [Group K] [TopologicalSpace K] [IsTopologicalGroup K] [LocallyCompactSpace K] [AddCommGroup P] [TopologicalSpace P] [DiscreteTopology P] [DistribMulAction K P] [ContinuousSMul K P] (ψ : K →ₜ* H) (q : N →+ P) (hq : ∀ (k : K) (n : N), q (ψ k • n) = k • q n) : continuousCohomologyMap2 G M K P (φ.comp ψ) (q.comp f) ⋯ = (continuousCohomologyMap2 H N K P ψ q hq).comp (continuousCohomologyMap2 G M H N φ f hf)

Pullback respects composition of compatible pairs, with the three groups and their coefficient modules in independent universes.

noncomputable def TauCeti.ContCohomology.continuousCohomologyMap2Equiv (G M : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [LocallyCompactSpace G] [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] [ContinuousSMul G M] (H N : Type v) [Group H] [TopologicalSpace H] [IsTopologicalGroup H] [LocallyCompactSpace H] [AddCommGroup N] [TopologicalSpace N] [DiscreteTopology N] [DistribMulAction H N] [ContinuousSMul H N] (φ : H ≃ₜ* G) (e : M ≃+ N) (he : ∀ (h : H) (m : M), e (φ h • m) = h • e m) : ↑(continuousCohomology 2 (ofDiscreteModule ℤ G M)).toModuleCat ≃+ ↑(continuousCohomology 2 (ofDiscreteModule ℤ H N)).toModuleCat

The additive equivalence of canonical second continuous cohomology groups induced by a compatible pair of a continuous multiplicative equivalence φ : H ≃ₜ* G and an additive equivalence e : M ≃+ N, with the universes of G and M independent of those of H and N. Its forward and inverse maps are continuousCohomologyMap2 along the pair and along its inverse.

@[simp]

theorem TauCeti.ContCohomology.continuousCohomologyMap2Equiv_apply (G M : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [LocallyCompactSpace G] [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] [ContinuousSMul G M] (H N : Type v) [Group H] [TopologicalSpace H] [IsTopologicalGroup H] [LocallyCompactSpace H] [AddCommGroup N] [TopologicalSpace N] [DiscreteTopology N] [DistribMulAction H N] [ContinuousSMul H N] (φ : H ≃ₜ* G) (e : M ≃+ N) (he : ∀ (h : H) (m : M), e (φ h • m) = h • e m) (x : ↑(continuousCohomology 2 (ofDiscreteModule ℤ G M)).toModuleCat) : (continuousCohomologyMap2Equiv G M H N φ e he) x = (continuousCohomologyMap2 G M H N (↑φ) e.toAddMonoidHom he) x

The equivalence is pullback along its forward compatible pair.

@[simp]

theorem TauCeti.ContCohomology.continuousCohomologyMap2Equiv_symm_apply (G M : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [LocallyCompactSpace G] [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] [ContinuousSMul G M] (H N : Type v) [Group H] [TopologicalSpace H] [IsTopologicalGroup H] [LocallyCompactSpace H] [AddCommGroup N] [TopologicalSpace N] [DiscreteTopology N] [DistribMulAction H N] [ContinuousSMul H N] (φ : H ≃ₜ* G) (e : M ≃+ N) (he : ∀ (h : H) (m : M), e (φ h • m) = h • e m) (x : ↑(continuousCohomology 2 (ofDiscreteModule ℤ H N)).toModuleCat) : (continuousCohomologyMap2Equiv G M H N φ e he).symm x = (continuousCohomologyMap2 H N G M (↑φ.symm) e.symm.toAddMonoidHom ⋯) x

The inverse equivalence is pullback along the inverse compatible pair.