class DifferentialFormSpace (Ω : ℕ → Type u_1) (VF : Type u_2) : Type (max u_1 u_2)

Axiomatic structure of a graded space $\Omega^\bullet$ of differential forms together with a space $VF$ of vector fields: includes wedge with functions and $1$-forms, exterior derivative $d$, interior product $\iota$, Lie derivative $\mathcal{L}$ and the algebraic relations they satisfy.

• instAddCommGroup (p : ℕ) : AddCommGroup (Ω p)
• instModule (p : ℕ) : Module ℝ (Ω p)
• fMul {p : ℕ} : Ω 0 → Ω p → Ω p
• wedge1 {p : ℕ} : Ω 1 → Ω p → Ω (p + 1)
• d {p : ℕ} : Ω p → Ω (p + 1)
• ι : VF → {p : ℕ} → Ω (p + 1) → Ω p
• L : VF → {p : ℕ} → Ω p → Ω p
• d_add {p : ℕ} (α β : Ω p) : d VF (α + β) = d VF α + d VF β
• d_smul {p : ℕ} (r : ℝ) (α : Ω p) : d VF (r • α) = r • d VF α
• d_squared {p : ℕ} (α : Ω p) : d VF (d VF α) = 0
• d_fMul {p : ℕ} (f : Ω 0) (α : Ω p) : d VF (fMul VF f α) = wedge1 VF (d VF f) α + fMul VF f (d VF α)
• fMul_add_left {p : ℕ} (f g : Ω 0) (α : Ω p) : fMul VF (f + g) α = fMul VF f α + fMul VF g α
• fMul_add_right {p : ℕ} (f : Ω 0) (α β : Ω p) : fMul VF f (α + β) = fMul VF f α + fMul VF f β
• fMul_smul {p : ℕ} (r : ℝ) (f : Ω 0) (α : Ω p) : fMul VF (r • f) α = r • fMul VF f α
• wedge1_add_right {p : ℕ} (ω : Ω 1) (α β : Ω p) : wedge1 VF ω (α + β) = wedge1 VF ω α + wedge1 VF ω β
• wedge1_smul_right {p : ℕ} (ω : Ω 1) (r : ℝ) (α : Ω p) : wedge1 VF ω (r • α) = r • wedge1 VF ω α
• ι_add (X : VF) {p : ℕ} (α β : Ω (p + 1)) : ι X (α + β) = ι X α + ι X β
• ι_smul (X : VF) {p : ℕ} (r : ℝ) (α : Ω (p + 1)) : ι X (r • α) = r • ι X α
• ι_fMul (X : VF) {p : ℕ} (f : Ω 0) (α : Ω (p + 1)) : ι X (fMul VF f α) = fMul VF f (ι X α)
• ι_wedge1 (X : VF) {p : ℕ} (ω : Ω 1) (α : Ω (p + 1)) : ι X (wedge1 VF ω α) = fMul VF (ι X ω) α - wedge1 VF ω (ι X α)
• ι_squared (X : VF) {p : ℕ} (α : Ω (p + 1 + 1)) : ι X (ι X α) = 0
• ι_ι_anticomm (X Y : VF) {p : ℕ} (α : Ω (p + 1 + 1)) : ι X (ι Y α) = -ι Y (ι X α)
• L_add (X : VF) {p : ℕ} (α β : Ω p) : L X (α + β) = L X α + L X β
• L_smul (X : VF) {p : ℕ} (r : ℝ) (α : Ω p) : L X (r • α) = r • L X α
• L_zero_eq_ι_d (X : VF) (f : Ω 0) : L X f = ι X (d VF f)
• L_comm_d (X : VF) {p : ℕ} (α : Ω p) : L X (d VF α) = d VF (L X α)
• L_fMul (X : VF) {p : ℕ} (f : Ω 0) (α : Ω p) : L X (fMul VF f α) = fMul VF (L X f) α + fMul VF f (L X α)
• ext_fdα {p : ℕ} (T : Ω (p + 1) → Ω (p + 1)) : (∀ (α β : Ω (p + 1)), T (α + β) = T α + T β) → (∀ (r : ℝ) (α : Ω (p + 1)), T (r • α) = r • T α) → (∀ (f : Ω 0) (α : Ω p), T (fMul VF f (d VF α)) = 0) → ∀ (β : Ω (p + 1)), T β = 0
• ι_one_form_nondegenerate (α : Ω 1) : (∀ (X : VF), ι X α = 0) → α = 0
• ι_two_form_nondegenerate (ω : Ω 2) : (∀ (X : VF), ι X ω = 0) → ω = 0

