Degree zero of continuous cohomology, and compatible pairs

Mathlib computes one degree of continuous cohomology: ContinuousCohomology.zeroIso identifies H⁰_cont(G, X) with the invariants X^G. That identification is only usable once it is known to transport the maps, and this file supplies exactly that. For a continuous homomorphism φ : H →ₜ* G and a morphism f : TopRep.res φ X ⟶ Y of topological H-representations, the square

H⁰_cont(G, X) --map φ f 0--> H⁰_cont(H, Y)
     |                             |
  zeroIso X                     zeroIso Y
     v                             v
    X^G  ----invariantsResMap---->  Y^H

commutes (TauCeti.ContinuousCohomology.map_comp_zeroIso_hom), and the three named instances of ContinuousCohomology.map — coefficient maps, restriction and inflation — inherit it.

Two consequences are recorded because later layers use them rather than the square itself. First, H⁰_cont(G, -) and the invariants functor are naturally isomorphic (TauCeti.ContinuousCohomology.zeroIsoNatIso). Second, inflation is an isomorphism in degree zero (TauCeti.ContinuousCohomology.isIso_infl_zero): (X^N)^{G/N} and X^G are canonically isomorphic by explicit mutually inverse maps that preserve the underlying vector. Restriction is a monomorphism in degree zero (TauCeti.ContinuousCohomology.mono_res_zero) because X^G ⊆ X^S.

The route to the square is the explicit evaluation formula TauCeti.ContinuousCohomology.coe_zeroIso_hom_π: a 0-cocycle of the homogeneous complex is an invariant element of C(G, X), and zeroIso reads off its value at 1. Compatible-pair functoriality precomposes with φ, and φ 1 = 1, which is the whole content.

This implements the "Degree 0" milestone of Layer 1, "the canonical carrier and its functoriality", of the human-authored roadmap at TauCetiRoadmap/ProfiniteCohomology/README.md, together with the invariant-class constructor degreeZeroClass that the same layer names.

Main definitions

• TauCeti.ContinuousCohomology.degreeZeroClass: the degree-zero class of an invariant vector.
• TauCeti.ContinuousCohomology.degreeZeroCocycle: the constant 0-cocycle of an invariant vector, a representative of its degree-zero class (π_degreeZeroCocycle).
• TauCeti.ContinuousCohomology.zeroIsoNatIso: H⁰_cont(G, -) ≅ (-)^G as functors.

Main results

• TauCeti.ContinuousCohomology.map_comp_zeroIso_hom: compatible-pair functoriality commutes with zeroIso.
• TauCeti.ContinuousCohomology.coeffMap_comp_zeroIso_hom, TauCeti.ContinuousCohomology.res_comp_zeroIso_hom, TauCeti.ContinuousCohomology.infl_comp_zeroIso_hom: the same for the three named instances.
• TauCeti.ContinuousCohomology.degreeZeroClass_eq_π: the degree-zero class of an invariant vector is the class of any 0-cocycle with that value at 1.
• TauCeti.ContinuousCohomology.map_degreeZeroClass: compatible-pair functoriality on classes of invariant vectors.
• TauCeti.ContinuousCohomology.isIso_infl_zero, TauCeti.ContinuousCohomology.mono_res_zero: the degree-zero edge of inflation-restriction.

