OAI/Topology/ArtinGroups/ParabolicIntersections/Basic.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

Parabolic subgroups for result 082-03

We use the Artin presentation and standard parabolics already used by Topology.ArtinGroups. In Mathlib's Coxeter matrix convention, a zero off-diagonal entry means an infinite label.

  1. def OAI.HarmonicArtin.ParabolicIntersections.conjugate line 18

    Source documentation

    g P g⁻¹, with membership expressed without existential witnesses.

    Distinct definitions of this name: ComparatorChallenges/ArtinParabolicIntersections.lean:36 (same statement text; different proof or body). Qualify references as OAI.HarmonicArtin.ParabolicIntersections.conjugate@path.

    def conjugate (g : G) (P : Subgroup G) : Subgroup G :=
…
  2. theorem OAI.HarmonicArtin.ParabolicIntersections.mem_conjugate line 21
  3. theorem OAI.HarmonicArtin.ParabolicIntersections.conjugate_one line 25
  4. theorem OAI.HarmonicArtin.ParabolicIntersections.conjugate_top line 29
  5. theorem OAI.HarmonicArtin.ParabolicIntersections.conjugate_bot line 33
  6. theorem OAI.HarmonicArtin.ParabolicIntersections.conjugate_mul line 44
  7. theorem OAI.HarmonicArtin.ParabolicIntersections.conjugate_inv_cancel line 50
  8. theorem OAI.HarmonicArtin.ParabolicIntersections.conjugate_mono line 54
  9. theorem OAI.HarmonicArtin.ParabolicIntersections.conjugate_le_conjugate_iff line 57
  10. theorem OAI.HarmonicArtin.ParabolicIntersections.conjugate_inf line 64
  11. def OAI.HarmonicArtin.ParabolicIntersections.conjugateOrderIso line 68

    Source documentation

    Conjugation as an order isomorphism of the subgroup lattice.

    def conjugateOrderIso (g : G) : Subgroup G ≃o Subgroup G where
…
  12. theorem OAI.HarmonicArtin.ParabolicIntersections.conjugate_sup line 75
  13. theorem OAI.HarmonicArtin.ParabolicIntersections.conjugate_eq_self line 79
  14. def OAI.HarmonicArtin.ParabolicIntersections.IsParabolic line 93

    Source documentation

    Conjugates of standard subgroups, with no spherical-type restriction.

    Also declared: ComparatorChallenges/ArtinParabolicIntersections.lean:42 (same declaration text).

    def IsParabolic (P : Subgroup (Artin M)) : Prop :=
…

    Mentions: OAI.HarmonicArtin.Artin

  15. theorem OAI.HarmonicArtin.ParabolicIntersections.standard_isParabolic line 96
  16. theorem OAI.HarmonicArtin.ParabolicIntersections.isParabolic_conjugate line 99
  17. theorem OAI.HarmonicArtin.ParabolicIntersections.standard_univ line 104
  18. theorem OAI.HarmonicArtin.ParabolicIntersections.standard_mono line 108
  19. theorem OAI.HarmonicArtin.ParabolicIntersections.standard_union line 112
  20. theorem OAI.HarmonicArtin.ParabolicIntersections.top_isParabolic line 116