OAI/RepresentationTheory/Saxl/SupportSeparation.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Saxl.hom_separates_of_simple_support line 16

   Source comment

   In a semisimple module, support containment is equivalent to separation by homomorphisms (multiplicities are immaterial for the band step).

   theorem hom_separates_of_simple_support {R : Type uR} {X : Type uX} {Y : Type uY} [Ring R]
       [AddCommGroup X] [Module R X] [AddCommGroup Y] [Module R Y]
       [IsSemisimpleModule R X]
       (h : ∀ S : Submodule R X, IsSimpleModule R S →
         ∃ f : S →ₗ[R] Y, f ≠ 0) (x : X) (hx : x ≠ 0) :
       ∃ f : X →ₗ[R] Y, f x ≠ 0 := by
   …

2. def OAI.Saxl.subrepModuleEquiv line 48

   Source comment

   The invariant-subspace and group-algebra subtype constructions agree.

   def subrepModuleEquiv {G : Type uG} {V : Type uV} [Group G] [AddCommGroup V] [Module ℂ V]
       {ρ : Representation ℂ G V} (S : Subrepresentation ρ) :
       S.toRepresentation.asModule ≃ₗ[ℂ[G]] S.asSubmodule where
   …

3. lemma OAI.Saxl.subrep_irreducible_of_simple line 70
4. theorem OAI.Saxl.intertwining_separates_of_simple_support line 84
5. def OAI.Saxl.subrepInclusion line 122
6. theorem OAI.Saxl.word_support_separates line 130

   Source comment

   All constituents needed from a d-letter permutation module are detected by a module containing each Specht type of height at most d.

   theorem word_support_separates {n d : ℕ} {V : Type uV} [AddCommGroup V] [Module ℂ V]
       (σ : Representation ℂ (Equiv.Perm (Fin n)) V)
       (h : ∀ (μ : YoungDiagram) (t : Tableau n μ), μ.colLen 0 ≤ d →
         ∃ f : Representation.IntertwiningMap (spechtRep t) σ, f ≠ 0)
       (x : WordSpace n d) (hx : x ≠ 0) :
       ∃ f : Representation.IntertwiningMap (wordRep n d) σ, f x ≠ 0 := by
   …

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