@[reducible, inline]

abbrev DiffForm (E : Type u_1) [NormedAddCommGroup E] [NormedSpace ℝ E] (n : ℕ) : Type u_1

A (concrete) differential $n$-form on a normed space $E$: a smooth map assigning to each point an alternating continuous $n$-linear form.

noncomputable def pullbackForm {E₁ : Type u_1} {E₂ : Type u_2} [NormedAddCommGroup E₁] [NormedSpace ℝ E₁] [NormedAddCommGroup E₂] [NormedSpace ℝ E₂] (f : E₁ → E₂) {n : ℕ} (ω : DiffForm E₂ n) : DiffForm E₁ n

Pullback of a differential form along a smooth map: $(f^*\omega)_x(v_1,\dots,v_n) = \omega_{f(x)}(df_x v_1, \dots, df_x v_n)$.

structure DeRhamConcrete.HasDeformationRetractConcrete {E_X : Type u_1} {E_U : Type u_2} [NormedAddCommGroup E_X] [NormedSpace ℝ E_X] [NormedAddCommGroup E_U] [NormedSpace ℝ E_U] (i : E_X → E_U) (π : E_U → E_X) : Type u_2

Concrete deformation retract data $i : X \hookrightarrow U$ and $\pi : U \to X$ with a chain homotopy operator $K$ satisfying $dK + Kd = \mathrm{id} - \pi^* i^*$, used to prove $i^* : H^*(U) \xrightarrow{\sim} H^*(X)$.

• smooth_i : ContDiff ℝ ⊤ i
• smooth_π : ContDiff ℝ ⊤ π
• retraction {n : ℕ} (ω : DiffForm E_X n) : pullbackForm i (pullbackForm π ω) = ω
• K {p : ℕ} : DiffForm E_U (p + 1) → DiffForm E_U p
• K_smul {p : ℕ} (r : ℝ) (β : DiffForm E_U (p + 1)) : self.K (r • β) = r • self.K β
• homotopy_formula {p : ℕ} (β : DiffForm E_U (p + 1)) : extDeriv (self.K β) + self.K (extDeriv β) = β - pullbackForm π (pullbackForm i β)
• K_vanishes {p : ℕ} (β : DiffForm E_U (p + 1)) : pullbackForm i (self.K β) = 0
• deg0_injectivity (β : DiffForm E_U 0) : extDeriv β = 0 → pullbackForm i β = 0 → β = 0
• smooth_forms_U {n : ℕ} (ω : DiffForm E_U n) : ContDiff ℝ ⊤ ω

theorem DeRhamConcrete.HasDeformationRetractConcrete.d_squared {E_X : Type u_1} {E_U : Type u_2} [NormedAddCommGroup E_X] [NormedSpace ℝ E_X] [NormedAddCommGroup E_U] [NormedSpace ℝ E_U] {i : E_X → E_U} {π : E_U → E_X} (hdr : HasDeformationRetractConcrete i π) {n : ℕ} (ω : DiffForm E_U n) : extDeriv (extDeriv ω) = 0

The exterior derivative squares to zero: $d \circ d = 0$ on smooth forms in $U$.

theorem DeRhamConcrete.HasDeformationRetractConcrete.d_sub {E_X : Type u_1} {E_U : Type u_2} [NormedAddCommGroup E_X] [NormedSpace ℝ E_X] [NormedAddCommGroup E_U] [NormedSpace ℝ E_U] {i : E_X → E_U} {π : E_U → E_X} (hdr : HasDeformationRetractConcrete i π) {n : ℕ} (ω₁ ω₂ : DiffForm E_U n) : extDeriv (ω₁ - ω₂) = extDeriv ω₁ - extDeriv ω₂

$d$ is linear in subtraction: $d(\omega_1 - \omega_2) = d\omega_1 - d\omega_2$.

theorem DeRhamConcrete.HasDeformationRetractConcrete.d_add {E_X : Type u_1} {E_U : Type u_2} [NormedAddCommGroup E_X] [NormedSpace ℝ E_X] [NormedAddCommGroup E_U] [NormedSpace ℝ E_U] {i : E_X → E_U} {π : E_U → E_X} (hdr : HasDeformationRetractConcrete i π) {n : ℕ} (ω₁ ω₂ : DiffForm E_U n) : extDeriv (ω₁ + ω₂) = extDeriv ω₁ + extDeriv ω₂

$d$ is additive: $d(\omega_1 + \omega_2) = d\omega_1 + d\omega_2$.

theorem DeRhamConcrete.HasDeformationRetractConcrete.i_comm_d {E_X : Type u_1} {E_U : Type u_2} [NormedAddCommGroup E_X] [NormedSpace ℝ E_X] [NormedAddCommGroup E_U] [NormedSpace ℝ E_U] {i : E_X → E_U} {π : E_U → E_X} (hdr : HasDeformationRetractConcrete i π) {n : ℕ} (ω : DiffForm E_U n) : pullbackForm i (extDeriv ω) = extDeriv (pullbackForm i ω)

