The ULift shell: transporting ChartedSpace/IsManifold/LieAddGroup along Homeomorph.ulift

Unit: jacobian-construction (docs/design/jacobian-construction.md §2, §7). The challenge's Jacobian X : Type u is universe-polymorphic in X, but the honest construction Jac₀ X := (Fin (genus X) → ℂ) ⧸ Λ lives in Type 0; Jacobian X := ULift.{u} (Jac₀ X) bridges the two. This file builds the (specialized, per design's R1 fallback) transport toolkit that moves ChartedSpace/IsManifold/LieAddGroup across Homeomorph.ulift : ULift (V ⧸ L) ≃ₜ V ⧸ L, for the same V, L as Torus.lean.

The key simplification throughout: ULift.up/ULift.down are an exact (not merely "eventual", unlike the lattice-shift business in Torus.lean) pair of mutually inverse continuous maps, so every chart composite involving them cancels by rfl. Consequently:

• ChartedSpace/IsManifold transport directly, reusing Torus.lean's analyticOnNhd_chartAt'_trans verbatim (the ULift-wrapped transition function/source agree exactly, not just up to congruence, with the unwrapped one).
• LieAddGroup transports via a cleaner route: ULift.down/ULift.up are themselves ω-smooth maps between ULift (V ⧸ L) and V ⧸ L (their chart composite, in matching charts at the same representative, is the identity on an open set), so addition/negation on ULift (V ⧸ L) factor through V ⧸ L's own contMDiff_add_torus/contMDiff_neg_torus by composition — no new analyticity computation.

ChartedSpace/IsManifold

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

The chart family for ULift (V ⧸ L): chartAt' L x, transported through Homeomorph.ulift.

Equations

• RS.uliftChartAt L x = Homeomorph.ulift.toOpenPartialHomeomorph.trans (RS.chartAt' L x)

theorem RS.uliftChartAt_mem_source {V : Type u_1} [NormedAddCommGroup V] (L : AddSubgroup V) [DiscreteTopology ↥L] (q : ULift.{u, u_1} (V ⧸ L)) : q ∈ (uliftChartAt L (Function.surjInv ⋯ q.down)).source

@[instance_reducible]

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

Equations

• RS.instChartedSpaceULift L = RS.chartedSpaceOfFamily' (RS.uliftChartAt L) (fun (q : ULift.{?u.2, ?u.1} (V ⧸ L)) => Function.surjInv ⋯ q.down) ⋯

theorem RS.chartAt_ulift_eq {V : Type u_1} [NormedAddCommGroup V] (L : AddSubgroup V) [DiscreteTopology ↥L] (q : ULift.{u, u_1} (V ⧸ L)) : chartAt V q = uliftChartAt L (Function.surjInv ⋯ q.down)

theorem RS.uliftChartAt_symm_apply {V : Type u_1} [NormedAddCommGroup V] (L : AddSubgroup V) [DiscreteTopology ↥L] (x w : V) : ↑(uliftChartAt L x).symm w = { down := ↑(chartAt' L x).symm w }

Homeomorph.ulift's associated OpenPartialHomeomorph.symm, precomposed into a uliftChartAt, cancels by rfl (PartialEquiv.coe_trans_symm).

theorem RS.uliftChartAt_target {V : Type u_1} [NormedAddCommGroup V] (L : AddSubgroup V) [DiscreteTopology ↥L] (x : V) : (uliftChartAt L x).target = (chartAt' L x).target

theorem RS.uliftChartAt_source' {V : Type u_1} [NormedAddCommGroup V] (L : AddSubgroup V) [DiscreteTopology ↥L] (x : V) : (uliftChartAt L x).source = ULift.down ⁻¹' (chartAt' L x).source

theorem RS.uliftChartAt_trans_eq {V : Type u_1} [NormedAddCommGroup V] (L : AddSubgroup V) [DiscreteTopology ↥L] (x x' : V) : ↑((uliftChartAt L x).symm.trans (uliftChartAt L x')) = ↑((chartAt' L x).symm.trans (chartAt' L x'))

The ULift-wrapped transition function agrees exactly with the unwrapped one (no neighborhood needed: ULift.up/.down cancel by rfl).

theorem RS.uliftChartAt_trans_source {V : Type u_1} [NormedAddCommGroup V] (L : AddSubgroup V) [DiscreteTopology ↥L] (x x' : V) : ((uliftChartAt L x).symm.trans (uliftChartAt L x')).source = ((chartAt' L x).symm.trans (chartAt' L x')).source

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

ULift (V ⧸ L) is an ω-manifold, by transporting Torus.lean's analyticOnNhd_chartAt'_trans exactly through the (rfl-cancelling) ULift wrapping.

ULift.down/ULift.up are ω-smooth

theorem RS.continuous_uliftDown {V : Type u_1} [NormedAddCommGroup V] (L : AddSubgroup V) : Continuous ULift.down

theorem RS.continuous_uliftUp {V : Type u_1} [NormedAddCommGroup V] (L : AddSubgroup V) : Continuous ULift.up

theorem RS.extChartAt_ulift_apply_eq {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℂ V] (L : AddSubgroup V) [DiscreteTopology ↥L] (q q' : ULift.{u, u_1} (V ⧸ L)) : ↑(extChartAt (modelWithCornersSelf ℂ V) q) q' = ↑(uliftChartAt L (Function.surjInv ⋯ q.down)) q'

theorem RS.extChartAt_ulift_symm_apply_eq {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℂ V] (L : AddSubgroup V) [DiscreteTopology ↥L] (q : ULift.{u, u_1} (V ⧸ L)) (w : V) : ↑(extChartAt (modelWithCornersSelf ℂ V) q).symm w = { down := ↑(chartAt' L (Function.surjInv ⋯ q.down)).symm w }

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

theorem RS.contMDiff_uliftDown {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℂ V] [CompleteSpace V] (L : AddSubgroup V) [DiscreteTopology ↥L] : ContMDiff (modelWithCornersSelf ℂ V) (modelWithCornersSelf ℂ V) ⊤ ULift.down

ULift.down is ω-smooth: in matching charts at the same representative, the composite is the identity on the (open) chart target.

theorem RS.contMDiff_uliftUp {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℂ V] [CompleteSpace V] (L : AddSubgroup V) [DiscreteTopology ↥L] : ContMDiff (modelWithCornersSelf ℂ V) (modelWithCornersSelf ℂ V) ⊤ ULift.up

ULift.up is ω-smooth: mirror-image argument to contMDiff_uliftDown.

LieAddGroup for ULift (V ⧸ L)

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

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

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