QuaternionLifts.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Composition of the concrete quaternion frame changes. These identities keep the action on both Weyl blocks, so they can be used at a single point without selecting a moving eigenframe.

structure OAI.PositiveEinsteinFour.QuaternionFrame.QuaternionLift line 18
Source documentation
A concrete oriented four-frame lift of a change in one quaternion basis. The opposite quaternion basis is fixed.
```
structure QuaternionLift (Q O : Fin 3 → Mat4) (A : Mat) where
…
```
theorem OAI.PositiveEinsteinFour.QuaternionFrame.intertwines_combination line 26
Source documentation
The generator intertwining identity extends to every imaginary quaternion.
```
theorem intertwines_combination (Q : Fin 3 → Mat4) (A : Mat) (P : Mat4)
    (hP : ∀ s, P * Q s = (∑ r, A r s • Q r) * P) (u : Fin 3 → ℝ) :
    P * imaginaryCombination Q u = imaginaryCombination Q (A *ᵥ u) * P := by
…
```
Mentions: OAI.PositiveEinsteinFour.QuaternionFrame.imaginaryCombination
def OAI.PositiveEinsteinFour.QuaternionFrame.QuaternionLift.mul line 44
Source documentation
Products of four-frame lifts induce the corresponding product of three-dimensional coefficient changes.
```
def QuaternionLift.mul {Q O : Fin 3 → Mat4} {A B : Mat}
    (P : QuaternionLift Q O A) (R : QuaternionLift Q O B) : QuaternionLift Q O (A * B) where
…
```
Mentions: OAI.PositiveEinsteinFour.QuaternionFrame.QuaternionLift
def OAI.PositiveEinsteinFour.QuaternionFrame.QuaternionLift.one line 70
Source documentation
The identity frame lifts the identity change in a quaternion basis.
```
def QuaternionLift.one (Q O : Fin 3 → Mat4) : QuaternionLift Q O 1 where
…
```
Mentions: OAI.PositiveEinsteinFour.QuaternionFrame.QuaternionLift
def OAI.PositiveEinsteinFour.QuaternionFrame.QuaternionLift.leftAxis line 81
Source documentation
Every unit axis reflection has an explicit left-quaternion lift.
```
def QuaternionLift.leftAxis (u : Fin 3 → ℝ) (hu : ∑ r, u r ^ 2 = 1) :
    QuaternionLift quaternionMatrix Angular.oppositeMatrix (axisReflection u) where
…
```
Mentions: OAI.PositiveEinsteinFour.QuaternionFrame.QuaternionLift, OAI.PositiveEinsteinFour.Angular.oppositeMatrix, OAI.PositiveEinsteinFour.QuaternionFrame.axisReflection
def OAI.PositiveEinsteinFour.QuaternionFrame.QuaternionLift.rightAxis line 92
Source documentation
Every unit axis reflection has an explicit right-quaternion lift.
```
def QuaternionLift.rightAxis (u : Fin 3 → ℝ) (hu : ∑ r, u r ^ 2 = 1) :
    QuaternionLift Angular.oppositeMatrix quaternionMatrix (axisReflection u) where
…
```
Mentions: OAI.PositiveEinsteinFour.QuaternionFrame.QuaternionLift, OAI.PositiveEinsteinFour.Angular.oppositeMatrix, OAI.PositiveEinsteinFour.QuaternionFrame.axisReflection