Transport along equalities of degrees in the homogeneous cochain complex

Mathlib's HomologicalComplex.XIsoOfEq transports an element of a complex along an equality of degrees. For the coinduced resolution TopRep.resolution X of a topological representation and for its complex of homogeneous cochains TopRep.homogeneousCochains X, this file records how such a transport is read: evaluating a transported element of the resolution at a point of the group is the transported value one degree down, and the transport of a homogeneous cochain is, on the underlying element of the resolution, the transport one degree up. Both rules are used wherever two constructions land in degrees that are equal but not definitionally so, as for the total degree m + n of a cup product built by recursion on m. On continuous cohomology the transport is degreeCast, the isomorphism continuousCohomology n X ≅ continuousCohomology k X along an equality n = k, and a cocycle that is the transport of another has the transported class (π_eq_degreeCast_π).

Main definitions

• TauCeti.ContinuousCohomology.degreeCast: transport of continuous cohomology along an equality of degrees.
• TauCeti.ContinuousCohomology.cocyclesDegreeCast: transport of cocycles along an equality of degrees.

theorem TauCeti.ContinuousCohomology.resolution_XIsoOfEq_hom_apply_apply {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {X : TopRep R G} {i j : ℕ} (h : i + 1 = j + 1) (F : ↑(X.resolutionX (i + 1))) (g : G) : ((TopRep.Hom.hom (HomologicalComplex.XIsoOfEq X.resolution h).hom) F) g = (TopRep.Hom.hom (HomologicalComplex.XIsoOfEq X.resolution ⋯).hom) (F g)

Evaluating a transported element of the resolution at a point of G is the transported value, one degree down.

theorem TauCeti.ContinuousCohomology.coe_homogeneousCochains_XIsoOfEq_hom_apply {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {X : TopRep R G} {p q : ℕ} (h : p = q) (v : ↑(X.homogeneousCochains.X p).toModuleCat) : ↑((CategoryTheory.ConcreteCategory.hom (HomologicalComplex.XIsoOfEq X.homogeneousCochains h).hom) v) = (TopRep.Hom.hom (HomologicalComplex.XIsoOfEq X.resolution ⋯).hom) ↑v

Transport along an equality of degrees in the complex of homogeneous cochains is transport along the corresponding equality in the resolution, one degree up.

noncomputable def TauCeti.ContinuousCohomology.degreeCast {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (X : TopRep R G) {n k : ℕ} (h : n = k) : continuousCohomology n X ≅ continuousCohomology k X

Transport of continuous cohomology along an equality of degrees: the isomorphism continuousCohomology n X ≅ continuousCohomology k X induced by n = k. It plays for continuous cohomology the role that HomologicalComplex.XIsoOfEq plays for the objects of a complex, and is needed wherever two constructions land in degrees that are equal but not definitionally so, as 0 + n and n.

Equations

• TauCeti.ContinuousCohomology.degreeCast X h = CategoryTheory.eqToIso ⋯

@[simp]

theorem TauCeti.ContinuousCohomology.degreeCast_rfl {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {X : TopRep R G} (n : ℕ) : degreeCast X ⋯ = CategoryTheory.Iso.refl (continuousCohomology n X)

Transport along n = n is the identity.

@[simp]

theorem TauCeti.ContinuousCohomology.degreeCast_symm {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {X : TopRep R G} {n k : ℕ} (h : n = k) : (degreeCast X h).symm = degreeCast X ⋯

The inverse of a transport is the transport along the reversed equality.

theorem TauCeti.ContinuousCohomology.degreeCast_hom_apply_heq {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {X : TopRep R G} {n k : ℕ} (h : n = k) (x : ↑(continuousCohomology n X).toModuleCat) : (CategoryTheory.ConcreteCategory.hom (degreeCast X h).hom) x ≍ x

Transport along an equality of degrees does not change a class, read as an element of a possibly different type.

@[simp]

theorem TauCeti.ContinuousCohomology.degreeCast_hom_comp_degreeCast_hom {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {X : TopRep R G} {n k l : ℕ} (h : n = k) (h' : k = l) : CategoryTheory.CategoryStruct.comp (degreeCast X h).hom (degreeCast X h').hom = (degreeCast X ⋯).hom

Two successive transports are the transport along the composite equality.

@[simp]

theorem TauCeti.ContinuousCohomology.degreeCast_hom_comp_degreeCast_hom_assoc {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {X : TopRep R G} {n k l : ℕ} (h : n = k) (h' : k = l) {Z : TopModuleCat R} (h✝ : continuousCohomology l X ⟶ Z) : CategoryTheory.CategoryStruct.comp (degreeCast X h).hom (CategoryTheory.CategoryStruct.comp (degreeCast X h').hom h✝) = CategoryTheory.CategoryStruct.comp (degreeCast X ⋯).hom h✝

Two successive transports are the transport along the composite equality.

noncomputable def TauCeti.ContinuousCohomology.cocyclesDegreeCast {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {X : TopRep R G} {n k : ℕ} (h : n = k) : ↑(ContinuousCohomology.cocycles X n).toModuleCat ≃ₗ[R] ↑(ContinuousCohomology.cocycles X k).toModuleCat

Transport of cocycles along an equality of degrees.

Equations

• TauCeti.ContinuousCohomology.cocyclesDegreeCast h = h ▸ LinearEquiv.refl R ↑(ContinuousCohomology.cocycles X n).toModuleCat

theorem TauCeti.ContinuousCohomology.iCycles_cocyclesDegreeCast {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {X : TopRep R G} {n k : ℕ} (h : n = k) (z : ↑(ContinuousCohomology.cocycles X n).toModuleCat) : (CategoryTheory.ConcreteCategory.hom (HomologicalComplex.iCycles X.homogeneousCochains k)) ((cocyclesDegreeCast h) z) = (CategoryTheory.ConcreteCategory.hom (HomologicalComplex.XIsoOfEq X.homogeneousCochains h).hom) ((CategoryTheory.ConcreteCategory.hom (HomologicalComplex.iCycles X.homogeneousCochains n)) z)

The underlying cochain of a transported cocycle is the corresponding transport in the homogeneous cochain complex.

theorem TauCeti.ContinuousCohomology.π_eq_degreeCast_π {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {X : TopRep R G} {n k : ℕ} (h : n = k) (z : ↑(ContinuousCohomology.cocycles X n).toModuleCat) (z' : ↑(ContinuousCohomology.cocycles X k).toModuleCat) (hz : (CategoryTheory.ConcreteCategory.hom (HomologicalComplex.iCycles X.homogeneousCochains k)) z' = (CategoryTheory.ConcreteCategory.hom (HomologicalComplex.XIsoOfEq X.homogeneousCochains h).hom) ((CategoryTheory.ConcreteCategory.hom (HomologicalComplex.iCycles X.homogeneousCochains n)) z)) : (CategoryTheory.ConcreteCategory.hom (ContinuousCohomology.π X k)) z' = (CategoryTheory.ConcreteCategory.hom (degreeCast X h).hom) ((CategoryTheory.ConcreteCategory.hom (ContinuousCohomology.π X n)) z)

Transport of a class along an equality of degrees. If the cocycle z' of degree k is, as a homogeneous cochain, the transport of the cocycle z of degree n along n = k, then the class of z' is the transport of the class of z.

@[simp]

theorem TauCeti.ContinuousCohomology.π_cocyclesDegreeCast {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {X : TopRep R G} {n k : ℕ} (h : n = k) (z : ↑(ContinuousCohomology.cocycles X n).toModuleCat) : (CategoryTheory.ConcreteCategory.hom (ContinuousCohomology.π X k)) ((cocyclesDegreeCast h) z) = (CategoryTheory.ConcreteCategory.hom (degreeCast X h).hom) ((CategoryTheory.ConcreteCategory.hom (ContinuousCohomology.π X n)) z)

The class of a transported cocycle is the transport of its class.