Maps that preserve a form in charts, and the top-form measures they preserve

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

TopFormMeasure.lean's invariance theorem topFormMeasure_map_eq takes its hypothesis in chart form: through any two charts, the map is differentiable and pulls the local representative of the form back to itself. This module names that hypothesis and gives it the closure properties that let a product manifold inherit it from its factors:

• DifferentialForm.PreservesLocalRep s g — g^* s = s, read in charts;
• preservesLocalRep_id — the identity preserves every family (the chart-change rule localRep_transition);
• PreservesLocalRep.wedgePow — a map preserving a 2-form preserves its iterated powers;
• ★ PreservesLocalRep.map_topFormMeasure — a homeomorphism preserving a top form in charts preserves its measure (topFormMeasure_map_eq, repackaged);
• ★ PreservesLocalRep.prodMap — a product of chart-preserving maps preserves the product family π₁^* α + π₂^* β on the product charted over E × F;
• IsChartTranslation E g — the chart expression of g has derivative the identity; IsChartTranslation.prodMap; preservesLocalRep_constFamily (on a translation atlas a chart translation preserves every constant family); ★ AddCircle.isChartTranslation_addLeft (translation of the circle is a chart translation of the translation atlas).

Honest scope

⚠️ Chart-level, not intrinsic. PreservesLocalRep is the chart form of "g is a symplectomorphism"; the pullback of a form along a map of manifolds is not built here, so no bundle-level statement g^* α = α is made.

⚠️ Self models only, inherited from ExteriorDerivative.lean.

References: Geometry/Manifold/TopFormMeasure.lean (topFormMeasure_map_eq); Geometry/Manifold/ProductForm.lean (localRep_prodFamily, prodSum_compContinuousLinearMap_prodMap); Geometry/Manifold/TranslationAtlasForm.lean (localRep_constFamily); Geometry/Manifold/Instances/AddCircleTranslation.lean (hasFDerivAt_transition); specs/BACKLOG.md (#29); specs/future-work.md.

The predicate

def DifferentialForm.PreservesLocalRep {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {M : Type u_2} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf ℝ E) (↑⊤) M] {G : Type u_3} [NormedAddCommGroup G] [NormedSpace ℝ G] {ι : Type u_4} [Fintype ι] (s : (x : M) → TangentSpace (modelWithCornersSelf ℝ E) x [⋀^ι]→L[ℝ] Bundle.Trivial M G x) (g : M → M) : Prop

g preserves the family s in charts (g^* s = s, read through any two charts): where the chart expression of g is defined it is differentiable, and the pullback of the local representative of s along its derivative is the local representative of s. This is the hypothesis topFormMeasure_map_eq reads.

Equations

• One or more equations did not get rendered due to their size.

theorem DifferentialForm.preservesLocalRep_id {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {M : Type u_2} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf ℝ E) (↑⊤) M] {G : Type u_3} [NormedAddCommGroup G] [NormedSpace ℝ G] {ι : Type u_4} [Fintype ι] (s : (x : M) → TangentSpace (modelWithCornersSelf ℝ E) x [⋀^ι]→L[ℝ] Bundle.Trivial M G x) : PreservesLocalRep s id

The identity preserves every family: the chart-change rule for local representatives.

theorem DifferentialForm.PreservesLocalRep.wedgePow {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {M : Type u_2} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf ℝ E) (↑⊤) M] {α : DifferentialForm (modelWithCornersSelf ℝ E) M (↑⊤) (Fin 2) ℝ} {g : M → M} (h : PreservesLocalRep (fun (x : M) => α x) g) (k : ℕ) : PreservesLocalRep (fun (x : M) => (α.wedgePow k) x) g

The iterated powers of a preserved 2-form are preserved.

theorem DifferentialForm.PreservesLocalRep.map_topFormMeasure {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {M : Type u_2} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf ℝ E) (↑⊤) M] {ι : Type u_4} [Fintype ι] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [MeasurableSpace M] [BorelSpace M] [DecidableEq ι] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] (e : Module.Basis ι ℝ E) {s : (x : M) → TangentSpace (modelWithCornersSelf ℝ E) x [⋀^ι]→L[ℝ] Bundle.Trivial M ℝ x} (c : ChartCover E M) (g : M ≃ₜ M) (h : PreservesLocalRep s ⇑g) : MeasureTheory.Measure.map (⇑g) (topFormMeasure μ e s c) = topFormMeasure μ e s c

★ A homeomorphism preserving a top-form family in charts preserves its measure.

Products

theorem DifferentialForm.PreservesLocalRep.prodMap {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] {G : Type u_5} [NormedAddCommGroup G] [NormedSpace ℝ G] {ι : Type u_6} [Fintype ι] {α : (x : M) → TangentSpace (modelWithCornersSelf ℝ E) x [⋀^ι]→L[ℝ] Bundle.Trivial M G x} {β : (y : N) → TangentSpace (modelWithCornersSelf ℝ F) y [⋀^ι]→L[ℝ] Bundle.Trivial N G y} {g₁ : M → M} {g₂ : N → N} (h₁ : PreservesLocalRep α g₁) (h₂ : PreservesLocalRep β g₂) : PreservesLocalRep (prodFamily α β) (Prod.map g₁ g₂)

★ A product of chart-preserving maps preserves the product family π₁^* α + π₂^* β, on the product charted over E × F.

Chart translations

def DifferentialForm.IsChartTranslation (E : Type u_1) [NormedAddCommGroup E] [NormedSpace ℝ E] {M : Type u_2} [TopologicalSpace M] [ChartedSpace E M] (g : M → M) : Prop

g is a translation in charts: through any two charts, its chart expression has derivative the identity wherever it is defined.

Equations

• One or more equations did not get rendered due to their size.

theorem DifferentialForm.preservesLocalRep_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) {g : M → M} (hg : IsChartTranslation E g) : PreservesLocalRep (constFamily ξ) g

On a translation atlas, a chart translation preserves every constant family.

theorem DifferentialForm.IsChartTranslation.prodMap {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {M : Type u_2} [TopologicalSpace M] [ChartedSpace E M] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace ℝ F] {N : Type u_4} [TopologicalSpace N] [ChartedSpace F N] {g₁ : M → M} {g₂ : N → N} (h₁ : IsChartTranslation E g₁) (h₂ : IsChartTranslation F g₂) : IsChartTranslation (E × F) (Prod.map g₁ g₂)

The product of two chart translations is a chart translation, for the product charted over E × F.

Translation of the circle

theorem AddCircle.isChartTranslation_addLeft {T : ℝ} [hT : Fact (0 < T)] (θ : AddCircle T) : DifferentialForm.IsChartTranslation ℝ fun (x : AddCircle T) => θ + x

★ Translation of the circle is a chart translation of the translation atlas: read through two translation charts, x ↦ θ + x is a translation of ℝ near every point.