Mathlib Map

Theorems · Definition · group theory

PSL.iwasawaT

{F : Type u_1} →
  [inst : Field F] →
    {ι : Type u_2} →
      [inst_1 : DecidableEq ι] →
        [inst_2 : Fintype ι] → Projectivization F (ι → F) → Subgroup (Matrix.ProjectiveSpecialLinearGroup ι F)

The candidate family of subgroups for the Iwasawa structure on PSL ι F acting on the projective space ℙ F (ι → F): the unipotent radical attached to the line through p.

Defined in
Mathlib.LinearAlgebra.Projectivization.PSL.Stabilizer
Cited by
1 results in Mathlib
Foundations
Depth 106 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
FieldDecidableEqFintype
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

PSL2.Iwasawa · cited by 1PSL2.IwasawaPSL.iSup_iwasawaT_eq_top · cited by 0PSL.iSup_iwasawaT_eq_topFintype · cited by 7736FintypeField · cited by 7404FieldSubgroup · cited by 3593SubgroupMatrix.SpecialLinearGroup · cited by 348Matrix.SpecialLinearGroupSubgroup.map · cited by 301Subgroup.mapSubgroup.center · cited by 121Subgroup.centerProjectivization · cited by 111ProjectivizationQuotientGroup.mk' · cited by 90QuotientGroup.mk'Projectivization.submodule · cited by 11Projectivization.submoduleMatrix.SpecialLinearGroup.lineStab · cited by 10SpecialLinearGroup.lineSt…Matrix.ProjectiveSpecialLinearGroup · cited by 9Matrix.ProjectiveSpecialL…PSL.iwasawaTCITED BYCITES

Cites11

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by2

Results whose statement or proof uses this declaration.