OAI/RepresentationTheory/Saxl/CyclicSector.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Saxl.averagedMap line 14

   Source comment

   Explicit finite-group induction on a linear map.

   def averagedMap {G : Type uG} {X : Type uX} {Y : Type uY} [Group G] [Fintype G]
       [AddCommGroup X] [Module ℂ X] [AddCommGroup Y] [Module ℂ Y]
       (ρ : Representation ℂ G X) (σ : Representation ℂ G Y) (f : X →ₗ[ℂ] Y) :
       Representation.IntertwiningMap ρ σ where
   …

2. lemma OAI.Saxl.averagedMap_apply line 34
3. theorem OAI.Saxl.sector_average_nonzero line 43

   Source comment

   Coordinate-sector induction, in precisely the nonzero-Hom form used in the staircase induction. The projector kills translates outside the stabilizer.

   theorem sector_average_nonzero {G : Type uG} {X : Type uX} {Y : Type uY} [Group G] [Fintype G]
       [AddCommGroup X] [Module ℂ X] [AddCommGroup Y] [Module ℂ Y]
       (ρ : Representation ℂ G X) (σ : Representation ℂ G Y)
       (H : Subgroup G) (f : X →ₗ[ℂ] Y) (hf : f ≠ 0)
       (he : ∀ g ∈ H, ∀ x, f (ρ g x) = σ g (f x))
       (P : Y →ₗ[ℂ] Y) (hP : ∀ x, P (f x) = f x)
       (hkill : ∀ g ∉ H, ∀ x, P (σ g (f x)) = 0) :
       averagedMap ρ σ f ≠ 0 := by
   …

   Mentions: OAI.Saxl.averagedMap

4. theorem OAI.Saxl.intertwining_lift_surjective line 78
5. def OAI.Saxl.wordSector line 98
6. theorem OAI.Saxl.sector_support_transfer line 103

   Source comment

   Concrete sector averaging produces a constituent of the full cyclic module from an equivariant map on its coordinate sector.

   theorem sector_support_transfer {n d : ℕ} {X : Type uX} [AddCommGroup X] [Module ℂ X]
       (ρ : Representation ℂ (Equiv.Perm (Fin n)) X)
       (D : Fin n → Prop) (A : Fin d → Prop) (z : WordSpace n d)
       (f : X →ₗ[ℂ] WordSpace n d) (hf : f ≠ 0)
       (he : ∀ g ∈ sectorGroup D, ∀ x, f (ρ g x) = wordRep n d g (f x))
       (hm : ∀ x, f x ∈ cyclic (wordRep n d) z)
       (hs : ∀ x w, f x w ≠ 0 → wordSector D A w) :
       ∃ F : Representation.IntertwiningMap ρ (cyclic (wordRep n d) z).toRepresentation,
         F ≠ 0 := by
   …

   Mentions: OAI.Saxl.WordSpace, OAI.Saxl.sectorGroup, OAI.Saxl.wordRep, OAI.Saxl.cyclic, OAI.Saxl.wordSector

7. lemma OAI.Saxl.intertwiner_cyclic_mem line 154
8. def OAI.Saxl.cyclicMap line 170
9. lemma OAI.Saxl.cyclicMap_surjective line 182
10. theorem OAI.Saxl.cyclic_projection_support line 214

    Source comment

    A genuine equivariant projection of a cyclic generator transfers every nonzero constituent map back to the original cyclic module by Maschke.

    theorem cyclic_projection_support {G : Type uG} {X : Type uX} {Y : Type uY} {Z : Type uZ} [Group G] [Finite G]
        [AddCommGroup X] [Module ℂ X] [AddCommGroup Y] [Module ℂ Y]
        [AddCommGroup Z] [Module ℂ Z]
        {ρ : Representation ℂ G X} {σ : Representation ℂ G Y} {τ : Representation ℂ G Z}
        (F : Representation.IntertwiningMap ρ σ) (v : X)
        (f : Representation.IntertwiningMap τ (cyclic σ (F v)).toRepresentation) (hf : f ≠ 0) :
        ∃ g : Representation.IntertwiningMap τ (cyclic ρ v).toRepresentation, g ≠ 0 := by
    …

    Mentions: OAI.Saxl.cyclic

11. lemma OAI.Saxl.cyclic_smul_eq line 233
12. lemma OAI.Saxl.cyclic_action_eq line 244
13. lemma OAI.Saxl.support_relabel line 253
14. def OAI.Saxl.restrictLetters line 267