Compactly supported de Rham cohomology

Smooth real-valued forms with compact topological support form a submodule of all smooth forms. The exterior derivative does not enlarge supports, so these forms are a subcomplex of the de Rham complex, the compactly supported de Rham complex; its cohomology is compactly supported de Rham cohomology H^•_c.

A compactly supported closed form has a class in H^•_c; every class arises this way, and a class vanishes exactly when its representative is the exterior derivative of a compactly supported form. The inclusion of complexes induces the comparison H^•_c(M) → H^•_dR(M), which takes the de Rham class of the representative; it is an isomorphism on compact manifolds, where every form is compactly supported.

On a manifold modelled on a finite-dimensional space, every alternating form of degree above the dimension is zero, so H^k_c(M) vanishes for k > dim M.

Pullback along a smooth proper map preserves compact support, so H^•_c is contravariant for smooth proper maps, and a diffeomorphism induces an isomorphism. Pullback along a general smooth map does not preserve compact support: the constant map ℝ → pt pulls the constant function 1 back to a function without compact support.

Main definitions

• TauCeti.compactlySupportedForms I M k: compactly supported smooth k-forms.
• TauCeti.compactlySupportedClosedForms I M k: compactly supported closed smooth k-forms.
• TauCeti.compactlySupportedDeRhamComplex I M: the compactly supported de Rham complex.
• TauCeti.compactlySupportedDeRhamCohomology I M k: its cohomology.
• TauCeti.compactlySupportedDeRhamCohomology.mk: the class of a compactly supported closed form.
• TauCeti.compactlySupportedDeRhamCohomology.toDeRhamCohomology: the comparison with de Rham cohomology.
• TauCeti.compactlySupportedDeRhamComplex.ι: the inclusion into the de Rham complex.
• TauCeti.compactlySupportedDeRhamComplex.map: the cochain map induced by a smooth proper map.
• TauCeti.compactlySupportedDeRhamCohomology.map: the induced map on cohomology.
• TauCeti.compactlySupportedDeRhamCohomology.equivOfDiffeomorph: the induced isomorphism for a diffeomorphism.
• TauCeti.subsingleton_compactlySupportedDeRhamCohomology_of_finrank_lt: H^k_c(M) = 0 above the dimension.

References

• John M. Lee, Introduction to Smooth Manifolds, 2nd ed., Chapter 17, "Cohomology with Compact Support".

def TauCeti.compactlySupportedForms {E : Type u_1} {H : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] (I : ModelWithCorners ℝ E H) (M : Type u_3) [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] (k : ℕ) : Submodule ℝ (SmoothForm I M ℝ k)

The submodule of smooth real-valued k-forms with compact topological support.

@[simp]

theorem TauCeti.mem_compactlySupportedForms {E : Type u_1} {H : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] {k : ℕ} {φ : SmoothForm I M ℝ k} : φ ∈ compactlySupportedForms I M k ↔ IsCompact (tsupport ↑φ)

A smooth form is compactly supported when its topological support is compact.

theorem TauCeti.cast_mem_compactlySupportedForms_iff {E : Type u_1} {H : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] {a b : ℕ} (h : a = b) {φ : SmoothForm I M ℝ a} : (LinearEquiv.cast h) φ ∈ compactlySupportedForms I M b ↔ φ ∈ compactlySupportedForms I M a

Transporting the degree of a smooth form preserves compact support.

@[simp]

theorem TauCeti.compactlySupportedForms_eq_top {E : Type u_1} {H : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] [CompactSpace M] (k : ℕ) : compactlySupportedForms I M k = ⊤

On a compact manifold every smooth form is compactly supported.

theorem TauCeti.mextDerivₗ_mem_compactlySupportedForms {E : Type u_1} {H : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 2 M] {k : ℕ} {φ : SmoothForm I M ℝ k} (hφ : φ ∈ compactlySupportedForms I M k) : (mextDerivₗ I k) φ ∈ compactlySupportedForms I M (k + 1)

