OAI/Geometry/ComplexBundle/LineStage.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

Doubling stages of line bundles and their Hilbert direct sums.

  1. theorem OAI.Kaplansky.continuous_twoScaled line 26
  2. def OAI.Kaplansky.lineSumDoublingStep line 45
  3. structure OAI.Kaplansky.LineStage line 61

    Source documentation

    A finite list of actual projective-product line bundles.

    structure LineStage {ι : Type*} (K : ι → ℕ) where
…
  4. abbrev OAI.Kaplansky.LineStage.Model line 71
  5. abbrev OAI.Kaplansky.LineStage.Fiber line 72
  6. abbrev OAI.Kaplansky.LineStage.Step line 74
  7. def OAI.Kaplansky.LineStage.double line 76
  8. def OAI.Kaplansky.LineStage.doublingStep line 79
  9. def OAI.Kaplansky.LineStage.tail line 81
  10. def OAI.Kaplansky.LineStage.tailStep line 85
  11. theorem OAI.Kaplansky.LineStage.double_card line 89
  12. theorem OAI.Kaplansky.LineStage.tail_card line 95
  13. instance OAI.Kaplansky.lineStage_finite line 115

    Source documentation

    The actual stage fibers have their finite-dimensional Hilbert-space instances directly from the finite orthogonal sum model.

    instance lineStage_finite (a : LineStage K) (y : ProjectiveProduct K) :
    FiniteDimensional ℂ (a.Fiber y) :=
…

    Mentions: OAI.Kaplansky.LineStage

  14. instance OAI.Kaplansky.lineStage_complete line 118
  15. def OAI.Kaplansky.LineStage.sum line 133
  16. def OAI.Kaplansky.LineStage.sumProj line 136
  17. theorem OAI.Kaplansky.LineStage.continuous_sumProj line 142
  18. def OAI.Kaplansky.LineStage.sumInj line 148
  19. theorem OAI.Kaplansky.LineStage.continuous_sumInj line 167
  20. theorem OAI.Kaplansky.LineStage.sumProj_sumInj_same line 198
  21. theorem OAI.Kaplansky.LineStage.sumProj_sumInj_ne line 207
  22. theorem OAI.Kaplansky.LineStage.sumProj_ext line 215
  23. theorem OAI.Kaplansky.continuous_lineStage_inner_over line 235

    Source documentation

    The actual Hermitian metric is continuous when evaluated on two bundle vectors over the same varying base, including vectors in the total space.

    theorem continuous_lineStage_inner_over (a : LineStage K) {X : Type*} [TopologicalSpace X]
    (b : X → ProjectiveProduct K) (hb : Continuous b)
    (v w : ∀ x, a.Fiber (b x))
    (hv : Continuous (fun x => TotalSpace.mk' a.Model (b x) (v x)))
    (hw : Continuous (fun x => TotalSpace.mk' a.Model (b x) (w x))) :
    Continuous (fun x => inner ℂ (v x) (w x)) := by
…

    Mentions: OAI.Kaplansky.LineStage

  24. theorem OAI.Kaplansky.LineStage.sum_inner line 263