OAI/RepresentationTheory/Young/Restriction.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CoordinateSweeps.CommutingRestriction.homAction line 29

   Source comment

   The action of a commuting group on the multiplicity space.

   def homAction (τ : Representation ℂ G V) (σ : Representation ℂ H V)
       (hc : ∀ g h, Commute (τ g) (σ h)) (ρ : Representation ℂ G W) :
       Representation ℂ H (ρ.IntertwiningMap τ) where
   …

2. lemma OAI.CoordinateSweeps.CommutingRestriction.homAction_apply line 43
3. def OAI.CoordinateSweeps.CommutingRestriction.inclusion line 47
4. lemma OAI.CoordinateSweeps.CommutingRestriction.homAction_fixedSum line 52
5. lemma OAI.CoordinateSweeps.CommutingRestriction.homAction_alternatingSum line 59
6. lemma OAI.CoordinateSweeps.CommutingRestriction.sum_intertwine line 68
7. theorem OAI.CoordinateSweeps.CommutingRestriction.joint_corner_multiplicity line 90

   Source comment

   Exact multiplicity lower bound from two commuting Young corners for the removed-hook argument.

   theorem joint_corner_multiplicity (τ : Representation ℂ (Equiv.Perm X) V)
       (σ : Representation ℂ (Equiv.Perm Y) V) (hc : ∀ g h, Commute (τ g) (σ h))
       (μ ν : YoungDiagram) (t : X ≃ Boxes μ) (u : Y ≃ Boxes ν)
       (δ : Representation ℂ (Equiv.Perm Y) Z) [δ.IsIrreducible] (hδ : hasShape ν u δ)
       (hne : (fixedSum (rowColor t) τ * alternatingSum (colColor t) τ) *
         (fixedSum (rowColor u) σ * alternatingSum (colColor u) σ) ≠ 0) :
       ∃ S : Subrepresentation τ, S.toRepresentation.IsIrreducible ∧ hasShape μ t S.toRepresentation ∧
         Module.finrank ℂ Z ≤ Module.finrank ℂ (S.toRepresentation.IntertwiningMap τ) := by
   …

8. lemma OAI.CoordinateSweeps.YoungCorner.signScalar_ne_zero line 146
9. lemma OAI.CoordinateSweeps.YoungCorner.fixedSum_absorb line 149
10. lemma OAI.CoordinateSweeps.YoungCorner.alternatingSum_absorb line 161
11. lemma OAI.CoordinateSweeps.YoungCorner.joint_of_full_corner line 177

    Source comment

    A split of the row and column stabilizers preserves a nonzero Young corner.

    lemma joint_of_full_corner (τ : Equiv.Perm X →* A)
        (fR fC : X → ℕ) (gR gC : Y → ℕ) (hR hC : Z → ℕ)
        (φ : Equiv.Perm Y →* Equiv.Perm X) (ψ : Equiv.Perm Z →* Equiv.Perm X)
        (hφR : ∀ r : colorStabilizer gR, φ r.val ∈ colorStabilizer fR)
        (hφC : ∀ c : colorStabilizer gC, φ c.val ∈ colorStabilizer fC)
        (hψR : ∀ r : colorStabilizer hR, ψ r.val ∈ colorStabilizer fR)
        (hψC : ∀ c : colorStabilizer hC, ψ c.val ∈ colorStabilizer fC)
        (hφs : ∀ g : Equiv.Perm Y, signScalar (φ g)=signScalar g)
        (hψs : ∀ g : Equiv.Perm Z, signScalar (ψ g)=signScalar g)
        (hcomm : ∀ g h, Commute (φ g) (ψ h))
        (hne : fixedSum fR τ * alternatingSum fC τ ≠ 0) :
        (fixedSum gR (τ.comp φ)*alternatingSum gC (τ.comp φ)) *
    …

    Mentions: OAI.CoordinateSweeps.YoungCorner.colorStabilizer, OAI.CoordinateSweeps.c, OAI.CoordinateSweeps.YoungCorner.signScalar, OAI.CoordinateSweeps.YoungCorner.fixedSum, OAI.CoordinateSweeps.YoungCorner.alternatingSum

