Hom.lean`

16 declarations, 0 contain sorry, 0 declared as axioms

Descent of canonical scaling and Hermitian bundle homomorphisms.

theorem OAI.Kaplansky.canonicalScaling_congr line 19

def OAI.Kaplansky.chartScaling line 26

Source documentation

Local normalization with harmless zero values outside a chart.

def chartScaling (H : VectorBundleCore ℂ Y (Fin n → Matrix (Fin r) (Fin d) ℂ) I)
    (T : I → Y → Fin n → Matrix (Fin r) (Fin d) ℂ)
    (hexp : ∀ a y, y ∈ H.baseSet a → Expanding (T a y)) (a : I) (y : Y) := by
…

Mentions: OAI.Kaplansky.Expanding

theorem OAI.Kaplansky.continuousOn_chartScaling line 32
theorem OAI.Kaplansky.exists_scaled_core_section line 48
def OAI.Kaplansky.frameTupleLinear line 89
def OAI.Kaplansky.frameTupleCLM line 95
theorem OAI.Kaplansky.frameTupleCLM_apply line 99
theorem OAI.Kaplansky.frameTuple_comp line 103
theorem OAI.Kaplansky.continuousOn_frameTupleCLM line 109

def OAI.Kaplansky.matrixHomCore line 124

Source documentation

Construct the actual Hom-tuple vector bundle from transition matrices and their verified cocycle. There is no bundle-realization hypothesis.

def matrixHomCore {Y I : Type*} [TopologicalSpace Y]
    (O : I → Set Y) (hO : ∀ i, IsOpen (O i)) (idx : Y → I) (hat : ∀ y, y ∈ O (idx y))
    (U : I → I → Y → Matrix (Fin d) (Fin d) ℂ)
    (V : I → I → Y → Matrix (Fin r) (Fin r) ℂ)
    (hUc : ∀ i j, ContinuousOn (U i j) (O i ∩ O j))
    (hVc : ∀ i j, ContinuousOn (V i j) (O i ∩ O j))
    (hUs : ∀ i y, y ∈ O i → U i i y = 1)
    (hVs : ∀ i y, y ∈ O i → V i i y = 1)
    (hUm : ∀ i j k y, y ∈ O i → y ∈ O j → y ∈ O k → U j k y * U i j y = U i k y)
    (hVm : ∀ i j k y, y ∈ O i → y ∈ O j → y ∈ O k → V j k y * V i j y = V i k y) :
    VectorBundleCore ℂ Y (Fin n → Matrix (Fin r) (Fin d) ℂ) I where
…

def OAI.Kaplansky.hermitianChartSet line 166
def OAI.Kaplansky.hermitianSourceTransition line 169
def OAI.Kaplansky.hermitianTargetTransition line 172
def OAI.Kaplansky.hermitianHomCore line 178
Source documentation
The Hom-tuple core is constructed from ordinary Hermitian bundles. The charts, orthonormalizations, transition matrices, and cocycle proofs are derived here; no unitary core is an input.
```
def hermitianHomCore
    (hE : ContinuousHermitianMetric (d := d) (E := E))
…
```
Mentions: OAI.Kaplansky.ContinuousHermitianMetric
theorem OAI.Kaplansky.hermitianHomCore_coordChange line 197
theorem OAI.Kaplansky.hermitianHomCore_unitary line 205