DirectSum.lean`

36 declarations, 0 contain sorry, 0 declared as axioms

Finite direct sums of line bundles, metrics, inclusions, and projections.

def OAI.Kaplansky.lineSumBaseSet line 19
Source documentation
The simultaneous finite cover for the direct sum of actual line cores.
```
def lineSumBaseSet (a : ∀ s, J s) : Set B := {x | ∀ s, x ∈ (C s).baseSet (a s)}
```
theorem OAI.Kaplansky.isOpen_lineSumBaseSet line 21
def OAI.Kaplansky.lineSumTransition line 29
Source documentation
Componentwise transition on the finite Hilbert direct sum.
```
def lineSumTransition (a b : ∀ s, J s) (x : B) :
    EuclideanSpace ℂ S →L[ℂ] EuclideanSpace ℂ S :=
…
```
theorem OAI.Kaplansky.lineSumTransition_apply line 37
theorem OAI.Kaplansky.continuousOn_lineSumTransition line 41
def OAI.Kaplansky.finiteLineSumCore line 54
Source documentation
A finite direct sum, with its ordinary vector-bundle topology and finite Hilbert-space fibers. Neither a trivialization nor a trivial bundle is asserted by the fact that the core uses a fixed model fiber.
```
def finiteLineSumCore : VectorBundleCore ℂ B (EuclideanSpace ℂ S) (∀ s, J s) where
…
```
def OAI.Kaplansky.finiteLineSumFiberEquiv line 70
Source documentation
The direct sum has the actual line-core fibers as its components.
```
def finiteLineSumFiberEquiv (x : B) :
    (finiteLineSumCore C).Fiber x ≃ₗ[ℂ] (∀ s, (C s).Fiber x) :=
…
```
Mentions: OAI.Kaplansky.finiteLineSumCore
theorem OAI.Kaplansky.finiteLineSum_finrank line 74
theorem OAI.Kaplansky.finiteLineSum_chart_component line 81
Source documentation
In every simultaneous chart, components agree with the individual line-bundle charts, which identifies the direct-sum gluing explicitly.
```
theorem finiteLineSum_chart_component (a : ∀ s, J s) (x : B)
    (v : (finiteLineSumCore C).Fiber x) (s : S) :
    (((finiteLineSumCore C).localTriv a) ⟨x,v⟩).2 s =
      (((C s).localTriv (a s)) ⟨x,finiteLineSumFiberEquiv C x v s⟩).2 := rfl
…
```
Mentions: OAI.Kaplansky.finiteLineSumCore, OAI.Kaplansky.finiteLineSumFiberEquiv
def OAI.Kaplansky.finiteLineSumComponent line 96
theorem OAI.Kaplansky.continuous_finiteLineSumComponent line 100
theorem OAI.Kaplansky.continuous_finiteLineSum_iff line 116
Source documentation
Continuity into the actual finite sum is exactly continuity of its base and all of its actual line-bundle components. This includes the empty sum.
```
theorem continuous_finiteLineSum_iff {X : Type*} [TopologicalSpace X]
    (f : X → TotalSpace (EuclideanSpace ℂ S) (finiteLineSumCore C).Fiber) :
    Continuous f ↔ Continuous (fun x => (f x).proj) ∧
      ∀ s, Continuous (fun x => finiteLineSumComponent C s (f x)) := by
…
```
Mentions: OAI.Kaplansky.finiteLineSumCore, OAI.Kaplansky.finiteLineSumComponent
instance OAI.Kaplansky.finiteLineSumFiberNormedAddCommGroup line 145
instance OAI.Kaplansky.finiteLineSumFiberInnerProductSpace line 149
def OAI.Kaplansky.LineCoreIsUnitary line 154
Source documentation
The ordinary isometry condition on the given line-bundle transitions.
```
def LineCoreIsUnitary : Prop := ∀ s a b x,
…
```
theorem OAI.Kaplansky.finiteLineSumTransition_inner line 158
theorem OAI.Kaplansky.finiteLineSum_chart_inner line 167

theorem OAI.Kaplansky.finiteLineSum_inner_continuousOn line 177

Source documentation

The fiberwise Hilbert metrics are continuous on the constructed bundle, proved in local charts. This is the continuous Hermitian metric condition for arbitrary continuous local sections.

theorem finiteLineSum_inner_continuousOn (hC : LineCoreIsUnitary C)
    (A : Set B) (v w : ∀ x, (finiteLineSumCore C).Fiber x)
    (hv : ContinuousOn (fun x => TotalSpace.mk' (EuclideanSpace ℂ S) x (v x)) A)
    (hw : ContinuousOn (fun x => TotalSpace.mk' (EuclideanSpace ℂ S) x (w x)) A) :
    ContinuousOn (fun x => inner ℂ (v x) (w x)) A := by
…

Mentions: OAI.Kaplansky.LineCoreIsUnitary, OAI.Kaplansky.finiteLineSumCore

def OAI.Kaplansky.lineSumInl line 203
def OAI.Kaplansky.lineSumInr line 219
theorem OAI.Kaplansky.lineSumInl_injective line 235
theorem OAI.Kaplansky.lineSumInr_injective line 241
theorem OAI.Kaplansky.continuous_lineSumInl line 247
theorem OAI.Kaplansky.continuous_lineSumInr line 263
def OAI.Kaplansky.lineSumReindex line 287
def OAI.Kaplansky.lineSumReindexTotalHomeomorph line 302
theorem OAI.Kaplansky.lineSumReindex_inner line 324
def OAI.Kaplansky.lineSumFst line 342
def OAI.Kaplansky.lineSumSnd line 348
theorem OAI.Kaplansky.continuous_lineSumFst line 354
theorem OAI.Kaplansky.continuous_lineSumSnd line 359
theorem OAI.Kaplansky.lineSumFst_inner line 364
theorem OAI.Kaplansky.lineSumSnd_inner line 374
theorem OAI.Kaplansky.lineSumFst_comp_inl line 384
theorem OAI.Kaplansky.lineSumSnd_comp_inr line 388
theorem OAI.Kaplansky.lineSum_inl_fst_add_inr_snd line 392