The exterior derivative of a compactly supported smooth form is compactly supported.

noncomputable def TauCeti.compactlySupportedForms.mextDerivₗ {E : Type u_1} {H : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] (I : ModelWithCorners ℝ E H) (M : Type u_3) [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 2 M] (k : ℕ) : ↥(compactlySupportedForms I M k) →ₗ[ℝ] ↥(compactlySupportedForms I M (k + 1))

The exterior derivative of compactly supported smooth forms, which does not enlarge supports.

@[simp]

theorem TauCeti.compactlySupportedForms.coe_mextDerivₗ {E : Type u_1} {H : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 2 M] (k : ℕ) (φ : ↥(compactlySupportedForms I M k)) : ↑((mextDerivₗ I M k) φ) = (TauCeti.mextDerivₗ I k) ↑φ

The exterior derivative of a compactly supported form is its exterior derivative as a smooth form.

@[simp]

theorem TauCeti.compactlySupportedForms.mextDerivₗ_comp_mextDerivₗ {E : Type u_1} {H : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 2 M] (k : ℕ) : mextDerivₗ I M (k + 1) ∘ₗ mextDerivₗ I M k = 0

Successive exterior derivatives of compactly supported forms compose to zero.

noncomputable def TauCeti.compactlySupportedDeRhamComplex {E : Type u_1} {H : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] (I : ModelWithCorners ℝ E H) (M : Type u_3) [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 2 M] : CochainComplex (ModuleCat ℝ) ℕ

The compactly supported de Rham complex: compactly supported smooth real-valued forms with the exterior derivative.

noncomputable def TauCeti.compactlySupportedDeRhamComplexXIso {E : Type u_1} {H : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 2 M] (k : ℕ) : (compactlySupportedDeRhamComplex I M).X k ≅ ↧↥(compactlySupportedForms I M k)

The canonical identification of the degree-k object with compactly supported smooth k-forms.

theorem TauCeti.compactlySupportedDeRhamComplex_d {E : Type u_1} {H : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 2 M] (k : ℕ) : CategoryTheory.CategoryStruct.comp ((compactlySupportedDeRhamComplex I M).d k (k + 1)) (compactlySupportedDeRhamComplexXIso I (k + 1)).hom = CategoryTheory.CategoryStruct.comp (compactlySupportedDeRhamComplexXIso I k).hom (ModuleCat.ofHom (compactlySupportedForms.mextDerivₗ I M k))

Under the canonical identifications of the objects, the differential of the compactly supported de Rham complex is the exterior derivative.

