RealModel.lean`

17 declarations, 0 contain sorry, 0 declared as axioms

Real models of complex bundles and smooth finite line sums.

def OAI.Kaplansky.complexCoreReal line 23
Source documentation
Restrict scalars while retaining the original complex transition maps as functions, and hence the original bundle atlas and topology.
```
def complexCoreReal : VectorBundleCore ℝ B F J where
…
```
theorem OAI.Kaplansky.complexCoreReal_toFiberBundleCore line 35
instance OAI.Kaplansky.complexCoreFiberRealModule line 37
instance OAI.Kaplansky.complexCoreRealFiberComplexModule line 39
instance OAI.Kaplansky.complexCoreFiberRealVectorBundle line 42
instance OAI.Kaplansky.complexCoreRealFiberComplexVectorBundle line 45

theorem OAI.Kaplansky.complexCoreReal_isContMDiff line 50

Source documentation

Real-smooth complex transition functions produce an ordinary real-smooth complex bundle, with no separate realization or atlas-compatibility assumption.

theorem complexCoreReal_isContMDiff
    {X H : Type*} [NormedAddCommGroup X] [NormedSpace ℝ X] [TopologicalSpace H]
    (I : ModelWithCorners ℝ X H) [ChartedSpace H B]
    (hC : ∀ a b, ContMDiffOn I 𝓘(ℝ,F →L[ℂ] F) ∞ (C.coordChange a b)
      (C.baseSet a ∩ C.baseSet b)) : (complexCoreReal C).IsContMDiff I ∞ where
…

Mentions: OAI.Kaplansky.complexCoreReal

theorem OAI.Kaplansky.complexCore_contMDiffVectorBundle line 60
def OAI.Kaplansky.lineDiagonal line 72
def OAI.Kaplansky.lineDiagonalLinear line 77
theorem OAI.Kaplansky.lineSumTransition_eq_diagonal line 86
theorem OAI.Kaplansky.finiteLineSumCore_transition_smooth line 94
def OAI.Kaplansky.changeModelCore line 127
Source documentation
A fixed linear change of model coordinates; the gluing is conjugated.
```
def changeModelCore : VectorBundleCore ℂ B G J where
…
```
def OAI.Kaplansky.changeModelCoreTotalHomeomorph line 140
Source documentation
The coordinate change is a homeomorphism of actual total spaces.
```
def changeModelCoreTotalHomeomorph : TotalSpace F C.Fiber ≃ₜ TotalSpace G (changeModelCore C e).Fiber where
…
```
Mentions: OAI.Kaplansky.changeModelCore
theorem OAI.Kaplansky.changeModelCore_transition_smooth line 175
instance OAI.Kaplansky.changeModelFiberNorm line 188
instance OAI.Kaplansky.changeModelFiberNormedSpace line 190