Pullback.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Pullback line bundles and their continuous chart identifications.

def OAI.Kaplansky.pullbackLineCore line 20
Source documentation
Pull a line core back along a continuous base map.
```
def pullbackLineCore : VectorBundleCore ℂ X ℂ J where
…
```
def OAI.Kaplansky.pullbackLineCoreTotalHomeomorph line 32
Source documentation
This is the ordinary topological pullback, not just a fiberwise copy.
```
def pullbackLineCoreTotalHomeomorph :
    TotalSpace ℂ (pullbackLineCore C f).Fiber ≃ₜ TotalSpace ℂ (f *ᵖ C.Fiber) where
…
```
Mentions: OAI.Kaplansky.pullbackLineCore
def OAI.Kaplansky.trivialLineCore line 56
Source documentation
A single global identity chart for the trivial complex line.
```
def trivialLineCore (B : Type*) [TopologicalSpace B] : VectorBundleCore ℂ B ℂ Unit where
…
```

theorem OAI.Kaplansky.continuous_pullbackLineCore_total_iff line 72

Source documentation

Continuity into the core pullback is exactly continuity in the base and continuity of the induced map to the original total space.

theorem continuous_pullbackLineCore_total_iff (C : VectorBundleCore ℂ B ℂ J)
    (f : C(A,B)) (g : X → A) (v : X → ℂ) :
    Continuous (fun x => TotalSpace.mk' ℂ (g x)
      (show (pullbackLineCore C f).Fiber (g x) from v x)) ↔
    Continuous g ∧ Continuous (fun x => TotalSpace.mk' ℂ (f (g x))
      (show C.Fiber (f (g x)) from v x)) := by
…

Mentions: OAI.Kaplansky.pullbackLineCore

theorem OAI.Kaplansky.continuous_pullbackLineSum_total_iff line 95

Source documentation

The same assertion for the actual finite Hermitian sum.

theorem continuous_pullbackLineSum_total_iff (C : ∀ s, VectorBundleCore ℂ B ℂ (J s))
    (f : C(A,B)) (g : X → A) (v : X → EuclideanSpace ℂ S) :
    Continuous (fun x => TotalSpace.mk' (EuclideanSpace ℂ S) (g x)
      (show (finiteLineSumCore (fun s => pullbackLineCore (C s) f)).Fiber (g x) from v x)) ↔
    Continuous g ∧ Continuous (fun x => TotalSpace.mk' (EuclideanSpace ℂ S) (f (g x))
      (show (finiteLineSumCore C).Fiber (f (g x)) from v x)) := by
…

Mentions: OAI.Kaplansky.finiteLineSumCore, OAI.Kaplansky.pullbackLineCore

def OAI.Kaplansky.chartBaseMap line 120
def OAI.Kaplansky.lineSumChartPullbackHomeomorph line 125
Source documentation
Pulling the actual sum into full chart coordinates gives exactly the restriction of its original total space, with its inherited topology.
```
def lineSumChartPullbackHomeomorph :
    TotalSpace (EuclideanSpace ℂ S)
      (finiteLineSumCore (fun s => pullbackLineCore (C s) (chartBaseMap U e))).Fiber ≃ₜ
    {z : TotalSpace (EuclideanSpace ℂ S) (finiteLineSumCore C).Fiber | z.proj ∈ U} where
…
```
Mentions: OAI.Kaplansky.finiteLineSumCore, OAI.Kaplansky.pullbackLineCore, OAI.Kaplansky.chartBaseMap
theorem OAI.Kaplansky.lineSumChartPullbackHomeomorph_base line 156
theorem OAI.Kaplansky.lineSumChartPullbackHomeomorph_fiber line 161