AddCircle T charted by translation: the atlas whose transitions are translations

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

Instances/AddCircle.lean (Q33) makes AddCircle T a manifold over EuclideanSpace ℝ (Fin 1) by transport from Circle, whose charts are stereographic. That structure is the right one for "AddCircle T is a manifold"; it is the wrong one for writing down a form on the circle or the torus, because in stereographic coordinates the invariant form dθ is not constant and every chart transition is a Möbius map.

This module carries the second, classical structure: the translation atlas, modelled on ℝ itself. The chart with cut point a is the inverse of the quotient map on (a, a + T) (Mathlib's AddCircle.openPartialHomeomorphCoe, read backwards), and any two charts differ by a translation by a multiple of T on each component of their overlap. Consequently

• every transition is analytic (instIsManifoldReal, an IsManifold 𝓘(ℝ, ℝ) ω instance), and
• ★ fderiv_chart_transition — the derivative of every chart transition is the identity, which is what makes a constant alternating map a well-defined smooth form on the circle and on the torus (TranslationAtlasForm.lean).

The model is ℝ, not EuclideanSpace ℝ (Fin 1), so the two charted-space instances on AddCircle T are keyed on different model types and never compete.

Honest scope

⚠️ 0 < T is a Fact, as in Mathlib's equivIco. The corpus's torus KTorus has T = 1.

⚠️ Two atlases, no comparison. Nothing here relates the translation structure to the stereographic one of Instances/AddCircle.lean; they are both manifold structures on the same topological space, and a diffeomorphism between them is neither stated nor needed.

References: Mathlib/Topology/Instances/AddCircle/Defs.lean (openPartialHomeomorphCoe, equivIco, continuousAt_equivIco); Geometry/Manifold/Instances/AddCircle.lean (the stereographic structure); Geometry/Manifold/TranslationAtlasForm.lean (the consumer); specs/BACKLOG.md (R-016′).

The translation charts

noncomputable def AddCircle.translationChart {T : ℝ} [hT : Fact (0 < T)] (a : ℝ) : OpenPartialHomeomorph (AddCircle T) ℝ

The translation chart with cut point a: the inverse of the quotient map on (a, a + T). Its source is the circle minus the point a, its target the open interval (a, a + T).

Equations

• AddCircle.translationChart a = (AddCircle.openPartialHomeomorphCoe T a).symm

@[simp]

theorem AddCircle.translationChart_source {T : ℝ} [hT : Fact (0 < T)] (a : ℝ) : (translationChart a).source = {↑a}ᶜ

@[simp]

theorem AddCircle.translationChart_target {T : ℝ} [hT : Fact (0 < T)] (a : ℝ) : (translationChart a).target = Set.Ioo a (a + T)

theorem AddCircle.translationChart_apply {T : ℝ} [hT : Fact (0 < T)] (a : ℝ) (x : AddCircle T) : ↑(translationChart a) x = ↑((equivIco T a) x)

@[simp]

theorem AddCircle.translationChart_symm_apply {T : ℝ} [hT : Fact (0 < T)] (a y : ℝ) : ↑(translationChart a).symm y = ↑y

@[simp]

theorem AddCircle.coe_translationChart {T : ℝ} [hT : Fact (0 < T)] (a : ℝ) (x : AddCircle T) : ↑(↑(translationChart a) x) = x

The chart is a section of the quotient map.

theorem AddCircle.exists_translationChart_coe_eq {T : ℝ} [hT : Fact (0 < T)] (a y : ℝ) : ∃ (n : ℤ), ↑(translationChart a) ↑y = y + n • T

The chart value differs from any lift by a multiple of the period.

The cut point avoiding a given point, and the atlas

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

A cut point the point x avoids: half a period past the lift of x in [0, T).

Equations

• x.cutPoint = ↑((AddCircle.equivIco T 0) x) + T / 2

theorem AddCircle.ne_coe_cutPoint {T : ℝ} [hT : Fact (0 < T)] (x : AddCircle T) : x ≠ ↑x.cutPoint

@[instance_reducible]

noncomputable instance AddCircle.instChartedSpaceReal {T : ℝ} [hT : Fact (0 < T)] : ChartedSpace ℝ (AddCircle T)

★ AddCircle T charted by translation, modelled on ℝ.

Equations

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

theorem AddCircle.chartAt_eq {T : ℝ} [hT : Fact (0 < T)] (x : AddCircle T) : chartAt ℝ x = translationChart x.cutPoint

theorem AddCircle.mem_atlas_iff {T : ℝ} [hT : Fact (0 < T)] (e : OpenPartialHomeomorph (AddCircle T) ℝ) : e ∈ atlas ℝ (AddCircle T) ↔ ∃ (a : ℝ), translationChart a = e

Transitions are translations, locally

theorem AddCircle.transition_eq {T : ℝ} [hT : Fact (0 < T)] (a b : ℝ) : ↑(translationChart b) ∘ ↑(translationChart a).symm = fun (y : ℝ) => ↑(translationChart b) ↑y

The transition from the chart with cut a to the chart with cut b, as a function on ℝ: read the point back on the circle and out through the second chart. Cut a plays no role in the formula, only in the domain.

theorem AddCircle.continuousAt_transition {T : ℝ} [hT : Fact (0 < T)] (b : ℝ) {y₀ : ℝ} (hy₀ : ↑y₀ ≠ ↑b) : ContinuousAt (fun (y : ℝ) => ↑(translationChart b) ↑y) y₀

theorem AddCircle.zsmul_eq_of_abs_sub_lt {T : ℝ} [hT : Fact (0 < T)] {m n : ℤ} (h : |m • T - n • T| < T) : m = n

Two multiples of the period closer than the period are equal.

theorem AddCircle.transition_eventuallyEq {T : ℝ} [hT : Fact (0 < T)] (b : ℝ) {y₀ : ℝ} (hy₀ : ↑y₀ ≠ ↑b) : (fun (y : ℝ) => ↑(translationChart b) ↑y) =ᶠ[nhds y₀] fun (y : ℝ) => y + (↑(translationChart b) ↑y₀ - y₀)

★ A transition is a translation near every point of its domain.

theorem AddCircle.hasFDerivAt_transition {T : ℝ} [hT : Fact (0 < T)] (b : ℝ) {y₀ : ℝ} (hy₀ : ↑y₀ ≠ ↑b) : HasFDerivAt (fun (y : ℝ) => ↑(translationChart b) ↑y) (ContinuousLinearMap.id ℝ ℝ) y₀

theorem AddCircle.contDiffAt_transition {T : ℝ} [hT : Fact (0 < T)] (b : ℝ) {y₀ : ℝ} (hy₀ : ↑y₀ ≠ ↑b) : ContDiffAt ℝ ⊤ (fun (y : ℝ) => ↑(translationChart b) ↑y) y₀

instance AddCircle.instIsManifoldReal {T : ℝ} [hT : Fact (0 < T)] : IsManifold (modelWithCornersSelf ℝ ℝ) ⊤ (AddCircle T)

★ The translation atlas is analytic: AddCircle T is a C^ω manifold over ℝ.

theorem AddCircle.fderiv_chart_transition {T : ℝ} [hT : Fact (0 < T)] (x₀ y : AddCircle T) : fderiv ℝ (↑(chartAt ℝ y) ∘ ↑(chartAt ℝ x₀).symm) (↑(chartAt ℝ x₀) y) = ContinuousLinearMap.id ℝ ℝ

★ The derivative of every chart transition is the identity, in the form the local-representative machinery of ExteriorDerivative.lean reads it. No membership hypothesis is needed: a chart is a section of the quotient map on the whole circle, so the point read back is y itself, which avoids its own cut point.

The quotient map is a local diffeomorphism with derivative the identity

theorem AddCircle.hasMFDerivAt_coe {T : ℝ} [hT : Fact (0 < T)] (t : ℝ) : HasMFDerivAt% QuotientAddGroup.mk t (ContinuousLinearMap.id ℝ ℝ)

★ The quotient map ℝ → AddCircle T has manifold derivative the identity for the translation atlas: read through the chart at ↑t it is a translation near t.