Constant forms on a translation atlas, and the area form of the torus

Category: 1-Mathlib (CSD-free; upstream target Mathlib.Geometry.Manifold).

A form on a manifold is a family of alternating maps on the tangent spaces with a smoothness condition read through the charts. When every chart transition is a translation, the tangent coordinate changes are all the identity, and a constant alternating map on the model is a global smooth form whose local representative in every chart is that constant. This module says that once, as a predicate on the atlas, and then reads the torus's area form off it.

• HasTranslationAtlas E M — the derivative of every chart transition is the identity, at every point where the local-representative machinery of ExteriorDerivative.lean reads it. Instances: AddCircle T charted by translation (Instances/AddCircleTranslation.lean), a product of two such (ProductSelfModel.lean), and a normed space charted on itself (instHasTranslationAtlasSelf, the case a form on a rectangle is read in);
• DifferentialForm.constForm ξ — the constant family as a C^∞ ι-form, with ★ localRep_constForm (its local representative in every chart is ξ) and ★ constForm_mextDeriv (it is closed: the flat d of a constant is zero);
• areaForm — the area form (u, v) ↦ u₁ v₂ − u₂ v₁ on ℝ × ℝ, as a continuous alternating 2-form, with areaForm_nondegenerate;
• ★★ torusAreaForm — the area form dθ₁ ∧ dθ₂ on AddCircle T × AddCircle T', a term of DifferentialForm 𝓘(ℝ, ℝ × ℝ) (AddCircle T × AddCircle T') ∞ (Fin 2) ℝ, and ★★ torusAreaForm_isSymplectic — the torus is a symplectic manifold;
• AddCircle.translationChartCover (two charts cover the circle) and AddCircle.hasMFDerivAt_coe_comp (a real curve pushed to the circle has the curve's derivative).

Honest scope

⚠️ Nothing is said about the torus's stereographic structure (Instances/AddCircle.lean); the symplectic torus here is the one charted by translation, over the model ℝ × ℝ.

⚠️ No volume identity. That torusAreaForm integrates to the Haar measure of the torus is not stated; the corpus's torus measure stays the product Haar measure it always was. (The area T · T' of a translation chart target, and the top power of torusAreaForm summed with the Fubini–Study form on a product chart, are Instances/ProjectiveSpaceTorusVolume.lean.)

References: Geometry/Manifold/ExteriorDerivative.lean (localRep, trivializationAt_snd, mextDeriv); Geometry/Manifold/SymplecticForm.lean (IsSymplectic); Geometry/Manifold/Instances/ProjectiveSpaceFubiniStudyForm.lean (the same construction for the Fubini–Study form, where the transitions are not translations and chart invariance is a theorem); Analysis/InnerProductSpace/KahlerClosed.lean (extDeriv_const_apply); specs/BACKLOG.md (R-016′).

Atlases whose transitions are translations

class HasTranslationAtlas (E : Type u_1) (M : Type u_2) [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace M] [ChartedSpace E M] : Prop

A translation atlas: the derivative of every chart transition is the identity, at every point where ExteriorDerivative.lean's local-representative machinery reads it.

• fderiv_chart_transition (x₀ y : M) : y ∈ (chartAt E x₀).source → fderiv ℝ (↑(chartAt E y) ∘ ↑(chartAt E x₀).symm) (↑(chartAt E x₀) y) = ContinuousLinearMap.id ℝ E

instance AddCircle.instHasTranslationAtlas {T : ℝ} [Fact (0 < T)] : HasTranslationAtlas ℝ (AddCircle T)

instance instHasTranslationAtlasSelf {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] : HasTranslationAtlas E E

A normed space charted on itself is a translation atlas: there is one chart and it is the identity, so every transition is the identity.

