The abstract torus layer: V ⧸ L for L : AddSubgroup V

Unit: jacobian-construction (docs/design/jacobian-construction.md §3–§9). This is the reusable core of the whole unit: for a complex normed space V (always instantiated at Fin n → ℂ) and an additive subgroup L, we build:

• AddCommGroup/TopologicalSpace/T2Space (V ⧸ L) — for every L, no discreteness needed (§3, the T2-via-closure trick, spiked).
• ChartedSpace V (V ⧸ L) / IsManifold 𝓘(ℂ, V) ω (V ⧸ L) — needs [DiscreteTopology L] (§4). Charts are raw representative charts: chartAt' L x sends a class near x to its unique representative in a fixed injectivity ball around x (a simplification of the design's "centered" charts — the transition maps are still exactly translations by a locally-constant lattice element, which is all that is needed; no recentering bookkeeping required).
• LieAddGroup 𝓘(ℂ, V) ω (V ⧸ L) — same hypothesis (§5): in the raw charts, addition/negation read as translation by a (possibly nonzero, but always locally-constant) lattice element, hence affine, hence analytic.
• CompactSpace (V ⧸ L) — needs the full IsZLattice ℝ L (§6, the IsZLattice.isCompact_range_of_periodic trick, spiked).
• The →ₜ+ functoriality substrate inducedHom (§9.2, spiked) and its ContMDiff-ness (§9.3).

These are genuine theorems/instances gated by typeclass hypotheses ([DiscreteTopology L], [IsZLattice ℝ L]); Lean cannot discharge these hypotheses for an arbitrary L, so they only fire once a caller supplies them — which is exactly the hook period-lattice-rank uses once it establishes discreteness/full-rank for the actual period subgroup.

§3. Free instances: AddCommGroup/TopologicalSpace/T2Space, no hypotheses at all

@[instance_reducible]

instance RS.instAddCommGroupQuotient {V : Type u_1} [NormedAddCommGroup V] (L : AddSubgroup V) : AddCommGroup (V ⧸ L)

Equations

• RS.instAddCommGroupQuotient L = inferInstance

@[instance_reducible]

instance RS.instTopologicalSpaceQuotient {V : Type u_1} [NormedAddCommGroup V] (L : AddSubgroup V) : TopologicalSpace (V ⧸ L)

Equations

• RS.instTopologicalSpaceQuotient L = inferInstance

instance RS.instT2SpaceQuotientTopologicalClosure {V : Type u_1} [NormedAddCommGroup V] (L : AddSubgroup V) : T2Space (V ⧸ L.topologicalClosure)

The quotient of V by the topological closure of any additive subgroup is Hausdorff — for every subgroup, no discreteness or full-rank input at all. This is what lets Jac₀ X := (Fin (genus X) → ℂ) ⧸ (periodSubgroup X).topologicalClosure be T2Space immediately, including at genus X = 0.

§4.1. Uniform injectivity radius

theorem RS.exists_uniform_injRadius {V : Type u_1} [NormedAddCommGroup V] (L : AddSubgroup V) [DiscreteTopology ↥L] : ∃ (ρ : ℝ), 0 < ρ ∧ ∀ ℓ ∈ L, ℓ ≠ 0 → 2 * ρ ≤ ‖ℓ‖

Every discrete additive subgroup of a normed space has a uniform injectivity radius: some ρ > 0 such that every nonzero element has norm at least 2ρ.

noncomputable def RS.injRadius {V : Type u_1} [NormedAddCommGroup V] (L : AddSubgroup V) [DiscreteTopology ↥L] : ℝ

A choice of uniform injectivity radius for L.

Equations

• RS.injRadius L = ⋯.choose

theorem RS.injRadius_pos {V : Type u_1} [NormedAddCommGroup V] (L : AddSubgroup V) [DiscreteTopology ↥L] : 0 < injRadius L

theorem RS.norm_le_of_mem_injRadius {V : Type u_1} [NormedAddCommGroup V] (L : AddSubgroup V) [DiscreteTopology ↥L] {ℓ : V} (hℓ : ℓ ∈ L) (hne : ℓ ≠ 0) : 2 * injRadius L ≤ ‖ℓ‖

theorem RS.mk_injOn_ball {V : Type u_1} [NormedAddCommGroup V] (L : AddSubgroup V) [DiscreteTopology ↥L] (x : V) : Set.InjOn QuotientAddGroup.mk (Metric.ball x (injRadius L))