theorem TauCeti.ContinuousCohomology.coe_zeroIso_hom_π {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (X : TopRep R G) (σ : ↑(ContinuousCohomology.cocycles X 0).toModuleCat) : ↑((CategoryTheory.ConcreteCategory.hom (ContinuousCohomology.zeroIso X).hom) ((CategoryTheory.ConcreteCategory.hom (ContinuousCohomology.π X 0)) σ)) = ↑((CategoryTheory.ConcreteCategory.hom (HomologicalComplex.iCycles X.homogeneousCochains 0)) σ) 1

The evaluation formula for zeroIso. A homogeneous 0-cochain of X is a G-invariant element of C(G, X); zeroIso sends the class of a 0-cocycle to its value at 1. Every compatible-pair square below, including its coefficient, restriction, and inflation specializations, follows from this formula together with φ 1 = 1.

theorem TauCeti.ContinuousCohomology.map_comp_zeroIso_hom {R : Type u} [Ring R] [TopologicalSpace R] {G H : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [Group H] [TopologicalSpace H] [IsTopologicalGroup H] (φ : H →ₜ* G) {X : TopRep R G} {Y : TopRep R H} (f : TopRep.res (↑φ) X ⟶ Y) : CategoryTheory.CategoryStruct.comp (ContinuousCohomology.map φ f 0) (ContinuousCohomology.zeroIso Y).hom = CategoryTheory.CategoryStruct.comp (ContinuousCohomology.zeroIso X).hom (TopRep.invariantsResMap (↑φ) f)

Degree zero is compatible with compatible pairs. For a continuous homomorphism φ : H →ₜ* G and a morphism f : TopRep.res φ X ⟶ Y, the map ContinuousCohomology.map φ f 0 becomes, under ContinuousCohomology.zeroIso, the map X^G ⟶ Y^H induced by f. This is what makes Layer 3's low-degree comparisons checkable at n = 0.

theorem TauCeti.ContinuousCohomology.map_comp_zeroIso_hom_assoc {R : Type u} [Ring R] [TopologicalSpace R] {G H : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [Group H] [TopologicalSpace H] [IsTopologicalGroup H] (φ : H →ₜ* G) {X : TopRep R G} {Y : TopRep R H} (f : TopRep.res (↑φ) X ⟶ Y) {Z : TopModuleCat R} (h : ↧↥Y.ρ.invariants ⟶ Z) : CategoryTheory.CategoryStruct.comp (ContinuousCohomology.map φ f 0) (CategoryTheory.CategoryStruct.comp (ContinuousCohomology.zeroIso Y).hom h) = CategoryTheory.CategoryStruct.comp (ContinuousCohomology.zeroIso X).hom (CategoryTheory.CategoryStruct.comp (TopRep.invariantsResMap (↑φ) f) h)

Degree zero is compatible with compatible pairs. For a continuous homomorphism φ : H →ₜ* G and a morphism f : TopRep.res φ X ⟶ Y, the map ContinuousCohomology.map φ f 0 becomes, under ContinuousCohomology.zeroIso, the map X^G ⟶ Y^H induced by f. This is what makes Layer 3's low-degree comparisons checkable at n = 0.

theorem TauCeti.ContinuousCohomology.coeffMap_comp_zeroIso_hom {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {X Y : TopRep R G} (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp (coeffMap f 0) (ContinuousCohomology.zeroIso Y).hom = CategoryTheory.CategoryStruct.comp (ContinuousCohomology.zeroIso X).hom ((TopRep.invariantsFunctor R G).map f)

Coefficient maps in degree zero are the maps induced on invariants.

theorem TauCeti.ContinuousCohomology.coeffMap_comp_zeroIso_hom_assoc {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {X Y : TopRep R G} (f : X ⟶ Y) {Z : TopModuleCat R} (h : ↧↥Y.ρ.invariants ⟶ Z) : CategoryTheory.CategoryStruct.comp (coeffMap f 0) (CategoryTheory.CategoryStruct.comp (ContinuousCohomology.zeroIso Y).hom h) = CategoryTheory.CategoryStruct.comp (ContinuousCohomology.zeroIso X).hom (CategoryTheory.CategoryStruct.comp (TopModuleCat.ofHom (TopRep.Hom.hom f).mapInvariants) h)

Coefficient maps in degree zero are the maps induced on invariants.

noncomputable def TauCeti.ContinuousCohomology.zeroIsoNatIso (R : Type u) [Ring R] [TopologicalSpace R] (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : continuousCohomologyFunctor R G 0 ≅ TopRep.invariantsFunctor R G

Degree-zero continuous cohomology is the invariants functor. The functorial form of ContinuousCohomology.zeroIso; its naturality is coeffMap_comp_zeroIso_hom.

Equations

• TauCeti.ContinuousCohomology.zeroIsoNatIso R G = CategoryTheory.NatIso.ofComponents (fun (X : TopRep R G) => ContinuousCohomology.zeroIso X) ⋯

@[simp]

theorem TauCeti.ContinuousCohomology.zeroIsoNatIso_hom_app {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (X : TopRep R G) : (zeroIsoNatIso R G).hom.app X = (ContinuousCohomology.zeroIso X).hom

The components of zeroIsoNatIso are Mathlib's ContinuousCohomology.zeroIso.

@[simp]

theorem TauCeti.ContinuousCohomology.zeroIsoNatIso_inv_app {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (X : TopRep R G) : (zeroIsoNatIso R G).inv.app X = (ContinuousCohomology.zeroIso X).inv

The inverse components of zeroIsoNatIso are the inverses of Mathlib's ContinuousCohomology.zeroIso.

theorem TauCeti.ContinuousCohomology.res_comp_zeroIso_hom {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (S : Subgroup G) (X : TopRep R G) : CategoryTheory.CategoryStruct.comp (res S X 0) (ContinuousCohomology.zeroIso (TopRep.res S.subtype X)).hom = CategoryTheory.CategoryStruct.comp (ContinuousCohomology.zeroIso X).hom (TopRep.invariantsResMap S.subtype (CategoryTheory.CategoryStruct.id (TopRep.res S.subtype X)))

Restriction in degree zero is the inclusion X^G ⊆ X^S of invariants.

theorem TauCeti.ContinuousCohomology.res_comp_zeroIso_hom_assoc {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (S : Subgroup G) (X : TopRep R G) {Z : TopModuleCat R} (h : ↧↥(X.ρ.restrict S.subtype).invariants ⟶ Z) : CategoryTheory.CategoryStruct.comp (res S X 0) (CategoryTheory.CategoryStruct.comp (ContinuousCohomology.zeroIso (TopRep.res S.subtype X)).hom h) = CategoryTheory.CategoryStruct.comp (ContinuousCohomology.zeroIso X).hom (CategoryTheory.CategoryStruct.comp (TopRep.invariantsResMap S.subtype (CategoryTheory.CategoryStruct.id (TopRep.res S.subtype X))) h)

Restriction in degree zero is the inclusion X^G ⊆ X^S of invariants.

theorem TauCeti.ContinuousCohomology.infl_comp_zeroIso_hom {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (N : Subgroup G) [N.Normal] (X : TopRep R G) : CategoryTheory.CategoryStruct.comp (infl N X 0) (ContinuousCohomology.zeroIso X).hom = CategoryTheory.CategoryStruct.comp (ContinuousCohomology.zeroIso (X.quotientToInvariants N)).hom (TopRep.invariantsResMap (QuotientGroup.mk' N) (X.quotientToInvariantsι N))

Inflation in degree zero is the inclusion (X^N)^{G/N} ⊆ X^G of invariants.

theorem TauCeti.ContinuousCohomology.infl_comp_zeroIso_hom_assoc {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (N : Subgroup G) [N.Normal] (X : TopRep R G) {Z : TopModuleCat R} (h : ↧↥X.ρ.invariants ⟶ Z) : CategoryTheory.CategoryStruct.comp (infl N X 0) (CategoryTheory.CategoryStruct.comp (ContinuousCohomology.zeroIso X).hom h) = CategoryTheory.CategoryStruct.comp (ContinuousCohomology.zeroIso (X.quotientToInvariants N)).hom (CategoryTheory.CategoryStruct.comp (TopRep.invariantsResMap (QuotientGroup.mk' N) (X.quotientToInvariantsι N)) h)

Inflation in degree zero is the inclusion (X^N)^{G/N} ⊆ X^G of invariants.

theorem TauCeti.ContinuousCohomology.zeroIso_inv_comp_map {R : Type u} [Ring R] [TopologicalSpace R] {G H : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [Group H] [TopologicalSpace H] [IsTopologicalGroup H] {X : TopRep R G} {Y : TopRep R H} (φ : H →ₜ* G) (f : TopRep.res (↑φ) X ⟶ Y) : CategoryTheory.CategoryStruct.comp (ContinuousCohomology.zeroIso X).inv (ContinuousCohomology.map φ f 0) = CategoryTheory.CategoryStruct.comp (TopRep.invariantsResMap (↑φ) f) (ContinuousCohomology.zeroIso Y).inv

The inverse form of map_comp_zeroIso_hom, which is what acts on classes.

theorem TauCeti.ContinuousCohomology.zeroIso_inv_comp_map_assoc {R : Type u} [Ring R] [TopologicalSpace R] {G H : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [Group H] [TopologicalSpace H] [IsTopologicalGroup H] {X : TopRep R G} {Y : TopRep R H} (φ : H →ₜ* G) (f : TopRep.res (↑φ) X ⟶ Y) {Z : TopModuleCat R} (h : continuousCohomology 0 Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (ContinuousCohomology.zeroIso X).inv (CategoryTheory.CategoryStruct.comp (ContinuousCohomology.map φ f 0) h) = CategoryTheory.CategoryStruct.comp (TopRep.invariantsResMap (↑φ) f) (CategoryTheory.CategoryStruct.comp (ContinuousCohomology.zeroIso Y).inv h)

The inverse form of map_comp_zeroIso_hom, which is what acts on classes.

noncomputable def TauCeti.ContinuousCohomology.degreeZeroClass {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (X : TopRep R G) (u : ↑X) (hu : ∀ (g : G), (X.ρ g) u = u) : ↑(continuousCohomology 0 X).toModuleCat

The degree-zero class of an invariant vector. Degree zero is the invariants, so an invariant element of X has a continuous cohomology class; this is zeroIso read backwards on elements.

Equations

• TauCeti.ContinuousCohomology.degreeZeroClass X u hu = (CategoryTheory.ConcreteCategory.hom (ContinuousCohomology.zeroIso X).inv) ⟨u, ⋯⟩

@[simp]

theorem TauCeti.ContinuousCohomology.coe_zeroIso_hom_degreeZeroClass {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {X : TopRep R G} (u : ↑X) (hu : ∀ (g : G), (X.ρ g) u = u) : ↑((CategoryTheory.ConcreteCategory.hom (ContinuousCohomology.zeroIso X).hom) (degreeZeroClass X u hu)) = u

zeroIso recovers the invariant vector a degree-zero class was built from.

theorem TauCeti.ContinuousCohomology.degreeZeroClass_eq_π {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {X : TopRep R G} (σ : ↑(ContinuousCohomology.cocycles X 0).toModuleCat) (u : ↑X) (hu : ∀ (g : G), (X.ρ g) u = u) (h : ↑((CategoryTheory.ConcreteCategory.hom (HomologicalComplex.iCycles X.homogeneousCochains 0)) σ) 1 = u) : degreeZeroClass X u hu = (CategoryTheory.ConcreteCategory.hom (ContinuousCohomology.π X 0)) σ

The degree-zero class of an invariant vector is the class of any 0-cocycle whose value at 1 is that vector. A homogeneous 0-cocycle is determined by its value at 1, so this identifies degreeZeroClass with the class map π X 0 on cocycles.

noncomputable def TauCeti.ContinuousCohomology.degreeZeroCocycle {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (X : TopRep R G) (u : ↑X) (hu : ∀ (g : G), (X.ρ g) u = u) : ↑(ContinuousCohomology.cocycles X 0).toModuleCat

The constant 0-cocycle of an invariant vector. The homogeneous 0-cochain g ↦ u is the image of u under the first differential TopRep.d X 0 of the resolution; it is invariant because u is, and a cocycle because the resolution is a complex. Its class is degreeZeroClass X u hu (π_degreeZeroCocycle).

Equations

• TauCeti.ContinuousCohomology.degreeZeroCocycle X u hu = (CategoryTheory.ConcreteCategory.hom (ContinuousCohomology.cocycles₀Iso X).inv) ((ContinuousCohomology.d₀kerIso X).symm ⟨u, ⋯⟩)

theorem TauCeti.ContinuousCohomology.coe_iCycles_degreeZeroCocycle {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {X : TopRep R G} (u : ↑X) (hu : ∀ (g : G), (X.ρ g) u = u) : ↑((CategoryTheory.ConcreteCategory.hom (HomologicalComplex.iCycles X.homogeneousCochains 0)) (degreeZeroCocycle X u hu)) = (TopRep.Hom.hom (X.d 0)) u

The constant 0-cocycle of u is, as a homogeneous cochain, the constant map g ↦ u.

@[simp]

theorem TauCeti.ContinuousCohomology.π_degreeZeroCocycle {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {X : TopRep R G} (u : ↑X) (hu : ∀ (g : G), (X.ρ g) u = u) : (CategoryTheory.ConcreteCategory.hom (ContinuousCohomology.π X 0)) (degreeZeroCocycle X u hu) = degreeZeroClass X u hu

The class of the constant 0-cocycle of an invariant vector is its degree-zero class.

theorem TauCeti.ContinuousCohomology.exists_degreeZeroClass_eq {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {X : TopRep R G} (x : ↑(continuousCohomology 0 X).toModuleCat) : ∃ (u : ↑X) (hu : ∀ (g : G), (X.ρ g) u = u), degreeZeroClass X u hu = x

Every degree-zero class is the class of an invariant vector.

@[simp]

theorem TauCeti.ContinuousCohomology.map_degreeZeroClass {R : Type u} [Ring R] [TopologicalSpace R] {G H : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [Group H] [TopologicalSpace H] [IsTopologicalGroup H] {X : TopRep R G} {Y : TopRep R H} (φ : H →ₜ* G) (f : TopRep.res (↑φ) X ⟶ Y) (u : ↑X) (hu : ∀ (g : G), (X.ρ g) u = u) : (CategoryTheory.ConcreteCategory.hom (ContinuousCohomology.map φ f 0)) (degreeZeroClass X u hu) = degreeZeroClass Y ((TopRep.Hom.hom f) u) ⋯

Compatible-pair functoriality on the class of an invariant vector.

theorem TauCeti.ContinuousCohomology.mono_res_zero {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (S : Subgroup G) (X : TopRep R G) : CategoryTheory.Mono (res S X 0)

Restriction is a monomorphism in degree zero. This is the degree-zero left edge of the inflation-restriction sequence: X^G ⊆ X^S.

theorem TauCeti.ContinuousCohomology.isIso_infl_zero {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (N : Subgroup G) [N.Normal] (X : TopRep R G) : CategoryTheory.IsIso (infl N X 0)

Inflation is an isomorphism in degree zero: H⁰(G ⧸ N, X^N), (X^N)^{G/N}, and X^G are canonically isomorphic, with the coefficient comparison preserving the underlying vector. This is the degree-zero edge of the inflation-restriction sequence.