Schur.lean`

15 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.NuclearUltrapower.FiniteUnitaryRep.scalar_of_commuting line 24

Source documentation

Schur's scalar lemma, proved from an actual eigenvalue over C.

theorem scalar_of_commuting {π : FiniteUnitaryRep.{u,v} Γ} (hπ : π.Irreducible)
    (T : π →ₗ[ℂ] π) (hT : ∀ g x, T (π.action g x) = π.action g (T x)) :
    ∃ c : ℂ, T = c • LinearMap.id := by
…

theorem OAI.NuclearUltrapower.FiniteUnitaryRep.isometry_of_intertwiner line 41

Source documentation

Every nonzero intertwiner out of an irreducible finite-dimensional unitary representation is a positive scalar multiple of an isometry. The target can be any Hilbert space, not necessarily separable or finite-dimensional.

theorem isometry_of_intertwiner {π : FiniteUnitaryRep.{u,v} Γ} (hπ : π.Irreducible)
    {K : Type*} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K]
    (σ : Γ →* (K ≃ₗᵢ[ℂ] K)) (T : π →L[ℂ] K) (hT0 : T ≠ 0)
    (hT : ∀ g x, T (π.action g x) = σ g (T x)) :
    ∃ U : π →ₗᵢ[ℂ] K, ∀ g x, U (π.action g x) = σ g (U x) := by
…

theorem OAI.NuclearUltrapower.FiniteUnitaryRep.equivalent_of_nonzero_intertwiner line 86

Source documentation

The unitary form of Schur's lemma used by the coordinate-quotient argument.

theorem equivalent_of_nonzero_intertwiner {π τ : FiniteUnitaryRep.{u,v} Γ}
    (hπ : π.Irreducible) (hτ : τ.Irreducible) (T : π →L[ℂ] τ) (hT0 : T ≠ 0)
    (hT : ∀ g x, T (π.action g x) = τ.action g (T x)) : π.Equivalent τ :=
…

def OAI.NuclearUltrapower.mixedTensorOperator line 103
Source documentation
The finite-rank operator represented by a rectangular Hilbert tensor.
```
def mixedTensorOperator : E ⊗[ℂ] StrongDual ℂ F →ₗ[ℂ] (F →L[ℂ] E) :=
…
```
theorem OAI.NuclearUltrapower.mixedTensorOperator_tmul line 113
theorem OAI.NuclearUltrapower.mixedTensorOperator_inner line 117
Source documentation
All matrix coefficients, using Lean's second-variable-linear inner product.
```
theorem mixedTensorOperator_inner (z : E ⊗[ℂ] StrongDual ℂ F) (v : F) (y : E) :
    ⟪y, mixedTensorOperator z v⟫_ℂ = ⟪y ⊗ₜ[ℂ] InnerProductSpace.toDual ℂ F v, z⟫_ℂ := by
…
```
Mentions: OAI.NuclearUltrapower.mixedTensorOperator
theorem OAI.NuclearUltrapower.mixedTensorOperator_injective line 125

theorem OAI.NuclearUltrapower.mixedTensorOperator_action line 140

Source documentation

Tensor invariance is the genuine intertwining equation.

theorem mixedTensorOperator_action (u : E ≃ₗᵢ[ℂ] E) (v : F ≃ₗᵢ[ℂ] F)
    (z : E ⊗[ℂ] StrongDual ℂ F) :
    mixedTensorOperator (TensorProduct.congrIsometry u (dualUnitary v) z) =
      (u : E →L[ℂ] E).comp ((mixedTensorOperator z).comp (v.symm : F →L[ℂ] F)) := by
…

Mentions: OAI.NuclearUltrapower.mixedTensorOperator, OAI.NuclearUltrapower.dualUnitary

def OAI.NuclearUltrapower.tensorContragredientRep line 148

theorem OAI.NuclearUltrapower.invariant_tensor_intertwines line 171

Source documentation

The invariant tensor defines an actual bounded intertwiner.

theorem invariant_tensor_intertwines
    (ρ : Γ →* (E ≃ₗᵢ[ℂ] E)) (π : Γ →* (F ≃ₗᵢ[ℂ] F))
    (z : E ⊗[ℂ] StrongDual ℂ F)
    (hz : ∀ g, tensorContragredientRep ρ π g z = z) (g : Γ) (x : F) :
    mixedTensorOperator z (π g x) = ρ g (mixedTensorOperator z x) := by
…

Mentions: OAI.NuclearUltrapower.tensorContragredientRep, OAI.NuclearUltrapower.mixedTensorOperator

theorem OAI.NuclearUltrapower.tensor_no_invariants_of_inequivalent line 184

Source documentation

Schur exclusion at each nonexceptional coordinate.

theorem tensor_no_invariants_of_inequivalent
    {π τ : FiniteUnitaryRep.{u,v} Γ} (hπ : π.Irreducible) (hτ : τ.Irreducible)
    (hne : ¬ τ.Equivalent π) (z : π ⊗[ℂ] StrongDual ℂ τ)
    (hz : ∀ g, tensorContragredientRep π.action τ.action g z = z) : z = 0 := by
…

Mentions: OAI.NuclearUltrapower.tensorContragredientRep

theorem OAI.NuclearUltrapower.mixedTensorOperator_surjective line 206
Source documentation
Every operator with finite-dimensional domain is represented by an actual algebraic tensor; no completed-tensor compactness argument is hidden here.
```
theorem mixedTensorOperator_surjective :
    Function.Surjective (mixedTensorOperator (E := E) (F := F)) := by
…
```
Mentions: OAI.NuclearUltrapower.mixedTensorOperator

theorem OAI.NuclearUltrapower.exists_invariant_tensor_of_intertwiner line 220

Source documentation

A nonzero finite-dimensional intertwiner gives a nonzero invariant tensor.

theorem exists_invariant_tensor_of_intertwiner {Γ : Type*} [Group Γ]
    (ρ : Γ →* (E ≃ₗᵢ[ℂ] E)) (π : Γ →* (F ≃ₗᵢ[ℂ] F))
    (T : F →L[ℂ] E) (hT : T ≠ 0)
    (hcomm : ∀ g x, T (π g x) = ρ g (T x)) :
    ∃ z : E ⊗[ℂ] StrongDual ℂ F, z ≠ 0 ∧
      ∀ g, tensorContragredientRep ρ π g z = z := by
…

Mentions: OAI.NuclearUltrapower.tensorContragredientRep

def OAI.NuclearUltrapower.finiteSubspaceRep line 249
Source documentation
The honest finite-dimensional subrepresentation on an invariant subspace.
```
def finiteSubspaceRep : FiniteUnitaryRep.{u,v} Γ where
…
```
theorem OAI.NuclearUltrapower.finiteSubspace_exists_irreducible line 266
Source documentation
Every nonzero finite subrepresentation contains an irreducible one, with an explicit isometric intertwiner into the original ambient Hilbert space.
```
theorem finiteSubspace_exists_irreducible :
    ∃ τ : FiniteUnitaryRep.{u,v} Γ, τ.Irreducible ∧
      ∃ T : τ →ₗᵢ[ℂ] K, ∀ g x, T (τ.action g x) = σ g (T x) := by
…
```