QuotientAddGroup.mk is injective on any ball of radius injRadius L.

§4.2. The raw representative chart family

noncomputable def RS.rawChartAux {V : Type u_1} [NormedAddCommGroup V] (L : AddSubgroup V) [DiscreteTopology ↥L] (x : V) : OpenPartialHomeomorph V (V ⧸ L)

The auxiliary chart going V → V ⧸ L: mk restricted to the injectivity ball around x, which is a continuous open injection, hence (by ofContinuousOpen) an OpenPartialHomeomorph.

Equations

• RS.rawChartAux L x = OpenPartialHomeomorph.ofContinuousOpen (Set.InjOn.toPartialEquiv QuotientAddGroup.mk (Metric.ball x (RS.injRadius L)) ⋯) ⋯ ⋯ ⋯

@[simp]

theorem RS.rawChartAux_apply {V : Type u_1} [NormedAddCommGroup V] (L : AddSubgroup V) [DiscreteTopology ↥L] (x z : V) : ↑(rawChartAux L x) z = ↑z

@[simp]

theorem RS.rawChartAux_source {V : Type u_1} [NormedAddCommGroup V] (L : AddSubgroup V) [DiscreteTopology ↥L] (x : V) : (rawChartAux L x).source = Metric.ball x (injRadius L)

noncomputable def RS.chartAt' {V : Type u_1} [NormedAddCommGroup V] (L : AddSubgroup V) [DiscreteTopology ↥L] (x : V) : OpenPartialHomeomorph (V ⧸ L) V

The chart at representative x : V: sends a class near x to its unique representative in ball x (injRadius L).

Equations

• RS.chartAt' L x = (RS.rawChartAux L x).symm

@[simp]

theorem RS.chartAt'_symm {V : Type u_1} [NormedAddCommGroup V] (L : AddSubgroup V) [DiscreteTopology ↥L] (x : V) : (chartAt' L x).symm = rawChartAux L x

@[simp]

theorem RS.chartAt'_source {V : Type u_1} [NormedAddCommGroup V] (L : AddSubgroup V) [DiscreteTopology ↥L] (x : V) : (chartAt' L x).source = QuotientAddGroup.mk '' Metric.ball x (injRadius L)

@[simp]

theorem RS.chartAt'_target {V : Type u_1} [NormedAddCommGroup V] (L : AddSubgroup V) [DiscreteTopology ↥L] (x : V) : (chartAt' L x).target = Metric.ball x (injRadius L)

theorem RS.chartAt'_apply_mk {V : Type u_1} [NormedAddCommGroup V] (L : AddSubgroup V) [DiscreteTopology ↥L] {x z : V} (hz : z ∈ Metric.ball x (injRadius L)) : ↑(chartAt' L x) ↑z = z

The defining property of chartAt': on a representative z inside the ball, the chart recovers z.

theorem RS.chartAt'_eq_add_of_mem_ball {V : Type u_1} [NormedAddCommGroup V] (L : AddSubgroup V) [DiscreteTopology ↥L] {x' w ℓ : V} (hℓ : ℓ ∈ L) (hmem : w + ℓ ∈ Metric.ball x' (injRadius L)) : ↑(chartAt' L x') ↑w = w + ℓ

If w + ℓ lands in the ball around x' for some ℓ ∈ L, the chart at x' reads the class of w as w + ℓ. This is the single computation underlying every transition/smoothness proof below.

theorem RS.chartAt'_eventuallyEq_add {V : Type u_1} [NormedAddCommGroup V] (L : AddSubgroup V) [DiscreteTopology ↥L] {x' w ℓ : V} (hℓ : ℓ ∈ L) (hmem : w + ℓ ∈ Metric.ball x' (injRadius L)) : (fun (w : V) => ↑(chartAt' L x') ↑w) =ᶠ[nhds w] fun (w : V) => w + ℓ

Local constancy: the identity chartAt' L x' (mk w) = w + ℓ persists on a whole neighborhood of w, for the same ℓ.

theorem RS.chartAt'_mem_source {V : Type u_1} [NormedAddCommGroup V] (L : AddSubgroup V) [DiscreteTopology ↥L] (q : V ⧸ L) : q ∈ (chartAt' L (Function.surjInv ⋯ q)).source

@[instance_reducible]

noncomputable instance RS.instChartedSpace {V : Type u_1} [NormedAddCommGroup V] (L : AddSubgroup V) [DiscreteTopology ↥L] : ChartedSpace V (V ⧸ L)

