OAI/Topology/ArtinGroups/ParabolicIntersections/RelativeFamily.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

The relative categorical family of paper 082-03

The family consists of actual bounded-projective homotopy classes in the extended diagram. Its initial color is the new relative color f; the auxiliary universal color is the one already adjoined by the fusion model.

  1. abbrev OAI.HarmonicArtin.ParabolicIntersections.RelativeLabel line 20
  2. abbrev OAI.HarmonicArtin.ParabolicIntersections.RelativeClass line 21
  3. abbrev OAI.HarmonicArtin.ParabolicIntersections.RelativeFamilySpace line 22
  4. def OAI.HarmonicArtin.ParabolicIntersections.relativeAction line 24
  5. def OAI.HarmonicArtin.ParabolicIntersections.relativeInitial line 27
  6. def OAI.HarmonicArtin.ParabolicIntersections.relativeFamily line 29
  7. theorem OAI.HarmonicArtin.ParabolicIntersections.relativeFamily_one line 32
  8. theorem OAI.HarmonicArtin.ParabolicIntersections.relativeFamily_mul line 36
  9. theorem OAI.HarmonicArtin.ParabolicIntersections.relative_generator_fixes_initial line 41

    Source documentation

    The easy inclusion in Proposition 8.3.

    theorem relative_generator_fixes_initial (s : S) (hs : s ∈ X) (L : RelativeLabel M X) :
    relativeAction M X (generator M s) (relativeInitial M X L) = relativeInitial M X L := by
…

    Mentions: OAI.HarmonicArtin.ParabolicIntersections.RelativeLabel, OAI.HarmonicArtin.ParabolicIntersections.relativeAction, OAI.HarmonicArtin.generator, OAI.HarmonicArtin.ParabolicIntersections.relativeInitial

  10. theorem OAI.HarmonicArtin.ParabolicIntersections.standard_fixes_relativeInitial line 49

    Source documentation

    Verified containment of the standard subgroup in the actual initial stabilizer.

    theorem standard_fixes_relativeInitial (g : Artin M) (hg : g ∈ artinParabolic M X)
    (L : RelativeLabel M X) :
    relativeAction M X g (relativeInitial M X L) = relativeInitial M X L := by
…

    Mentions: OAI.HarmonicArtin.Artin, OAI.HarmonicArtin.artinParabolic, OAI.HarmonicArtin.ParabolicIntersections.RelativeLabel, OAI.HarmonicArtin.ParabolicIntersections.relativeAction, OAI.HarmonicArtin.ParabolicIntersections.relativeInitial

  11. instance OAI.HarmonicArtin.ParabolicIntersections.relativeFamilyMulAction line 58
  12. theorem OAI.HarmonicArtin.ParabolicIntersections.relativeFamily_eq_smul line 67
  13. theorem OAI.HarmonicArtin.ParabolicIntersections.standard_le_relative_stabilizer line 70