Tits System

Results named in Tau Ceti's TauCeti.GroupTheory.TitsSystem modules and in no roadmap's section, as Tau Ceti has them at commit ace60277.

TheoremThe Bruhat decomposition of a standard parabolic#

an element lies in P_J exactly when its Bruhat cell is indexed by the Weyl subgroup generated by J.

TauCeti.TitsSystem.mem_standardParabolic_iff.{u} {G : Type u} [Group G] (T : TauCeti.TitsSystem G)
  {J : Set ↑T.simple} {g : G} :
  g ∈ T.standardParabolic J ↔ ∃ w ∈ Subgroup.closure (Subtype.val '' J), g ∈ T.bruhatCell w
Lean

Formalized in Tau Ceti as TauCeti.TitsSystem.mem_standardParabolic_iff.

Sources
LeanTauCeti.TitsSystem.mem_standardParabolic_iff
Used by 2
Used byTits's simplicity theorem · Tits's theorem on normal subgroups

TheoremThe key step of Tits's theorem on normal subgroups#

If H is normal, a simple reflection whose Bruhat cell lies in H ⊔ B commutes with every simple reflection whose cell does not.

TauCeti.TitsSystem.simple_mul_comm_of_bruhatCell_subset_sup.{u} {G : Type u} [Group G]
  (T : TauCeti.TitsSystem G) {H : Subgroup G} [H.Normal] {s t : T.WeylGroup} (hs : s ∈ T.simple)
  (ht : t ∈ T.simple) (hsH : T.bruhatCell s ⊆ ↑(H ⊔ T.subgroupB))
  (htH : ¬T.bruhatCell t ⊆ ↑(H ⊔ T.subgroupB)) : s * t = t * s
Lean

Formalized in Tau Ceti as TauCeti.TitsSystem.simple_mul_comm_of_bruhatCell_subset_sup.

Sources
LeanTauCeti.TitsSystem.simple_mul_comm_of_bruhatCell_subset_sup
Used by 1
Used byTits's theorem on normal subgroups

TheoremTits's simplicity criterion for the normal closure of U#

Under the hypotheses of TauCeti.TitsSystem.le_normalCore_subgroupOf_or_eq_top_of_normal, the quotient H⁺ / (Z ∩ H⁺) of the normal closure H⁺ of U by its intersection with Z = ⋂ g B g⁻¹ is simple whenever it is nontrivial.

TauCeti.TitsSystem.isSimpleGroup_quotient_normalCore_subgroupOf.{u} {G : Type u} [Group G]
  (T : TauCeti.TitsSystem G) {U : Subgroup G} (hirr : T.IsIrreducible) [Group.IsSolvable ↥U]
  (hBU : T.subgroupB ≤ Subgroup.normalizer ↑U)
  (hsplit : T.subgroupB ≤ U ⊔ T.subgroupB ⊓ T.subgroupN)
  [Group.IsPerfect ↥(Subgroup.normalClosure ↑U)]
  [Nontrivial
      (↥(Subgroup.normalClosure ↑U) ⧸
        T.subgroupB.normalCore.subgroupOf (Subgroup.normalClosure ↑U))] :
  IsSimpleGroup
    (↥(Subgroup.normalClosure ↑U) ⧸ T.subgroupB.normalCore.subgroupOf (Subgroup.normalClosure ↑U))
Lean

Formalized in Tau Ceti as TauCeti.TitsSystem.isSimpleGroup_quotient_normalCore_subgroupOf.

Sources
LeanTauCeti.TitsSystem.isSimpleGroup_quotient_normalCore_subgroupOf
Uses 1
Proof usesTits's theorem on normal subgroups

TheoremTits's simplicity theorem#

Suppose there is at least one simple reflection, the Weyl group is irreducible, G is perfect, and U is a solvable subgroup normalized by B whose conjugates generate G. Then the quotient of G by the normal core ⋂ g B g⁻¹ of B is simple.