12. def OAI.CoordinateSweeps.YoungCorner.hookPart line 243
13. lemma OAI.CoordinateSweeps.YoungCorner.mem_hookPart line 253
14. def OAI.CoordinateSweeps.YoungCorner.shifted line 257
15. lemma OAI.CoordinateSweeps.YoungCorner.shifted_injective line 258
16. def OAI.CoordinateSweeps.YoungCorner.removedPart line 264
17. lemma OAI.CoordinateSweeps.YoungCorner.mem_removedPart line 272
18. def OAI.CoordinateSweeps.YoungCorner.boxesSplit line 277
19. lemma OAI.CoordinateSweeps.YoungCorner.boxesSplit_inl line 304
20. lemma OAI.CoordinateSweeps.YoungCorner.boxesSplit_inr line 306
21. def OAI.CoordinateSweeps.YoungCorner.leftPerm line 311
22. def OAI.CoordinateSweeps.YoungCorner.rightPerm line 322
23. lemma OAI.CoordinateSweeps.YoungCorner.leftPerm_inl line 333
24. lemma OAI.CoordinateSweeps.YoungCorner.leftPerm_inr line 335
25. lemma OAI.CoordinateSweeps.YoungCorner.rightPerm_inl line 337
26. lemma OAI.CoordinateSweeps.YoungCorner.rightPerm_inr line 339
27. lemma OAI.CoordinateSweeps.YoungCorner.splitPerm_commute line 342
28. lemma OAI.CoordinateSweeps.YoungCorner.leftPerm_rows line 349
29. lemma OAI.CoordinateSweeps.YoungCorner.leftPerm_cols line 357
30. lemma OAI.CoordinateSweeps.YoungCorner.rightPerm_rows line 365
31. lemma OAI.CoordinateSweeps.YoungCorner.rightPerm_cols line 373
32. lemma OAI.CoordinateSweeps.YoungCorner.rectangle_card_le line 385
33. lemma OAI.CoordinateSweeps.YoungCorner.removedPart_rank_lt line 396
34. lemma OAI.CoordinateSweeps.YoungCorner.hookPart_property line 411
35. lemma OAI.CoordinateSweeps.YoungCorner.split_card line 414
36. lemma OAI.CoordinateSweeps.YoungCorner.signScalar_leftPerm line 425
37. lemma OAI.CoordinateSweeps.YoungCorner.signScalar_rightPerm line 429
38. lemma OAI.CoordinateSweeps.YoungCorner.hook_removed_joint line 433
39. theorem OAI.CoordinateSweeps.YoungCorner.hook_removed_multiplicity line 445

    Source comment

    Retained-hook multiplicity for the hook part and translated removed partition.

    theorem hook_removed_multiplicity {V W : Type} [AddCommGroup V] [Module ℂ V]
        [FiniteDimensional ℂ V] [AddCommGroup W] [Module ℂ W] [FiniteDimensional ℂ W]
        (μ : YoungDiagram) (p : ℕ) (τ : Representation ℂ (Equiv.Perm (Boxes μ)) V)
        (hτ : hasShape μ (Equiv.refl _) τ)
        (δ : Representation ℂ (Equiv.Perm (Boxes (removedPart μ p))) W) [δ.IsIrreducible]
        (hδ : hasShape (removedPart μ p) (Equiv.refl _) δ) :
        ∃ S : Subrepresentation (τ.comp (leftPerm (boxesSplit μ p))),
          S.toRepresentation.IsIrreducible ∧ hasShape (hookPart μ p) (Equiv.refl _) S.toRepresentation ∧
          Module.finrank ℂ W ≤ Module.finrank ℂ
            (S.toRepresentation.IntertwiningMap (τ.comp (leftPerm (boxesSplit μ p)))) := by
    …

    Mentions: OAI.CoordinateSweeps.YoungCorner.Boxes, OAI.CoordinateSweeps.YoungCorner.hasShape, OAI.CoordinateSweeps.YoungCorner.removedPart, OAI.CoordinateSweeps.YoungCorner.leftPerm, OAI.CoordinateSweeps.YoungCorner.boxesSplit, OAI.CoordinateSweeps.YoungCorner.hookPart