instance Prod.instHasTranslationAtlas {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {M : Type u_3} {N : Type u_4} [TopologicalSpace M] [ChartedSpace E M] [TopologicalSpace N] [ChartedSpace F N] [IsManifold (modelWithCornersSelf ℝ E) (↑⊤) M] [IsManifold (modelWithCornersSelf ℝ F) (↑⊤) N] [HasTranslationAtlas E M] [HasTranslationAtlas F N] : HasTranslationAtlas (E × F) (M × N)

A product of translation atlases is a translation atlas.

Constant forms

def DifferentialForm.constFamily {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {M : Type u_2} [TopologicalSpace M] [ChartedSpace E M] {G : Type u_3} [NormedAddCommGroup G] [NormedSpace ℝ G] {ι : Type u_4} (ξ : E [⋀^ι]→L[ℝ] G) (x : M) : TangentSpace (modelWithCornersSelf ℝ E) x [⋀^ι]→L[ℝ] Bundle.Trivial M G x

The constant family x ↦ ξ on the tangent spaces.

Equations

• DifferentialForm.constFamily ξ x = ξ

theorem DifferentialForm.constFamily_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {M : Type u_2} [TopologicalSpace M] [ChartedSpace E M] {G : Type u_3} [NormedAddCommGroup G] [NormedSpace ℝ G] {ι : Type u_4} (ξ : E [⋀^ι]→L[ℝ] G) (x : M) : constFamily ξ x = ξ

theorem DifferentialForm.trivializationAt_constFamily_snd {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {M : Type u_2} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf ℝ E) (↑⊤) M] [HasTranslationAtlas E M] {G : Type u_3} [NormedAddCommGroup G] [NormedSpace ℝ G] {ι : Type u_4} [Fintype ι] (ξ : E [⋀^ι]→L[ℝ] G) (x₀ y : M) (hy : y ∈ (chartAt E x₀).source) : (↑(trivializationAt (E [⋀^ι]→L[ℝ] G) (fun (x : M) => TangentSpace (modelWithCornersSelf ℝ E) x [⋀^ι]→L[ℝ] Bundle.Trivial M G x) x₀) ⟨y, constFamily ξ y⟩).2 = ξ

Through the tangent trivialisation at x₀, the constant family reads as the constant: the coordinate change is the identity on a translation atlas.

theorem DifferentialForm.localRep_constFamily {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {M : Type u_2} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf ℝ E) (↑⊤) M] [HasTranslationAtlas E M] {G : Type u_3} [NormedAddCommGroup G] [NormedSpace ℝ G] {ι : Type u_4} [Fintype ι] (ξ : E [⋀^ι]→L[ℝ] G) (x₀ : M) {w : E} (hw : w ∈ (chartAt E x₀).target) : localRep (constFamily ξ) x₀ w = ξ

★ The local representative of the constant family, in every chart, is the constant.

theorem DifferentialForm.contMDiff_constFamily {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {M : Type u_2} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf ℝ E) (↑⊤) M] [HasTranslationAtlas E M] {G : Type u_3} [NormedAddCommGroup G] [NormedSpace ℝ G] {ι : Type u_4} [Fintype ι] (ξ : E [⋀^ι]→L[ℝ] G) : ContMDiff (modelWithCornersSelf ℝ E) ((modelWithCornersSelf ℝ E).prod (modelWithCornersSelf ℝ (E [⋀^ι]→L[ℝ] G))) ↑⊤ fun (x : M) => ⟨x, constFamily ξ x⟩

The constant family is a C^∞ section.

def DifferentialForm.constForm {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {M : Type u_2} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf ℝ E) (↑⊤) M] [HasTranslationAtlas E M] {G : Type u_3} [NormedAddCommGroup G] [NormedSpace ℝ G] {ι : Type u_4} [Fintype ι] (ξ : E [⋀^ι]→L[ℝ] G) : DifferentialForm (modelWithCornersSelf ℝ E) M (↑⊤) ι G

★ The constant form x ↦ ξ on a manifold with a translation atlas.

Equations

• DifferentialForm.constForm ξ = { toFun := DifferentialForm.constFamily ξ, contMDiff_toFun := ⋯ }

@[simp]

theorem DifferentialForm.constForm_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {M : Type u_2} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf ℝ E) (↑⊤) M] [HasTranslationAtlas E M] {G : Type u_3} [NormedAddCommGroup G] [NormedSpace ℝ G] {ι : Type u_4} [Fintype ι] (ξ : E [⋀^ι]→L[ℝ] G) (x : M) : (constForm ξ) x = ξ

theorem DifferentialForm.mextDerivFamily_constFamily {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {M : Type u_2} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf ℝ E) (↑⊤) M] [HasTranslationAtlas E M] {G : Type u_3} [NormedAddCommGroup G] [NormedSpace ℝ G] {k : ℕ} (ξ : E [⋀^Fin k]→L[ℝ] G) (x : M) : mextDerivFamily (constFamily ξ) x = 0

The constant form is closed, pointwise: its local representative near the chart image of x is the constant, whose flat d is zero.

theorem DifferentialForm.constForm_mextDeriv {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {M : Type u_2} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf ℝ E) (↑⊤) M] [HasTranslationAtlas E M] {G : Type u_3} [NormedAddCommGroup G] [NormedSpace ℝ G] {k : ℕ} (ξ : E [⋀^Fin k]→L[ℝ] G) : (constForm ξ).mextDeriv = 0

★ The constant form is closed.

The area form on ℝ × ℝ

def TorusForm.area (u v : ℝ × ℝ) : ℝ

The area pairing (u, v) ↦ u₁ v₂ − u₂ v₁ on ℝ × ℝ.

Equations

• TorusForm.area u v = u.1 * v.2 - u.2 * v.1

theorem TorusForm.area_self (u : ℝ × ℝ) : area u u = 0

theorem TorusForm.area_swap (u v : ℝ × ℝ) : area u v = -area v u

