OAI/Topology/ArtinGroups/ParabolicIntersections/RelativeInitialStabilizer.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The initial stabilizer in the relative diagram

The sole input below is the unrestricted standard-parabolic embedding theorem: van der Lek, The Homotopy Type of Complex Hyperplane Complements (1983), Chapter II, §4, Theorem 4.13(i). See also Charney–Paris, Convexity of parabolic subgroups in Artin groups (2014), §1, p. 2, https://arxiv.org/abs/1401.7634. The exact case needed is injectivity of the canonical inclusion from the original Artin presentation into the presentation with one additional color. The categorical stabilizer identity is proved below, not assumed.

  1. structure OAI.HarmonicArtin.ParabolicIntersections.VanDerLekRelativeEmbedding line 23
  2. lemma OAI.HarmonicArtin.ParabolicIntersections.relativeFrame_commuting_type line 27
  3. theorem OAI.HarmonicArtin.ParabolicIntersections.relative_initial_stabilizer line 36

    Source documentation

    Proposition 8.3, conditional only on the published embedding input.

    theorem relative_initial_stabilizer (hEmb:VanDerLekRelativeEmbedding M X) :
    MulAction.stabilizer (Artin M) (relativeInitial M X) = artinParabolic M X := by
…

    Mentions: OAI.HarmonicArtin.ParabolicIntersections.VanDerLekRelativeEmbedding, OAI.HarmonicArtin.Artin, OAI.HarmonicArtin.ParabolicIntersections.relativeInitial, OAI.HarmonicArtin.artinParabolic