Tuples.lean`

14 declarations, 0 contain sorry, 0 declared as axioms

Normalized Hermitian tuples, doubling, and unitary equivalence.

structure OAI.Kaplansky.NormalizedHermitianTuple line 20
Source documentation
A normalized tuple with the adjoint identity proved for its displayed reverse maps. No existence or topological obstruction is assumed here.
```
structure NormalizedHermitianTuple (E F : Type*)
    [NormedAddCommGroup E] [InnerProductSpace ℂ E]
    [NormedAddCommGroup F] [InnerProductSpace ℂ F] where
…
```
def OAI.Kaplansky.NormalizedHermitianTuple.congr line 39
Source documentation
Transport the actual tuple and its actual adjoints through unitary coordinates. The row and column identities are preserved.
```
def congr (T : NormalizedHermitianTuple E F)
    (e : E ≃ₗᵢ[ℂ] E') (f : F ≃ₗᵢ[ℂ] F') : NormalizedHermitianTuple E' F' where
…
```
Mentions: OAI.Kaplansky.NormalizedHermitianTuple
theorem OAI.Kaplansky.NormalizedHermitianTuple.reverse_eq_adjoint line 71
Source documentation
The reverse map is the unique adjoint, not an unconstrained witness.
```
theorem reverse_eq_adjoint [FiniteDimensional ℂ E] [FiniteDimensional ℂ F]
    (T : NormalizedHermitianTuple E F) (i : Fin 24) :
    T.reverse i = LinearMap.adjoint (T.forward i) := by
…
```
Mentions: OAI.Kaplansky.NormalizedHermitianTuple

structure OAI.Kaplansky.UnitaryBundleEquiv line 91

Source documentation

A fiberwise unitary equivalence compatible with the actual total-space topologies, even when the bundle models use different coordinates.

structure UnitaryBundleEquiv (U V : Type*) (E F : B → Type*)
    [∀ x, NormedAddCommGroup (E x)] [∀ x, InnerProductSpace ℂ (E x)]
    [∀ x, NormedAddCommGroup (F x)] [∀ x, InnerProductSpace ℂ (F x)]
    [TopologicalSpace (TotalSpace U E)] [TopologicalSpace (TotalSpace V F)] where
…

def OAI.Kaplansky.UnitaryBundleEquiv.symm line 107
def OAI.Kaplansky.UnitaryBundleEquiv.trans line 112

structure OAI.Kaplansky.ContinuousNormalizedStep line 121

Source documentation

The normalized maps and their true adjoints vary continuously over the specified ordinary topological bundles.

structure ContinuousNormalizedStep (U V : Type*) (E F : B → Type*)
    [∀ x, NormedAddCommGroup (E x)] [∀ x, InnerProductSpace ℂ (E x)]
    [∀ x, NormedAddCommGroup (F x)] [∀ x, InnerProductSpace ℂ (F x)]
    [TopologicalSpace (TotalSpace U E)] [TopologicalSpace (TotalSpace V F)] where
…

def OAI.Kaplansky.ContinuousNormalizedStep.congr line 140
def OAI.Kaplansky.twoOfTwentyFour line 155
theorem OAI.Kaplansky.sum_twoOfTwentyFour line 158
def OAI.Kaplansky.doublingScale line 162
theorem OAI.Kaplansky.doublingScale_conj line 164
theorem OAI.Kaplansky.doublingScale_sq line 165

def OAI.Kaplansky.doublingTuple line 171

Source documentation

Two scaled orthogonal inclusions, padded by twenty-two zero maps. These algebraic hypotheses are discharged by the actual sum coordinates.

def doublingTuple {E F : Type*} [NormedAddCommGroup E] [InnerProductSpace ℂ E]
    [NormedAddCommGroup F] [InnerProductSpace ℂ F]
    (I₀ I₁ : E →ₗ[ℂ] F) (P₀ P₁ : F →ₗ[ℂ] E)
    (h₀ : ∀ v w, inner ℂ (P₀ w) v = inner ℂ w (I₀ v))
    (h₁ : ∀ v w, inner ℂ (P₁ w) v = inner ℂ w (I₁ v))
    (hP₀ : P₀.comp I₀ = LinearMap.id) (hP₁ : P₁.comp I₁ = LinearMap.id)
    (hI : I₀.comp P₀ + I₁.comp P₁ = LinearMap.id) : NormalizedHermitianTuple E F where
…

Mentions: OAI.Kaplansky.NormalizedHermitianTuple