class HasComplexScalars (Ω : ℕ → Type u_1) (VF : Type u_2) [inst : DifferentialFormSpace Ω VF] : Type u_1

Provides a compatible $\mathbb{C}$-module structure on each $\Omega^p$ via scalar-tower with $\mathbb{R}$, used for complex-valued differential forms.

• instComplexModule (p : ℕ) : Module ℂ (Ω p)
• instScalarTower (p : ℕ) : IsScalarTower ℝ ℂ (Ω p)
• instSMulCommClass (p : ℕ) : SMulCommClass ℝ ℂ (Ω p)

theorem DifferentialFormSpace.fMul_zero {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] {p : ℕ} (f : Ω 0) : fMul VF f 0 = 0

Multiplication of a function by the zero $p$-form yields zero: $f \cdot 0 = 0$.

theorem DifferentialFormSpace.d_zero_val {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] {p : ℕ} : d VF 0 = 0

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

theorem DifferentialFormSpace.ι_zero_val {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] (X : VF) {p : ℕ} : ι X 0 = 0

Interior product with the zero form is zero: $\iota_X 0 = 0$.

theorem DifferentialFormSpace.d_neg {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] {p : ℕ} (α : Ω p) : d VF (-α) = -d VF α

The exterior derivative commutes with negation: $d(-\alpha) = -d\alpha$.

theorem DifferentialFormSpace.cartan_step {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] (X : VF) {p : ℕ} (ih : ∀ (γ : Ω p), d VF (L X γ) = d VF (ι X (d VF γ))) (β : Ω (p + 1)) : L X β = d VF (ι X β) + ι X (d VF β)

Inductive step in the proof of Cartan's magic formula: from the relation $d(\mathcal{L}_X \gamma) = d(\iota_X d\gamma)$ at degree $p$, deduce $\mathcal{L}_X \beta = d(\iota_X \beta) + \iota_X(d\beta)$ at degree $p+1$.

theorem DifferentialFormSpace.cartan_formula {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] (X : VF) {p : ℕ} (α : Ω (p + 1)) : L X α = d VF (ι X α) + ι X (d VF α)

Cartan's magic formula: $\mathcal{L}_X \alpha = d(\iota_X \alpha) + \iota_X(d\alpha)$ on any differential form.

def DifferentialFormSpace.IsClosed' {Ω : ℕ → Type u_1} (VF : Type u_3) [inst : DifferentialFormSpace Ω VF] {p : ℕ} (α : Ω p) : Prop

A differential form $\alpha$ is closed when $d\alpha = 0$.

def DifferentialFormSpace.IsExact' {Ω : ℕ → Type u_1} (VF : Type u_3) [inst : DifferentialFormSpace Ω VF] {p : ℕ} (α : Ω (p + 1)) : Prop

A differential $(p+1)$-form $\alpha$ is exact when $\alpha = d\beta$ for some $p$-form $\beta$.

