CLS_low_two_rank_classification to CL_LIT_SQTK_simple_list
TheoremCLS_low_two_rank_classification#
The milestone module CFSG.Milestones.CLS_low_two_rank_classification, one of those CFSG/Milestones.lean imports.
It declares 1 result, quoted from CFSG/Milestones/CLS_low_two_rank_classification.lean in AxiomMath/CFSG at commit 69cb972f, Apache-2.0:
CFSG.Milestones.cls_low_two_rank_classification (theorem, line 12). Proved here.
theorem _root_.CFSG.Milestones.cls_low_two_rank_classification
(G : Type) [Group G] [Finite G] [IsSimpleGroup G]
(hnonab : ∃ a b : G, a * b ≠ b * a) (heven : Even (Nat.card G))
(hrank : twoRank G ≤ 2) : CFSG.Blueprint.Catalog G
The files of 1 case theorem import it, directly or through other files: CFSG.Assembly.rank_three_even.
Uses 1 · Used by 2
TheoremCLS_rank_three_even_classification#
The milestone module CFSG.Milestones.CLS_rank_three_even_classification, one of those CFSG/Milestones.lean imports.
It declares 1 result, quoted from CFSG/Milestones/CLS_rank_three_even_classification.lean in AxiomMath/CFSG at commit 69cb972f, Apache-2.0:
CFSG.Milestones.cls_rank_three_even_classification (theorem, line 2613). Proved here.
theorem _root_.CFSG.Milestones.cls_rank_three_even_classification
(G : Type) [Group G] [Finite G] [IsSimpleGroup G]
(hnonab : ∃ a b : G, a * b ≠ b * a) (hK : KProper InCatalog G) (hchar : IsCharTwoType G)
(he : evenRank G = 3) : InCatalog G
No case theorem's file imports it, directly or through other files.
Uses 1
TheoremCL_LIT_AS_vol_I_background#
The milestone module CFSG.Milestones.CL_LIT_AS_vol_I_background, one of those CFSG/Milestones.lean imports.
It declares 6 results, quoted from CFSG/Milestones/CL_LIT_AS_vol_I_background.lean in AxiomMath/CFSG at commit 69cb972f, Apache-2.0:
CFSG.Milestones.cl_lit_as_vol_i_background_1 (theorem, line 19). Proved here.
theorem _root_.CFSG.Milestones.cl_lit_as_vol_i_background_1
(p f : ℕ) [Fact p.Prime] (hf : 1 ≤ f) (H : Subgroup PSL(2, GaloisField p f)) :
(IsElemAbelian p H ∧ ∃ m : ℕ, m ≤ f ∧ Nat.card H = p ^ m) ∨
(IsCyclic H ∧ (Nat.card H ∣ (p ^ f + 1) / Nat.gcd 2 (p ^ f - 1) ∨
Nat.card H ∣ (p ^ f - 1) / Nat.gcd 2 (p ^ f - 1))) ∨
(∃ z : ℕ, (z ∣ (p ^ f + 1) / Nat.gcd 2 (p ^ f - 1) ∨
z ∣ (p ^ f - 1) / Nat.gcd 2 (p ^ f - 1)) ∧ Nonempty (H ≃* DihedralGroup z)) ∨
((p ≠ 2 ∨ Even f) ∧ Nonempty (H ≃* alternatingGroup (Fin 4))) ∨
(16 ∣ p ^ (2 * f) - 1 ∧ Nonempty (H ≃* Equiv.Perm (Fin 4))) ∨
((p = 5 ∨ 5 ∣ p ^ (2 * f) - 1) ∧ Nonempty (H ≃* alternatingGroup (Fin 5))) ∨
(∃ (m t : ℕ) (P : Subgroup H) (_ : P.Normal), IsElemAbelian p P ∧
Nat.card P = p ^ m ∧ IsCyclic (H ⧸ P) ∧ Nat.card (H ⧸ P) = t ∧ t ∣ p ^ m - 1 ∧
t ∣ (p ^ f - 1) / Nat.gcd 2 (p ^ f - 1)) ∨
(∃ m : ℕ, m ∣ f ∧ Nonempty (H ≃* PSL(2, GaloisField p m))) ∨
(∃ m : ℕ, 2 * m ∣ f ∧ Nonempty (H ≃* PGL(2, GaloisField p m)))
CFSG.Milestones.cl_lit_as_vol_i_background_2 (theorem, line 43). Proved here.
theorem _root_.CFSG.Milestones.cl_lit_as_vol_i_background_2 :
(∀ n : ℕ, 2 ≤ n → quasithinH1CardSL 2 (GaloisField 2 n) = 2 ^ n) ∧
(∀ n : ℕ, 2 ≤ n → quasithinH1CardSL 3 (GaloisField 2 n) = 1) ∧
quasithinH1CardSL 3 (ZMod 2) = 2 ∧
(∀ n : ℕ, 2 ≤ n →
Nat.card (groupCohomology (Rep.of (quasithinH1MatrixRep
(Matrix.symplecticGroup (Fin 2) (GaloisField 2 n)).subtype)) 1) = 2 ^ n) ∧
quasithinH1CardSL 4 (ZMod 2) = 1 ∧
quasithinH1CardSL 5 (ZMod 2) = 1
CFSG.Milestones.cl_lit_as_vol_i_background_3 (theorem, line 61). Proved here.
theorem _root_.CFSG.Milestones.cl_lit_as_vol_i_background_3 :
quasithinMultiplierCyclic (alternatingGroup (Fin 9)) 2 ∧
(∀ (p k : ℕ) [Fact p.Prime], p ≠ 2 → 9 < p ^ k →
quasithinMultiplierCyclic PSL(2, GaloisField p k) 2) ∧
quasithinMultiplierCyclic (quasithinPSU 4 2 1) 2 ∧
quasithinMultiplierCyclic PSL(4, ZMod 3) 2 ∧
quasithinMultiplierCyclic quasithinJ3 3 ∧
quasithinMultiplierCyclic quasithinMcL 3 ∧
quasithinMultiplierCyclic (quasithinG2 (ZMod 3)) 3 ∧
(∀ (p k : ℕ) [Fact p.Prime], p ≠ 2 → 0 < k → 3 ∣ p ^ k - 1 →
quasithinMultiplierCyclic PSL(3, GaloisField p k) 3) ∧
(∀ (p k : ℕ) [Fact p.Prime], p ≠ 2 → 0 < k → 3 ∣ p ^ k + 1 →
quasithinMultiplierCyclic (PSU3 p k) 3) ∧
(∀ (r m : ℕ) [Fact r.Prime], r = 2 ^ 2 ^ m + 1 → 3 < r →
quasithinMultiplierCyclic PSL(4, ZMod r) 4) ∧
(∀ (s m : ℕ) [Fact s.Prime], s = 2 ^ m - 1 → 3 < s →
quasithinMultiplierCyclic (quasithinPSU 4 s 1) 4) ∧
quasithinMultiplierCyclic (quasithinPSU 5 2 2) 5 ∧
Nonempty (quasithinHopfMultiplier (quasithinPSU 4 3 1) ≃*
Multiplicative (ZMod 3 × ZMod 3 × ZMod 4)) ∧
quasithinMultiplierCyclic (Matrix.symplecticGroup (Fin 3) (ZMod 2)) 2 ∧
(∀ (p : ℕ) [Fact p.Prime], 5 ≤ p → quasithinMultiplierCyclic (quasithinPSp 2 (ZMod p)) 2)
CFSG.Milestones.cl_lit_as_vol_i_background_4 (theorem, line 92). Proved here.
theorem _root_.CFSG.Milestones.cl_lit_as_vol_i_background_4 :
quasithinMultiplierCyclic PSL(4, ZMod 2) 2 ∧
quasithinMultiplierCyclic (quasithinG2 (GaloisField 2 2)) 2 ∧
quasithinMultiplierCyclic quasithinM12 2 ∧
quasithinMultiplierCyclic quasithinJ2 2 ∧
quasithinMultiplierCyclic quasithinHS 2 ∧
quasithinMultiplierCyclic quasithinRu 2 ∧
(∀ (p k : ℕ) [Fact p.Prime], p ≠ 2 → 0 < k → p ^ k ≠ 3 → p ^ k ≠ 9 →
quasithinMultiplierCyclic PSL(2, GaloisField p k) 2) ∧
(∀ (p k : ℕ) [Fact p.Prime], 0 < k → 3 ∣ p ^ k - 1 → p ^ k ≠ 4 →
quasithinMultiplierCyclic PSL(3, GaloisField p k) 3) ∧
(∀ (p k : ℕ) [Fact p.Prime], 0 < k → 3 ∣ p ^ k + 1 → p ^ k ≠ 2 →
quasithinMultiplierCyclic (PSU3 p k) 3) ∧
quasithinMultiplierCyclic (alternatingGroup (Fin 6)) 6 ∧
quasithinMultiplierCyclic (alternatingGroup (Fin 7)) 6 ∧
quasithinMultiplierCyclic quasithinM22 12 ∧
Nonempty (quasithinHopfMultiplier (Sz 1) ≃* Multiplicative (ZMod 2 × ZMod 2)) ∧
Nonempty (quasithinHopfMultiplier PSL(3, GaloisField 2 2) ≃*
Multiplicative (ZMod 4 × ZMod 4 × ZMod 3))
CFSG.Milestones.cl_lit_as_vol_i_background_partial (theorem, line 120). Proved here.
theorem _root_.CFSG.Milestones.cl_lit_as_vol_i_background_partial
: CFSG.ASVolI.Statement
CFSG.Milestones.cl_lit_as_vol_i_background (theorem, line 127). Proved here.
theorem _root_.CFSG.Milestones.cl_lit_as_vol_i_background
: CFSG.ASVolI.Statement
The files of 1 case theorem import it, directly or through other files: CFSG.Assembly.rank_three_even.
TheoremCL_LIT_Aschbacher_1983_uniqueness_case_rank_three#
The milestone module CFSG.Milestones.CL_LIT_Aschbacher_1983_uniqueness_case_rank_three, one of those CFSG/Milestones.lean imports.
It declares 1 result, quoted from CFSG/Milestones/CL_LIT_Aschbacher_1983_uniqueness_case_rank_three.lean in AxiomMath/CFSG at commit 69cb972f, Apache-2.0:
CFSG.Milestones.cl_lit_aschbacher_1983_uniqueness_case_rank_three (theorem, line 3162). Proved here.
theorem _root_.CFSG.Milestones.cl_lit_aschbacher_1983_uniqueness_case_rank_three
(G : Type) [Group G] [Finite G] [IsSimpleGroup G]
(hnonab : ∃ a b : G, a * b ≠ b * a)
(hK : IsKProper G) (hchar : IsCharTwoType G) (he : evenRank G = 3) :
¬ uniqueThreeUC G
The files of 1 case theorem import it, directly or through other files: CFSG.Assembly.rank_three_even.
Uses 5 · Used by 1
TheoremCL_LIT_Aschbacher_component_type_theorem_5#
The milestone module CFSG.Milestones.CL_LIT_Aschbacher_component_type_theorem_5, one of those CFSG/Milestones.lean imports.
It declares 1 result, quoted from CFSG/Milestones/CL_LIT_Aschbacher_component_type_theorem_5.lean in AxiomMath/CFSG at commit 69cb972f, Apache-2.0:
CFSG.Milestones.cl_lit_aschbacher_component_type_theorem_5 (theorem, line 11). Proved here.
theorem _root_.CFSG.Milestones.cl_lit_aschbacher_component_type_theorem_5
(G : Type) [Group G] [Finite G]
(D : Subgroup G) (r : ℕ) (hr : 1 ≤ r)
(Abar : Fin r → Subgroup (D ⧸ aschbacherThm5OddCore D))
(hdistinct : Function.Injective Abar)
(hsemisimple : ∀ i, aschbacherThm5IsSemisimple (Abar i))
(hcomm : ∀ i j, i ≠ j → ∀ x ∈ Abar i, ∀ y ∈ Abar j, x * y = y * x)
(hgen : ⨆ i, Abar i = ⊤)
(hperm : ∀ h ∈ Subgroup.normalizer (D : Set G), ∀ i, ∃ j,
(aschbacherThm5Preimage D (Abar i)).map (MulAut.conj h).toMonoidHom =
aschbacherThm5Preimage D (Abar j))
(hi : ∀ (i j : Fin r) (t g : G), (∃ k : ℕ, t ^ (2 ^ k) = 1) → t ∉ Subgroup.center G →
aschbacherThm5Centralizes (aschbacherThm5Core D) (aschbacherThm5Preimage D (Abar i)) t →
aschbacherThm5Centralizes (aschbacherThm5Core D) (aschbacherThm5Preimage D (Abar j))
(g⁻¹ * t * g) →
g ∈ Subgroup.normalizer (D : Set G))
(hii : ∀ (i : Fin r) (g : G) (X : Subgroup G),
X ≤ (Subgroup.normalizer (D : Set G)).map (MulAut.conj g⁻¹).toMonoidHom →
(∀ a ∈ aschbacherThm5Preimage D (Abar i), ∃ x ∈ X, ∃ o ∈ aschbacherThm5Core D,
a = x * o) →
g ∈ Subgroup.normalizer (D : Set G))
(hH : Subgroup.normalizer (D : Set G) ≠ ⊤) :
r = 1 ∨
(r = 2 ∧ ∀ i j : Fin r, i ≠ j →
(∀ d ∈ D, ∃ a ∈ aschbacherThm5Preimage D (Abar i),
∃ b ∈ aschbacherThm5Preimage D (Abar j), d = a * b) ∧
pRank 2 (aschbacherThm5Preimage D (Abar i)) = 1 ∧
∀ a₁ ∈ aschbacherThm5Preimage D (Abar i), ∀ a₂ ∈ aschbacherThm5Preimage D (Abar j),
orderOf a₁ = 2 → orderOf a₂ = 2 → a₁ * a₂ = a₂ * a₁ →
aschbacherThm5Centralizes (aschbacherThm5Core D)
(aschbacherThm5Preimage D (Abar i)) a₁ →
aschbacherThm5Centralizes (aschbacherThm5Core D)
(aschbacherThm5Preimage D (Abar j)) a₂ →
a₁ = a₂ ∨ a₁ * a₂ ∈ Subgroup.center G)
The files of 3 case theorems import it, directly or through other files: CFSG.Assembly.component_type, CFSG.Assembly.rank_three_even, CFSG.Assembly.large_even.
Uses 6 · Used by 2
TheoremCL_LIT_Aschbacher_proper_two_generated_core#
The milestone module CFSG.Milestones.CL_LIT_Aschbacher_proper_two_generated_core, one of those CFSG/Milestones.lean imports.
It declares 1 result, quoted from CFSG/Milestones/CL_LIT_Aschbacher_proper_two_generated_core.lean in AxiomMath/CFSG at commit 69cb972f, Apache-2.0:
CFSG.Milestones.cl_lit_aschbacher_proper_two_generated_core (theorem, line 12). Proved here.
theorem _root_.CFSG.Milestones.cl_lit_aschbacher_proper_two_generated_core
(G : Type) [Group G] [Finite G] [IsSimpleGroup G]
(hnonab : ∃ a b : G, a * b ≠ b * a)
(S : Sylow 2 G) (hrank : 3 ≤ pRank 2 (S : Subgroup G))
(hcore : properTwoGenCoreGamma (S : Subgroup G) 2 ≠ ⊤) :
properTwoGenCoreGamma (S : Subgroup G) 1 ≠ ⊤ ∨ Nonempty (G ≃* properTwoGenCoreJ1)
The files of 3 case theorems import it, directly or through other files: CFSG.Assembly.component_type, CFSG.Assembly.rank_three_even, CFSG.Assembly.large_even.
Uses 3 · Used by 1
TheoremCL_LIT_Borel_Tits_local_parabolic#
The milestone module CFSG.Milestones.CL_LIT_Borel_Tits_local_parabolic, one of those CFSG/Milestones.lean imports.
It declares 2 results, quoted from CFSG/Milestones/CL_LIT_Borel_Tits_local_parabolic.lean in AxiomMath/CFSG at commit 69cb972f, Apache-2.0:
CFSG.Milestones.cl_lit_borel_tits_local_parabolic (theorem, line 12). Proved here.
theorem _root_.CFSG.Milestones.cl_lit_borel_tits_local_parabolic
(r k n : ℕ) [Fact r.Prime] (hk : 0 < k) (hn : 2 ≤ n) (hsmall : n = 2 → 4 ≤ r ^ k)
(U : Subgroup PSL(n, GaloisField r k)) (hU : U ≠ ⊥) (hUr : IsPGroup r U) :
∃ (S : Sylow r PSL(n, GaloisField r k)) (P : Subgroup PSL(n, GaloisField r k)),
P ≠ ⊤ ∧
Subgroup.normalizer (U : Set PSL(n, GaloisField r k)) ≤ P ∧
pCoreOf r (Subgroup.normalizer (U : Set PSL(n, GaloisField r k))) ≤ pCoreOf r P ∧
Subgroup.normalizer ((S : Subgroup PSL(n, GaloisField r k)) :
Set PSL(n, GaloisField r k)) ≤ P
CFSG.Milestones.cl_lit_borel_tits_local_parabolic_all_models (theorem, line 29). Proved here.
theorem cl_lit_borel_tits_local_parabolic_all_models
(X : Type) [Group X] (t : Assembly.LowTwoRank.StatedLieTag) (n r f : ℕ)
(hmodel : Blueprint.LieModel X t n r f)
(U : Subgroup X) (hU : U ≠ ⊥) (hUr : IsPGroup r U) :
∃ (S : Sylow r X) (P : Subgroup X), P ≠ ⊤ ∧
Subgroup.normalizer (U : Set X) ≤ P ∧
Open.pCoreOf r (Subgroup.normalizer (U : Set X)) ≤ Open.pCoreOf r P ∧ U ≤ Open.pCoreOf r P ∧
(t ≠ .Tits → Subgroup.normalizer ((S : Subgroup X) : Set X) ≤ P) ∧
(t = .Tits → (S : Subgroup X) ≤ P)
The files of 4 case theorems import it, directly or through other files: CFSG.Assembly.component_type, CFSG.Assembly.quasithin, CFSG.Assembly.rank_three_even, CFSG.Assembly.large_even.
Uses 1 · Used by 2
TheoremCL_LIT_Curtis_Tits_presentation_theorem#
The milestone module CFSG.Milestones.CL_LIT_Curtis_Tits_presentation_theorem, one of those CFSG/Milestones.lean imports.
It declares 1 result, quoted from CFSG/Milestones/CL_LIT_Curtis_Tits_presentation_theorem.lean in AxiomMath/CFSG at commit 69cb972f, Apache-2.0:
CFSG.Milestones.cl_lit_curtis_tits_presentation_theorem (theorem, line 19). Proved here.
theorem cl_lit_curtis_tits_presentation_theorem (t : StatedLieTag) (n p f : ℕ)
(hadm : StatedLieAdmissible t n p f) (hrank : 3 ≤ bnRank t n) :
CurtisTitsConclusion.{w} (lieUniversal t n p f hadm.1).D t n p f
The files of 4 case theorems import it, directly or through other files: CFSG.Assembly.component_type, CFSG.Assembly.quasithin, CFSG.Assembly.rank_three_even, CFSG.Assembly.large_even.
Uses 1 · Used by 6
TheoremCL_LIT_Fischer_3T_existence_uniqueness#
The milestone module CFSG.Milestones.CL_LIT_Fischer_3T_existence_uniqueness, one of those CFSG/Milestones.lean imports.
It declares 2 results, quoted from CFSG/Milestones/CL_LIT_Fischer_3T_existence_uniqueness.lean in AxiomMath/CFSG at commit 69cb972f, Apache-2.0:
CFSG.Milestones.cl_lit_fischer_3t_existence_uniqueness (theorem, line 15). Proved here.
theorem _root_.CFSG.Milestones.cl_lit_fischer_3t_existence_uniqueness :
∀ k ∈ ({22, 23, 24} : Set ℕ),
(∃ (G : Type) (_ : Group G) (_ : Finite G) (D : Set G),
fischerEUIsCenterlessPair D ∧ fischerEUType k D ∧
(∀ D' : Set G, fischerEUIsPair D' → D' = D) ∧
∀ d ∈ D, fischerEULocalStructure k d) ∧
(∀ (G H : Type) [Group G] [Group H] [Finite G] [Finite H] (D : Set G) (E : Set H),
fischerEUIsCenterlessPair D → fischerEUType k D →
fischerEUIsCenterlessPair E → fischerEUType k E →
∃ φ : G ≃* H, φ '' D = E)
CFSG.Milestones.cl_lit_fischer_3t_existence_uniqueness_full (theorem, line 34). Proved here.
theorem cl_lit_fischer_3t_existence_uniqueness_full :
∀ k : Fin 3, Subgroup.center (Carrier k) = ⊥ ∧ IsSimpleGroup (commutator (Carrier k)) ∧
∃ D : Set (Carrier k), HasType k (Carrier k) D ∧
(∀ E : Set (Carrier k), Pair (Carrier k) E → E = D) ∧ LocalStructure k D ∧
∀ (X : Type) [Group X] (E : Set X), Pair X E →
Subgroup.center X = ⊥ → IsSimpleGroup (commutator X) → HasType k X E →
∃ iso : X ≃* Carrier k, iso '' E = D
The files of 4 case theorems import it, directly or through other files: CFSG.Assembly.component_type, CFSG.Assembly.quasithin, CFSG.Assembly.rank_three_even, CFSG.Assembly.large_even.
TheoremCL_LIT_Fischer_three_transposition_theorem#
The milestone module CFSG.Milestones.CL_LIT_Fischer_three_transposition_theorem, one of those CFSG/Milestones.lean imports.
It declares 3 results, quoted from CFSG/Milestones/CL_LIT_Fischer_three_transposition_theorem.lean in AxiomMath/CFSG at commit 69cb972f, Apache-2.0:
CFSG.Milestones.cl_lit_fischer_three_transposition_theorem (theorem, line 15). Proved here.
theorem _root_.CFSG.Milestones.cl_lit_fischer_three_transposition_theorem
(G : Type) [Group G] [Finite G] (D : Set G)
(hclass : ∃ d₀ : G, D = {g | IsConj d₀ g})
(hinv : ∀ d ∈ D, orderOf d = 2)
(hprod : ∀ d ∈ D, ∀ e ∈ D, orderOf (d * e) ∈ ({1, 2, 3} : Set ℕ))
(hgen : Subgroup.closure D = ⊤)
(hcenter : Subgroup.center G = ⊥)
(hsimple : IsSimpleGroup (commutator G)) :
(∃ m : ℕ, (m = 3 ∨ 5 ≤ m) ∧
∃ φ : G ≃* Equiv.Perm (Fin m), ∀ g : G, g ∈ D ↔ (φ g).IsSwap) ∨
(∃ m : ℕ, 2 ≤ m ∧ ∃ b : LinearMap.BilinForm (ZMod 2) (Fin (2 * m) → ZMod 2),
(∀ x, b x x = 0) ∧ (∀ x, (∀ y, b x y = 0) → x = 0) ∧
fischerLinearModel D
(fischerMatrixGroup fun A => ∀ x y, b (A *ᵥ x) (A *ᵥ y) = b x y)
(fischerTransvections (fun x y => b x y) fun v => v ≠ 0)) ∨
(∃ m : ℕ, 2 ≤ m ∧ ∃ Q : QuadraticForm (ZMod 2) (Fin (2 * m) → ZMod 2),
(∀ x, (∀ y, QuadraticMap.polar Q x y = 0) → x = 0) ∧
(m = 2 → ¬ ∃ W : Submodule (ZMod 2) (Fin (2 * m) → ZMod 2),
Module.finrank (ZMod 2) W = 2 ∧ ∀ w ∈ W, Q w = 0) ∧
fischerLinearModel D
(fischerMatrixGroup fun A => ∀ x, Q (A *ᵥ x) = Q x)
(fischerTransvections (QuadraticMap.polar Q) fun v => Q v = 1)) ∨
(∃ m : ℕ, 4 ≤ m ∧
fischerCentralQuotientModel D
(fischerMatrixGroup fun A => A.det = 1 ∧
∀ x y, fischerHermitianF4 m (A *ᵥ x) (A *ᵥ y) = fischerHermitianF4 m x y)
(fischerTransvections (fischerHermitianF4 m)
fun v => v ≠ 0 ∧ fischerHermitianF4 m v v = 0)) ∨
(∃ m : ℕ, 5 ≤ m ∧ ∃ f : LinearMap.BilinForm (ZMod 3) (Fin m → ZMod 3),
(∀ x y, f x y = f y x) ∧ (∀ x, (∀ y, f x y = 0) → x = 0) ∧
fischerCentralQuotientModel D
(Subgroup.closure (fischerTransvections (fun x y => f x y) fun v => f v v = 1))
(fischerTransvections (fun x y => f x y) fun v => f v v = 1)) ∨
(Nat.card G = 2 ^ 17 * 3 ^ 9 * 5 ^ 2 * 7 * 11 * 13 ∧ Nat.card D = 3510) ∨
(Nat.card G = 2 ^ 18 * 3 ^ 13 * 5 ^ 2 * 7 * 11 * 13 * 17 * 23 ∧ Nat.card D = 31671) ∨
(Nat.card G = 2 ^ 22 * 3 ^ 16 * 5 ^ 2 * 7 ^ 3 * 11 * 13 * 17 * 23 * 29 ∧
Nat.card D = 306936)
CFSG.Milestones.cl_lit_fischer_three_transposition_theorem_pinned (theorem, line 59). Proved here.
theorem _root_.CFSG.Milestones.cl_lit_fischer_three_transposition_theorem_pinned
(G : Type) [Group G] [Finite G] (D : Set G)
(hclass : ∃ d₀ : G, D = {g | IsConj d₀ g})
(hinv : ∀ d ∈ D, orderOf d = 2)
(hprod : ∀ d ∈ D, ∀ e ∈ D, orderOf (d * e) ∈ ({1, 2, 3} : Set ℕ))
(hgen : Subgroup.closure D = ⊤)
(hcenter : Subgroup.center G = ⊥)
(hsimple : IsSimpleGroup (commutator G)) :
(∃ m : ℕ, (m = 3 ∨ 5 ≤ m) ∧
∃ φ : G ≃* Equiv.Perm (Fin m), ∀ g : G, g ∈ D ↔ (φ g).IsSwap) ∨
(∃ m : ℕ, 2 ≤ m ∧ ∃ b : LinearMap.BilinForm (ZMod 2) (Fin (2 * m) → ZMod 2),
(∀ x, b x x = 0) ∧ (∀ x, (∀ y, b x y = 0) → x = 0) ∧
fischerLinearModel D
(fischerMatrixGroup fun A => ∀ x y, b (A *ᵥ x) (A *ᵥ y) = b x y)
(fischerTransvections (fun x y => b x y) fun v => v ≠ 0)) ∨
(∃ m : ℕ, 2 ≤ m ∧ ∃ Q : QuadraticForm (ZMod 2) (Fin (2 * m) → ZMod 2),
(∀ x, (∀ y, QuadraticMap.polar Q x y = 0) → x = 0) ∧
(m = 2 → ¬ ∃ W : Submodule (ZMod 2) (Fin (2 * m) → ZMod 2),
Module.finrank (ZMod 2) W = 2 ∧ ∀ w ∈ W, Q w = 0) ∧
fischerLinearModel D
(fischerMatrixGroup fun A => ∀ x, Q (A *ᵥ x) = Q x)
(fischerTransvections (QuadraticMap.polar Q) fun v => Q v = 1)) ∨
(∃ m : ℕ, 4 ≤ m ∧
fischerCentralQuotientModel D
(fischerMatrixGroup fun A => A.det = 1 ∧
∀ x y, fischerHermitianF4 m (A *ᵥ x) (A *ᵥ y) = fischerHermitianF4 m x y)
(fischerTransvections (fischerHermitianF4 m)
fun v => v ≠ 0 ∧ fischerHermitianF4 m v v = 0)) ∨
(∃ m : ℕ, 5 ≤ m ∧ ∃ f : LinearMap.BilinForm (ZMod 3) (Fin m → ZMod 3),
(∀ x y, f x y = f y x) ∧ (∀ x, (∀ y, f x y = 0) → x = 0) ∧
fischerCentralQuotientModel D
(Subgroup.closure (fischerTransvections (fun x y => f x y) fun v => f v v = 1))
(fischerTransvections (fun x y => f x y) fun v => f v v = 1)) ∨
(∃ φ : G ≃* Blueprint.NativeSporadic.Fi22, Blueprint.Fischer.Pair _ (φ '' D) ∧
∀ E : Set Blueprint.NativeSporadic.Fi22, Blueprint.Fischer.Pair _ E → E = φ '' D) ∨
(∃ φ : G ≃* Blueprint.NativeSporadic.Fi23, Blueprint.Fischer.Pair _ (φ '' D) ∧
∀ E : Set Blueprint.NativeSporadic.Fi23, Blueprint.Fischer.Pair _ E → E = φ '' D) ∨
(∃ φ : G ≃* MulAut Blueprint.NativeSporadic.Fi24prime, Blueprint.Fischer.Pair _ (φ '' D) ∧
∀ E : Set (MulAut Blueprint.NativeSporadic.Fi24prime),
Blueprint.Fischer.Pair _ E → E = φ '' D)
CFSG.Milestones.cl_lit_fischer_three_transposition_theorem_recognition (theorem, line 111). Proved here.
theorem _root_.CFSG.Milestones.cl_lit_fischer_three_transposition_theorem_recognition
(G : Type) [Group G] [Finite G] (D : Set G)
(hclass : ∃ d₀ : G, D = {g | IsConj d₀ g})
(hinv : ∀ d ∈ D, orderOf d = 2)
(hprod : ∀ d ∈ D, ∀ e ∈ D, orderOf (d * e) ∈ ({1, 2, 3} : Set ℕ))
(hgen : Subgroup.closure D = ⊤)
(hcenter : Subgroup.center G = ⊥)
(hsimple : IsSimpleGroup (commutator G))
(d : G) (hd : d ∈ D) :
let C := Subgroup.centralizer ({d} : Set G)
(Nonempty (G ≃* Blueprint.NativeSporadic.Fi22) ↔
∃ K : Subgroup G, IsComponentOf K C ∧
Blueprint.LieModel (K ⧸ Subgroup.center K) .PSU 6 2 1) ∧
(Nonempty (G ≃* Blueprint.NativeSporadic.Fi23) ↔
∃ K : Subgroup G, IsComponentOf K C ∧
Nonempty ((K ⧸ Subgroup.center K) ≃* Blueprint.NativeSporadic.Fi22)) ∧
(Nonempty (G ≃* MulAut Blueprint.NativeSporadic.Fi24prime) ↔
∃ K : Subgroup G, IsComponentOf K C ∧
Nonempty ((K ⧸ Subgroup.center K) ≃* Blueprint.NativeSporadic.Fi23)) ∧
(Nonempty (G ≃* Blueprint.NativeSporadic.Fi22) →
commutator C = ⊤ ∧ (Subgroup.center C).map C.subtype = Subgroup.zpowers d ∧
Nat.card (Subgroup.center C) = 2 ∧
Blueprint.LieModel (C ⧸ Subgroup.center C) .PSU 6 2 1) ∧
(Nonempty (G ≃* Blueprint.NativeSporadic.Fi23) →
commutator C = ⊤ ∧ (Subgroup.center C).map C.subtype = Subgroup.zpowers d ∧
Nat.card (Subgroup.center C) = 2 ∧
Nonempty ((C ⧸ Subgroup.center C) ≃* Blueprint.NativeSporadic.Fi22)) ∧
(Nonempty (G ≃* MulAut Blueprint.NativeSporadic.Fi24prime) →
∃ K : Subgroup G, Nonempty (K ≃* Blueprint.NativeSporadic.Fi23) ∧
C = Subgroup.zpowers d ⊔ K ∧ Subgroup.zpowers d ⊓ K = ⊥ ∧
Subgroup.zpowers d ≤ Subgroup.centralizer (K : Set G))
The files of 4 case theorems import it, directly or through other files: CFSG.Assembly.component_type, CFSG.Assembly.quasithin, CFSG.Assembly.rank_three_even, CFSG.Assembly.large_even.
Uses 3 · Used by 8
TheoremCL_LIT_GH74_sectional_two_rank_four#
The milestone module CFSG.Milestones.CL_LIT_GH74_sectional_two_rank_four, one of those CFSG/Milestones.lean imports.
It declares 2 results, quoted from CFSG/Milestones/CL_LIT_GH74_sectional_two_rank_four.lean in AxiomMath/CFSG at commit 69cb972f, Apache-2.0:
CFSG.Milestones.cl_lit_gh74_sectional_two_rank_four (theorem, line 1638). Proved here.
theorem _root_.CFSG.Milestones.cl_lit_gh74_sectional_two_rank_four
(G : Type) [Group G] [Finite G] [IsSimpleGroup G]
(hnonab : ∃ a b : G, a * b ≠ b * a)
(hrank : 3 ≤ twoRank G)
(hsect : ∀ P : Subgroup G, IsPGroup 2 P →
∃ s : Finset G, s.card ≤ 4 ∧ Subgroup.closure (s : Set G) = P) :
Nat.card G ∈ gorensteinHarada74Orders
CFSG.Milestones.cl_lit_gh74_sectional_two_rank_four_models (theorem, line 1659). Proved here.
theorem cl_lit_gh74_sectional_two_rank_four_models
(G : Type) [Group G] [Finite G] [IsSimpleGroup G]
(hnonab : ∃ a b : G, a * b ≠ b * a) (hrank : 3 ≤ Open.twoRank G)
(hsect : ∀ P : Subgroup G, IsPGroup 2 P →
∃ s : Finset G, s.card ≤ 4 ∧ Subgroup.closure (s : Set G) = P) :
(∃ p f : ℕ, p.Prime ∧ p ≠ 2 ∧ 1 ≤ f ∧
(Blueprint.LieModel G .G2 0 p f ∨ Blueprint.LieModel G .trialityD4 0 p f)) ∨
(∃ p f : ℕ, p.Prime ∧ p ≠ 2 ∧ 1 ≤ f ∧ Blueprint.LieModel G .PSp 2 p f) ∨
(∃ f : ℕ, Blueprint.LieModel G .twistedG2 0 3 f) ∨
(∃ p f : ℕ, p.Prime ∧ p ≠ 2 ∧ 1 ≤ f ∧ p ^ f % 8 ≠ 1 ∧
Blueprint.LieModel G .PSL 4 p f) ∨
(∃ p f : ℕ, p.Prime ∧ p ≠ 2 ∧ 1 ≤ f ∧ p ^ f % 8 ≠ 7 ∧
Blueprint.LieModel G .PSU 4 p f) ∨
(∃ p f : ℕ, p.Prime ∧ 1 ≤ f ∧ p ^ f % 4 = 3 ∧ Blueprint.LieModel G .PSL 5 p f) ∨
(∃ p f : ℕ, p.Prime ∧ 1 ≤ f ∧ p ^ f % 4 = 1 ∧ Blueprint.LieModel G .PSU 5 p f) ∨
(Blueprint.LieModel G .PSL 2 2 3 ∨ Blueprint.LieModel G .PSL 2 2 4 ∨
Blueprint.LieModel G .PSL 3 2 2 ∨ Blueprint.LieModel G .twistedB2 0 2 3) ∨
(∃ n : ℕ, 8 ≤ n ∧ n ≤ 11 ∧ Nonempty (G ≃* alternatingGroup (Fin n))) ∨
(Blueprint.NativeSporadic.IsSporadic G .M12 ∨ Blueprint.NativeSporadic.IsSporadic G .M22 ∨
Blueprint.NativeSporadic.IsSporadic G .M23 ∨ Blueprint.NativeSporadic.IsSporadic G .J1 ∨
Blueprint.NativeSporadic.IsSporadic G .J2 ∨ Blueprint.NativeSporadic.IsSporadic G .J3 ∨
Blueprint.NativeSporadic.IsSporadic G .McL ∨ Blueprint.NativeSporadic.IsSporadic G .Ly)
The files of 3 case theorems import it, directly or through other files: CFSG.Assembly.component_type, CFSG.Assembly.rank_three_even, CFSG.Assembly.large_even.
Uses 11 · Used by 6
TheoremCL_LIT_GL83_Theorem_C_preuniqueness_rank_three#
The milestone module CFSG.Milestones.CL_LIT_GL83_Theorem_C_preuniqueness_rank_three, one of those CFSG/Milestones.lean imports.
It declares 1 result, quoted from CFSG/Milestones/CL_LIT_GL83_Theorem_C_preuniqueness_rank_three.lean in AxiomMath/CFSG at commit 69cb972f, Apache-2.0:
CFSG.Milestones.cl_lit_gl83_theorem_c_preuniqueness_rank_three (theorem, line 3334). Proved here.
theorem _root_.CFSG.Milestones.cl_lit_gl83_theorem_c_preuniqueness_rank_three
(G : Type) [Group G] [Finite G] [IsSimpleGroup G]
(hnonab : ∃ a b : G, a * b ≠ b * a)
(hK : IsKProper G) (hchar : IsCharTwoType G) (he : evenRank G = 3)
(hpre : rankThreeAschCoreLocal G 2) :
rankThreeUC G
The files of 1 case theorem import it, directly or through other files: CFSG.Assembly.rank_three_even.
Uses 6 · Used by 1
TheoremCL_LIT_GMS_Monster_uniqueness#
The milestone module CFSG.Milestones.CL_LIT_GMS_Monster_uniqueness, one of those CFSG/Milestones.lean imports.
It declares 2 results, quoted from CFSG/Milestones/CL_LIT_GMS_Monster_uniqueness.lean in AxiomMath/CFSG at commit 69cb972f, Apache-2.0:
CFSG.Milestones.cl_lit_gms_monster_uniqueness (theorem, line 17). Proved here.
theorem cl_lit_gms_monster_uniqueness
(d₀ : B) (hd₀ : orderOf d₀ = 2)
(hrank : Matrix.rank (d₀.val.val - 1) = 1860)
(G : Type) [Group G] [Finite G] (a z : G) (hG : GMSF1Type d₀ a z) :
Nonempty (G ≃* CFSG.Monster.Griess.AutO)
CFSG.Milestones.cl_lit_gms_monster_uniqueness_of_two (theorem, line 27). Proved here.
theorem cl_lit_gms_monster_uniqueness_of_two
(d₀ : B) (hd₀ : orderOf d₀ = 2)
(hrank : Matrix.rank (d₀.val.val - 1) = 1860)
(G H : Type) [Group G] [Group H] [Finite G] [Finite H] (a z : G) (b y : H)
(hG : GMSF1Type d₀ a z) (hH : GMSF1Type d₀ b y) :
Nonempty (G ≃* H)
The files of 4 case theorems import it, directly or through other files: CFSG.Assembly.component_type, CFSG.Assembly.quasithin, CFSG.Assembly.rank_three_even, CFSG.Assembly.large_even.
Uses 3 · Used by 7
TheoremCL_LIT_Gilman_Solomon_maximal_unbalancing_reduction#
The milestone module CFSG.Milestones.CL_LIT_Gilman_Solomon_maximal_unbalancing_reduction, one of those CFSG/Milestones.lean imports.
It declares 3 results, quoted from CFSG/Milestones/CL_LIT_Gilman_Solomon_maximal_unbalancing_reduction.lean in AxiomMath/CFSG at commit 69cb972f, Apache-2.0:
CFSG.Milestones.cl_lit_gilman_solomon_maximal_unbalancing_reduction (theorem, line 2449). Proved here.
theorem _root_.CFSG.Milestones.cl_lit_gilman_solomon_maximal_unbalancing_reduction
(X : Type) [Group X] [Finite X] [IsSimpleGroup X]
(hnonab : ∃ a b : X, a * b ≠ b * a)
(hK : IsKProper X)
(hunbal : ∃ z : X, orderOf z = 2 ∧
fusionOddCore (Subgroup.centralizer ({z} : Set X)) ≠ ⊥)
(hnotLie : ∀ p : ℕ, p.Prime → p ≠ 2 → Nat.card X ∉ lieOrdersChar p)
(hnotAlt : ∀ n : ℕ, 7 ≤ n → n % 4 = 3 → IsEmpty (X ≃* alternatingGroup (Fin n)))
(htriple : ∃ (a b : X) (J : Subgroup X), fusionUnbalancingTriple a b J) :
∃ (x y : X) (L : Subgroup X),
fusionMaximalUnbalancingTriple x y L ∧ fusionMaximalComponent L ∧
((Nonempty (L ⧸ fusionOddCore L ≃* alternatingGroup (Fin 7)) ∨
∃ (p f : ℕ) (_ : Fact p.Prime), p ≠ 2 ∧ 1 ≤ f ∧ 5 ≤ p ^ f ∧
Nonempty (L ⧸ fusionOddCore L ≃* PSL(2, GaloisField p f))) ∨
(Nonempty (L ⧸ fusionOddCore L ≃* fusionHe) ∨
Nonempty (L ⧸ fusionZStar L ≃* PSL(3, GaloisField 2 2))))
CFSG.Milestones.cl_lit_gilman_solomon_maximal_unbalancing_reduction_native (theorem, line 2494). Proved here.
theorem cl_lit_gilman_solomon_maximal_unbalancing_reduction_native
(X : Type) [Group X] [Finite X] [IsSimpleGroup X]
(hnonab : ∃ a b : X, a * b ≠ b * a)
(hK : Assembly.KProper Blueprint.Catalog X)
(hunbal : ∃ z : X, orderOf z = 2 ∧
oddCore (Subgroup.centralizer ({z} : Set X)) ≠ ⊥)
(hnotOutcome : ¬ OutcomeLocal.UOutcome X)
(htriple : ∃ (a b : X) (J : Subgroup X), GSUnbalancingTriple a b J) :
∃ (x y : X) (L : Subgroup X), GSMaximalUnbalancingTriple x y L ∧
GSMaximalComponent L ∧
((Nonempty (L ⧸ pPrimeCore 2 L ≃* alternatingGroup (Fin 7)) ∨
∃ p f : ℕ, p.Prime ∧ p ≠ 2 ∧ 1 ≤ f ∧ 5 ≤ p ^ f ∧
Blueprint.LieModel (L ⧸ pPrimeCore 2 L) .PSL 2 p f) ∨
(Nonempty (L ⧸ pPrimeCore 2 L ≃* Blueprint.NativeSporadic.He) ∨
Blueprint.LieModel (L ⧸ Open.fusionZStar L) .PSL 3 2 2))
CFSG.Milestones.cl_lit_gilman_solomon_maximal_unbalancing_reduction_models (theorem, line 2531). Proved here.
theorem _root_.CFSG.Milestones.cl_lit_gilman_solomon_maximal_unbalancing_reduction_models
(X : Type) [Group X] [Finite X] [IsSimpleGroup X]
(hnonab : ∃ a b : X, a * b ≠ b * a)
(hK : IsKProper X)
(hunbal : ∃ z : X, orderOf z = 2 ∧
fusionOddCore (Subgroup.centralizer ({z} : Set X)) ≠ ⊥)
(hnotOutcome : ¬ (Models.OddLieType X ∨
∃ n : ℕ, 7 ≤ n ∧ n % 4 = 3 ∧ Nonempty (X ≃* alternatingGroup (Fin n))))
(htriple : ∃ (a b : X) (J : Subgroup X), fusionUnbalancingTriple a b J) :
∃ (x y : X) (L : Subgroup X), fusionMaximalUnbalancingTriple x y L ∧
fusionMaximalComponent L ∧
((Nonempty (L ⧸ fusionOddCore L ≃* alternatingGroup (Fin 7)) ∨
∃ p f : ℕ, p.Prime ∧ p ≠ 2 ∧ 1 ≤ f ∧ 5 ≤ p ^ f ∧
Models.LieModel (L ⧸ fusionOddCore L) .PSL 2 p f) ∨
(Blueprint.NativeSporadic.IsSporadic (L ⧸ fusionOddCore L) .He ∨
Models.LieModel (L ⧸ fusionZStar L) .PSL 3 2 2))
No case theorem's file imports it, directly or through other files.
Sources
TheoremCL_LIT_Goldschmidt_strongly_closed_abelian#
The milestone module CFSG.Milestones.CL_LIT_Goldschmidt_strongly_closed_abelian, one of those CFSG/Milestones.lean imports.
It declares 1 result, quoted from CFSG/Milestones/CL_LIT_Goldschmidt_strongly_closed_abelian.lean in AxiomMath/CFSG at commit 69cb972f, Apache-2.0:
CFSG.Milestones.cl_lit_goldschmidt_strongly_closed_abelian (theorem, line 15). Proved here.
theorem _root_.CFSG.Milestones.cl_lit_goldschmidt_strongly_closed_abelian
(X : Type) [Group X] [Finite X]
(S : Sylow 2 X) (A : Subgroup X) (hAS : A ≤ S) (hAab : IsMulCommutative A)
(hclosed : ∀ a ∈ A, ∀ g : X, g⁻¹ * a * g ∈ (S : Subgroup X) → g⁻¹ * a * g ∈ A) :
let M : Subgroup X := Subgroup.normalClosure (A : Set X)
let π := QuotientGroup.mk' (goldschmidtOddCore M)
let T := ((S : Subgroup X).subgroupOf M).map π ⊓ goldschmidtLayer (M ⧸ goldschmidtOddCore M)
pCore 2 (M ⧸ goldschmidtOddCore M) ⊔ goldschmidtLayer (M ⧸ goldschmidtOddCore M) = ⊤ ∧
(A.subgroupOf M).map π =
pCore 2 (M ⧸ goldschmidtOddCore M) ⊔ Subgroup.closure {t | t ∈ T ∧ t ^ 2 = 1} ∧
∀ K : Subgroup (M ⧸ goldschmidtOddCore M), IsComponentOf K ⊤ →
goldschmidtSimpleType (K ⧸ Subgroup.center K)
The files of 4 case theorems import it, directly or through other files: CFSG.Assembly.component_type, CFSG.Assembly.quasithin, CFSG.Assembly.rank_three_even, CFSG.Assembly.large_even.
TheoremCL_LIT_Goldschmidt_strongly_closed_abelian_models#
The milestone module CFSG.Milestones.CL_LIT_Goldschmidt_strongly_closed_abelian_models, which CFSG/Milestones.lean does not import.
It declares 1 result, quoted from CFSG/Milestones/CL_LIT_Goldschmidt_strongly_closed_abelian_models.lean in AxiomMath/CFSG at commit 69cb972f, Apache-2.0:
CFSG.Milestones.cl_lit_goldschmidt_strongly_closed_abelian_models (theorem, line 9). Proved here.
theorem _root_.CFSG.Milestones.cl_lit_goldschmidt_strongly_closed_abelian_models
(X : Type) [Group X] [Finite X]
(S : Sylow 2 X) (A : Subgroup X) (hAS : A ≤ S) (hAab : IsMulCommutative A)
(hclosed : ∀ a ∈ A, ∀ g : X, g⁻¹ * a * g ∈ (S : Subgroup X) → g⁻¹ * a * g ∈ A) :
let M : Subgroup X := Subgroup.normalClosure (A : Set X)
let π := QuotientGroup.mk' (goldschmidtOddCore M)
let T := ((S : Subgroup X).subgroupOf M).map π ⊓ goldschmidtLayer (M ⧸ goldschmidtOddCore M)
pCore 2 (M ⧸ goldschmidtOddCore M) ⊔ goldschmidtLayer (M ⧸ goldschmidtOddCore M) = ⊤ ∧
(A.subgroupOf M).map π =
pCore 2 (M ⧸ goldschmidtOddCore M) ⊔ Subgroup.closure {t | t ∈ T ∧ t ^ 2 = 1} ∧
∀ K : Subgroup (M ⧸ goldschmidtOddCore M), IsComponentOf K ⊤ →
CFSG.Goldschmidt.SimpleModels (K ⧸ Subgroup.center K)
The files of 4 case theorems import it, directly or through other files: CFSG.Assembly.component_type, CFSG.Assembly.quasithin, CFSG.Assembly.rank_three_even, CFSG.Assembly.large_even.
TheoremCL_LIT_Gorenstein_Walter_L_balance#
The milestone module CFSG.Milestones.CL_LIT_Gorenstein_Walter_L_balance, one of those CFSG/Milestones.lean imports.
It declares 1 result, quoted from CFSG/Milestones/CL_LIT_Gorenstein_Walter_L_balance.lean in AxiomMath/CFSG at commit 69cb972f, Apache-2.0:
CFSG.Milestones.cl_lit_gorenstein_walter_l_balance (theorem, line 11). Proved here.
theorem _root_.CFSG.Milestones.cl_lit_gorenstein_walter_l_balance
(X : Type) [Group X] [Finite X] (hK : lBalanceIsKGroup X)
(p : ℕ) (hp : p.Prime) (P : Subgroup X) (hP : IsPGroup p P) :
lBalancePLayer p (Subgroup.normalizer (P : Set X)) ≤ lBalancePLayer p ⊤ ∧
lBalancePLayer p (Subgroup.centralizer (P : Set X)) ≤ lBalancePLayer p ⊤ ∧
(lBalancePrimeCore p (⊤ : Subgroup X) = ⊥ →
∀ a ∈ lBalancePLayer p (Subgroup.normalizer (P : Set X)),
∀ b ∈ lBalancePrimeCore p (Subgroup.normalizer (P : Set X)), a * b = b * a)
The files of 4 case theorems import it, directly or through other files: CFSG.Assembly.component_type, CFSG.Assembly.quasithin, CFSG.Assembly.rank_three_even, CFSG.Assembly.large_even.
Uses 15 · Used by 7
TheoremCL_LIT_Griess_Schur_multipliers_Lie_type#
The milestone module CFSG.Milestones.CL_LIT_Griess_Schur_multipliers_Lie_type, one of those CFSG/Milestones.lean imports.
It declares 11 results, quoted from CFSG/Milestones/CL_LIT_Griess_Schur_multipliers_Lie_type.lean in AxiomMath/CFSG at commit 69cb972f, Apache-2.0:
CFSG.Milestones.cl_lit_griess_schur_multipliers_lie_type (theorem, line 22). Proved here.
theorem _root_.CFSG.Milestones.cl_lit_griess_schur_multipliers_lie_type
(p k n : ℕ) [Fact p.Prime] (hk : 0 < k) (hn : 2 ≤ n) (hsmall : n = 2 → 4 ≤ p ^ k) :
commutator PSL(n, GaloisField p k) = ⊤ ∧
Nonempty (griessHopfMultiplier PSL(n, GaloisField p k) ≃*
Multiplicative (ZMod (Nat.gcd n (p ^ k - 1)) ×
ZMod (griessPSLExceptional n (p ^ k)).1 × ZMod (griessPSLExceptional n (p ^ k)).2))
CFSG.Milestones.cl_lit_griess_schur_multipliers_all_models (theorem, line 37). Proved here.
theorem cl_lit_griess_schur_multipliers_all_models
(X : Type) [Group X] (t : Assembly.LowTwoRank.StatedLieTag) (n p f : ℕ)
(hmodel : Models.LieModel X t n p f) :
commutator X = ⊤ ∧
Nonempty (griessHopfMultiplier X ≃* generic t n p f × exceptional t n p f)
CFSG.Milestones.cl_lit_griess_schur_multipliers_all_models_statement (theorem, line 45). Proved here.
theorem cl_lit_griess_schur_multipliers_all_models_statement :
GriessAllModelsStatement
CFSG.Milestones.cl_lit_griess_schur_multipliers_central_covers (theorem, line 49). Proved here.
theorem cl_lit_griess_schur_multipliers_central_covers
(X : Type) [Group X] (t : Assembly.LowTwoRank.StatedLieTag) (n p f : ℕ)
(hmodel : Models.LieModel X t n p f) :
((∀ S : Sylow 2 (griessHopfMultiplier X), Nat.card S ≤ 2) →
∀ (L : Type) [Group L] [Finite L], IsQuasisimple L →
Nonempty ((L ⧸ Subgroup.center L) ≃* X) →
∀ S : Sylow 2 (Subgroup.center L), Nat.card S ≤ 2) ∧
((∀ S : Sylow 2 (griessHopfMultiplier X), Nat.card S = 2) →
∀ (L L' : Type) [Group L] [Group L'] [Finite L] [Finite L'],
IsQuasisimple L → IsQuasisimple L' →
Nat.card (Subgroup.center L) = 2 → Nat.card (Subgroup.center L') = 2 →
Nonempty ((L ⧸ Subgroup.center L) ≃* X) →
Nonempty ((L' ⧸ Subgroup.center L') ≃* X) → Nonempty (L ≃* L'))
CFSG.Milestones.cl_lit_griess_schur_multipliers_all_native_models (theorem, line 66). Proved here.
theorem cl_lit_griess_schur_multipliers_all_native_models
(X : Type) [Group X] (t : Assembly.LowTwoRank.StatedLieTag) (n p f : ℕ)
(hmodel : Blueprint.LieModel X t n p f) :
commutator X = ⊤ ∧
Nonempty (griessHopfMultiplier X ≃* generic t n p f × exceptional t n p f)
CFSG.Milestones.cl_lit_griess_schur_multipliers_native_central_covers (theorem, line 74). Proved here.
theorem cl_lit_griess_schur_multipliers_native_central_covers
(X : Type) [Group X] (t : Assembly.LowTwoRank.StatedLieTag) (n p f : ℕ)
(_hmodel : Blueprint.LieModel X t n p f) :
((∀ S : Sylow 2 (griessHopfMultiplier X), Nat.card S ≤ 2) →
∀ (L : Type) [Group L] [Finite L], IsQuasisimple L →
Nonempty ((L ⧸ Subgroup.center L) ≃* X) →
∀ S : Sylow 2 (Subgroup.center L), Nat.card S ≤ 2) ∧
((∀ S : Sylow 2 (griessHopfMultiplier X), Nat.card S = 2) →
∀ (L L' : Type) [Group L] [Group L'] [Finite L] [Finite L'],
IsQuasisimple L → IsQuasisimple L' →
Nat.card (Subgroup.center L) = 2 → Nat.card (Subgroup.center L') = 2 →
Nonempty ((L ⧸ Subgroup.center L) ≃* X) →
Nonempty ((L' ⧸ Subgroup.center L') ≃* X) → Nonempty (L ≃* L'))
CFSG.Milestones.cl_lit_griess_schur_multipliers_central_covers_z2 (theorem, line 91). Proved here.
theorem cl_lit_griess_schur_multipliers_central_covers_z2
(X : Type) [Group X] (t : Assembly.LowTwoRank.StatedLieTag) (n p f : ℕ)
(hmodel : Models.LieModel X t n p f)
(ht : t = .PSp ∧ n = 3 ∧ p = 2 ∧ f = 1 ∨ t = .G2 ∧ n = 0 ∧ p = 2 ∧ f = 2 ∨
t = .F4 ∧ n = 0 ∧ p = 2 ∧ f = 1) :
Nonempty (griessHopfMultiplier X ≃* Multiplicative (ZMod 2)) ∧
(∀ (L : Type) [Group L] [Finite L], IsQuasisimple L →
Nonempty ((L ⧸ Subgroup.center L) ≃* X) →
∀ S : Sylow 2 (Subgroup.center L), Nat.card S ≤ 2) ∧
(∀ (L L' : Type) [Group L] [Group L'] [Finite L] [Finite L'],
IsQuasisimple L → IsQuasisimple L' →
Nat.card (Subgroup.center L) = 2 → Nat.card (Subgroup.center L') = 2 →
Nonempty ((L ⧸ Subgroup.center L) ≃* X) →
Nonempty ((L' ⧸ Subgroup.center L') ≃* X) → Nonempty (L ≃* L'))
CFSG.Milestones.cl_lit_griess_schur_multipliers_native_central_covers_z2 (theorem, line 107). Proved here.
theorem cl_lit_griess_schur_multipliers_native_central_covers_z2
(X : Type) [Group X] (t : Assembly.LowTwoRank.StatedLieTag) (n p f : ℕ)
(hmodel : Blueprint.LieModel X t n p f)
(ht : t = .PSp ∧ n = 3 ∧ p = 2 ∧ f = 1 ∨ t = .G2 ∧ n = 0 ∧ p = 2 ∧ f = 2 ∨
t = .F4 ∧ n = 0 ∧ p = 2 ∧ f = 1) :
Nonempty (griessHopfMultiplier X ≃* Multiplicative (ZMod 2)) ∧
(∀ (L : Type) [Group L] [Finite L], IsQuasisimple L →
Nonempty ((L ⧸ Subgroup.center L) ≃* X) →
∀ S : Sylow 2 (Subgroup.center L), Nat.card S ≤ 2) ∧
(∀ (L L' : Type) [Group L] [Group L'] [Finite L] [Finite L'],
IsQuasisimple L → IsQuasisimple L' →
Nat.card (Subgroup.center L) = 2 → Nat.card (Subgroup.center L') = 2 →
Nonempty ((L ⧸ Subgroup.center L) ≃* X) →
Nonempty ((L' ⧸ Subgroup.center L') ≃* X) → Nonempty (L ≃* L'))
CFSG.Milestones.cl_lit_griess_schur_multipliers_native_central_covers_unrestricted (theorem, line 123). Proved here.
theorem cl_lit_griess_schur_multipliers_native_central_covers_unrestricted
(X : Type) [Group X] (t : Assembly.LowTwoRank.StatedLieTag) (n p f : ℕ)
(hmodel : Blueprint.LieModel X t n p f) :
((∀ S : Sylow 2 (griessHopfMultiplier X), Nat.card S ≤ 2) →
∀ (L : Type) [Group L], CFSG.IsQuasisimple L →
Nonempty ((L ⧸ Subgroup.center L) ≃* X) →
∀ S : Sylow 2 (Subgroup.center L), Nat.card S ≤ 2) ∧
((∀ S : Sylow 2 (griessHopfMultiplier X), Nat.card S = 2) →
∀ (L L' : Type) [Group L] [Group L'],
CFSG.IsQuasisimple L → CFSG.IsQuasisimple L' →
Nat.card (Subgroup.center L) = 2 → Nat.card (Subgroup.center L') = 2 →
Nonempty ((L ⧸ Subgroup.center L) ≃* X) →
Nonempty ((L' ⧸ Subgroup.center L') ≃* X) → Nonempty (L ≃* L'))
CFSG.Milestones.cl_lit_griess_schur_multipliers_native_central_covers_z2_unrestricted (theorem, line 139). Proved here.
theorem cl_lit_griess_schur_multipliers_native_central_covers_z2_unrestricted
(X : Type) [Group X] (t : Assembly.LowTwoRank.StatedLieTag) (n p f : ℕ)
(hmodel : Blueprint.LieModel X t n p f)
(ht : t = .PSp ∧ n = 3 ∧ p = 2 ∧ f = 1 ∨ t = .G2 ∧ n = 0 ∧ p = 2 ∧ f = 2 ∨
t = .F4 ∧ n = 0 ∧ p = 2 ∧ f = 1) :
Nonempty (griessHopfMultiplier X ≃* Multiplicative (ZMod 2)) ∧
(∀ (L : Type) [Group L], CFSG.IsQuasisimple L →
Nonempty ((L ⧸ Subgroup.center L) ≃* X) →
∀ S : Sylow 2 (Subgroup.center L), Nat.card S ≤ 2) ∧
(∀ (L L' : Type) [Group L] [Group L'],
CFSG.IsQuasisimple L → CFSG.IsQuasisimple L' →
Nat.card (Subgroup.center L) = 2 → Nat.card (Subgroup.center L') = 2 →
Nonempty ((L ⧸ Subgroup.center L) ≃* X) →
Nonempty ((L' ⧸ Subgroup.center L') ≃* X) → Nonempty (L ≃* L'))
CFSG.Milestones.cl_lit_griess_schur_multipliers_g2_four_root_lifts (theorem, line 171). Proved here.
theorem cl_lit_griess_schur_multipliers_g2_four_root_lifts
(L : Type) [Group L] (hL : IsQuasisimple L) (hZ : Nat.card (Subgroup.center L) = 2)
(hmodel : Blueprint.LieModel (L ⧸ Subgroup.center L) .G2 0 2 2) :
(∀ x : L, IsG2FourLongRootInvolution (x : L ⧸ Subgroup.center L) → orderOf x = 2) ∧
(∀ x : L, IsG2FourShortRootInvolution (x : L ⧸ Subgroup.center L) → orderOf x = 4)
The files of 4 case theorems import it, directly or through other files: CFSG.Assembly.component_type, CFSG.Assembly.quasithin, CFSG.Assembly.rank_three_even, CFSG.Assembly.large_even.
Uses 3 · Used by 5
TheoremCL_LIT_Monster_existence_Griess_Conway#
The milestone module CFSG.Milestones.CL_LIT_Monster_existence_Griess_Conway, one of those CFSG/Milestones.lean imports.
It declares 3 results, quoted from CFSG/Milestones/CL_LIT_Monster_existence_Griess_Conway.lean in AxiomMath/CFSG at commit 69cb972f, Apache-2.0:
CFSG.Milestones.cl_lit_monster_existence_griess_conway_1 (theorem, line 16). Proved here.
theorem _root_.CFSG.Milestones.cl_lit_monster_existence_griess_conway_1 :
∃ (G : Type) (_ : Group G) (_ : Finite G), IsSimpleGroup G ∧ Nat.card G = monsterOrder ∧
∃ a z : G, MonsterIsF1Type a z ∧ ¬ IsConj a z ∧
∀ t : G, orderOf t = 2 → IsConj a t ∨ IsConj z t
CFSG.Milestones.cl_lit_monster_existence_griess_conway_2 (theorem, line 29). Proved here.
theorem _root_.CFSG.Milestones.cl_lit_monster_existence_griess_conway_2 :
∃ (G : Type) (_ : Group G) (_ : Finite G), IsSimpleGroup G ∧ Nat.card G = monsterOrder ∧
∃ a z : G, MonsterIsF1Type a z ∧ ¬ IsConj a z ∧
(∀ t : G, orderOf t = 2 → IsConj a t ∨ IsConj z t) ∧ MonsterTwoAGraphData a z
CFSG.Milestones.cl_lit_monster_existence_griess_conway (theorem, line 44). Proved here.
theorem cl_lit_monster_existence_griess_conway :
MonsterExistenceStatement MGriess
The files of 4 case theorems import it, directly or through other files: CFSG.Assembly.component_type, CFSG.Assembly.quasithin, CFSG.Assembly.rank_three_even, CFSG.Assembly.large_even.
Uses 3 · Used by 6
TheoremCL_LIT_SQTK_simple_list#
The milestone module CFSG.Milestones.CL_LIT_SQTK_simple_list, one of those CFSG/Milestones.lean imports.
It declares 1 result, quoted from CFSG/Milestones/CL_LIT_SQTK_simple_list.lean in AxiomMath/CFSG at commit 69cb972f, Apache-2.0:
CFSG.Milestones.cl_lit_sqtk_simple_list_section (theorem, line 14). Proved here.
theorem cl_lit_sqtk_simple_list_section
(X : Type) [Group X] [Finite X] (hSQTK : IsSQTKCat X)
(H : Subgroup X) (N : Subgroup H) [N.Normal] [IsSimpleGroup (H ⧸ N)]
(hnonab : ∃ a b : H ⧸ N, a * b ≠ b * a) : SQTKSimpleList (H ⧸ N)
The files of 4 case theorems import it, directly or through other files: CFSG.Assembly.component_type, CFSG.Assembly.quasithin, CFSG.Assembly.rank_three_even, CFSG.Assembly.large_even.
Uses 1 · Used by 6
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.