theorem TorusForm.abs_area_le (u v : ℝ × ℝ) : |area u v| ≤ 2 * (‖u‖ * ‖v‖)

def TorusForm.areaBilin : ℝ × ℝ →ₗ[ℝ] ℝ × ℝ →ₗ[ℝ] ℝ

The area pairing as a bilinear map.

Equations

• TorusForm.areaBilin = LinearMap.mk₂ ℝ TorusForm.area ⋯ ⋯ ⋯ ⋯

noncomputable def TorusForm.areaCLM : ℝ × ℝ →L[ℝ] ℝ × ℝ →L[ℝ] ℝ

The area pairing as a continuous bilinear map.

Equations

• TorusForm.areaCLM = TorusForm.areaBilin.mkContinuous₂ 2 ⋯

@[simp]

theorem TorusForm.areaCLM_apply (u v : ℝ × ℝ) : (areaCLM u) v = area u v

noncomputable def TorusForm.areaMulti : ℝ × ℝ [×2]→L[ℝ] ℝ

The area pairing as a continuous multilinear map on Fin 2 → ℝ × ℝ.

Equations

• TorusForm.areaMulti = ((continuousMultilinearCurryFin1 ℝ (ℝ × ℝ) ℝ).symm.toLinearIsometry.toContinuousLinearMap ∘SL TorusForm.areaCLM).uncurryLeft

@[simp]

theorem TorusForm.areaMulti_apply (v : Fin 2 → ℝ × ℝ) : areaMulti v = area (v 0) (v 1)

noncomputable def TorusForm.areaForm : (ℝ × ℝ) [⋀^Fin 2]→L[ℝ] ℝ

★ The area form dx ∧ dy on ℝ × ℝ, as a continuous alternating 2-form.

Equations

• TorusForm.areaForm = { toContinuousMultilinearMap := TorusForm.areaMulti, map_eq_zero_of_eq' := TorusForm.areaForm._proof_1 }

@[simp]

theorem TorusForm.areaForm_apply (v : Fin 2 → ℝ × ℝ) : areaForm v = area (v 0) (v 1)

theorem TorusForm.areaForm_nondegenerate {v : ℝ × ℝ} (hv : v ≠ 0) : ∃ (w : ℝ × ℝ), areaForm ![v, w] ≠ 0

★ The area form is non-degenerate: a nonzero vector pairs non-trivially with its quarter turn.

A two-chart cover of the circle

theorem AddCircle.coe_half_ne_zero {T : ℝ} [hT : Fact (0 < T)] : ↑(T / 2) ≠ 0

theorem AddCircle.cutPoint_zero {T : ℝ} [hT : Fact (0 < T)] : cutPoint 0 = T / 2

theorem AddCircle.cutPoint_coe_half {T : ℝ} [hT : Fact (0 < T)] : cutPoint ↑(T / 2) = T

noncomputable def AddCircle.translationChartCover {T : ℝ} [hT : Fact (0 < T)] : ChartCover ℝ (AddCircle T)

Two translation charts cover the circle: the ones with cut points T/2 and T ≡ 0.

Equations

• AddCircle.translationChartCover = { m := 2, pt := ![0, ↑(T / 2)], cover := ⋯ }

Curves on the circle

theorem AddCircle.hasMFDerivAt_coe_comp {T : ℝ} [Fact (0 < T)] {g : ℝ → ℝ} {g' s : ℝ} (hg : HasDerivAt g g' s) : HasMFDerivAt% (fun (u : ℝ) => ↑(g u)) s (ContinuousLinearMap.smulRight 1 g')

A real curve pushed to the circle: the manifold derivative is the curve's derivative (hasMFDerivAt_coe composed with the curve).

The torus as a symplectic manifold

noncomputable def AddCircle.torusAreaForm {T T' : ℝ} [Fact (0 < T)] [Fact (0 < T')] : DifferentialForm (modelWithCornersSelf ℝ (ℝ × ℝ)) (AddCircle T × AddCircle T') (↑⊤) (Fin 2) ℝ

★★ The area form dθ₁ ∧ dθ₂ on the torus AddCircle T × AddCircle T', charted by translation over ℝ × ℝ: the constant form with model areaForm.

Equations

• AddCircle.torusAreaForm = DifferentialForm.constForm TorusForm.areaForm

@[simp]

theorem AddCircle.torusAreaForm_apply {T T' : ℝ} [Fact (0 < T)] [Fact (0 < T')] (x : AddCircle T × AddCircle T') : torusAreaForm x = TorusForm.areaForm

theorem AddCircle.torusAreaForm_isSymplectic {T T' : ℝ} [Fact (0 < T)] [Fact (0 < T')] : torusAreaForm.IsSymplectic

★★ The torus is a symplectic manifold: the area form is closed (it is constant in every chart) and non-degenerate (it is the area form).