40. lemma OAI.CoordinateSweeps.YoungCorner.leftPerm_range_of_fix_right line 468
41. lemma OAI.CoordinateSweeps.RestrictionBound.orbit_span_top line 499
42. theorem OAI.CoordinateSweeps.RestrictionBound.dimension_le_pow_mul line 522

    Source comment

    A pointwise-stabilizer constituent generates at most n^k copies of its vector space. This is the exact logarithmic dimension upper bound in06:eq22.

    theorem dimension_le_pow_mul (ρ : Representation ℂ (Equiv.Perm Ω) V) [ρ.IsIrreducible]
        (a : I → Ω) (W : Submodule ℂ V) (hW : W ≠ ⊥)
        (hstable : ∀ g : Equiv.Perm Ω, (∀ i, g (a i)=a i) → ∀ w ∈ W, ρ g w ∈ W) :
        Module.finrank ℂ V ≤ (Fintype.card Ω)^(Fintype.card I)*Module.finrank ℂ W := by
    …

    Mentions: OAI.CoordinateSweeps.a

43. theorem OAI.CoordinateSweeps.YoungCorner.hook_dimension_upper line 572

    Source comment

    The retained hook gives a dimension upper bound (source06:eq22).

    theorem hook_dimension_upper {V : Type} [AddCommGroup V] [Module ℂ V]
        [FiniteDimensional ℂ V] (μ : YoungDiagram) (p : ℕ)
        (τ : Representation ℂ (Equiv.Perm (Boxes μ)) V) [τ.IsIrreducible]
        (S : Subrepresentation (τ.comp (leftPerm (boxesSplit μ p)))) (hS : S ≠ ⊥) :
        Module.finrank ℂ V ≤ (Fintype.card (Boxes μ))^(Fintype.card (Boxes (removedPart μ p))) *
          Module.finrank ℂ S.toSubmodule := by
    …

    Mentions: OAI.CoordinateSweeps.YoungCorner.Boxes, OAI.CoordinateSweeps.YoungCorner.leftPerm, OAI.CoordinateSweeps.YoungCorner.boxesSplit, OAI.CoordinateSweeps.YoungCorner.removedPart

44. def OAI.CoordinateSweeps.YoungCorner.colorEquiv line 590
45. lemma OAI.CoordinateSweeps.YoungCorner.fixedSum_reparam line 600
46. lemma OAI.CoordinateSweeps.YoungCorner.alternatingSum_reparam line 603
47. lemma OAI.CoordinateSweeps.YoungCorner.hasShape_reparam line 610
48. def OAI.Representation.IntertwiningMap.reparamEquiv line 624

    Source comment

    Reparameterizing a group does not alter the Hom multiplicity.

    def reparamEquiv (ρ : Representation ℂ Γ V) (τ : Representation ℂ Γ W) (e : Λ ≃* Γ) :
        ρ.IntertwiningMap τ ≃ₗ[ℂ] Representation.IntertwiningMap (ρ.comp e.toMonoidHom) (τ.comp e.toMonoidHom) where
    …

49. def OAI.Representation.IntertwiningMap.sourceEquiv line 636

    Source comment

    Changing the source realization by an equivalence preserves Hom.

    def sourceEquiv {U : Type*} [AddCommGroup U] [Module ℂ U]
        {ρ : Representation ℂ Γ V} {σ : Representation ℂ Γ U}
        (e : Representation.Equiv ρ σ) (τ : Representation ℂ Γ W) :
        ρ.IntertwiningMap τ ≃ₗ[ℂ] σ.IntertwiningMap τ where
    …