ProjectionBundle.lean`

20 declarations, 0 contain sorry, 0 declared as axioms

The projection line bundle and its dual.

def OAI.Kaplansky.projectionLineTransition line 16
theorem OAI.Kaplansky.projectionLineTransition_self line 19
theorem OAI.Kaplansky.projectionLineTransition_comp line 24
theorem OAI.Kaplansky.projectionLineTransition_star line 31
theorem OAI.Kaplansky.projectionLineTransition_unitary line 35
theorem OAI.Kaplansky.continuousOn_projectionLineTransition line 41
def OAI.Kaplansky.projectionLineCore line 48
Source documentation
A genuine complex line-bundle core on the compact space of orthogonal rank-one projections. Its transition functions are constructed, not assumed.
```
def projectionLineCore (d : ℕ) : VectorBundleCore ℂ (projectionSpace d 1) ℂ (Fin d) where
…
```
Mentions: OAI.Kaplansky.projectionSpace
def OAI.Kaplansky.projectionLineFiberEquiv line 63
Source documentation
Identify each constructed fiber with the actual projected line in Euclidean space.
```
def projectionLineFiberEquiv (p : projectionSpace d 1) :
    (projectionLineCore d).Fiber p ≃ₗ[ℂ] projectionLine p where
…
```
Mentions: OAI.Kaplansky.projectionSpace, OAI.Kaplansky.projectionLineCore, OAI.Kaplansky.projectionLine
theorem OAI.Kaplansky.projectionLine_realization_chart line 79
abbrev OAI.Kaplansky.ProjectionLineTotal line 88
def OAI.Kaplansky.projectionLineRealization line 91
theorem OAI.Kaplansky.continuous_projectionLineRealization line 94
def OAI.Kaplansky.projectionLineToTotal line 110
def OAI.Kaplansky.projectionLineFromTotal line 113
theorem OAI.Kaplansky.projectionLineFromTotal_chart line 116
theorem OAI.Kaplansky.continuous_projectionLineFromTotal line 126
def OAI.Kaplansky.projectionLineTotalHomeomorph line 146
Source documentation
The constructed line bundle is homeomorphic to the actual incidence subspace of the compact projection base times Euclidean space.
```
def projectionLineTotalHomeomorph (d : ℕ) :
    TotalSpace ℂ (projectionLineCore d).Fiber ≃ₜ ProjectionLineTotal d where
…
```
Mentions: OAI.Kaplansky.projectionLineCore, OAI.Kaplansky.ProjectionLineTotal
def OAI.Kaplansky.projectionDualLineCore line 174
Source documentation
The dual (hyperplane) line core, with inverse unitary transitions.
```
def projectionDualLineCore (d : ℕ) : VectorBundleCore ℂ (projectionSpace d 1) ℂ (Fin d) where
…
```
Mentions: OAI.Kaplansky.projectionSpace
def OAI.Kaplansky.projectionDualLineFiberEquiv line 189
Source documentation
The constructed dual fiber is the full algebraic dual of the actual line.
```
def projectionDualLineFiberEquiv (p : projectionSpace d 1) :
    (projectionDualLineCore d).Fiber p ≃ₗ[ℂ] (projectionLine p →ₗ[ℂ] ℂ) where
…
```
Mentions: OAI.Kaplansky.projectionSpace, OAI.Kaplansky.projectionDualLineCore, OAI.Kaplansky.projectionLine

theorem OAI.Kaplansky.projectionDualLine_pairing_chart line 212

Source documentation

Evaluation of the dual on the line is independent of the local chart.

theorem projectionDualLine_pairing_chart (p : projectionSpace d 1)
    (z : (projectionDualLineCore d).Fiber p) (w : (projectionLineCore d).Fiber p)
    (i : Fin d) (hi : p ∈ projectionChartSet i) :
    ((projectionDualLineCore d).localTriv i ⟨p,z⟩).2 *
      ((projectionLineCore d).localTriv i ⟨p,w⟩).2 = (show ℂ from z) * (show ℂ from w) := by
…

Mentions: OAI.Kaplansky.projectionSpace, OAI.Kaplansky.projectionDualLineCore, OAI.Kaplansky.projectionLineCore, OAI.Kaplansky.projectionChartSet