The explicit model against the canonical object, in degrees one and two

The explicit low-degree complex presents H¹(G, M) and H²(G, M) as Z¹/B¹ and Z²/B², honest subquotients of the continuous functions on G and on G × G, while the canonical object is Mathlib's continuousCohomology n X for X the image TauCeti.ofDiscreteModule ℤ G M of M under the coefficient dictionary. This file identifies the two in degrees one and two.

The passage happens one level at a time. CochainComparison.lean identifies the inhomogeneous cochains with the canonical homogeneous ones, and CocycleComparison.lean cuts that down to the cocycles in degrees one and two. What remains, and is the content of this file, is the passage from cocycles to classes: the canonical homology is the cokernel of HomologicalComplex.toCycles, so a cocycle has trivial canonical class exactly when it is a canonical boundary, and TauCeti.ContCohomology.mem_B1_iff_cocycleEquiv1_mem_range together with its landed degree-two counterpart says that those are precisely the explicit coboundaries.

The comparison is stated twice, and the two statements are not interchangeable. The additive equivalence holds over an arbitrary topological group in degree one, and over a locally compact one in degree two, the local compactness being what supplies ContinuousMap.uncurry for the degree-two cochain comparison. The isomorphism in TopModuleCat ℤ needs G compact, and its source is the discrete carrier TauCeti.ContCohomology.DiscreteH1, not the quotient topology that H¹ inherits from the pointwise topology on G → M: that inherited topology is not discrete in general, so discreteness cannot be assumed, whereas the canonical side is discrete by TauCeti.discreteTopology_continuousCohomology. A comparison stated in TopModuleCat ℤ against the inherited topology would be false while its underlying additive statement stayed true, which is why the discrete synonyms exist.

Main definitions

• TauCeti.ContCohomology.explicitH1AddEquivContinuousCohomology and explicitH2AddEquivContinuousCohomology: the comparisons as additive equivalences.
• TauCeti.ContCohomology.explicitH1IsoContinuousCohomology and explicitH2IsoContinuousCohomology: the comparisons as isomorphisms in TopModuleCat ℤ.
• TopRep.explicitH1AddEquivContinuousCohomologyOfDiscrete and TopRep.explicitH2AddEquivContinuousCohomologyOfDiscrete: the comparisons for the carrier of a discrete smooth representation over any scalars, obtained from the ℤ-comparisons by restricting scalars.

Main results

• TauCeti.ContCohomology.explicitH1AddEquivContinuousCohomology_apply and explicitH2AddEquivContinuousCohomology_apply: the comparisons send the class of an explicit cocycle to the homology class of the cocycle it corresponds to.
• TauCeti.ContCohomology.explicitH1AddEquivContinuousCohomology_map and explicitH1AddEquivContinuousCohomology_coeffMap: the degree-one comparison carries the explicit pullback along a compatible pair, and in particular the explicit coefficient map, to the canonical one; TopRep.explicitH1AddEquivContinuousCohomologyOfDiscrete_map is the same naturality for discrete representations over any scalars.
• TauCeti.ContCohomology.explicitIso_map: the same naturality in compatible pairs for the degree-one comparison in TopModuleCat ℤ, with explicitIso_res and explicitIso_coeffMap as its restriction and coefficient-map specializations.
• TauCeti.ContCohomology.explicitH2AddEquivContinuousCohomology_map and explicitH2AddEquivContinuousCohomology_coeffMap: the degree-two comparison carries the explicit pullback along a compatible pair, and in particular the explicit coefficient map, to the canonical one; TopRep.explicitH2AddEquivContinuousCohomologyOfDiscrete_map is the same naturality for discrete representations over any scalars.

References

• J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, 2nd ed., Ch. I, §2: the identification of the inhomogeneous description of continuous cohomology with the homogeneous one. The isomorphisms built here are the degree-one and degree-two cases.

theorem TauCeti.ContCohomology.addEquiv_eqToHom_ne_zero {A : Type u_1} [AddCommGroup A] {B C : TopModuleCat ℤ} (e : B = C) (f : A ≃+ ↑B.toModuleCat) (x : A) (hx : x ≠ 0) : (TopModuleCat.Hom.hom (CategoryTheory.eqToHom e)) (f x) ≠ 0

An additive equivalence followed by transport between equal TopModuleCat objects preserves nonzero elements. This applies to the explicit-to-canonical cohomology comparison.