Pullback along $i$ commutes with the exterior derivative: $i^*(d\omega) = d(i^*\omega)$.

theorem DeRhamConcrete.HasDeformationRetractConcrete.i_sub {E_X : Type u_1} {E_U : Type u_2} [NormedAddCommGroup E_X] [NormedSpace ℝ E_X] [NormedAddCommGroup E_U] [NormedSpace ℝ E_U] {i : E_X → E_U} {π : E_U → E_X} (_hdr : HasDeformationRetractConcrete i π) {n : ℕ} (ω₁ ω₂ : DiffForm E_U n) : pullbackForm i (ω₁ - ω₂) = pullbackForm i ω₁ - pullbackForm i ω₂

Pullback distributes over subtraction: $i^*(\omega_1 - \omega_2) = i^*\omega_1 - i^*\omega_2$.

theorem DeRhamConcrete.HasDeformationRetractConcrete.π_zero {E_X : Type u_1} {E_U : Type u_2} [NormedAddCommGroup E_X] [NormedSpace ℝ E_X] [NormedAddCommGroup E_U] [NormedSpace ℝ E_U] {i : E_X → E_U} {π : E_U → E_X} (_hdr : HasDeformationRetractConcrete i π) {n : ℕ} : pullbackForm π 0 = 0

Pullback of the zero form by $\pi$ is the zero form: $\pi^* 0 = 0$.

theorem DeRhamConcrete.cohomology_isomorphism_surjectivity_concrete {E_X : Type u_1} {E_U : Type u_2} [NormedAddCommGroup E_X] [NormedSpace ℝ E_X] [NormedAddCommGroup E_U] [NormedSpace ℝ E_U] (i : E_X → E_U) (π : E_U → E_X) (hdr : HasDeformationRetractConcrete i π) {p : ℕ} (α : DiffForm E_X p) : ∃ (β : DiffForm E_U p), pullbackForm i β = α

Surjectivity at the cocycle level: every form $\alpha$ on $X$ is the pullback $i^*\beta$ of a form $\beta$ on $U$ (take $\beta = \pi^*\alpha$).

theorem DeRhamConcrete.cohomology_isomorphism_injectivity_concrete {E_X : Type u_1} {E_U : Type u_2} [NormedAddCommGroup E_X] [NormedSpace ℝ E_X] [NormedAddCommGroup E_U] [NormedSpace ℝ E_U] (i : E_X → E_U) (π : E_U → E_X) (hdr : HasDeformationRetractConcrete i π) (p : ℕ) (β : DiffForm E_U (p + 1)) : extDeriv β = 0 → (∃ (γ : DiffForm E_X p), pullbackForm i β = extDeriv γ) → ∃ (η : DiffForm E_U p), β = extDeriv η

Injectivity at cohomology level: a closed form $\beta$ on $U$ whose restriction $i^*\beta$ is exact is itself exact, proved using the chain-homotopy formula.

theorem DeRhamConcrete.cohomology_isomorphism {E_X : Type u_1} {E_U : Type u_2} [NormedAddCommGroup E_X] [NormedSpace ℝ E_X] [NormedAddCommGroup E_U] [NormedSpace ℝ E_U] (i : E_X → E_U) (π : E_U → E_X) (hdr : HasDeformationRetractConcrete i π) : (∀ {p : ℕ} (α : DiffForm E_X p), ∃ (β : DiffForm E_U p), pullbackForm i β = α) ∧ (∀ (p : ℕ) (β : DiffForm E_U (p + 1)), extDeriv β = 0 → (∃ (γ : DiffForm E_X p), pullbackForm i β = extDeriv γ) → ∃ (η : DiffForm E_U p), β = extDeriv η) ∧ ∀ (β : DiffForm E_U 0), extDeriv β = 0 → pullbackForm i β = 0 → β = 0

Corollary 1: for a deformation retract $i: X \hookrightarrow U$, the pullback $i^* : H^*(U, \mathbb{R}) \to H^*(X, \mathbb{R})$ is an isomorphism (surjective on cocycles, injective in positive degree, and injective on degree-$0$ closed forms).

theorem pullbackForm_id {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {n : ℕ} (ω : DiffForm E n) : pullbackForm id ω = ω

Pullback along the identity is the identity: $\mathrm{id}^*\omega = \omega$.

theorem extDeriv_zero_eq_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {n : ℕ} : extDeriv 0 = 0

The exterior derivative of the zero form is zero: $d 0 = 0$.

theorem contDiff_of_subsingleton_domain {E' : Type u_2} {F : Type u_3} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [Subsingleton E'] [NormedAddCommGroup F] [NormedSpace ℝ F] (f : E' → F) : ContDiff ℝ ⊤ f

Any function out of a subsingleton normed space is smooth (it is constant).

noncomputable def DeRhamConcrete.HasDeformationRetractConcrete.ofSubsingleton (E' : Type u_2) [NormedAddCommGroup E'] [NormedSpace ℝ E'] [Subsingleton E'] : HasDeformationRetractConcrete id id

The trivial deformation retract instance on a subsingleton (e.g., a point), with $K \equiv 0$.