Tensor.lean`

15 declarations, 0 contain sorry, 0 declared as axioms

Tensor line bundles, metrics, and finite frames.

theorem OAI.Kaplansky.complexLineMap_scalar line 16
def OAI.Kaplansky.tensorLineCore line 25
Source documentation
Tensor product of two actual line cores. Its transition functions are the products of the two line transition functions.
```
def tensorLineCore : VectorBundleCore ℂ B ℂ (J × K) where
…
```
def OAI.Kaplansky.tensorLinePair line 57
Source documentation
Multiplication in core fibers is the tensor pairing. This formula is compatible with every tensor-product chart.
```
def tensorLinePair (x : B) (v : C.Fiber x) (w : D.Fiber x) : (tensorLineCore C D).Fiber x :=
…
```
Mentions: OAI.Kaplansky.tensorLineCore
theorem OAI.Kaplansky.tensorLinePair_chart line 60

theorem OAI.Kaplansky.continuous_tensorLinePair_section line 74

Source documentation

Products of continuous sections are continuous in the tensor bundle topology; the chart compatibility, not fiberwise continuity alone, establishes the statement.

theorem continuous_tensorLinePair_section (s : ∀ x, C.Fiber x) (t : ∀ x, D.Fiber x)
    (hs : Continuous (fun x => TotalSpace.mk' ℂ x (s x)))
    (ht : Continuous (fun x => TotalSpace.mk' ℂ x (t x))) :
    Continuous (fun x => TotalSpace.mk' ℂ x (tensorLinePair C D x (s x) (t x))) := by
…

Mentions: OAI.Kaplansky.tensorLinePair

theorem OAI.Kaplansky.tensorLinePair_ne_zero line 87
def OAI.Kaplansky.lineFrameEquiv line 99
Source documentation
Coordinates relative to an actual nowhere-zero line section.
```
def lineFrameEquiv (b : B) : C.Fiber b ≃ₗ[ℂ] ℂ where
…
```
theorem OAI.Kaplansky.lineFrameEquiv_chart line 111
def OAI.Kaplansky.lineFrameHomeomorph line 130
Source documentation
A nonzero continuous frame gives a homeomorphism for the original line-core topology, with complex-linear fibers.
```
def lineFrameHomeomorph : TotalSpace ℂ C.Fiber ≃ₜ B × ℂ where
…
```
def OAI.Kaplansky.finiteLineFrameEquiv line 165
def OAI.Kaplansky.finiteLineFrameHomeomorph line 170
theorem OAI.Kaplansky.finiteLineFrameHomeomorph_zero_iff line 190
theorem OAI.Kaplansky.tensorLineCore_coordChange_eq_comp line 205

theorem OAI.Kaplansky.tensorLineCore_unitary line 215

Source documentation

Tensoring unitary line transitions preserves the actual Hermitian metric. No determinant or orientation premise is required.

theorem tensorLineCore_unitary
    (hC : ∀ i j x, x ∈ C.baseSet i → x ∈ C.baseSet j → ∀ z w : ℂ,
      inner ℂ (C.coordChange i j x z) (C.coordChange i j x w) = inner ℂ z w)
    (hD : ∀ i j x, x ∈ D.baseSet i → x ∈ D.baseSet j → ∀ z w : ℂ,
      inner ℂ (D.coordChange i j x z) (D.coordChange i j x w) = inner ℂ z w)
    (i j : J × K) (x : B) (hi : x ∈ (tensorLineCore C D).baseSet i)
    (hj : x ∈ (tensorLineCore C D).baseSet j) (z w : ℂ) :
    inner ℂ ((tensorLineCore C D).coordChange i j x z)
      ((tensorLineCore C D).coordChange i j x w) = inner ℂ z w := by
…

Mentions: OAI.Kaplansky.tensorLineCore

theorem OAI.Kaplansky.tensorLineSum_unitary line 227