Multiplicity.lean`

20 declarations, 0 contain sorry, 0 declared as axioms

def OAI.RowColumn.algebraicAverage line 16
lemma OAI.RowColumn.intertwiner_has_retraction line 32
Source documentation
Averaging an algebraic left inverse produces a genuine equivariant retraction. Used to transfer the signed-slot commutant bound to the hook Specht module.
```
lemma intertwiner_has_retraction (L : Representation.IntertwiningMap ρ σ)
    (hL : Function.Injective L) :
    ∃ R : Representation.IntertwiningMap σ ρ, ∀ v, R (L v) = v := by
…
```
def OAI.RowColumn.extendCommutant line 53
lemma OAI.RowColumn.extendCommutant_injective line 61
lemma OAI.RowColumn.commutant_finrank_le_of_embedding line 73
lemma OAI.RowColumn.adjoint_intertwines line 94
def OAI.RowColumn.copyIdempotent line 107
lemma OAI.RowColumn.adjoint_copy_apply line 120
lemma OAI.RowColumn.copyIdempotent_apply line 132

lemma OAI.RowColumn.copyIdempotent_independent line 145

Source documentation

Orthogonal nonzero copies supply linearly independent elements of the commutant by their actual range projections.

lemma copyIdempotent_independent [Nontrivial V]
    (hI : ∀ i, Intertwines ρ τ (I i).toLinearMap)
    (hρ : IsUnitary ρ) (hτ : IsUnitary τ)
    (ho : ∀ i j, i ≠ j → ∀ v w, inner ℂ (I i v) (I j w) = 0) :
    LinearIndependent ℂ (copyIdempotent I hI hρ hτ) := by
…

Mentions: OAI.RowColumn.Intertwines, OAI.RowColumn.copyIdempotent

lemma OAI.RowColumn.copy_count_le_commutant line 161
def OAI.RowColumn.lineGroupCongr line 176
def OAI.RowColumn.commutantOfComp line 194
lemma OAI.RowColumn.commutantOfComp_injective line 203
lemma OAI.RowColumn.commutant_comp_finrank_le line 209
abbrev OAI.RowColumn.hookLineTarget line 220
def OAI.RowColumn.hookLineEmbedding line 224
lemma OAI.RowColumn.hookLineEmbedding_injective line 234
lemma OAI.RowColumn.hook_line_commutant_bound line 242
Source documentation
Polynomial commutant estimate for the actual hook Specht representation restricted to arbitrary fibres. This is the required first multiplicity bound for both row and column restrictions in the occupied theorem.
```
lemma hook_line_commutant_bound :
    Module.finrank ℂ (Representation.IntertwiningMap
      ((relabelledUnitary a e).comp (lineGroup f).subtype)
      ((relabelledUnitary a e).comp (lineGroup f).subtype)) ≤
      (Fintype.card S + 1) ^ (4 * Fintype.card L * h ^ 2) := by
…
```
Mentions: OAI.RowColumn.lineGroup
lemma OAI.RowColumn.hook_line_copy_count line 256