StageMaps.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Continuous stage maps and trivial input stages.

def OAI.Kaplansky.lineStageTrivialTotalHomeomorph line 17
Source documentation
A sum consisting entirely of trivial projective-product lines has a global chart, for the existing bundle topology.
```
def lineStageTrivialTotalHomeomorph (a : LineStage K)
    (h : ∀ s, a.label s=none) (y₀ : ProjectiveProduct K) :
    TotalSpace a.Model a.Fiber ≃ₜ ProjectiveProduct K × a.Model := by
…
```
Mentions: OAI.Kaplansky.LineStage
theorem OAI.Kaplansky.lineStageTrivialTotalHomeomorph_apply line 39

theorem OAI.Kaplansky.lineStageTrivial_section line 56

Source documentation

Constant model vectors are genuine continuous sections of this trivial bundle in its original topology.

theorem lineStageTrivial_section (a : LineStage K) (h : ∀ s, a.label s=none)
    (y₀ : ProjectiveProduct K) (v : a.Model) :
    Continuous (fun y => TotalSpace.mk' a.Model y (show a.Fiber y from v)) := by
…

Mentions: OAI.Kaplansky.LineStage

structure OAI.Kaplansky.ContinuousStageMap line 79
Source documentation
A linear map between the actual bundles, continuous on total spaces.
```
structure ContinuousStageMap (a b : LineStage K) where
…
```
Mentions: OAI.Kaplansky.LineStage
def OAI.Kaplansky.ContinuousStageMap.comp line 87
def OAI.Kaplansky.ContinuousStageMap.smul line 91
def OAI.Kaplansky.ContinuousStageMap.sum line 99
def OAI.Kaplansky.ContinuousStageMap.proj line 109
def OAI.Kaplansky.ContinuousStageMap.inj line 113