CyclicTensor.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Saxl.equivOfSubrepEq line 13

theorem OAI.Saxl.young_orbit_map line 20

Source comment

Positive Young rule as a concrete orbit map (including reordered contents).

theorem young_orbit_map {n : ℕ} (θ τ : YoungDiagram) (t : Tableau n τ)
    (hc : τ.card = θ.card) (hd : Dominates τ θ)
    (w : Fin n → Fin (θ.colLen 0)) (e : Equiv.Perm (Fin (θ.colLen 0)))
    (hw : ∀ j, (Finset.univ.filter (fun i => w i = e j)).card = θ.rowLen j) :
    ∃ F : Representation.IntertwiningMap (wordRep n (θ.colLen 0)) (spechtRep t),
      F (Pi.single w 1) ≠ 0 := by
…

Mentions: OAI.Saxl.Tableau, OAI.Saxl.Dominates, OAI.Saxl.wordRep, OAI.Saxl.spechtRep

def OAI.Saxl.intertwiningRangeEquiv line 74
def OAI.Saxl.staircaseCyclicInclusion line 85
def OAI.Saxl.intertwiningLiftSubrep line 91
lemma OAI.Saxl.intertwiningLiftSubrep_injective line 101
def OAI.Saxl.staircaseToTensor line 114
Source comment
The genuine cyclic module is embedded in the actual staircase Specht square.
```
def staircaseToTensor (m : ℕ) :
    Representation.IntertwiningMap (staircaseCyclic m).toRepresentation
      ((spechtRep (stairTableau m)).tprod (spechtRep (stairTableau m))) :=
…
```
Mentions: OAI.Saxl.staircaseCyclic, OAI.Saxl.spechtRep, OAI.Saxl.stairTableau
lemma OAI.Saxl.staircaseToTensor_injective line 128
def OAI.Saxl.CyclicSaxlConjecture line 140
Source comment
Every Specht type occurs in the specified staircase cyclic module.
```
def CyclicSaxlConjecture : Prop :=
…
```
theorem OAI.Saxl.saxl_of_cyclic_support line 146
Source comment
A proof of cyclic support proves the original Kronecker-multiplicity target.
```
theorem saxl_of_cyclic_support (h : CyclicSaxlConjecture) : SaxlConjecture := by
…
```
Mentions: OAI.Saxl.CyclicSaxlConjecture, OAI.Saxl.SaxlConjecture