noncomputable def TauCeti.ContCohomology.explicitH1AddEquivContinuousCohomology (G M : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] [ContinuousSMul G M] : H1 G M ≃+ ↑(continuousCohomology 1 (ofDiscreteModule ℤ G M)).toModuleCat

The explicit H¹(G, M) is Mathlib's continuousCohomology 1 of the canonical object attached to M, as an additive equivalence.

No hypothesis on G beyond being a topological group is used: the cochain comparison in degree one is a currying with no local-compactness condition, and passing to a subquotient needs none either. The companion TauCeti.ContCohomology.explicitH1IsoContinuousCohomology upgrades this to TopModuleCat ℤ, and that upgrade does need G compact.

Equations

• TauCeti.ContCohomology.explicitH1AddEquivContinuousCohomology G M = QuotientAddGroup.liftEquiv ((TauCeti.ContCohomology.B1 G M).addSubgroupOf (TauCeti.ContCohomology.Z1 G M)) ⋯ ⋯

@[simp]

theorem TauCeti.ContCohomology.explicitH1AddEquivContinuousCohomology_apply (G M : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] [ContinuousSMul G M] (c : ↥(Z1 G M)) : (explicitH1AddEquivContinuousCohomology G M) ↑c = (CategoryTheory.ConcreteCategory.hom (HomologicalComplex.homologyπ (ofDiscreteModule ℤ G M).homogeneousCochains 1)) ((cocycleEquiv1 G M) c)

The comparison sends the class of a continuous one-cocycle to the canonical homology class of the cocycle it corresponds to.

@[simp]

theorem TauCeti.ContCohomology.explicitH1AddEquivContinuousCohomology_symm_apply (G M : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] [ContinuousSMul G M] (c : ↑(ContinuousCohomology.cocycles (ofDiscreteModule ℤ G M) 1).toModuleCat) : (explicitH1AddEquivContinuousCohomology G M).symm ((CategoryTheory.ConcreteCategory.hom (HomologicalComplex.homologyπ (ofDiscreteModule ℤ G M).homogeneousCochains 1)) c) = ↑((cocycleEquiv1 G M).symm c)

The inverse comparison sends a canonical homology class to the explicit class of the corresponding inhomogeneous cocycle.

theorem TauCeti.ContCohomology.explicitH1AddEquivContinuousCohomology_map (G M : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] [ContinuousSMul G M] (H N : Type u) [Group H] [TopologicalSpace H] [IsTopologicalGroup 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 : H1 G M) : (CategoryTheory.ConcreteCategory.hom (ContinuousCohomology.map φ (ofDiscreteModulePair (↑φ) f.toIntLinearMap ⋯) 1)) ((explicitH1AddEquivContinuousCohomology G M) x) = (explicitH1AddEquivContinuousCohomology H N) ((explicitMap1 G M H N φ f ⋯ hf) x)

Naturality of the degree-one comparison. The comparison carries the explicit pullback along a compatible pair to Mathlib's canonical continuous-cohomology map along the same pair. Restriction and coefficient maps below are specializations of this square.

theorem TauCeti.ContCohomology.explicitH1AddEquivContinuousCohomology_coeffMap (G M : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] [ContinuousSMul G M] (N : Type u) [AddCommGroup N] [TopologicalSpace N] [DiscreteTopology N] [DistribMulAction G N] [ContinuousSMul G N] (f : M →+[G] N) (x : H1 G M) : (CategoryTheory.ConcreteCategory.hom (ContinuousCohomology.coeffMap (ofDiscreteModuleMap f.toAddMonoidHom.toIntLinearMap ⋯) 1)) ((explicitH1AddEquivContinuousCohomology G M) x) = (explicitH1AddEquivContinuousCohomology G N) ((explicitCoeff1 G M f ⋯) x)

The degree-one comparison carries the explicit coefficient map to the canonical coefficient map TauCeti.ContinuousCohomology.coeffMap attached to the same equivariant homomorphism, the degree-one counterpart of TauCeti.ContCohomology.explicitH0Iso_coeffMap.

Degree two

noncomputable def TauCeti.ContCohomology.explicitH2AddEquivContinuousCohomology (G M : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] [ContinuousSMul G M] [LocallyCompactSpace G] : H2 G M ≃+ ↑(continuousCohomology 2 (ofDiscreteModule ℤ G M)).toModuleCat

