OAI/Topology/ArtinGroups/ParabolicIntersections/PointedFamily.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

The existing categorical action with an arbitrary original color as frame.

  1. abbrev OAI.HarmonicArtin.ParabolicIntersections.PointedLabel line 21
  2. abbrev OAI.HarmonicArtin.ParabolicIntersections.PointedClass line 22
  3. abbrev OAI.HarmonicArtin.ParabolicIntersections.PointedFamilySpace line 23
  4. def OAI.HarmonicArtin.ParabolicIntersections.pointedAction line 25
  5. def OAI.HarmonicArtin.ParabolicIntersections.pointedInitial line 28
  6. def OAI.HarmonicArtin.ParabolicIntersections.pointedFamily line 31
  7. theorem OAI.HarmonicArtin.ParabolicIntersections.pointedAction_generator line 34
  8. theorem OAI.HarmonicArtin.ParabolicIntersections.pointed_orthogonal line 38
  9. theorem OAI.HarmonicArtin.ParabolicIntersections.pointed_generator_fixes_initial line 53

    Source documentation

    A color nonadjacent to the frame fixes each initial projective.

    theorem pointed_generator_fixes_initial (s f : S) (hsf : M s f = 2)
    (L : PointedLabel M) :
    pointedAction M (generator M s) (pointedInitial M f L) = pointedInitial M f L := by
…

    Mentions: OAI.HarmonicArtin.ParabolicIntersections.PointedLabel, OAI.HarmonicArtin.ParabolicIntersections.pointedAction, OAI.HarmonicArtin.generator, OAI.HarmonicArtin.ParabolicIntersections.pointedInitial

  10. theorem OAI.HarmonicArtin.ParabolicIntersections.pointed_standard_fixes_initial line 71

    Source documentation

    The whole standard subgroup of nonadjacent colors fixes the frame.

    theorem pointed_standard_fixes_initial (X : Set S) (f : S)
    (hX : ∀ s ∈ X, M s f = 2) (g : Artin M) (hg : g ∈ artinParabolic M X)
    (L : PointedLabel M) :
    pointedAction M g (pointedInitial M f L) = pointedInitial M f L := by
…

    Mentions: OAI.HarmonicArtin.Artin, OAI.HarmonicArtin.artinParabolic, OAI.HarmonicArtin.ParabolicIntersections.PointedLabel, OAI.HarmonicArtin.ParabolicIntersections.pointedAction, OAI.HarmonicArtin.ParabolicIntersections.pointedInitial

  11. instance OAI.HarmonicArtin.ParabolicIntersections.pointedFamilyMulAction line 88