Normalized.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

Normalized test maps, slot regrouping, and unitary coordinate changes.

abbrev OAI.Kaplansky.TestNextCoordinates line 17

theorem OAI.Kaplansky.exists_test_coordinate_expanding_maps line 23

Source documentation

The actual 24-map expansion transported into the same concrete Hermitian coordinate bundles used by ordinary bundle normalization.

theorem exists_test_coordinate_expanding_maps {m R j : ℕ} (hm : 0<m) (hj : j<R) :
    ∃ T : ∀ y, Fin 24 → TestSourceCoordinates m R j hj y →ₗ[ℂ] TestNextCoordinates m R j hj y,
      (∀ i, Continuous (fun z : TotalSpace (Fin (testRank m R j) → ℂ) (TestSourceCoordinates m R j hj) =>
        TotalSpace.mk' (Fin (testRank m R (j+1)) → ℂ) z.proj (T z.proj i z.2))) ∧
      ∀ y, IntrinsicExpanding (T y) := by
…

Mentions: OAI.Kaplansky.TestSourceCoordinates, OAI.Kaplansky.TestNextCoordinates, OAI.Kaplansky.testRank, OAI.Kaplansky.IntrinsicExpanding

theorem OAI.Kaplansky.exists_test_normalized_maps line 46
def OAI.Kaplansky.testNextSlotEquiv line 71
theorem OAI.Kaplansky.testNextLabel_eq line 79
def OAI.Kaplansky.testNextStageTotalHomeomorph line 93
Source documentation
The regrouped target and E_{j+1} are isomorphic as actual topological bundles, not merely vector spaces of the same rank.
```
def testNextStageTotalHomeomorph (m R j : ℕ) (hj : j<R) :
    TotalSpace (EuclideanSpace ℂ (TestNextSlot m R j)) (smoothNextCore m R j hj).Fiber ≃ₜ
      TotalSpace (EuclideanSpace ℂ (TestBundleSlot m R (j+1)))
        (SmoothTestBundle m R (j+1) (j+1) hj (Nat.le_refl (j+1))) := by
…
```
Mentions: OAI.Kaplansky.TestNextSlot, OAI.Kaplansky.smoothNextCore, OAI.Kaplansky.TestBundleSlot, OAI.Kaplansky.SmoothTestBundle

def OAI.Kaplansky.finiteCoordinateUnitary line 121

Source documentation

The finite-coordinate change preserves the actual Hermitian metric and the actual total-space topology simultaneously.

def finiteCoordinateUnitary {S ι : Type*} [Fintype S] [Fintype ι]
    (K : ι → ℕ) (label : S → Option ι) (d : ℕ) (hd : Fintype.card S=d) :
    UnitaryBundleEquiv (EuclideanSpace ℂ S) (Fin d → ℂ)
      (SmoothLineSumBundle K label) (FiniteCoordinateBundle K label d hd) where
…

Mentions: OAI.Kaplansky.UnitaryBundleEquiv, OAI.Kaplansky.FiniteCoordinateBundle

def OAI.Kaplansky.lineSumReindexUnitary line 136

Source documentation

Reindexing an orthogonal line sum is unitary on fibers and continuous in both directions on the actual total space.

def lineSumReindexUnitary {B S T : Type*} [TopologicalSpace B] [Fintype S] [Fintype T]
    {J : S → Type*} (C : ∀ s, VectorBundleCore ℂ B ℂ (J s)) (e : T ≃ S) :
    UnitaryBundleEquiv (EuclideanSpace ℂ T) (EuclideanSpace ℂ S)
      (finiteLineSumCore (fun t => C (e t))).Fiber (finiteLineSumCore C).Fiber where
…

Mentions: OAI.Kaplansky.UnitaryBundleEquiv, OAI.Kaplansky.finiteLineSumCore

instance OAI.Kaplansky.smoothNext_norm line 146
instance OAI.Kaplansky.smoothNext_inner line 150
def OAI.Kaplansky.testNextStageUnitary line 156
Source documentation
The replacement-plus-fresh target is the standard next stage as an ordinary Hermitian bundle, so normalization survives this regrouping.
```
def testNextStageUnitary (m R j : ℕ) (hj : j<R) :
    UnitaryBundleEquiv (EuclideanSpace ℂ (TestNextSlot m R j))
      (EuclideanSpace ℂ (TestBundleSlot m R (j+1)))
      (smoothNextCore m R j hj).Fiber
      (SmoothTestBundle m R (j+1) (j+1) hj (Nat.le_refl (j+1))) := by
…
```
Mentions: OAI.Kaplansky.UnitaryBundleEquiv, OAI.Kaplansky.TestNextSlot, OAI.Kaplansky.TestBundleSlot, OAI.Kaplansky.smoothNextCore, OAI.Kaplansky.SmoothTestBundle
def OAI.Kaplansky.TestCoordinateStepType line 196