The explicit H²(G, M) is Mathlib's continuousCohomology 2 of the canonical object attached to M, as an additive equivalence.

The group is locally compact because the inverse of the degree-two cochain comparison uncurries, which is where the compact-open exponential law enters; a profinite group qualifies.

Equations

• TauCeti.ContCohomology.explicitH2AddEquivContinuousCohomology G M = QuotientAddGroup.liftEquiv ((TauCeti.ContCohomology.B2 G M).addSubgroupOf (TauCeti.ContCohomology.Z2 G M)) ⋯ ⋯

@[simp]

theorem TauCeti.ContCohomology.explicitH2AddEquivContinuousCohomology_apply (G M : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] [ContinuousSMul G M] [LocallyCompactSpace G] (c : ↥(Z2 G M)) : (explicitH2AddEquivContinuousCohomology G M) ↑c = (CategoryTheory.ConcreteCategory.hom (HomologicalComplex.homologyπ (ofDiscreteModule ℤ G M).homogeneousCochains 2)) ((cocycleEquiv2 G M) c)

The comparison sends the class of a continuous two-cocycle to the canonical homology class of the cocycle it corresponds to.

@[simp]

theorem TauCeti.ContCohomology.explicitH2AddEquivContinuousCohomology_symm_apply (G M : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] [ContinuousSMul G M] [LocallyCompactSpace G] (c : ↑(ContinuousCohomology.cocycles (ofDiscreteModule ℤ G M) 2).toModuleCat) : (explicitH2AddEquivContinuousCohomology G M).symm ((CategoryTheory.ConcreteCategory.hom (HomologicalComplex.homologyπ (ofDiscreteModule ℤ G M).homogeneousCochains 2)) c) = ↑((cocycleEquiv2 G M).symm c)

The inverse comparison sends a canonical homology class to the explicit class of the corresponding inhomogeneous cocycle.

theorem TauCeti.ContCohomology.explicitH2AddEquivContinuousCohomology_map (G M : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] [ContinuousSMul G M] [LocallyCompactSpace G] (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 : H2 G M) : (CategoryTheory.ConcreteCategory.hom (ContinuousCohomology.map φ (ofDiscreteModulePair (↑φ) f.toIntLinearMap ⋯) 2)) ((explicitH2AddEquivContinuousCohomology G M) x) = (explicitH2AddEquivContinuousCohomology H N) ((explicitMap2 G M H N φ f ⋯ hf) x)

The degree-two comparison carries the explicit pullback TauCeti.ContCohomology.explicitMap2 along a compatible pair to Mathlib's ContinuousCohomology.map along the same pair. This is the naturality equation used to transport general compatible-pair maps between the two models.

theorem TauCeti.ContCohomology.explicitH2AddEquivContinuousCohomology_coeffMap (G M : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] [ContinuousSMul G M] [LocallyCompactSpace G] (N : Type u) [AddCommGroup N] [TopologicalSpace N] [DiscreteTopology N] [DistribMulAction G N] [ContinuousSMul G N] (f : M →+[G] N) (x : H2 G M) : (CategoryTheory.ConcreteCategory.hom (ContinuousCohomology.coeffMap (ofDiscreteModuleMap f.toAddMonoidHom.toIntLinearMap ⋯) 2)) ((explicitH2AddEquivContinuousCohomology G M) x) = (explicitH2AddEquivContinuousCohomology G N) ((explicitCoeff2 G M f ⋯) x)

The degree-two comparison carries the explicit coefficient map to the canonical coefficient map TauCeti.ContinuousCohomology.coeffMap attached to the same equivariant homomorphism. This naturality equation transports coefficient maps between the two models.

The comparisons as isomorphisms of topological modules

Compactness of G enters only here, and only through TauCeti.discreteTopology_continuousCohomology: it makes the canonical side discrete, so that the additive equivalences above are automatically homeomorphisms onto it. Local compactness, which degree two needs, follows from compactness for a topological group.

noncomputable def TauCeti.ContCohomology.explicitH1IsoContinuousCohomology (G M : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] [ContinuousSMul G M] [CompactSpace G] : ↧(DiscreteH1 G M) ≅ continuousCohomology 1 (ofDiscreteModule ℤ G M)

The degree-one comparison in TopModuleCat ℤ. The source is the discrete carrier TauCeti.ContCohomology.DiscreteH1, and not H¹ with the quotient topology inherited from the pointwise topology on G → M, which is not discrete in general.

