theorem SL2Gen.transvection_mem_lineStab {ι : Type u_1} {F : Type u_2} [Field F] [DecidableEq ι] [Fintype ι] {i j : ι} (hij : i ≠ j) (b : F) : Matrix.SpecialLinearGroup.transvection hij b ∈ Matrix.SpecialLinearGroup.lineStab (F ∙ Pi.single i 1)

A transvection transvection i j hij b lies in lineStab (span F {Pi.single i 1}).

theorem SL2Gen.transvection_mem_lineStab_sup {F : Type u_2} [Field F] (t : Matrix.TransvectionStruct (Fin 2) F) : t.toSpecialLinearGroup ∈ Matrix.SpecialLinearGroup.lineStab (F ∙ Pi.single 0 1) ⊔ Matrix.SpecialLinearGroup.lineStab (F ∙ Pi.single 1 1)

Every transvection in SL ι F whose indices are (i₁, i₂) or (i₂, i₁) is in the join of lineStab(span F {e_{i₁}}) and lineStab(span F {e_{i₂}}).

theorem SL2Gen.SL_card_two_lineStab_sup_eq_top {F : Type u_2} [Field F] : Matrix.SpecialLinearGroup.lineStab (F ∙ Pi.single 0 1) ⊔ Matrix.SpecialLinearGroup.lineStab (F ∙ Pi.single 1 1) = ⊤

SL-level generation: in the 2-element-index case, the join of the two lineStab subgroups attached to the two coordinate axes is all of SL ι F.

theorem PSL.iSup_lineStab_eq_top {F : Type u_2} [Field F] : ⨆ (p : Projectivization F (Fin 2 → F)), Matrix.SpecialLinearGroup.lineStab p.submodule = ⊤

At the SL level: when Fintype.card ι = 2, the supremum over all projective points of the lineStab subgroups equals ⊤ in SL ι F.

theorem PSL.iSup_iwasawaT_eq_top {F : Type u_2} [Field F] : iSup iwasawaT = ⊤

The Iwasawa generator property: when Fintype.card ι = 2, the supremum of the iwasawaT subgroups equals all of PSL.

@[reducible, inline]

noncomputable abbrev PSL2.Iwasawa {F : Type u_2} [Field F] : MulAction.IwasawaStructure (Matrix.ProjectiveSpecialLinearGroup (Fin 2) F) (Projectivization F (Fin 2 → F))

The Iwasawa structure on PSL(2, F).

Equations

• PSL2.Iwasawa = { T := PSL.iwasawaT, is_comm := ⋯, is_conj := ⋯, is_generator := ⋯ }

theorem SL2Simple.PSL_commutator_eq_top {F : Type u_2} [Field F] (hF : ∃ (a : F), a ≠ 0 ∧ a ^ 2 ≠ 1) : commutator (Matrix.ProjectiveSpecialLinearGroup (Fin 2) F) = ⊤

commutator (PSL ι F) = ⊤.

instance SL2Simple.PSL_nontrivial {ι : Type u_1} {F : Type u_2} [Field F] [DecidableEq ι] [Fintype ι] [Nontrivial ι] : Nontrivial (Matrix.ProjectiveSpecialLinearGroup ι F)

PSL ι F is nontrivial whenever ι has at least two elements (and F is a field, hence in particular nontrivial).

theorem Matrix.ProjectiveSpecialLinearGroup.rank_two_simple' {F : Type u_2} [Field F] (hF : ∃ (a : F), a ≠ 0 ∧ a ^ 2 ≠ 1) : IsSimpleGroup (ProjectiveSpecialLinearGroup (Fin 2) F)

theorem Matrix.ProjectiveSpecialLinearGroup.rank_two_simple {F : Type u_2} [Field F] (hF : 4 ≤ Nat.card F) : IsSimpleGroup (ProjectiveSpecialLinearGroup (Fin 2) F)