theorem TauCeti.compactlySupportedDeRhamComplex_d_assoc {E : Type u_1} {H : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 2 M] (k : ℕ) {Z : ModuleCat ℝ} (h : ↧↥(compactlySupportedForms I M (k + 1)) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((compactlySupportedDeRhamComplex I M).d k (k + 1)) (CategoryTheory.CategoryStruct.comp (compactlySupportedDeRhamComplexXIso I (k + 1)).hom h) = CategoryTheory.CategoryStruct.comp (compactlySupportedDeRhamComplexXIso I k).hom (CategoryTheory.CategoryStruct.comp (ModuleCat.ofHom (compactlySupportedForms.mextDerivₗ I M k)) h)

Under the canonical identifications of the objects, the differential of the compactly supported de Rham complex is the exterior derivative.

theorem TauCeti.compactlySupportedDeRhamComplex_d_apply {E : Type u_1} {H : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 2 M] (k : ℕ) (x : ↑((compactlySupportedDeRhamComplex I M).X k)) : (CategoryTheory.ConcreteCategory.hom ((compactlySupportedDeRhamComplex I M).d k (k + 1))) x = (CategoryTheory.ConcreteCategory.hom (compactlySupportedDeRhamComplexXIso I (k + 1)).inv) ((compactlySupportedForms.mextDerivₗ I M k) ((CategoryTheory.ConcreteCategory.hom (compactlySupportedDeRhamComplexXIso I k).hom) x))

The differential of the compactly supported de Rham complex, evaluated on an element.

theorem TauCeti.compactlySupportedDeRhamComplex_d_eq_zero_of_mem_closedForms {E : Type u_1} {H : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 2 M] (k : ℕ) {φ : ↥(compactlySupportedForms I M k)} (hφ : ↑φ ∈ closedForms I M k) : (CategoryTheory.ConcreteCategory.hom ((compactlySupportedDeRhamComplex I M).d k (k + 1))) ((CategoryTheory.ConcreteCategory.hom (compactlySupportedDeRhamComplexXIso I k).inv) φ) = 0

A closed compactly supported form, viewed in the compactly supported de Rham complex, is killed by the differential.

@[reducible, inline]

abbrev TauCeti.compactlySupportedDeRhamCohomology {E : Type u_1} {H : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] (I : ModelWithCorners ℝ E H) (M : Type u_3) [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 2 M] (k : ℕ) : Type (max u_1 u_3)

Compactly supported de Rham cohomology is the categorical homology of the compactly supported de Rham complex.

noncomputable def TauCeti.compactlySupportedDeRhamComplex.ι {E : Type u_1} {H : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] (I : ModelWithCorners ℝ E H) (M : Type u_3) [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 2 M] : compactlySupportedDeRhamComplex I M ⟶ deRhamComplex I M

The inclusion of the compactly supported de Rham complex into the de Rham complex.

theorem TauCeti.compactlySupportedDeRhamComplex.ι_f {E : Type u_1} {H : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 2 M] (k : ℕ) : CategoryTheory.CategoryStruct.comp ((ι I M).f k) (deRhamComplexXIso I k).hom = CategoryTheory.CategoryStruct.comp (compactlySupportedDeRhamComplexXIso I k).hom (ModuleCat.ofHom (compactlySupportedForms I M k).subtype)

Under the canonical identifications of the objects, the inclusion is the inclusion of compactly supported forms into smooth forms.

theorem TauCeti.compactlySupportedDeRhamComplex.ι_f_assoc {E : Type u_1} {H : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 2 M] (k : ℕ) {Z : ModuleCat ℝ} (h : ↧(SmoothForm I M ℝ k) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((ι I M).f k) (CategoryTheory.CategoryStruct.comp (deRhamComplexXIso I k).hom h) = CategoryTheory.CategoryStruct.comp (compactlySupportedDeRhamComplexXIso I k).hom (CategoryTheory.CategoryStruct.comp (ModuleCat.ofHom (compactlySupportedForms I M k).subtype) h)

Under the canonical identifications of the objects, the inclusion is the inclusion of compactly supported forms into smooth forms.

instance TauCeti.compactlySupportedDeRhamComplex.isIso_ι {E : Type u_1} {H : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 2 M] [CompactSpace M] : CategoryTheory.IsIso (ι I M)

On a compact manifold the compactly supported de Rham complex is the de Rham complex.

noncomputable def TauCeti.compactlySupportedClosedForms {E : Type u_1} {H : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] (I : ModelWithCorners ℝ E H) (M : Type u_3) [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 2 M] (k : ℕ) : Submodule ℝ (SmoothForm I M ℝ k)

The submodule of compactly supported closed smooth forms.

@[simp]

theorem TauCeti.mem_compactlySupportedClosedForms {E : Type u_1} {H : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 2 M] {k : ℕ} {φ : SmoothForm I M ℝ k} : φ ∈ compactlySupportedClosedForms I M k ↔ φ ∈ compactlySupportedForms I M k ∧ φ ∈ closedForms I M k

A smooth form is compactly supported and closed when it is both compactly supported and closed.

theorem TauCeti.compactlySupportedClosedForms_le_compactlySupportedForms {E : Type u_1} {H : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 2 M] (k : ℕ) : compactlySupportedClosedForms I M k ≤ compactlySupportedForms I M k

A compactly supported closed form is compactly supported.

theorem TauCeti.compactlySupportedClosedForms_le_closedForms {E : Type u_1} {H : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 2 M] (k : ℕ) : compactlySupportedClosedForms I M k ≤ closedForms I M k

A compactly supported closed form is closed.

noncomputable def TauCeti.compactlySupportedForms.toClosedOfFinrankLe {E : Type u_1} {H : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 2 M] [FiniteDimensional ℝ E] {k : ℕ} (h : Module.finrank ℝ E ≤ k) : ↥(compactlySupportedForms I M k) →ₗ[ℝ] ↥(compactlySupportedClosedForms I M k)

In degree at least the model dimension, every compactly supported form is closed.

@[simp]

theorem TauCeti.compactlySupportedForms.coe_toClosedOfFinrankLe {E : Type u_1} {H : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 2 M] [FiniteDimensional ℝ E] {k : ℕ} (h : Module.finrank ℝ E ≤ k) (φ : ↥(compactlySupportedForms I M k)) : ↑((toClosedOfFinrankLe I h) φ) = ↑φ

Viewing a top-degree compactly supported form as closed does not change the smooth form.

noncomputable def TauCeti.exactCompactlySupportedForms {E : Type u_1} {H : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] (I : ModelWithCorners ℝ E H) (M : Type u_3) [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 2 M] (k : ℕ) : Submodule ℝ (SmoothForm I M ℝ k)

Compactly supported exact forms are exterior derivatives of compactly supported forms in positive degree, and zero in degree zero.

@[simp]

theorem TauCeti.exactCompactlySupportedForms_zero {E : Type u_1} {H : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 2 M] : exactCompactlySupportedForms I M 0 = ⊥

There are no nonzero compactly supported exact forms in degree zero.

@[simp]

theorem TauCeti.exactCompactlySupportedForms_succ {E : Type u_1} {H : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 2 M] (k : ℕ) : exactCompactlySupportedForms I M (k + 1) = Submodule.map (mextDerivₗ I k) (compactlySupportedForms I M k)

In positive degree, compactly supported exact forms are the image of compactly supported forms under the exterior derivative.

theorem TauCeti.exactCompactlySupportedForms_le_exactForms {E : Type u_1} {H : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 2 M] (k : ℕ) : exactCompactlySupportedForms I M k ≤ exactForms I M k

A compactly supported exact form is exact.

theorem TauCeti.exactCompactlySupportedForms_le_compactlySupportedClosedForms {E : Type u_1} {H : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 2 M] (k : ℕ) : exactCompactlySupportedForms I M k ≤ compactlySupportedClosedForms I M k

A compactly supported exact form is compactly supported and closed.

noncomputable def TauCeti.compactlySupportedDeRhamCohomology.mk {E : Type u_1} {H : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 2 M] (k : ℕ) : ↥(compactlySupportedClosedForms I M k) →ₗ[ℝ] compactlySupportedDeRhamCohomology I M k

The compactly supported cohomology class of a compactly supported closed form.

theorem TauCeti.compactlySupportedDeRhamCohomology.mk_eq_moduleCatHomologyClass {E : Type u_1} {H : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 2 M] (k : ℕ) : mk I k = HomologicalComplex.moduleCatHomologyClass (compactlySupportedDeRhamComplex I M) ⋯ (ModuleCat.Hom.hom (compactlySupportedDeRhamComplexXIso I k).inv ∘ₗ Submodule.inclusion ⋯) ⋯

The class map is the homology class map of the inclusion of compactly supported closed forms into the compactly supported de Rham complex.

theorem TauCeti.compactlySupportedDeRhamCohomology.mk_surjective {E : Type u_1} {H : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 2 M] (k : ℕ) : Function.Surjective ⇑(mk I k)

Every compactly supported cohomology class is represented by a compactly supported closed form.

@[simp]

theorem TauCeti.compactlySupportedDeRhamCohomology.mk_eq_zero_iff {E : Type u_1} {H : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 2 M] (k : ℕ) (φ : ↥(compactlySupportedClosedForms I M k)) : (mk I k) φ = 0 ↔ ↑φ ∈ exactCompactlySupportedForms I M k

A compactly supported closed form represents zero precisely when it is the exterior derivative of a compactly supported form.

theorem TauCeti.compactlySupportedDeRhamCohomology.ker_mk {E : Type u_1} {H : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 2 M] (k : ℕ) : (mk I k).ker = Submodule.comap (compactlySupportedClosedForms I M k).subtype (exactCompactlySupportedForms I M k)

The kernel of the class map is the submodule of compactly supported exact forms inside compactly supported closed forms.

theorem TauCeti.compactlySupportedDeRhamCohomology.mk_eq_mk_iff {E : Type u_1} {H : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 2 M] (k : ℕ) (φ ψ : ↥(compactlySupportedClosedForms I M k)) : (mk I k) φ = (mk I k) ψ ↔ ↑φ - ↑ψ ∈ exactCompactlySupportedForms I M k

Two compactly supported closed forms have the same class precisely when they differ by a compactly supported exact form.

noncomputable def TauCeti.compactlySupportedDeRhamCohomology.toDeRhamCohomology {E : Type u_1} {H : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] (I : ModelWithCorners ℝ E H) (M : Type u_3) [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 2 M] (k : ℕ) : compactlySupportedDeRhamCohomology I M k →ₗ[ℝ] deRhamCohomology I M k

The comparison map from compactly supported to ordinary de Rham cohomology, induced on cohomology by the inclusion of complexes.

@[simp]

theorem TauCeti.compactlySupportedDeRhamCohomology.toDeRhamCohomology_mk {E : Type u_1} {H : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 2 M] (k : ℕ) (φ : ↥(compactlySupportedClosedForms I M k)) : (toDeRhamCohomology I M k) ((mk I k) φ) = (deRhamCohomology.mk I k) ⟨↑φ, ⋯⟩

The comparison map sends the class of a compactly supported closed form to the de Rham class of the underlying closed form.

theorem TauCeti.compactlySupportedDeRhamCohomology.toDeRhamCohomology_bijective {E : Type u_1} {H : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 2 M] [CompactSpace M] (k : ℕ) : Function.Bijective ⇑(toDeRhamCohomology I M k)

On a compact manifold compactly supported and ordinary de Rham cohomology agree.

theorem TauCeti.compactlySupportedDeRhamComplex.homologyMap_ι {E : Type u_1} {H : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 2 M] (k : ℕ) : HomologicalComplex.homologyMap (ι I M) k = ModuleCat.ofHom (compactlySupportedDeRhamCohomology.toDeRhamCohomology I M k)

The map induced on cohomology by the inclusion of complexes is the comparison map.

theorem TauCeti.subsingleton_compactlySupportedDeRhamCohomology_of_finrank_lt {E : Type u_1} {H : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] (I : ModelWithCorners ℝ E H) (M : Type u_3) [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 2 M] [FiniteDimensional ℝ E] {k : ℕ} (hk : Module.finrank ℝ E < k) : Subsingleton (compactlySupportedDeRhamCohomology I M k)

Compactly supported cohomology vanishes in degrees above the dimension of the model, where every alternating form is zero.

noncomputable def TauCeti.compactlySupportedForms.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] [TopologicalSpace M'] [ChartedSpace H' M'] [IsManifold I 1 M] [IsManifold I' 1 M'] (f : M → M') (hf : ContMDiff I I' (↑⊤) f) (hp : IsProperMap f) (k : ℕ) : ↥(compactlySupportedForms I' M' k) →ₗ[ℝ] ↥(compactlySupportedForms I M k)

Pullback of compactly supported smooth forms along a smooth proper map.

@[simp]

theorem TauCeti.compactlySupportedForms.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] [TopologicalSpace M'] [ChartedSpace H' M'] [IsManifold I 1 M] [IsManifold I' 1 M'] (f : M → M') (hf : ContMDiff I I' (↑⊤) f) (hp : IsProperMap f) (k : ℕ) (φ : ↥(compactlySupportedForms I' M' k)) : ↑((mpullback f hf hp k) φ) = (SmoothForm.mpullback f hf) ↑φ

The pullback of a compactly supported form is its pullback as a smooth form.

@[simp]

theorem TauCeti.compactlySupportedForms.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 1 M] (k : ℕ) : mpullback id ⋯ ⋯ k = LinearMap.id

Pullback of compactly supported forms by the identity is the identity linear map.

theorem TauCeti.compactlySupportedForms.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] [TopologicalSpace M'] [ChartedSpace H' M'] [TopologicalSpace M''] [ChartedSpace H'' M''] [IsManifold I 1 M] [IsManifold I' 1 M'] [IsManifold I'' 1 M''] (f : M → M') (g : M' → M'') (hf : ContMDiff I I' (↑⊤) f) (hg : ContMDiff I' I'' (↑⊤) g) (hfp : IsProperMap f) (hgp : IsProperMap g) (k : ℕ) : mpullback (g ∘ f) ⋯ ⋯ k = mpullback f hf hfp k ∘ₗ mpullback g hg hgp k

Pullback of compactly supported forms reverses composition.

theorem TauCeti.compactlySupportedForms.mextDerivₗ_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] [TopologicalSpace M'] [ChartedSpace H' M'] [IsManifold I 2 M] [IsManifold I' 2 M'] (f : M → M') (hf : ContMDiff I I' (↑⊤) f) (hp : IsProperMap f) (k : ℕ) (φ : ↥(compactlySupportedForms I' M' k)) : (mextDerivₗ I M k) ((mpullback f hf hp k) φ) = (mpullback f hf hp (k + 1)) ((mextDerivₗ I' M' k) φ)

Pullback of compactly supported forms along a smooth proper map commutes with the exterior derivative.

theorem TauCeti.SmoothForm.mpullback_mem_exactCompactlySupportedForms {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] [TopologicalSpace M'] [ChartedSpace H' M'] [IsManifold I 2 M] [IsManifold I' 2 M'] (f : M → M') (hf : ContMDiff I I' (↑⊤) f) (hp : IsProperMap f) {k : ℕ} {φ : SmoothForm I' M' ℝ k} (hφ : φ ∈ exactCompactlySupportedForms I' M' k) : (mpullback f hf) φ ∈ exactCompactlySupportedForms I M k

Pullback along a smooth proper map preserves compactly supported exact forms.

noncomputable def TauCeti.compactlySupportedClosedForms.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] [TopologicalSpace M'] [ChartedSpace H' M'] [IsManifold I 2 M] [IsManifold I' 2 M'] (f : M → M') (hf : ContMDiff I I' (↑⊤) f) (hp : IsProperMap f) (k : ℕ) : ↥(compactlySupportedClosedForms I' M' k) →ₗ[ℝ] ↥(compactlySupportedClosedForms I M k)

Pullback of compactly supported closed forms along a smooth proper map.

@[simp]

theorem TauCeti.compactlySupportedClosedForms.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] [TopologicalSpace M'] [ChartedSpace H' M'] [IsManifold I 2 M] [IsManifold I' 2 M'] (f : M → M') (hf : ContMDiff I I' (↑⊤) f) (hp : IsProperMap f) (k : ℕ) (φ : ↥(compactlySupportedClosedForms I' M' k)) : ↑((mpullback f hf hp k) φ) = (SmoothForm.mpullback f hf) ↑φ

The pullback of a compactly supported closed form is its pullback as a smooth form.

theorem TauCeti.compactlySupportedClosedForms.coe_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] [TopologicalSpace M'] [ChartedSpace H' M'] [IsManifold I 2 M] [IsManifold I' 2 M'] (f : M → M') (hf : ContMDiff I I' (↑⊤) f) (hp : IsProperMap f) (k : ℕ) (φ : ↥(compactlySupportedClosedForms I' M' k)) : ↑↑((mpullback f hf hp k) φ) = TauCeti.mpullback I I' f ↑↑φ

The underlying rough form of the pullback of a compactly supported closed form is the rough pullback of its underlying rough form.

@[simp]

theorem TauCeti.compactlySupportedClosedForms.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 compactly supported closed forms by the identity is the identity linear map.

theorem TauCeti.compactlySupportedClosedForms.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] [TopologicalSpace M'] [ChartedSpace H' M'] [TopologicalSpace M''] [ChartedSpace H'' M''] [IsManifold I 2 M] [IsManifold I' 2 M'] [IsManifold I'' 2 M''] (f : M → M') (g : M' → M'') (hf : ContMDiff I I' (↑⊤) f) (hg : ContMDiff I' I'' (↑⊤) g) (hfp : IsProperMap f) (hgp : IsProperMap g) (k : ℕ) : mpullback (g ∘ f) ⋯ ⋯ k = mpullback f hf hfp k ∘ₗ mpullback g hg hgp k

Pullback of compactly supported closed forms reverses composition.

noncomputable def TauCeti.compactlySupportedDeRhamCohomology.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] [TopologicalSpace M'] [ChartedSpace H' M'] [IsManifold I 2 M] [IsManifold I' 2 M'] (f : M → M') (hf : ContMDiff I I' (↑⊤) f) (hp : IsProperMap f) (k : ℕ) : compactlySupportedDeRhamCohomology I' M' k →ₗ[ℝ] compactlySupportedDeRhamCohomology I M k

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

@[simp]

theorem TauCeti.compactlySupportedDeRhamCohomology.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] [TopologicalSpace M'] [ChartedSpace H' M'] [IsManifold I 2 M] [IsManifold I' 2 M'] (f : M → M') (hf : ContMDiff I I' (↑⊤) f) (hp : IsProperMap f) (k : ℕ) (φ : ↥(compactlySupportedClosedForms I' M' k)) : (map f hf hp k) ((mk I' k) φ) = (mk I k) ((compactlySupportedClosedForms.mpullback f hf hp k) φ)

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

