Sections.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Gluing, homotopy, and operations on vector bundle sections.

theorem OAI.Kaplansky.continuous_bundle_add_over line 25

Source documentation

Addition over a varying base, with the actual total-space topology.

theorem continuous_bundle_add_over {X : Type*} [TopologicalSpace X]
    (b : X → B) (hb : Continuous b) (v w : ∀ x, E (b x))
    (hv : Continuous (fun x => TotalSpace.mk' V (b x) (v x)))
    (hw : Continuous (fun x => TotalSpace.mk' V (b x) (w x))) :
    Continuous (fun x => TotalSpace.mk' V (b x) (v x + w x)) := by
…

theorem OAI.Kaplansky.continuous_bundle_smul_over line 43

Source documentation

Scalar multiplication over a varying base.

theorem continuous_bundle_smul_over {X : Type*} [TopologicalSpace X]
    (b : X → B) (hb : Continuous b) (c : X → ℂ) (hc : Continuous c)
    (v : ∀ x, E (b x))
    (hv : Continuous (fun x => TotalSpace.mk' V (b x) (v x))) :
    Continuous (fun x => TotalSpace.mk' V (b x) (c x • v x)) := by
…

def OAI.Kaplansky.bundleSectionHomotopy line 61

Source documentation

The genuine global affine homotopy of two continuous bundle sections. It permits intermediate degenerate zeros.

def bundleSectionHomotopy (s t : ∀ b, E b)
    (hs : Continuous (fun b => TotalSpace.mk' V b (s b)))
    (ht : Continuous (fun b => TotalSpace.mk' V b (t b))) :
    ContinuousMap.Homotopy ⟨_, hs⟩ ⟨_, ht⟩ where
…

def OAI.Kaplansky.compactifiedSection line 78
Source documentation
The map of a section into the one-point compactification of its actual total space.
```
def compactifiedSection (s : ∀ b, E b)
    (hs : Continuous (fun b => TotalSpace.mk' V b (s b))) :
    C(B, OnePoint (TotalSpace V E)) :=
…
```

def OAI.Kaplansky.compactifiedSectionHomotopy line 86

Source documentation

Global section independence at the level of homotopy, without a regularity or finiteness assumption on any intermediate zero set.

def compactifiedSectionHomotopy (s t : ∀ b, E b)
    (hs : Continuous (fun b => TotalSpace.mk' V b (s b)))
    (ht : Continuous (fun b => TotalSpace.mk' V b (t b))) :
    ContinuousMap.Homotopy (compactifiedSection s hs) (compactifiedSection t ht) :=
…

Mentions: OAI.Kaplansky.compactifiedSection

theorem OAI.Kaplansky.glue_core_section line 99

Source documentation

Gluing compatible local coordinate functions produces a continuous section of the ordinary, potentially nontrivial vector bundle.

theorem glue_core_section (H : VectorBundleCore 𝕜 Y F I)
    (L : I → Y → F) (hL : ∀ a, ContinuousOn (L a) (H.baseSet a))
    (hcompat : ∀ a b y, y ∈ H.baseSet a → y ∈ H.baseSet b →
      H.coordChange a b y (L a y) = L b y) :
    ∃ s : ∀ y, H.Fiber y,
      Continuous (fun y => TotalSpace.mk' F y (s y)) ∧
      ∀ a y, y ∈ H.baseSet a → (H.localTriv a ⟨y,s y⟩).2 = L a y := by
…

theorem OAI.Kaplansky.continuousOn_bundle_sum line 134

Source documentation

Finite sums of continuous local sections in an ordinary vector bundle.

theorem continuousOn_bundle_sum {ι : Type*} (u : Finset ι) (v : ι → ∀ y, E y) {s : Set Y}
    (hv : ∀ i ∈ u, ContinuousOn (fun y => TotalSpace.mk' V y (v i y)) s) :
    ContinuousOn (fun y => TotalSpace.mk' V y (∑ i ∈ u, v i y)) s := by
…

theorem OAI.Kaplansky.continuousOn_bundle_smul line 152

Source documentation

Scalar multiplication of continuous local sections.

theorem continuousOn_bundle_smul (f : Y → 𝕜) (v : ∀ y, E y) {s : Set Y}
    (hf : ContinuousOn f s) (hv : ContinuousOn (fun y => TotalSpace.mk' V y (v y)) s) :
    ContinuousOn (fun y => TotalSpace.mk' V y (f y • v y)) s := by
…