AddCircle T is an analytic manifold, and so is the torus

Category: 1-Mathlib (CSD-free; upstream target Mathlib.Geometry.Manifold.Instances, beside Sphere.lean). Mathlib charts Circle (the unit complex numbers) and proves it an analytic Lie group, but AddCircle T = ℝ ⧸ ℤ • T — the type the corpus's torus fibre is built on — has no ChartedSpace at the pin, and Mathlib/Geometry/Manifold/Instances/Quotient.lean lists the quotient IsManifold as its own TODO.

Transport along a homeomorphism. For f : M ≃ₜ M' and a charted space M, the atlas { f.symm ≫ₕ e | e ∈ atlas M } charts M', and its transitions are exactly M's: (f.symm ≫ₕ e).symm ≫ₕ (f.symm ≫ₕ e') = e.symm ≫ₕ (f ≫ₕ f.symm) ≫ₕ e' = e.symm ≫ₕ e' on the nose (Homeomorph.symm_trans_self). So every groupoid M has, M' has (hasGroupoid_transport), and in particular IsManifold I n M' for every I, n. This is the general statement; nothing about the circle is used until the last section.

• Homeomorph.transportChartedSpace f — the transported charted space (a def, not an instance: a type may already carry a charted space);
• ★ Homeomorph.hasGroupoid_transport / isManifold_transport — the transported structure has every groupoid the source has; transitions are the source's transitions, on the nose (transport_transition).
• AddCircle.instChartedSpace, ★ AddCircle.instIsManifold — AddCircle T (T ≠ 0) is an analytic manifold, transported from Circle along AddCircle.homeomorphCircle.
• ★ AddCircle.instIsManifoldProd — the torus AddCircle T × AddCircle T' is an analytic manifold (Mathlib's product instance, once each factor is one).

Honest scope

⚠️ T ≠ 0 is a Fact. The homeomorphism AddCircle T ≃ₜ Circle needs T ≠ 0; the instance takes it as [Fact (T ≠ 0)], which Mathlib's AddCircle API already uses for T > 0 (Fact (0 < T) gives it). The corpus's fibre is AddCircle (1 : ℝ).

⚠️ Not stated: that homeomorphCircle itself is C^ω for the transported structure (it is the identity in charts, a one-line contMDiffAt_iff argument) — nothing consumes it.

⚠️ The transported atlas is not the "obvious" one. A reader expecting charts AddCircle T → ℝ from QuotientAddGroup.mk finds instead charts through Circle ⊂ ℂ into EuclideanSpace ℝ (Fin 1) (the stereographic charts of the unit sphere in ℂ). The model is 𝓡 1, not 𝓘(ℝ, ℝ). That is what Mathlib's Circle has, and the transport inherits it; a direct 𝓘(ℝ, ℝ) atlas would be a second instance and is not built.

References: specs/generator-layer-scoping.md §11 (Q33); specs/reconstruction-status.md §2a (A3); Mathlib/Geometry/Manifold/Instances/Sphere.lean (Circle's instances); Mathlib/Analysis/SpecialFunctions/Complex/Circle.lean (AddCircle.homeomorphCircle).

Transport of a charted space and its groupoids along a homeomorphism

@[instance_reducible]

def Homeomorph.transportChartedSpace {H : Type u_1} {M : Type u_2} {M' : Type u_3} [TopologicalSpace H] [TopologicalSpace M] [TopologicalSpace M'] [ChartedSpace H M] (f : M ≃ₜ M') : ChartedSpace H M'

The charted space on M' transported from M along f: the charts are f.symm ≫ₕ e for e a chart of M.

Equations

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

theorem Homeomorph.transport_transition {H : Type u_1} {M : Type u_2} {M' : Type u_3} [TopologicalSpace H] [TopologicalSpace M] [TopologicalSpace M'] (f : M ≃ₜ M') (e e' : OpenPartialHomeomorph M H) : (f.symm.toOpenPartialHomeomorph.trans e).symm.trans (f.symm.toOpenPartialHomeomorph.trans e') = e.symm.trans e'

The transitions of the transported atlas are the transitions of the source atlas, on the nose: f ≫ₕ f.symm cancels.

theorem Homeomorph.hasGroupoid_transport {H : Type u_1} {M : Type u_2} {M' : Type u_3} [TopologicalSpace H] [TopologicalSpace M] [TopologicalSpace M'] [ChartedSpace H M] (f : M ≃ₜ M') (G : StructureGroupoid H) [HasGroupoid M G] : HasGroupoid M' G

★ The transported structure has every groupoid the source has.

theorem Homeomorph.isManifold_transport {H : Type u_1} {M : Type u_2} {M' : Type u_3} [TopologicalSpace H] [TopologicalSpace M] [TopologicalSpace M'] [ChartedSpace H M] (f : M ≃ₜ M') {𝕜 : Type u_4} {E : Type u_5} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] (I : ModelWithCorners 𝕜 E H) (n : WithTop ℕ∞) [IsManifold I n M] : IsManifold I n M'

★ A manifold structure transports along a homeomorphism.

AddCircle T

@[instance_reducible]

noncomputable instance AddCircle.instChartedSpace {T : ℝ} [hT : Fact (T ≠ 0)] : ChartedSpace (EuclideanSpace ℝ (Fin 1)) (AddCircle T)

AddCircle T is charted by the stereographic charts of Circle ⊂ ℂ, through homeomorphCircle.

Equations

• AddCircle.instChartedSpace = (AddCircle.homeomorphCircle ⋯).symm.transportChartedSpace

instance AddCircle.instIsManifold {T : ℝ} [hT : Fact (T ≠ 0)] : IsManifold (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin 1))) ⊤ (AddCircle T)

★ AddCircle T is an analytic manifold.

The torus

instance AddCircle.instIsManifoldProd {T T' : ℝ} [Fact (T ≠ 0)] [Fact (T' ≠ 0)] : IsManifold ((modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin 1))).prod (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin 1)))) ⊤ (AddCircle T × AddCircle T')

★ The torus AddCircle T × AddCircle T' is an analytic manifold, modelled on EuclideanSpace ℝ (Fin 1) × EuclideanSpace ℝ (Fin 1). Mathlib's product instance, once each factor has one.