TauCeti.TitsSystem.isSimpleGroup_quotient_normalCore.{u} {G : Type u} [Group G]
  (T : TauCeti.TitsSystem G) (hS : T.simple.Nonempty) (hirr : T.IsIrreducible) [Group.IsPerfect G]
  {U : Subgroup G} [Group.IsSolvable ↥U] (hBU : T.subgroupB ≤ Subgroup.normalizer ↑U)
  (hU : Subgroup.normalClosure ↑U = ⊤) : IsSimpleGroup (G ⧸ T.subgroupB.normalCore)
Informally uses
Lean

Formalized in Tau Ceti as TauCeti.TitsSystem.isSimpleGroup_quotient_normalCore.

Other forms

Tits's simplicity theorem, for normal subgroups. Formalized in Tau Ceti as TauCeti.TitsSystem.le_normalCore_or_eq_top_of_normal.

TauCeti.TitsSystem.le_normalCore_or_eq_top_of_normal.{u} {G : Type u} [Group G]
  (T : TauCeti.TitsSystem G) (hirr : T.IsIrreducible) [Group.IsPerfect G] {U : Subgroup G}
  [Group.IsSolvable ↥U] (hBU : T.subgroupB ≤ Subgroup.normalizer ↑U)
  (hU : Subgroup.normalClosure ↑U = ⊤) (H : Subgroup G) [H.Normal] :
  H ≤ T.subgroupB.normalCore ∨ H = ⊤
Sources
LeanTauCeti.TitsSystem.isSimpleGroup_quotient_normalCore · TauCeti.TitsSystem.le_normalCore_or_eq_top_of_normal
Uses 1 · Used by 1
Proof usesThe Bruhat decomposition of a standard parabolic
Used byTits's theorem on normal subgroups

TheoremTits's theorem on normal subgroups#

For a normal subgroup H, the subgroup H ⊔ B is a standard parabolic P_J for a set J of simple reflections that commutes elementwise with its complement.

TauCeti.TitsSystem.exists_standardParabolic_eq_sup_of_normal.{u} {G : Type u} [Group G]
  (T : TauCeti.TitsSystem G) (H : Subgroup G) [H.Normal] :
  ∃ J, T.standardParabolic J = H ⊔ T.subgroupB ∧ ∀ s ∈ J, ∀ t ∉ J, ↑s * ↑t = ↑t * ↑s
Lean

Formalized in Tau Ceti as TauCeti.TitsSystem.exists_standardParabolic_eq_sup_of_normal.

Other forms

Tits's theorem on normal subgroups of the normal closure of U. Formalized in Tau Ceti as TauCeti.TitsSystem.le_normalCore_subgroupOf_or_eq_top_of_normal.

TauCeti.TitsSystem.le_normalCore_subgroupOf_or_eq_top_of_normal.{u} {G : Type u} [Group G]
  (T : TauCeti.TitsSystem G) {U : Subgroup G} (hirr : T.IsIrreducible) [Group.IsSolvable ↥U]
  (hBU : T.subgroupB ≤ Subgroup.normalizer ↑U)
  (hsplit : T.subgroupB ≤ U ⊔ T.subgroupB ⊓ T.subgroupN)
  [Group.IsPerfect ↥(Subgroup.normalClosure ↑U)] (K : Subgroup ↥(Subgroup.normalClosure ↑U))
  [K.Normal] : K ≤ T.subgroupB.normalCore.subgroupOf (Subgroup.normalClosure ↑U) ∨ K = ⊤
Sources
LeanTauCeti.TitsSystem.exists_standardParabolic_eq_sup_of_normal · TauCeti.TitsSystem.le_normalCore_subgroupOf_or_eq_top_of_normal
Uses 3 · Used by 1
Proof usesThe Bruhat decomposition of a standard parabolic · The key step of Tits's theorem on normal subgroups · Tits's simplicity theorem
Used byTits's simplicity criterion for the normal closure of U

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.