ChartedSpace V (V ⧸ L), given a discrete additive subgroup L.

Equations

• RS.instChartedSpace L = RS.chartedSpaceOfFamily' (RS.chartAt' L) (fun (q : V ⧸ L) => Function.surjInv ⋯ q) ⋯

@[simp]

theorem RS.chartAt_eq {V : Type u_1} [NormedAddCommGroup V] (L : AddSubgroup V) [DiscreteTopology ↥L] (q : V ⧸ L) : chartAt V q = chartAt' L (Function.surjInv ⋯ q)

theorem RS.extChartAt_apply_eq {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℂ V] (L : AddSubgroup V) [DiscreteTopology ↥L] (q q' : V ⧸ L) : ↑(extChartAt (modelWithCornersSelf ℂ V) q) q' = ↑(chartAt' L (Function.surjInv ⋯ q)) q'

The canonical chart at q, evaluated at any point, agrees with chartAt' at the same representative.

theorem RS.extChartAt_symm_apply_eq {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℂ V] (L : AddSubgroup V) [DiscreteTopology ↥L] (q : V ⧸ L) (w : V) : ↑(extChartAt (modelWithCornersSelf ℂ V) q).symm w = ↑w

theorem RS.extChartAt_self_eq {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℂ V] (L : AddSubgroup V) [DiscreteTopology ↥L] (q : V ⧸ L) : ↑(extChartAt (modelWithCornersSelf ℂ V) q) q = Function.surjInv ⋯ q

§4.3. IsManifold: transitions are translations by a locally-constant lattice element

theorem RS.analyticOnNhd_chartAt'_trans {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℂ V] (L : AddSubgroup V) [DiscreteTopology ↥L] (x x' : V) : AnalyticOnNhd ℂ (↑((chartAt' L x).symm.trans (chartAt' L x'))) ((chartAt' L x).symm.trans (chartAt' L x')).source

The transition map between two raw representative charts is analytic on its whole source (translation by a locally-constant lattice element). Exposed standalone (not just inside the IsManifold instance) so the ULift transport toolkit can reuse it verbatim.

instance RS.isManifold_torus {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℂ V] (L : AddSubgroup V) [DiscreteTopology ↥L] : IsManifold (modelWithCornersSelf ℂ V) ⊤ (V ⧸ L)

The torus V ⧸ L is an ω-manifold modelled on V (raw representative charts; transitions are translations by a locally-constant lattice element).

§5. LieAddGroup: addition/negation are affine in the raw charts

theorem RS.continuous_add_torus {V : Type u_1} [NormedAddCommGroup V] (L : AddSubgroup V) : Continuous fun (p : (V ⧸ L) × V ⧸ L) => p.1 + p.2

theorem RS.continuous_neg_torus {V : Type u_1} [NormedAddCommGroup V] (L : AddSubgroup V) : Continuous fun (q : V ⧸ L) => -q

theorem RS.contMDiff_add_torus {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℂ V] (L : AddSubgroup V) [DiscreteTopology ↥L] [CompleteSpace V] : ContMDiff ((modelWithCornersSelf ℂ V).prod (modelWithCornersSelf ℂ V)) (modelWithCornersSelf ℂ V) ⊤ fun (p : (V ⧸ L) × V ⧸ L) => p.1 + p.2

Addition on the torus is ω-smooth: in aligned raw charts (codomain chart representative chosen at a fixed lattice offset from the sum of the domain representatives), the chart composite is affine.

theorem RS.contMDiff_neg_torus {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℂ V] (L : AddSubgroup V) [DiscreteTopology ↥L] [CompleteSpace V] : ContMDiff (modelWithCornersSelf ℂ V) (modelWithCornersSelf ℂ V) ⊤ fun (q : V ⧸ L) => -q

Negation on the torus is ω-smooth: same affine-chart-composite argument as addition.

instance RS.lieAddGroup_torus {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℂ V] (L : AddSubgroup V) [DiscreteTopology ↥L] [CompleteSpace V] : LieAddGroup (modelWithCornersSelf ℂ V) ⊤ (V ⧸ L)

The torus V ⧸ L is an additive Lie group.

§6. CompactSpace, given the full-rank hypothesis

instance RS.compactSpace_torus {V : Type u_1} [NormedAddCommGroup V] (L : Submodule ℤ V) [DiscreteTopology ↥L] [NormedSpace ℝ V] [FiniteDimensional ℝ V] [IsZLattice ℝ L] : CompactSpace (V ⧸ L.toAddSubgroup)

The torus V ⧸ L.toAddSubgroup is compact, given that L is a full-rank ℤ-lattice (IsZLattice ℝ L): a periodic continuous map onto a normed space has compact range.

§9. The →ₜ+ functoriality substrate

def RS.inducedHom {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℂ V] {V' : Type u_2} [NormedAddCommGroup V'] [NormedSpace ℂ V'] [FiniteDimensional ℂ V] (L : AddSubgroup V) (L' : AddSubgroup V') (T : V →ₗ[ℂ] V') (hT : L ≤ AddSubgroup.comap T.toAddMonoidHom L') : V ⧸ L →ₜ+ V' ⧸ L'

The →ₜ+ functoriality substrate: a ℂ-linear map T : V →ₗ[ℂ] V' with L ≤ L'.comap T induces a continuous additive homomorphism on the quotients.

Equations

• RS.inducedHom L L' T hT = { toAddMonoidHom := QuotientAddGroup.map L L' T.toAddMonoidHom hT, continuous_toFun := ⋯ }

@[simp]

theorem RS.inducedHom_apply_mk {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℂ V] {V' : Type u_2} [NormedAddCommGroup V'] [NormedSpace ℂ V'] [FiniteDimensional ℂ V] {L : AddSubgroup V} {L' : AddSubgroup V'} {T : V →ₗ[ℂ] V'} (hT : L ≤ AddSubgroup.comap T.toAddMonoidHom L') (x : V) : (inducedHom L L' T hT) ↑x = ↑(T x)

theorem RS.analyticAt_linearMap {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℂ V] {V' : Type u_2} [NormedAddCommGroup V'] [NormedSpace ℂ V'] [FiniteDimensional ℂ V] (T : V →ₗ[ℂ] V') (x : V) : AnalyticAt ℂ (⇑T) x

Any ℂ-linear map between finite-dimensional normed spaces is entire (analytic at every point): it is continuous (finite-dimensional domain), hence bounded, hence its own convergent power series.

theorem RS.contMDiff_inducedHom {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℂ V] {V' : Type u_2} [NormedAddCommGroup V'] [NormedSpace ℂ V'] [CompleteSpace V'] [FiniteDimensional ℂ V] {L : AddSubgroup V} {L' : AddSubgroup V'} [DiscreteTopology ↥L] [DiscreteTopology ↥L'] {T : V →ₗ[ℂ] V'} (hT : L ≤ AddSubgroup.comap T.toAddMonoidHom L') : ContMDiff (modelWithCornersSelf ℂ V) (modelWithCornersSelf ℂ V') ⊤ ⇑(inducedHom L L' T hT)

The induced map on tori is ω-smooth, given discreteness of both lattices (needed for the manifold structure on either side; no further hypothesis on T/hT beyond linearity).

Functoriality of inducedHom (requested by jacobian-functoriality,

docs/requests/jacobian-construction.md)

theorem RS.inducedHom_id {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℂ V] [FiniteDimensional ℂ V] (L : AddSubgroup V) (hT : L ≤ AddSubgroup.comap LinearMap.id.toAddMonoidHom L) : inducedHom L L LinearMap.id hT = ContinuousAddMonoidHom.id (V ⧸ L)

inducedHom at the identity is the identity (QuotientAddGroup.map functoriality).

theorem RS.inducedHom_comp {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℂ V] {V' : Type u_2} [NormedAddCommGroup V'] [NormedSpace ℂ V'] [FiniteDimensional ℂ V] [FiniteDimensional ℂ V'] {V'' : Type u_3} [NormedAddCommGroup V''] [NormedSpace ℂ V''] (L : AddSubgroup V) (L' : AddSubgroup V') (L'' : AddSubgroup V'') (T : V →ₗ[ℂ] V') (T' : V' →ₗ[ℂ] V'') (hT : L ≤ AddSubgroup.comap T.toAddMonoidHom L') (hT' : L' ≤ AddSubgroup.comap T'.toAddMonoidHom L'') (hTT' : L ≤ AddSubgroup.comap (T' ∘ₗ T).toAddMonoidHom L'') : (inducedHom L' L'' T' hT').comp (inducedHom L L' T hT) = inducedHom L L'' (T' ∘ₗ T) hTT'

inducedHom is compositional (QuotientAddGroup.map functoriality).