Maximal abelian subgroup

Stream: maths

[Alex Brodbelt]

I've have managed to state some of the theorems that are stated on pen and paper; they may need modication later on, but I figure its better to see if I can state everything provided the new definitions made and then see from there(?)

-I am having trouble setting up theorems that state that X is isomorphic to Y, I was wondering if I could get some help on this front theorem_2_6_iii and theorem_2_6_v_a.

• For lemma_1_5 I will need some version of the jordan normal form for 2x2 matrices over an algebraically closed field, I am vaguely aware that the jordan normal form theorem is not in mathlib, but are there weaker versions in mathlib or elsewhere?

• For `theorem_2_6_iii I am not how to coerce A \inf Bto be of type Subgroup SL(2,F) or coerce center SL(2,F) to be of type Subgroup G (as by assumption center SL(2,F) \leq G but I can't figure out what less than or equal to means in this context whether it is subgroup or if it means G contains the center when seen as sets.

If there are any general tips or advice I would love to hear what you have to say :)

Thanks in advance

p.s: let me know if I should move this to another thread and close the current one

import Mathlib

namespace ElementaryAbelian

def IsElementaryAbelian (p : ℕ) [Fact (Nat.Prime p)] (G : Type*) [CommGroup G] : Prop  :=
  ∀ g : G, g ^ p = 1

/- If `G` is elementary abelian then G is a `p`-Group -/
theorem IsPSubgroup_of_IsElementaryAbelian {G : Type*} [CommGroup G] { p : ℕ } [Fact (Nat.Prime p)] (hG : IsElementaryAbelian p G) : IsPGroup p G := fun g => ⟨1, by rw [pow_one, hG]⟩

end ElementaryAbelian

namespace MaximalAbelian

open Subgroup

def IsMaximalAbelian (G : Type*) [Group G] (H : Subgroup G) : Prop := Maximal (IsCommutative) H

-- def NonCentral

def MaximalAbelianSubgroups { G : Type*} [Group G](H : Subgroup G) : Set (Subgroup H) :=
  { K : Subgroup H | @IsMaximalAbelian H _ K}

end MaximalAbelian

namespace SpecialLinearGroup

universe u

open Matrix MatrixGroups

variable (F : Type u) [Field F]

instance : Group SL(2,F) := by infer_instance
section one

def T {F : Type*} [Field F] (τ : F): SL(2, F) :=
  ⟨!![1, 0; τ, 1], by norm_num [Matrix.det_fin_two_of]⟩

def D {F : Type*} [Field F] (δ : Fˣ) : SL(2, F) :=
  ⟨!![(δ : F), (0 : F); (0 :F) , (δ⁻¹ : F)], by norm_num [Matrix.det_fin_two_of]⟩

def W : SL(2, F) :=
  ⟨!![0,1;-1,0], by norm_num [Matrix.det_fin_two_of]⟩


open Subgroup

/- Lemma 1.3. Z(SL(2,F)) = ⟨ -I ⟩ .-/
def center_of_SL_2_F : center SL(2,F) ≃* rootsOfUnity 2 F  := by apply Matrix.SpecialLinearGroup.center_equiv_rootsOfUnity' 2

/- Requires Jordan Normal Form -/
/- Lemma 1.5. Each element of SL(2,F) is conjugate to either D δ for some δ ∈ Fˣ, or to  ± T τ for some τ ∈ F .-/
lemma lemma_1_5 [IsAlgClosed F] (S : SL(2,F)) : ∃ δ : Fˣ, IsConj S (D δ) ∨ ∃ τ : F, IsConj S (T τ) := by sorry

end one

section two

open MaximalAbelian Subgroup

/- Let G be an arbitrary finite subgroup of SL(2, F) containing Z(SL(2, F)) -/
variable {G : Type*} (G : Subgroup (SL(2,F))) [Finite G] (hG : center (SL(2, F)) ≤ G)

namespace IsPGroup

/- Lemma 2.1. If G is a finite group of order pm where p is prime and m > 0,
then p divides |Z(G)|.-/
lemma p_dvd_card_center {H : Type*} {p : ℕ} (hp:  Nat.Prime p) [Group H] [Finite H] [Nontrivial H] (hH : IsPGroup p H) : p ∣ Nat.card (center H) := by
  let inst : Fact (Nat.Prime p) := by exact { out := hp }
  have card_H_eq_pow_prime : ∃ n > 0, Nat.card H = p ^ n := by rwa [← hH.nontrivial_iff_card]
  suffices ∃ k > 0, Nat.card (center H) = p ^ k by
    obtain ⟨k, kpos, hk⟩ := this
    use p^(k-1)
    rw [hk, ← Nat.pow_add_one', Nat.sub_add_cancel]
    linarith
  obtain ⟨n, npos, hn⟩ := card_H_eq_pow_prime
  exact IsPGroup.card_center_eq_prime_pow hn npos

end IsPGroup

/- Lemma 2.2: Every finite subgroup of a multiplicative group of a field is cyclic. -/
lemma lemma_2_2 (H : Subgroup Fˣ) [Finite H]: IsCyclic H := subgroup_units_cyclic H

/- Theorem 2.3 (i) If x ∈ G\Z then we have CG (x) ∈ M. -/
theorem theorem_2_3_i
  (x : SL(2,F))
  (hx : x ∈ (G.carrier \ (Subgroup.center SL(2,F)).carrier)) :
  Subgroup.centralizer {⟨x, by aesop⟩} ∈ MaximalAbelianSubgroups G := by sorry

/- Theorem 2.3 (ii) For any two distinct subgroups A and B of M, we have A ∩ B = Z. -/
theorem theorem_2_6_ii
  (A B : Subgroup G)
  (hA : A ∈ MaximalAbelianSubgroups G)
  (hB : B ∈ MaximalAbelianSubgroups G)
  (A_neq_B: A ≠ B)
  (hG : center SL(2,F) ≤ G) :
  ((A) ⊓ (B)) = ((center SL(2,F))) := by sorry

/- Theorem 2.3 (iii) An element A of M is either a cyclic group whose order is relatively prime
to p, or of the form Q × Z where Q is an elementary abelian Sylow p-subgroup
of G. -/
theorem theorem_2_6_iii
  (A : Subgroup G)
  (hA : A ∈ MaximalAbelianSubgroups G) :
  (IsCyclic A ∧ Nat.Coprime (Nat.card A) p) ∨
  (∃ Q : Sylow p G, IsElementaryAbelian Q → ∃ φ : A →* (Q.toSubgroup.prod (center SL(2,F)))) := by sorry

/- Theorem 2.3 (iv a) If A ∈ M and |A| is relatively prime to p, then we have [NG (A) : A] ≤ 2. -/
theorem theorem_2_3_iv_a (A : Subgroup G) (hA : A ∈ MaximalAbelianSubgroups G) (hA' : Nat.Coprime (Nat.card A) p) : A.normalizer.index ≤ 2 := by sorry

/- Theorem 2.3 (iv b) Furthermore, if [NG (A) : A] = 2, then there is an element y of NG (A)\A such that, yxy⁻¹ = x⁻¹  for all x ∈ A. -/
theorem theorem_2_3_iv_b (A : Subgroup G) (hA : A ∈ MaximalAbelianSubgroups G) (hA' : Nat.Coprime (Nat.card A) p) (hNA : A.normalizer.index = 2)
  (x : A) : ∃ y ∈ A.normalizer.carrier \ A, y * x * y⁻¹ = x⁻¹ := by sorry

/- Theorem 2.3 (v a) Let Q be a Sylow p-subgroup of G. If Q 6= {IG }, then there is a cyclic subgroup K of G such that NG (Q) = QK.  -/
theorem theorem_2_6_v_a { p : ℕ } (hp : Nat.Prime p) (Q : Sylow p G) (h : Q.toSubgroup ≠ ⊥) : ∃ K : Subgroup G, IsCyclic K → Q.toSubgroup.normalizer ≃* Q.toSubgroup.prod K:= by sorry

/- Theorem 2.3 (v b)If |K| > |Z|, then K ∈ M. -/
theorem theorem_2_6_v_b { p : ℕ }
  (hp : Nat.Prime p)
  (Q : Sylow p G)
  (h : Q.toSubgroup ≠ ⊥)
  (K :  Subgroup G)
  (hK : IsCyclic K)
  (NG_iso_prod_QK : Q.toSubgroup.normalizer ≃* Q.toSubgroup.prod K)
  (h: Nat.card K > Nat.card (center SL(2,F))) :
  K ∈ MaximalAbelianSubgroups G := by sorry


/- Conjugacy of Maximal Abelian subgroups -/
/-
Definition. The set Ci = {xAi x−1 : x ∈ G} is called the conjugacy class of
A ∈ M.
-/


/- Let Aᵢ* be the non-central part of Aᵢ ∈ M (is this set difference(?))-/

/- let M∗ be the set of all Aᵢ* and let Cᵢ* be the conjugacy class of Aᵢ* .-/


/-
Clᵢ = {x Aᵢx⁻¹ : x ∈ G}

For some Ai ∈ M and A∗i ∈ M∗ let,
Ci = ⋃ x ∈ G, x * Aᵢ * x⁻¹, and Cᵢ* = ⋃ x ∈ G, x Aᵢ* x⁻¹

It’s evident that Cᵢ* = Cᵢ \ Z(SL(2,F)) and that there is a Cᵢ corresponding to each
Cᵢ . Clearly we have the relation, |Cᵢ*| = |Aᵢ*||Clᵢ*| (clearly on pen and paper smh...) -/
end two

[Notification Bot]

A message was moved here from #Is there code for X? > Maximal abelian subgroup by Johan Commelin.

[Johan Commelin]

Could you please give a bit more detail about your first question: what do you mean with having trouble to show results about isomorphisms?

[Johan Commelin]

And how is it relevant to your codeblock?

[Yao Liu]

maximal torus is an important concept, in many settings. would there be a way to minimize duplicate work?

[Kevin Buzzard]

But a maximal torus isn't a subgroup, it's a subvariety (or a subgroupvariety), so one needs a different type.

[Oliver Nash]

Regarding the missing Jordan normal form results, since we have: docs#Module.End.exists_isNilpotent_isSemisimple we lack only the classification of nilpotent endomorphisms / matrices.

But for 2x2 matrices, this piece is much easier so hopefully you shouldn’t be blocked here.

[Alex Brodbelt]

Johan Commelin said:

Could you please give a bit more detail about your first question: what do you mean with having trouble to show results about isomorphisms?

The two theorems which state that a group X is isomorphic to a group Y don't typecheck as X ≃* Y is of type MulEquiv and I was wondering how to state it as a proposition or state it in such a way that I can use it later on in other theorems.

For instance, Theorem 2.3 (iii) states:
An element $A$ of $M$ (where $M$ is the set of maximal abelian subgroups of $G$ as subgroup of $SL(2,F)$ containting the center of $SL(2,F)$) is either a cyclic group whose order is relatively prime
to $p$, or of the form $Q \times Z(SL(2,F))$ where $Q$ is an elementary abelian Sylow $p$-subgroup
of $G$.

On pen and paper I would say that $A$ is isomorphic to the direct product of $Q$ and $Z(SL(2,F))$ but in Lean I can't state this as a theorem I figure it might be defining a type MulEquiv through def but I'm not sure how to do it as I have never done this before.

I was also posting this code block so as to receive some feedback in case something I've done looks horribly wrong.

[Ruben Van de Velde]

So this may be one of the cases where with pen and paper we say "we prove (i.e. theorem) these two are isomorphic" when we actually mean "we define (i.e. def) an isomorphism between them"

[Ruben Van de Velde]

If you really want to say "there exists an isomorphism", you can do theorem x : Nonempty (X ≃* Y)

[Alex Brodbelt]

I will need to use this isomorphism later on, from your experience which is the best way to do this or something to keep in mind?

[Antoine Chambert-Loir]

In your case, it seems that your can state an equality of subgroups, plus the fact that the center and the subgroup $Q$ are disjoint.

[Yaël Dillies]

Btw we have elementary abelian groups in PFR, but I recently refactored them out to use Module (ZMod n) G instead (@Johan Commelin will remember reviewing the relevant PR to mathlib). Sadly, this trick only works for additive groups. so I don't know what to do about multiplicative ones