Functoriality of de Rham cohomology

A smooth map pulls smooth forms back and commutes with the exterior derivative. Consequently it induces a contravariant map on the de Rham complex and on de Rham cohomology. The induced map sends the class of a closed form to the class of its pullback, preserves identity maps, and reverses composition. In particular a diffeomorphism induces a linear equivalence on de Rham cohomology, TauCeti.deRhamCohomology.equivOfDiffeomorph.

Pullback also defines a cochain map of de Rham complexes, TauCeti.deRhamComplex.map, which induces the map on cohomology (TauCeti.deRhamComplex.homologyMap_map). It is stated for manifolds whose model vector spaces share one universe and whose underlying types share another, so that their de Rham complexes live in the same category of complexes of modules.

References

• John M. Lee, Introduction to Smooth Manifolds, 2nd ed., Chapter 17.

noncomputable def TauCeti.closedForms.mpullback {E : Type u_1} {H : Type u_2} {E' : Type u_3} {H' : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [NormedAddCommGroup E'] [NormedSpace ℝ E'] [TopologicalSpace H'] {I : ModelWithCorners ℝ E H} {I' : ModelWithCorners ℝ E' H'} {M : Type u_7} {M' : Type u_8} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 2 M] [TopologicalSpace M'] [ChartedSpace H' M'] [IsManifold I' 2 M'] (f : M → M') (hf : ContMDiff I I' (↑⊤) f) (k : ℕ) : ↥(closedForms I' M' k) →ₗ[ℝ] ↥(closedForms I M k)

Pullback of closed smooth forms along a smooth map.

@[simp]

theorem TauCeti.closedForms.coe_mpullback {E : Type u_1} {H : Type u_2} {E' : Type u_3} {H' : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [NormedAddCommGroup E'] [NormedSpace ℝ E'] [TopologicalSpace H'] {I : ModelWithCorners ℝ E H} {I' : ModelWithCorners ℝ E' H'} {M : Type u_7} {M' : Type u_8} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 2 M] [TopologicalSpace M'] [ChartedSpace H' M'] [IsManifold I' 2 M'] (f : M → M') (hf : ContMDiff I I' (↑⊤) f) (k : ℕ) (φ : ↥(closedForms I' M' k)) : ↑((mpullback f hf k) φ) = (SmoothForm.mpullback f hf) ↑φ

The underlying smooth form of a pullback of a closed form is the usual smooth pullback.

@[simp]

theorem TauCeti.closedForms.mpullback_id {E : Type u_1} {H : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_7} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 2 M] (k : ℕ) : mpullback id ⋯ k = LinearMap.id

Pullback of closed forms by the identity is the identity linear map.

theorem TauCeti.closedForms.mpullback_comp {E : Type u_1} {H : Type u_2} {E' : Type u_3} {H' : Type u_4} {E'' : Type u_5} {H'' : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [NormedAddCommGroup E'] [NormedSpace ℝ E'] [TopologicalSpace H'] [NormedAddCommGroup E''] [NormedSpace ℝ E''] [TopologicalSpace H''] {I : ModelWithCorners ℝ E H} {I' : ModelWithCorners ℝ E' H'} {I'' : ModelWithCorners ℝ E'' H''} {M : Type u_7} {M' : Type u_8} {M'' : Type u_9} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 2 M] [TopologicalSpace M'] [ChartedSpace H' M'] [IsManifold I' 2 M'] [TopologicalSpace M''] [ChartedSpace H'' M''] [IsManifold I'' 2 M''] (f : M → M') (g : M' → M'') (hf : ContMDiff I I' (↑⊤) f) (hg : ContMDiff I' I'' (↑⊤) g) (k : ℕ) : mpullback (g ∘ f) ⋯ k = mpullback f hf k ∘ₗ mpullback g hg k

Pullback of closed forms reverses composition.

theorem TauCeti.closedForms.mpullback_mem_exactForms {E : Type u_1} {H : Type u_2} {E' : Type u_3} {H' : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [NormedAddCommGroup E'] [NormedSpace ℝ E'] [TopologicalSpace H'] {I : ModelWithCorners ℝ E H} {I' : ModelWithCorners ℝ E' H'} {M : Type u_7} {M' : Type u_8} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 2 M] [TopologicalSpace M'] [ChartedSpace H' M'] [IsManifold I' 2 M'] (f : M → M') (hf : ContMDiff I I' (↑⊤) f) (k : ℕ) (φ : ↥(closedForms I' M' k)) (hφ : ↑φ ∈ exactForms I' M' k) : ↑((mpullback f hf k) φ) ∈ exactForms I M k

Pullback preserves exact forms.

noncomputable def TauCeti.deRhamCohomology.map {E : Type u_1} {H : Type u_2} {E' : Type u_3} {H' : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [NormedAddCommGroup E'] [NormedSpace ℝ E'] [TopologicalSpace H'] {I : ModelWithCorners ℝ E H} {I' : ModelWithCorners ℝ E' H'} {M : Type u_7} {M' : Type u_8} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 2 M] [TopologicalSpace M'] [ChartedSpace H' M'] [IsManifold I' 2 M'] (f : M → M') (hf : ContMDiff I I' (↑⊤) f) (k : ℕ) : deRhamCohomology I' M' k →ₗ[ℝ] deRhamCohomology I M k

The contravariant map on de Rham cohomology induced by a smooth map.

@[simp]

theorem TauCeti.deRhamCohomology.map_mk {E : Type u_1} {H : Type u_2} {E' : Type u_3} {H' : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [NormedAddCommGroup E'] [NormedSpace ℝ E'] [TopologicalSpace H'] {I : ModelWithCorners ℝ E H} {I' : ModelWithCorners ℝ E' H'} {M : Type u_7} {M' : Type u_8} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 2 M] [TopologicalSpace M'] [ChartedSpace H' M'] [IsManifold I' 2 M'] (f : M → M') (hf : ContMDiff I I' (↑⊤) f) (k : ℕ) (φ : ↥(closedForms I' M' k)) : (map f hf k) ((mk I' k) φ) = (mk I k) ((closedForms.mpullback f hf k) φ)

The induced map sends the class of a closed form to the class of its pullback.

@[simp]

theorem TauCeti.deRhamCohomology.map_id {E : Type u_1} {H : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_7} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 2 M] (k : ℕ) : map id ⋯ k = LinearMap.id

The map on de Rham cohomology induced by the identity is the identity.

theorem TauCeti.deRhamCohomology.map_comp {E : Type u_1} {H : Type u_2} {E' : Type u_3} {H' : Type u_4} {E'' : Type u_5} {H'' : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [NormedAddCommGroup E'] [NormedSpace ℝ E'] [TopologicalSpace H'] [NormedAddCommGroup E''] [NormedSpace ℝ E''] [TopologicalSpace H''] {I : ModelWithCorners ℝ E H} {I' : ModelWithCorners ℝ E' H'} {I'' : ModelWithCorners ℝ E'' H''} {M : Type u_7} {M' : Type u_8} {M'' : Type u_9} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 2 M] [TopologicalSpace M'] [ChartedSpace H' M'] [IsManifold I' 2 M'] [TopologicalSpace M''] [ChartedSpace H'' M''] [IsManifold I'' 2 M''] (f : M → M') (g : M' → M'') (hf : ContMDiff I I' (↑⊤) f) (hg : ContMDiff I' I'' (↑⊤) g) (k : ℕ) : map (g ∘ f) ⋯ k = map f hf k ∘ₗ map g hg k

Pullback on de Rham cohomology reverses composition of smooth maps.

noncomputable def TauCeti.deRhamCohomology.equivOfDiffeomorph {E : Type u_1} {H : Type u_2} {E' : Type u_3} {H' : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [NormedAddCommGroup E'] [NormedSpace ℝ E'] [TopologicalSpace H'] {I : ModelWithCorners ℝ E H} {I' : ModelWithCorners ℝ E' H'} {M : Type u_7} {M' : Type u_8} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 2 M] [TopologicalSpace M'] [ChartedSpace H' M'] [IsManifold I' 2 M'] (Φ : Diffeomorph I I' M M' ↑⊤) (k : ℕ) : deRhamCohomology I' M' k ≃ₗ[ℝ] deRhamCohomology I M k

A smooth diffeomorphism Φ : M ≃ M' induces a linear equivalence H^k(M') ≃ H^k(M) on de Rham cohomology: pullback along Φ, with inverse pullback along Φ.symm.

@[simp]

theorem TauCeti.deRhamCohomology.equivOfDiffeomorph_apply {E : Type u_1} {H : Type u_2} {E' : Type u_3} {H' : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [NormedAddCommGroup E'] [NormedSpace ℝ E'] [TopologicalSpace H'] {I : ModelWithCorners ℝ E H} {I' : ModelWithCorners ℝ E' H'} {M : Type u_7} {M' : Type u_8} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 2 M] [TopologicalSpace M'] [ChartedSpace H' M'] [IsManifold I' 2 M'] (Φ : Diffeomorph I I' M M' ↑⊤) (k : ℕ) (c : deRhamCohomology I' M' k) : (equivOfDiffeomorph Φ k) c = (map ⇑Φ ⋯ k) c

The equivalence induced by a diffeomorphism is pullback along it.

@[simp]

theorem TauCeti.deRhamCohomology.equivOfDiffeomorph_symm_apply {E : Type u_1} {H : Type u_2} {E' : Type u_3} {H' : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [NormedAddCommGroup E'] [NormedSpace ℝ E'] [TopologicalSpace H'] {I : ModelWithCorners ℝ E H} {I' : ModelWithCorners ℝ E' H'} {M : Type u_7} {M' : Type u_8} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 2 M] [TopologicalSpace M'] [ChartedSpace H' M'] [IsManifold I' 2 M'] (Φ : Diffeomorph I I' M M' ↑⊤) (k : ℕ) (c : deRhamCohomology I M k) : (equivOfDiffeomorph Φ k).symm c = (map ⇑Φ.symm ⋯ k) c

The inverse of the equivalence induced by a diffeomorphism is pullback along its inverse.

The induced cochain maps compare complexes in one universe, so the model spaces share a universe, as do the manifolds.

noncomputable def TauCeti.deRhamComplex.map {E E' : Type u} {H : Type u_1} {H' : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [NormedAddCommGroup E'] [NormedSpace ℝ E'] [TopologicalSpace H'] {I : ModelWithCorners ℝ E H} {I' : ModelWithCorners ℝ E' H'} {M M' : Type v} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 2 M] [TopologicalSpace M'] [ChartedSpace H' M'] [IsManifold I' 2 M'] (f : M → M') (hf : ContMDiff I I' (↑⊤) f) : deRhamComplex I' M' ⟶ deRhamComplex I M

The cochain map of de Rham complexes induced by a smooth map, given in each degree by pullback of smooth forms.

theorem TauCeti.deRhamComplex.map_f {E E' : Type u} {H : Type u_1} {H' : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [NormedAddCommGroup E'] [NormedSpace ℝ E'] [TopologicalSpace H'] {I : ModelWithCorners ℝ E H} {I' : ModelWithCorners ℝ E' H'} {M M' : Type v} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 2 M] [TopologicalSpace M'] [ChartedSpace H' M'] [IsManifold I' 2 M'] (f : M → M') (hf : ContMDiff I I' (↑⊤) f) (k : ℕ) : CategoryTheory.CategoryStruct.comp ((map f hf).f k) (deRhamComplexXIso I k).hom = CategoryTheory.CategoryStruct.comp (deRhamComplexXIso I' k).hom (ModuleCat.ofHom (SmoothForm.mpullback f hf))

Under the canonical identifications of the objects, the induced cochain map is pullback of smooth forms.

theorem TauCeti.deRhamComplex.map_f_assoc {E E' : Type u} {H : Type u_1} {H' : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [NormedAddCommGroup E'] [NormedSpace ℝ E'] [TopologicalSpace H'] {I : ModelWithCorners ℝ E H} {I' : ModelWithCorners ℝ E' H'} {M M' : Type v} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 2 M] [TopologicalSpace M'] [ChartedSpace H' M'] [IsManifold I' 2 M'] (f : M → M') (hf : ContMDiff I I' (↑⊤) f) (k : ℕ) {Z : ModuleCat ℝ} (h : ↧(SmoothForm I M ℝ k) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((map f hf).f k) (CategoryTheory.CategoryStruct.comp (deRhamComplexXIso I k).hom h) = CategoryTheory.CategoryStruct.comp (deRhamComplexXIso I' k).hom (CategoryTheory.CategoryStruct.comp (ModuleCat.ofHom (SmoothForm.mpullback f hf)) h)

Under the canonical identifications of the objects, the induced cochain map is pullback of smooth forms.

theorem TauCeti.deRhamComplex.map_f_inv_apply {E E' : Type u} {H : Type u_1} {H' : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [NormedAddCommGroup E'] [NormedSpace ℝ E'] [TopologicalSpace H'] {I : ModelWithCorners ℝ E H} {I' : ModelWithCorners ℝ E' H'} {M M' : Type v} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 2 M] [TopologicalSpace M'] [ChartedSpace H' M'] [IsManifold I' 2 M'] (f : M → M') (hf : ContMDiff I I' (↑⊤) f) (k : ℕ) (φ : SmoothForm I' M' ℝ k) : (CategoryTheory.ConcreteCategory.hom ((map f hf).f k)) ((CategoryTheory.ConcreteCategory.hom (deRhamComplexXIso I' k).inv) φ) = (CategoryTheory.ConcreteCategory.hom (deRhamComplexXIso I k).inv) ((SmoothForm.mpullback f hf) φ)

The induced cochain map, on a form read through the canonical identification of the degree-k object, is pullback of that form.

@[simp]

theorem TauCeti.deRhamComplex.map_id {E : Type u} {H : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type v} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 2 M] : map id ⋯ = CategoryTheory.CategoryStruct.id (deRhamComplex I M)

The identity map induces the identity cochain map.

theorem TauCeti.deRhamComplex.map_comp {E E' E'' : Type u} {H : Type u_1} {H' : Type u_2} {H'' : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [NormedAddCommGroup E'] [NormedSpace ℝ E'] [TopologicalSpace H'] [NormedAddCommGroup E''] [NormedSpace ℝ E''] [TopologicalSpace H''] {I : ModelWithCorners ℝ E H} {I' : ModelWithCorners ℝ E' H'} {I'' : ModelWithCorners ℝ E'' H''} {M M' M'' : Type v} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 2 M] [TopologicalSpace M'] [ChartedSpace H' M'] [IsManifold I' 2 M'] [TopologicalSpace M''] [ChartedSpace H'' M''] [IsManifold I'' 2 M''] (f : M → M') (g : M' → M'') (hf : ContMDiff I I' (↑⊤) f) (hg : ContMDiff I' I'' (↑⊤) g) : map (g ∘ f) ⋯ = CategoryTheory.CategoryStruct.comp (map g hg) (map f hf)

The induced cochain maps reverse composition of smooth maps.

theorem TauCeti.deRhamComplex.homologyMap_map {E E' : Type u} {H : Type u_1} {H' : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [NormedAddCommGroup E'] [NormedSpace ℝ E'] [TopologicalSpace H'] {I : ModelWithCorners ℝ E H} {I' : ModelWithCorners ℝ E' H'} {M M' : Type v} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 2 M] [TopologicalSpace M'] [ChartedSpace H' M'] [IsManifold I' 2 M'] (f : M → M') (hf : ContMDiff I I' (↑⊤) f) (k : ℕ) : HomologicalComplex.homologyMap (map f hf) k = ModuleCat.ofHom (deRhamCohomology.map f hf k)

The map induced on cohomology by the cochain map of a smooth map is pullback on de Rham cohomology.