@[simp]

theorem TauCeti.compactlySupportedDeRhamCohomology.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 compactly supported cohomology induced by the identity is the identity.

theorem TauCeti.compactlySupportedDeRhamCohomology.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] [TopologicalSpace M'] [ChartedSpace H' M'] [TopologicalSpace M''] [ChartedSpace H'' M''] [IsManifold I 2 M] [IsManifold I' 2 M'] [IsManifold I'' 2 M''] (f : M → M') (g : M' → M'') (hf : ContMDiff I I' (↑⊤) f) (hg : ContMDiff I' I'' (↑⊤) g) (hfp : IsProperMap f) (hgp : IsProperMap g) (k : ℕ) : map (g ∘ f) ⋯ ⋯ k = map f hf hfp k ∘ₗ map g hg hgp k

Pullback on compactly supported cohomology reverses composition of smooth proper maps.

theorem TauCeti.compactlySupportedDeRhamCohomology.toDeRhamCohomology_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] [TopologicalSpace M'] [ChartedSpace H' M'] [IsManifold I 2 M] [IsManifold I' 2 M'] (f : M → M') (hf : ContMDiff I I' (↑⊤) f) (hp : IsProperMap f) (k : ℕ) (c : compactlySupportedDeRhamCohomology I' M' k) : (toDeRhamCohomology I M k) ((map f hf hp k) c) = (deRhamCohomology.map f hf k) ((toDeRhamCohomology I' M' k) c)

The comparison with de Rham cohomology commutes with pullback along smooth proper maps.

noncomputable def TauCeti.compactlySupportedDeRhamCohomology.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] [TopologicalSpace M'] [ChartedSpace H' M'] [IsManifold I 2 M] [IsManifold I' 2 M'] (Φ : Diffeomorph I I' M M' ↑⊤) (k : ℕ) : compactlySupportedDeRhamCohomology I' M' k ≃ₗ[ℝ] compactlySupportedDeRhamCohomology I M k

A diffeomorphism Φ : M ≃ M', which is a proper map, induces a linear equivalence H^k_c(M') ≃ H^k_c(M) on compactly supported de Rham cohomology: pullback along Φ, with inverse pullback along Φ.symm.