The canonical side is the image of M under the coefficient dictionary and not an arbitrary object of TopRep ℤ G: a general object need not be discrete, and the explicit complex is not a description of its cohomology.

Equations

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

theorem TauCeti.ContCohomology.explicitH1IsoContinuousCohomology_hom_apply (G M : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] [ContinuousSMul G M] [CompactSpace G] (x : DiscreteH1 G M) : (CategoryTheory.ConcreteCategory.hom (explicitH1IsoContinuousCohomology G M).hom) x = (explicitH1AddEquivContinuousCohomology G M) ((discreteH1Equiv G M) x)

The degree-one isomorphism of topological modules is the additive comparison, read on the discrete carrier.

@[simp]

theorem TauCeti.ContCohomology.explicitH1IsoContinuousCohomology_inv_apply (G M : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] [ContinuousSMul G M] [CompactSpace G] (c : ↑(ContinuousCohomology.cocycles (ofDiscreteModule ℤ G M) 1).toModuleCat) : (CategoryTheory.ConcreteCategory.hom (explicitH1IsoContinuousCohomology G M).inv) ((CategoryTheory.ConcreteCategory.hom (HomologicalComplex.homologyπ (ofDiscreteModule ℤ G M).homogeneousCochains 1)) c) = (discreteH1Equiv G M).symm ↑((cocycleEquiv1 G M).symm c)

The inverse degree-one isomorphism sends a canonical homology class to the discrete carrier of the corresponding explicit cocycle class.

Transport in degree one

theorem TauCeti.ContCohomology.explicitIso_map (G M : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] [ContinuousSMul G M] [CompactSpace G] (H N : Type u) [Group H] [TopologicalSpace H] [IsTopologicalGroup H] [CompactSpace 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 : DiscreteH1 G M) : (CategoryTheory.ConcreteCategory.hom (ContinuousCohomology.map φ (ofDiscreteModulePair (↑φ) f.toIntLinearMap ⋯) 1)) ((CategoryTheory.ConcreteCategory.hom (explicitH1IsoContinuousCohomology G M).hom) x) = (CategoryTheory.ConcreteCategory.hom (explicitH1IsoContinuousCohomology H N).hom) ((discreteH1Equiv H N).symm ((explicitMap1 G M H N φ f ⋯ hf) ((discreteH1Equiv G M) x)))

Transport of compatible-pair pullback in degree one. The isomorphisms of topological modules carry the explicit pullback to Mathlib's canonical map. Compactness is needed only to equip the canonical cohomology objects with their discrete topology.

theorem TauCeti.ContCohomology.explicitIso_res (G M : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] [ContinuousSMul G M] [CompactSpace G] (S : Subgroup G) [CompactSpace ↥S] (x : DiscreteH1 G M) : (CategoryTheory.ConcreteCategory.hom (ContinuousCohomology.res S (ofDiscreteModule ℤ G M) 1)) ((CategoryTheory.ConcreteCategory.hom (explicitH1IsoContinuousCohomology G M).hom) x) = (CategoryTheory.ConcreteCategory.hom (explicitH1IsoContinuousCohomology (↥S) M).hom) ((discreteH1Equiv (↥S) M).symm ((explicitRes1 G M S) ((discreteH1Equiv G M) x)))

Transport of restriction in degree one. The comparison carries restriction of explicit cohomology classes to canonical restriction along the subgroup inclusion.

theorem TauCeti.ContCohomology.explicitIso_coeffMap (G M : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] [ContinuousSMul G M] [CompactSpace G] (N : Type u) [AddCommGroup N] [TopologicalSpace N] [DiscreteTopology N] [DistribMulAction G N] [ContinuousSMul G N] (f : M →+[G] N) (x : DiscreteH1 G M) : (CategoryTheory.ConcreteCategory.hom (ContinuousCohomology.coeffMap (ofDiscreteModuleMap f.toAddMonoidHom.toIntLinearMap ⋯) 1)) ((CategoryTheory.ConcreteCategory.hom (explicitH1IsoContinuousCohomology G M).hom) x) = (CategoryTheory.ConcreteCategory.hom (explicitH1IsoContinuousCohomology G N).hom) ((discreteH1Equiv G N).symm ((explicitCoeff1 G M f ⋯) ((discreteH1Equiv G M) x)))

