SpechtDuality.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Saxl.subrepPairMap line 12

Source comment

The ordinary bilinear coordinate pairing restricted to any invariant word subspace.

def subrepPairMap {n d : ℕ} (S : Subrepresentation (wordRep n d)) :
    Representation.IntertwiningMap S.toRepresentation S.toRepresentation.dual where
…

Mentions: OAI.Saxl.wordRep

lemma OAI.Saxl.subrepPairMap_injective line 25
def OAI.Saxl.subrepSelfDual line 41
Source comment
Complex conjugation-stable invariant word subspaces are canonically self-dual via bilinear evaluation, yielding equivariant projections.
```
def subrepSelfDual {n d : ℕ} (S : Subrepresentation (wordRep n d))
    (hS : ∀ x ∈ S.toSubmodule, star x ∈ S.toSubmodule) :
    Representation.Equiv S.toRepresentation S.toRepresentation.dual :=
…
```
Mentions: OAI.Saxl.wordRep
def OAI.Saxl.spechtSelfDual line 50
Source comment
Actual self-duality of every complex Specht representation.
```
def spechtSelfDual {n : ℕ} {μ : YoungDiagram} (t : Tableau n μ) :
    Representation.Equiv (spechtRep t) (spechtRep t).dual :=
…
```
Mentions: OAI.Saxl.Tableau, OAI.Saxl.spechtRep

def OAI.Saxl.subrepPairFromAmbient line 55

Source comment

Restriction of the ambient bilinear coordinate pairing to an invariant subspace.

def subrepPairFromAmbient {n d : ℕ} (S : Subrepresentation (wordRep n d)) :
    Representation.IntertwiningMap (wordRep n d) S.toRepresentation.dual where
…

Mentions: OAI.Saxl.wordRep

def OAI.Saxl.subrepProject line 72

Source comment

The genuine equivariant orthogonal-coordinate projection.

def subrepProject {n d : ℕ} (S : Subrepresentation (wordRep n d))
    (hS : ∀ x ∈ S.toSubmodule, star x ∈ S.toSubmodule) :
    Representation.IntertwiningMap (wordRep n d) S.toRepresentation :=
…

Mentions: OAI.Saxl.wordRep

lemma OAI.Saxl.subrepProject_pair line 77
def OAI.Saxl.wordMap line 85
Source comment
A tensor power of a single letter-linear map, in ordinary word coordinates.
```
def wordMap {n d e : ℕ} (L : Fin d → Fin e → ℂ) :
    Representation.IntertwiningMap (wordRep n d) (wordRep n e) where
…
```
Mentions: OAI.Saxl.wordRep
lemma OAI.Saxl.wordMap_single line 112

theorem OAI.Saxl.hom_to_cyclic_of_pair line 120

Source comment

A nonzero contraction with a real cyclic vector gives an actual nonzero intertwiner into its cyclic representation.

theorem hom_to_cyclic_of_pair {n d e : ℕ} (L : Fin d → Fin e → ℂ)
    (S : Subrepresentation (wordRep n d)) (x : S.toSubmodule)
    (u : WordSpace n e) (hu : star u = u)
    (h : dotProduct (wordMap L x.val) u ≠ 0) :
    ∃ f : Representation.IntertwiningMap S.toRepresentation
      (cyclic (wordRep n e) u).toRepresentation, f ≠ 0 := by
…

Mentions: OAI.Saxl.wordRep, OAI.Saxl.WordSpace, OAI.Saxl.wordMap, OAI.Saxl.cyclic