OAI/Topology/ArtinGroups/ParabolicIntersections/PointedInitialStabilizer.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The initial pointed-family stabilizer inside a frame-avoiding standard subgroup.

  1. lemma OAI.HarmonicArtin.ParabolicIntersections.initial_containing_subset line 11
  2. theorem OAI.HarmonicArtin.ParabolicIntersections.pointed_initial_stabilizer_le line 29

    Source documentation

    The only frame-avoiding words fixing the initial family are generated by the colors that commute with the frame.

    theorem pointed_initial_stabilizer_le (Y:Set S) (hf:f∉Y)
    (a:Artin M) (ha:a∈artinParabolic M Y)
    (hfix:pointedFamily M f a=pointedFamily M f 1) :
    a∈artinParabolic M {i | i∈Y ∧ M i f=2} := by
…

    Mentions: OAI.HarmonicArtin.Artin, OAI.HarmonicArtin.artinParabolic, OAI.HarmonicArtin.ParabolicIntersections.pointedFamily