Transport of coefficient maps in degree one. The comparison carries the explicit coefficient map to the canonical map induced by the same equivariant homomorphism.

noncomputable def TauCeti.ContCohomology.explicitH2IsoContinuousCohomology (G M : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] [ContinuousSMul G M] [CompactSpace G] : ↧(DiscreteH2 G M) ≅ continuousCohomology 2 (ofDiscreteModule ℤ G M)

The degree-two comparison in TopModuleCat ℤ.

Equations

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

theorem TauCeti.ContCohomology.explicitH2IsoContinuousCohomology_hom_apply (G M : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] [ContinuousSMul G M] [CompactSpace G] (x : DiscreteH2 G M) : (CategoryTheory.ConcreteCategory.hom (explicitH2IsoContinuousCohomology G M).hom) x = (explicitH2AddEquivContinuousCohomology G M) ((discreteH2Equiv G M) x)

The degree-two isomorphism of topological modules is the additive comparison, read on the discrete carrier.

@[simp]

theorem TauCeti.ContCohomology.explicitH2IsoContinuousCohomology_inv_apply (G M : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] [ContinuousSMul G M] [CompactSpace G] (c : ↑(ContinuousCohomology.cocycles (ofDiscreteModule ℤ G M) 2).toModuleCat) : (CategoryTheory.ConcreteCategory.hom (explicitH2IsoContinuousCohomology G M).inv) ((CategoryTheory.ConcreteCategory.hom (HomologicalComplex.homologyπ (ofDiscreteModule ℤ G M).homogeneousCochains 2)) c) = (discreteH2Equiv G M).symm ↑((cocycleEquiv2 G M).symm c)

The inverse degree-two isomorphism sends a canonical homology class to the discrete carrier of the corresponding explicit cocycle class.

Discrete smooth representations over any scalars

The continuous cohomology of a discrete X : TopRep k G is that of its carrier X.V as a discrete ℤ-module (TauCeti.ContCohomology.ofDiscreteModuleRestrictScalarsIntEquiv), so the ℤ-comparisons above identify the explicit H¹ and H² of X.V with continuousCohomology 1 X and continuousCohomology 2 X.