@[simp]

theorem TauCeti.compactlySupportedDeRhamCohomology.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] [TopologicalSpace M'] [ChartedSpace H' M'] [IsManifold I 2 M] [IsManifold I' 2 M'] (Φ : Diffeomorph I I' M M' ↑⊤) (k : ℕ) (c : compactlySupportedDeRhamCohomology I' M' k) : (equivOfDiffeomorph Φ k) c = (map ⇑Φ ⋯ ⋯ k) c

The equivalence induced by a diffeomorphism is pullback along it.

@[simp]

theorem TauCeti.compactlySupportedDeRhamCohomology.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] [TopologicalSpace M'] [ChartedSpace H' M'] [IsManifold I 2 M] [IsManifold I' 2 M'] (Φ : Diffeomorph I I' M M' ↑⊤) (k : ℕ) (c : compactlySupportedDeRhamCohomology 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.

theorem TauCeti.compactlySupportedDeRhamCohomology.equivOfDiffeomorph_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] [TopologicalSpace M'] [ChartedSpace H' M'] [IsManifold I 2 M] [IsManifold I' 2 M'] (Φ : Diffeomorph I I' M M' ↑⊤) (k : ℕ) (φ : ↥(compactlySupportedClosedForms I' M' k)) : (equivOfDiffeomorph Φ k) ((mk I' k) φ) = (mk I k) ((compactlySupportedClosedForms.mpullback ⇑Φ ⋯ ⋯ k) φ)

