Bundles.lean`

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

Test bundles, Hermitian metrics, and their trivial initial stage.

def OAI.Kaplansky.testLineChartIndex line 16
Source documentation
The zero label denotes L₀; positive labels denote hyperplane pullbacks.
```
def testLineChartIndex (m R : ℕ) : Option (Fin R) → Type
  | none => Unit
  | some i => Fin (testProjectiveDimension m R i + 1)
```
Mentions: OAI.Kaplansky.testProjectiveDimension
def OAI.Kaplansky.testLineCore line 20
def OAI.Kaplansky.testLineCoreHyperplaneHomeomorph line 29
Source documentation
The positive-labelled line is topologically the preserved hyperplane pullback, including its total-space topology.
```
def testLineCoreHyperplaneHomeomorph (m R : ℕ) (i : Fin R) :
    TotalSpace ℂ (testLineCore m R (some i)).Fiber ≃ₜ
      TotalSpace ℂ (TestHyperplaneLine m R i) :=
…
```
Mentions: OAI.Kaplansky.testLineCore, OAI.Kaplansky.TestHyperplaneLine
def OAI.Kaplansky.testSummandLineIndex line 34
theorem OAI.Kaplansky.testSummandLineIndex_zero line 37
abbrev OAI.Kaplansky.TestBundleSlot line 40
def OAI.Kaplansky.testBundleCore line 42
abbrev OAI.Kaplansky.TestBundle line 46
instance OAI.Kaplansky.(instance at line 48) line 48
instance OAI.Kaplansky.(instance at line 51) line 51
theorem OAI.Kaplansky.testBundle_finrank line 54
theorem OAI.Kaplansky.continuous_testBundle_component line 60
Source documentation
Actual topological component maps, one for every occurrence of each line.
```
theorem continuous_testBundle_component (m R j : ℕ) (hj : j≤R)
    (s : TestBundleSlot m R j) :
    Continuous (finiteLineSumComponent
      (fun s : TestBundleSlot m R j => testLineCore m R (testSummandLineIndex hj s.1)) s) :=
…
```
Mentions: OAI.Kaplansky.TestBundleSlot, OAI.Kaplansky.finiteLineSumComponent, OAI.Kaplansky.testLineCore, OAI.Kaplansky.testSummandLineIndex
theorem OAI.Kaplansky.complex_unit_mul_inner line 75
theorem OAI.Kaplansky.testLineCore_unitary line 83
theorem OAI.Kaplansky.testBundleLineCores_unitary line 95
instance OAI.Kaplansky.testBundleFiberNormedAddCommGroup line 100
instance OAI.Kaplansky.testBundleFiberInnerProductSpace line 104
theorem OAI.Kaplansky.testBundle_inner_continuousOn line 108
theorem OAI.Kaplansky.testBundle_zero_baseSet line 122
def OAI.Kaplansky.testBundleZeroTotalHomeomorph line 138
Source documentation
A global linear bundle chart for E₀. This proves topological triviality, not just that its fibers have the desired dimension.
```
def testBundleZeroTotalHomeomorph (m R : ℕ) :
    TotalSpace (EuclideanSpace ℂ (TestBundleSlot m R 0)) (TestBundle m R 0 (Nat.zero_le R)) ≃ₜ
      BundleTestBase m R × EuclideanSpace ℂ (TestBundleSlot m R 0) := by
…
```
Mentions: OAI.Kaplansky.TestBundleSlot, OAI.Kaplansky.TestBundle, OAI.Kaplansky.BundleTestBase
theorem OAI.Kaplansky.testBundleZeroTotalHomeomorph_apply line 148