noncomputable def TopRep.explicitH1AddEquivContinuousCohomologyOfDiscrete {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {k : Type u_1} [Ring k] [TopologicalSpace k] (X : TopRep k G) [DiscreteTopology ↑X] [ContinuousSMul G ↑X] : TauCeti.ContCohomology.H1 G ↑X ≃+ ↑(continuousCohomology 1 X).toModuleCat

The explicit H¹ of the carrier of a discrete smooth representation X over any scalars, with the action read off from X, is Mathlib's continuousCohomology 1 X.

Equations

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

theorem TopRep.explicitH1AddEquivContinuousCohomologyOfDiscrete_apply {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {k : Type u_1} [Ring k] [TopologicalSpace k] (X : TopRep k G) [DiscreteTopology ↑X] [ContinuousSMul G ↑X] (x : TauCeti.ContCohomology.H1 G ↑X) : X.explicitH1AddEquivContinuousCohomologyOfDiscrete x = (TauCeti.ContCohomology.ofDiscreteModuleRestrictScalarsIntEquiv X 1) ((TauCeti.ContCohomology.explicitH1AddEquivContinuousCohomology G ↑X) x)

The degree-one comparison for a discrete X is the ℤ-comparison of its carrier followed by ofDiscreteModuleRestrictScalarsIntEquiv.

theorem TopRep.explicitH1AddEquivContinuousCohomologyOfDiscrete_map {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {k : Type u_1} [Ring k] [TopologicalSpace k] (X : TopRep k G) [DiscreteTopology ↑X] [ContinuousSMul G ↑X] {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] (Y : TopRep k H) [DiscreteTopology ↑Y] [ContinuousSMul H ↑Y] (φ : H →ₜ* G) (F : res (↑φ) X ⟶ Y) (f : ↑X →+ ↑Y) (hF : ∀ (m : ↑(res (↑φ) X)), (Hom.hom F) m = f m) (hf : ∀ (h : H) (m : ↑X), f (φ h • m) = h • f m) (x : TauCeti.ContCohomology.H1 G ↑X) : (CategoryTheory.ConcreteCategory.hom (ContinuousCohomology.map φ F 1)) (X.explicitH1AddEquivContinuousCohomologyOfDiscrete x) = Y.explicitH1AddEquivContinuousCohomologyOfDiscrete ((TauCeti.ContCohomology.explicitMap1 G (↑X) H (↑Y) φ f ⋯ hf) x)

The degree-one comparison for discrete representations is natural in compatible pairs: it carries the explicit pullback along φ and the underlying additive map f of a morphism F : res φ X ⟶ Y to Mathlib's ContinuousCohomology.map φ F.

noncomputable def TopRep.explicitH2AddEquivContinuousCohomologyOfDiscrete {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {k : Type u_1} [Ring k] [TopologicalSpace k] (X : TopRep k G) [DiscreteTopology ↑X] [ContinuousSMul G ↑X] [LocallyCompactSpace G] : TauCeti.ContCohomology.H2 G ↑X ≃+ ↑(continuousCohomology 2 X).toModuleCat

The explicit H² of the carrier of a discrete smooth representation X over any scalars, with the action read off from X, is Mathlib's continuousCohomology 2 X.

Equations

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

theorem TopRep.explicitH2AddEquivContinuousCohomologyOfDiscrete_apply {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {k : Type u_1} [Ring k] [TopologicalSpace k] (X : TopRep k G) [DiscreteTopology ↑X] [ContinuousSMul G ↑X] [LocallyCompactSpace G] (x : TauCeti.ContCohomology.H2 G ↑X) : X.explicitH2AddEquivContinuousCohomologyOfDiscrete x = (TauCeti.ContCohomology.ofDiscreteModuleRestrictScalarsIntEquiv X 2) ((TauCeti.ContCohomology.explicitH2AddEquivContinuousCohomology G ↑X) x)

The degree-two comparison for a discrete X is the ℤ-comparison of its carrier followed by ofDiscreteModuleRestrictScalarsIntEquiv.

theorem TauCeti.ContCohomology.iCycles_ofDiscreteModuleCocyclesRestrictScalarsIntIso_hom_two_apply {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {k : Type u_1} [Ring k] [TopologicalSpace k] (X : TopRep k G) [DiscreteTopology ↑X] (w : ↑(ContinuousCohomology.cocycles (ofDiscreteModule ℤ G ↑X) 2).toModuleCat) (g₀ g₁ g₂ : G) : ((↑((CategoryTheory.ConcreteCategory.hom (HomologicalComplex.iCycles X.homogeneousCochains 2)) ((CategoryTheory.ConcreteCategory.hom (ofDiscreteModuleCocyclesRestrictScalarsIntIso X 2).hom) w)) g₀) g₁) g₂ = ((↑((CategoryTheory.ConcreteCategory.hom (HomologicalComplex.iCycles (ofDiscreteModule ℤ G ↑X).homogeneousCochains 2)) w) g₀) g₁) g₂

In degree two, ofDiscreteModuleCocyclesRestrictScalarsIntIso does not change the values of a homogeneous cocycle.

theorem TopRep.explicitH2AddEquivContinuousCohomologyOfDiscrete_map {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {k : Type u_1} [Ring k] [TopologicalSpace k] (X : TopRep k G) [DiscreteTopology ↑X] [ContinuousSMul G ↑X] [LocallyCompactSpace G] {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] [LocallyCompactSpace H] (Y : TopRep k H) [DiscreteTopology ↑Y] [ContinuousSMul H ↑Y] (φ : H →ₜ* G) (F : res (↑φ) X ⟶ Y) (f : ↑X →+ ↑Y) (hF : ∀ (m : ↑(res (↑φ) X)), (Hom.hom F) m = f m) (hf : ∀ (h : H) (m : ↑X), f (φ h • m) = h • f m) (x : TauCeti.ContCohomology.H2 G ↑X) : (CategoryTheory.ConcreteCategory.hom (ContinuousCohomology.map φ F 2)) (X.explicitH2AddEquivContinuousCohomologyOfDiscrete x) = Y.explicitH2AddEquivContinuousCohomologyOfDiscrete ((TauCeti.ContCohomology.explicitMap2 G (↑X) H (↑Y) φ f ⋯ hf) x)

The degree-two comparison for discrete representations is natural in compatible pairs: it carries the explicit pullback along φ and the underlying additive map f of a morphism F : res φ X ⟶ Y to Mathlib's ContinuousCohomology.map φ F.