The equivalence induced by a diffeomorphism sends the class of a compactly supported closed form to the class of its pullback.

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

noncomputable def TauCeti.compactlySupportedDeRhamComplex.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) (hp : IsProperMap f) : compactlySupportedDeRhamComplex I' M' ⟶ compactlySupportedDeRhamComplex I M

The cochain map between compactly supported de Rham complexes induced by a smooth proper map.

theorem TauCeti.compactlySupportedDeRhamComplex.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) (hp : IsProperMap f) (k : ℕ) : CategoryTheory.CategoryStruct.comp ((map f hf hp).f k) (compactlySupportedDeRhamComplexXIso I k).hom = CategoryTheory.CategoryStruct.comp (compactlySupportedDeRhamComplexXIso I' k).hom (ModuleCat.ofHom (compactlySupportedForms.mpullback f hf hp k))

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

theorem TauCeti.compactlySupportedDeRhamComplex.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) (hp : IsProperMap f) (k : ℕ) {Z : ModuleCat ℝ} (h : ↧↥(compactlySupportedForms I M k) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((map f hf hp).f k) (CategoryTheory.CategoryStruct.comp (compactlySupportedDeRhamComplexXIso I k).hom h) = CategoryTheory.CategoryStruct.comp (compactlySupportedDeRhamComplexXIso I' k).hom (CategoryTheory.CategoryStruct.comp (ModuleCat.ofHom (compactlySupportedForms.mpullback f hf hp k)) h)

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

@[simp]

theorem TauCeti.compactlySupportedDeRhamComplex.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 (compactlySupportedDeRhamComplex I M)

The cochain map induced by the identity is the identity.

theorem TauCeti.compactlySupportedDeRhamComplex.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) (hfp : IsProperMap f) (hgp : IsProperMap g) : map (g ∘ f) ⋯ ⋯ = CategoryTheory.CategoryStruct.comp (map g hg hgp) (map f hf hfp)

The induced cochain maps reverse composition of smooth proper maps.

theorem TauCeti.compactlySupportedDeRhamComplex.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) (hp : IsProperMap f) (k : ℕ) : HomologicalComplex.homologyMap (map f hf hp) k = ModuleCat.ofHom (compactlySupportedDeRhamCohomology.map f hf hp k)

The map induced on cohomology by the cochain map of a smooth proper map is pullback on compactly supported cohomology.