OAI/Topology/ArtinGroups/ParabolicIntersections/VisualFactorMalnormal.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Weak malnormality for the vertex factors, and hence their parabolics.

  1. lemma OAI.HarmonicArtin.ParabolicIntersections.trivial_pair_endpoint_type line 15
  2. lemma OAI.HarmonicArtin.ParabolicIntersections.visual_trivial_pair_distinct_type line 41

    Source documentation

    A nondegenerate segment with trivial stabilizer in either vertex orbit.

    lemma visual_trivial_pair_distinct_type (hIrred : IsIrreducible M) (b : Bool) :
    ∃ u v : VisualVertex M Y Z, u≠v ∧ u.1=b ∧ v.1=b ∧
      pairStabilizer (G := Artin M) u v=⊥ := by
…

    Mentions: OAI.HarmonicArtin.ParabolicIntersections.IsIrreducible, OAI.HarmonicArtin.ParabolicIntersections.VisualVertex, OAI.HarmonicArtin.Artin

  3. lemma OAI.HarmonicArtin.ParabolicIntersections.visual_trivial_pair_type line 52

    Source documentation

    Both endpoints may be taken in either vertex orbit.

    lemma visual_trivial_pair_type (hIrred : IsIrreducible M) (b : Bool) :
    ∃ u v : VisualVertex M Y Z, u.1=b ∧ v.1=b ∧
      pairStabilizer (G := Artin M) u v=⊥ := by
…

    Mentions: OAI.HarmonicArtin.ParabolicIntersections.IsIrreducible, OAI.HarmonicArtin.ParabolicIntersections.VisualVertex, OAI.HarmonicArtin.Artin

  4. theorem OAI.HarmonicArtin.ParabolicIntersections.visual_factor_weaklyMalnormal line 63

    Source documentation

    Each vertex factor of a visual splitting is weakly malnormal.

    theorem visual_factor_weaklyMalnormal (hIrred : IsIrreducible M) (b : Bool) :
    WeaklyMalnormal (artinParabolic M (visualSide Y Z b)) := by
…

    Mentions: OAI.HarmonicArtin.ParabolicIntersections.IsIrreducible, OAI.HarmonicArtin.ParabolicIntersections.WeaklyMalnormal, OAI.HarmonicArtin.artinParabolic, OAI.HarmonicArtin.ParabolicIntersections.visualSide

  5. theorem OAI.HarmonicArtin.ParabolicIntersections.visual_subgroup_weaklyMalnormal line 75

    Source documentation

    Any parabolic lying in a vertex factor inherits its weak malnormality.

    theorem visual_subgroup_weaklyMalnormal (hIrred : IsIrreducible M)
    (b : Bool) (P : Subgroup (Artin M)) (hP : P≤artinParabolic M (visualSide Y Z b)) :
    WeaklyMalnormal P :=
…

    Mentions: OAI.HarmonicArtin.ParabolicIntersections.IsIrreducible, OAI.HarmonicArtin.Artin, OAI.HarmonicArtin.artinParabolic, OAI.HarmonicArtin.ParabolicIntersections.visualSide, OAI.HarmonicArtin.ParabolicIntersections.WeaklyMalnormal