theorem DifferentialFormSpace.exact_is_closed {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] {p : ℕ} (α : Ω (p + 1)) (h : IsExact' VF α) : IsClosed' VF α

Every exact form is closed, since $d^2 = 0$.

def DifferentialFormSpace.deRhamSetoid {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] (p : ℕ) : Setoid { α : Ω (p + 1) // IsClosed' VF α }

The setoid on closed $(p+1)$-forms whose quotient yields the de Rham cohomology $H^{p+1}_{dR}$: $\alpha \sim \beta$ iff $\alpha - \beta$ is exact.

class IsEuclideanDFS (Ω : ℕ → Type u_1) (VF : Type u_2) [inst : DifferentialFormSpace Ω VF] : Type

Marker class for a differential form space modelled on Euclidean space of positive dimension dim.

• dim : ℕ
• dim_pos : 0 < dim Ω VF

theorem poincare_homotopy_operator_axiom {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] [IsEuclideanDFS Ω VF] : ∃ (K : (p : ℕ) → Ω (p + 1) → Ω p), (∀ (p : ℕ) (α : Ω (p + 1)), DifferentialFormSpace.d VF (K p α) + K (p + 1) (DifferentialFormSpace.d VF α) = α) ∧ ∀ (p : ℕ), K p 0 = 0

Poincaré homotopy operator on Euclidean space: there exist linear maps $K_p : \Omega^{p+1} \to \Omega^p$ satisfying $dK + Kd = \mathrm{id}$ and $K\,0 = 0$.

theorem poincare_lemma {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] [eucl : IsEuclideanDFS Ω VF] {p : ℕ} (α : Ω (p + 1)) (hclosed : DifferentialFormSpace.IsClosed' VF α) : DifferentialFormSpace.IsExact' VF α

Poincaré lemma: on Euclidean space, every closed differential form is exact.

structure DFSMorphism (Ω₁ : ℕ → Type u_1) (VF₁ : Type u_2) (Ω₂ : ℕ → Type u_3) (VF₂ : Type u_4) [inst₁ : DifferentialFormSpace Ω₁ VF₁] [inst₂ : DifferentialFormSpace Ω₂ VF₂] : Type (max u_1 u_3)

A morphism of differential form spaces: a pullback on forms that is linear and commutes with the exterior derivative.

• pullback {p : ℕ} : Ω₂ p → Ω₁ p
• pullback_add {p : ℕ} (α β : Ω₂ p) : self.pullback (α + β) = self.pullback α + self.pullback β
• pullback_smul {p : ℕ} (r : ℝ) (α : Ω₂ p) : self.pullback (r • α) = r • self.pullback α
• pullback_comm_d {p : ℕ} (α : Ω₂ p) : self.pullback (DifferentialFormSpace.d VF₂ α) = DifferentialFormSpace.d VF₁ (self.pullback α)

theorem DFSMorphism.pullback_closed {Ω₁ : ℕ → Type u_1} {VF₁ : Type u_2} {Ω₂ : ℕ → Type u_3} {VF₂ : Type u_4} [inst₁ : DifferentialFormSpace Ω₁ VF₁] [inst₂ : DifferentialFormSpace Ω₂ VF₂] (φ : DFSMorphism Ω₁ VF₁ Ω₂ VF₂) {p : ℕ} (α : Ω₂ p) (h : DifferentialFormSpace.IsClosed' VF₂ α) : DifferentialFormSpace.IsClosed' VF₁ (φ.pullback α)

The pullback of a closed form along a morphism of differential form spaces is closed.

theorem DFSMorphism.pullback_exact {Ω₁ : ℕ → Type u_1} {VF₁ : Type u_2} {Ω₂ : ℕ → Type u_3} {VF₂ : Type u_4} [inst₁ : DifferentialFormSpace Ω₁ VF₁] [inst₂ : DifferentialFormSpace Ω₂ VF₂] (φ : DFSMorphism Ω₁ VF₁ Ω₂ VF₂) {p : ℕ} (α : Ω₂ (p + 1)) (h : DifferentialFormSpace.IsExact' VF₂ α) : DifferentialFormSpace.IsExact' VF₁ (φ.pullback α)

The pullback of an exact form along a morphism of differential form spaces is exact.

def DFSMorphism.id {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] : DFSMorphism Ω VF Ω VF

The identity morphism of differential form spaces, with trivial pullback.

@[simp]

theorem DFSMorphism.id_pullback {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] {p : ℕ} (α : Ω p) : id.pullback α = α

The identity DFS-morphism acts as the identity on forms.