chore(Matrix/GeneralLinearGroup/Projective): sort out namespace and golf the proof (leanprover-community#40666)

Author: Whysoserioushah

Mathlib/GroupTheory/QuotientGroup/Defs.lean

@@ -278,6 +278,12 @@ theorem ker_lift (φ : G →* M) (HN : N ≤ φ.ker) :
   rw [← congrArg MonoidHom.ker (lift_comp_mk' N φ HN), ← MonoidHom.comap_ker,
     Subgroup.map_comap_eq_self_of_surjective (mk'_surjective N)]
 
+@[to_additive]
+lemma injective_lift_iff (φ : G →* M) (HN : N ≤ φ.ker) :
+    Function.Injective (QuotientGroup.lift N φ HN) ↔ N = φ.ker := by
+  rw [← MonoidHom.ker_eq_bot_iff, QuotientGroup.ker_lift, Subgroup.map_eq_bot_iff]
+  grind [QuotientGroup.ker_mk']
+
 /-- A surjective group homomorphism `φ : G →* H` with `N = ker(φ)` descends (i.e. `lift`s) to a
 group isomorphism `G/N ≃* H`. -/
 @[to_additive /-- A surjective `AddGroup` homomorphism `φ : G →+ H` with `N = ker(φ)` descends

Mathlib/LinearAlgebra/Matrix/GeneralLinearGroup/Basic.lean

@@ -46,7 +46,7 @@ lemma mem_center_iff_val_mem_range_scalar {g : GL n R} :
     refine Matrix.mem_range_scalar_of_commute_transvectionStruct fun t ↦ ?_
     simpa [Units.ext_iff] using! Subgroup.mem_center_iff.mp hg (.mk _ _ t.mul_inv t.inv_mul)
   · refine fun ⟨a, ha⟩ ↦ Subgroup.mem_center_iff.mpr fun h ↦ ?_
-    simpa [Units.ext_iff, ← ha] using! (scalar_commute a (mul_comm a ·) h.val).symm
+    simp [-scalar_apply, Units.ext_iff, ← ha, Matrix.scalar_comm a (Commute.all _)]
 
 @[deprecated (since := "2026-02-08")]
 alias mem_center_iff_val_eq_scalar := mem_center_iff_val_mem_range_scalar
@@ -74,8 +74,31 @@ lemma center_eq_range_scalar :
 @[deprecated (since := "2026-02-08")]
 alias center_eq_range_units := center_eq_range_scalar
 
+lemma map_center_le {S : Type*} [CommRing S] (f : R →+* S) :
+    Subgroup.center (GL n R) ≤ (Subgroup.center (GL n S)).comap (map f) := fun u hu ↦ by
+  simp only [GeneralLinearGroup.center_eq_range_scalar, MonoidHom.mem_range,
+    Subgroup.mem_comap] at hu ⊢
+  obtain ⟨r, rfl⟩ := hu
+  exact ⟨(Units.map f) r, GeneralLinearGroup.map_scalar _ _ |>.symm⟩
+
 end Center
 
 end GeneralLinearGroup
 
+lemma SpecialLinearGroup.toGL_mem_center_iff {n R : Type*} [Fintype n] [DecidableEq n] [CommRing R]
+    (g : SpecialLinearGroup n R) :
+    toGL g ∈ Subgroup.center (GL n R) ↔ g ∈ Subgroup.center (SpecialLinearGroup n R) := by
+  if hn : IsEmpty n then simp [Subgroup.center_eq_top] else
+  replace hn : Nonempty n := by simpa using hn
+  obtain ⟨i⟩ := hn
+  simp only [GeneralLinearGroup.center_eq_range_scalar, MonoidHom.mem_range,
+    mem_center_iff, scalar_apply]
+  refine ⟨fun ⟨r, hr⟩ ↦ ⟨r, by simpa [Units.ext_iff] using congr(GeneralLinearGroup.det $hr),
+    by simpa [Units.ext_iff] using hr⟩, fun ⟨r, hr1, hr⟩ ↦ ⟨⟨r, g⁻¹.1 i i, ?_, ?_⟩,
+      by simp [Units.ext_iff, hr]⟩⟩
+  · simpa [-mul_inv_cancel, ← hr, ← pow_succ',
+      Nat.sub_one_add_one Fintype.card_pos.ne.symm] using
+        Matrix.ext_iff.2 (Subtype.ext_iff.1 (mul_inv_cancel g)) i i
+  · simpa [-inv_mul_cancel, ← hr] using Matrix.ext_iff.2 (Subtype.ext_iff.1 (inv_mul_cancel g)) i i
+
 end Matrix

Mathlib/LinearAlgebra/Matrix/GeneralLinearGroup/Defs.lean

@@ -52,23 +52,25 @@ variable {n : Type u} [DecidableEq n] [Fintype n] {R : Type v}
 
 variable (n) in
 /-- Scalar matrix as an element of `GL n R`. -/
-@[simps!]
 def scalar [Semiring R] : Rˣ →* GL n R :=
   Units.map (Matrix.scalar n).toMonoidHom
 
-#adaptation_note /-- As of nightly-2026-04-29, the simpNF linter is failing here.
-Assistance investigating this would be appreciated. -/
-attribute [nolint simpNF] _root_.Matrix.GeneralLinearGroup.val_inv_scalar_apply
-
 section CoeFnInstance
 
 instance instCoeFun [Semiring R] : CoeFun (GL n R) fun _ => n → n → R where
   coe A := (A : Matrix n n R)
 
+@[simp]
+lemma coe_scalar [Semiring R] (u : Rˣ) : ↑(scalar n u) = Matrix.scalar n u.1 := rfl
+
 end CoeFnInstance
 
 variable [CommRing R]
 
+lemma scalar_commute (u : Rˣ) (A : GL n R) : scalar n u * A = A * scalar n u := by
+  ext : 1
+  rw [Units.val_mul, Units.val_mul, coe_scalar, Matrix.scalar_comm _ (Commute.all _)]
+
 /-- The determinant of a unit matrix is itself a unit. -/
 @[simps]
 def det : GL n R →* Rˣ where
@@ -220,6 +222,11 @@ lemma coe_map_inv_mul_map (g : GL n R) : g.val⁻¹.map f * g.val.map f = 1 := b
   rw [← Matrix.map_mul]
   simp only [isUnits_det_units, nonsing_inv_mul, map_zero, map_one, Matrix.map_one]
 
+lemma map_scalar (u : Rˣ) : map f (scalar n u) = scalar n (Units.map f u) := by
+  ext
+  simp [Matrix.diagonal_apply]
+  split <;> simp
+
 section kronecker
 variable {R m : Type*} [CommSemiring R] [Fintype m] [DecidableEq m]
 

Mathlib/LinearAlgebra/Matrix/GeneralLinearGroup/Projective.lean

@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2026 Yury G. Kudryashov. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Yury G. Kudryashov
+Authors: Yury G. Kudryashov, Edison Xie
 -/
 module
 
@@ -17,11 +17,22 @@ In this file we define `Matrix.ProjGenLinGroup n R` as the quotient of `GL n R`
 We introduce notation `PGL(n, R)` for this group,
 which works if `n` is either a finite type or a natural number.
 If `n` is a number, then `PGL(n, R)` is interpreted as `PGL(Fin n, R)`.
+
+## Main definitions
+
+* `Matrix.SpecialLinearGroup.toPGL` is the natural map from `SL(n, R)` to `PGL(n, R)`.
+
+* `Matrix.ProjectiveSpecialLinearGroup.toPGL` is the natural
+  inclusion from `PSL(n, R)` to `PGL(n, R)`.
+
+* `Matrix.ProjectiveSpecialLinearGroup.isoPSLOfAlgClosed` is an isomorphism between
+  `PGL(n, F)` and `PSL(n, F)` in the case of an algebraically closed field.
+
 -/
 
 open scoped MatrixGroups
 
-public section
+@[expose] public section
 
 namespace Matrix
 
@@ -61,6 +72,9 @@ theorem ker_mk : mk.ker = Subgroup.center (GL n R) := QuotientGroup.ker_mk' _
 theorem mk_eq_one {g : GL n R} : mk g = 1 ↔ g ∈ Subgroup.center (GL n R) := by
   rw [← MonoidHom.mem_ker, ker_mk]
 
+@[simp]
+lemma mk_one : mk (1 : GL n R) = 1 := rfl
+
 @[simp]
 theorem mk_scalar (u : Rˣ) : mk (.scalar n u) = 1 := by
   rw [← MonoidHom.mem_ker, ker_mk, GeneralLinearGroup.center_eq_range_scalar]
@@ -71,41 +85,43 @@ theorem induction_on {motive : PGL(n, R) → Prop} (g : PGL(n, R))
     (mk : ∀ g : GL n R, motive (ProjGenLinGroup.mk g)) : motive g :=
   Quotient.inductionOn g mk
 
+end ProjGenLinGroup
+
 section isoPSL
 
+variable {n R : Type*} [Fintype n] [DecidableEq n] [CommRing R]
+
+open Matrix.ProjGenLinGroup
+
+namespace SpecialLinearGroup
+
+/-- The natural map from `SL(n, R)` to `PGL(n, R)` by composing the maps from `SL` to `GL` and the
+  quotient map from `GL` to `PGL`. -/
+abbrev toPGL : SpecialLinearGroup n R →* PGL(n, R) := mk.comp toGL
+
+lemma toPGL_ker : toPGL.ker = Subgroup.center (SpecialLinearGroup n R) := by
+  ext; simp [toGL_mem_center_iff]
+
+end SpecialLinearGroup
+
+namespace ProjectiveSpecialLinearGroup
+
 open Matrix.SpecialLinearGroup
 
 /-- The natural inclusion map from `PSL(n, R)` to `PGL(n, R)` induced by the inclusion
   map from `SL(n, R)` to `GL(n, R)`. -/
-@[expose]
-def _root_.Matrix.ProjectiveSpecialLinearGroup.toPGL :
-    ProjectiveSpecialLinearGroup n R →* PGL(n, R) :=
-  QuotientGroup.lift _ (mk.comp toGL) fun x hx ↦ by
-    simp only [mem_center_iff, scalar_apply, MonoidHom.mem_ker, MonoidHom.coe_comp,
-      Function.comp_apply, mk_eq_one, GeneralLinearGroup.mem_center_iff_val_mem_range_scalar,
-      coe_GL_coe_matrix, Set.mem_range] at hx ⊢
-    exact ⟨hx.choose, hx.choose_spec.2⟩
+def toPGL : ProjectiveSpecialLinearGroup n R →* PGL(n, R) :=
+  QuotientGroup.lift _ SpecialLinearGroup.toPGL <| le_of_eq toPGL_ker.symm
 
 @[simp]
-lemma _root_.Matrix.ProjectiveSpecialLinearGroup.toPGL_mk (g : SpecialLinearGroup n R) :
+lemma toPGL_mk (g : SpecialLinearGroup n R) :
     ProjectiveSpecialLinearGroup.toPGL g = mk (toGL g) := rfl
 
-lemma _root_.Matrix.ProjectiveSpecialLinearGroup.toPGL_injective :
-    Function.Injective (ProjectiveSpecialLinearGroup.toPGL (n := n) (R := R)) := fun x y h ↦ by
-  induction x using QuotientGroup.induction_on with | H x =>
-  induction y using QuotientGroup.induction_on with | H y =>
-  simp only [ProjectiveSpecialLinearGroup.toPGL_mk, mk_eq_mk_iff] at h
-  rw [← QuotientGroup.mk'_apply, ← QuotientGroup.mk'_apply]
-  simp only [QuotientGroup.mk'_eq_mk', mem_center_iff]
-  obtain ⟨u, hu'⟩ := h
-  have hu : u.1 ^ Fintype.card n = 1 := by
-    simpa [Units.ext_iff] using congr(Matrix.GeneralLinearGroup.det $hu')
-  set z : SpecialLinearGroup n R := ⟨scalar n u.1, by simpa using hu⟩ with hz_eq
-  have hz : (GeneralLinearGroup.scalar n) u = toGL z := by ext; simp [hz_eq]
-  refine ⟨z, ⟨u.1, hu, by simp [hz_eq]⟩, ?_⟩
-  rwa [hz, ← map_mul, toGL_inj] at hu'
-
-lemma _root_.Matrix.ProjectiveSpecialLinearGroup.toPGL_surj_of_roots
+lemma toPGL_injective :
+    Function.Injective (ProjectiveSpecialLinearGroup.toPGL (n := n) (R := R)) :=
+  QuotientGroup.injective_lift_iff _ _ _ |>.2 toPGL_ker.symm
+
+lemma toPGL_surj_of_roots
     (hR : ∀ r : Rˣ, ∃ k : Rˣ, k ^ Fintype.card n = r) :
     Function.Surjective (ProjectiveSpecialLinearGroup.toPGL (n := n) (R := R)) := fun g ↦ by
   induction g using Matrix.ProjGenLinGroup.induction_on with | mk g =>
@@ -117,10 +133,10 @@ lemma _root_.Matrix.ProjectiveSpecialLinearGroup.toPGL_surj_of_roots
   use QuotientGroup.mk ⟨r.1 • g.1, hr⟩
   simp only [ProjectiveSpecialLinearGroup.toPGL_mk, mk_eq_mk_iff]
   refine ⟨r⁻¹, Units.ext ?_⟩
-  simp only [Units.val_mul, coe_GL_coe_matrix,GeneralLinearGroup.val_scalar_apply]
+  simp only [Units.val_mul, coe_GL_coe_matrix, GeneralLinearGroup.coe_scalar]
   simp [← Matrix.mul_smul, ← Matrix.diagonal_smul, Pi.smul_def, smul_eq_mul]
 
-lemma _root_.Matrix.ProjectiveSpecialLinearGroup.toPGL_surj_iff [Nonempty n] :
+lemma toPGL_surj_iff [Nonempty n] :
     Function.Surjective (ProjectiveSpecialLinearGroup.toPGL (n := n) (R := R)) ↔
       ∀ r : Rˣ, ∃ k : Rˣ, k ^ Fintype.card n = r := by
   refine ⟨fun h r ↦ ?_, ProjectiveSpecialLinearGroup.toPGL_surj_of_roots⟩
@@ -156,9 +172,13 @@ noncomputable def isoPSLOfAlgClosed {F : Type*} [Field F] [IsAlgClosed F] :
   MulEquiv.symm (MulEquiv.ofBijective Matrix.ProjectiveSpecialLinearGroup.toPGL
     ⟨Matrix.ProjectiveSpecialLinearGroup.toPGL_injective, Function.surjective_to_subsingleton _⟩)
 
+end ProjectiveSpecialLinearGroup
+
 end isoPSL
 
-variable {M : Type*} [Monoid M]
+namespace ProjGenLinGroup
+
+variable {n R : Type*} [Fintype n] [DecidableEq n] [CommRing R] {M : Type*} [Monoid M]
 
 /-- Lift a monoid homomorphism `f : GL n R →* M` that vanishes on all scalar matrices
 to a homomorphism from `PGL(n, R)`. -/
@@ -191,6 +211,23 @@ theorem mk_smul {α : Type*} [MulAction (GL n R) α] (h) (g : GL n R) (a : α) :
     mk g • a = g • a := by
   rfl
 
+/-- The monoid hom between `PGL(n, R)` and `PGL(n, S)` induced by a
+  ring homomorphism `f : R →+* S`. -/
+def map {S : Type*} [CommRing S] (f : R →+* S) : PGL(n, R) →* PGL(n, S) :=
+  QuotientGroup.map _ _ (GeneralLinearGroup.map (n := n) f) <| GeneralLinearGroup.map_center_le f
+
+@[simp]
+lemma map_id : map (RingHom.id R) = MonoidHom.id (PGL(n, R)) := QuotientGroup.map_id _
+
+@[simp]
+lemma map_mk {S : Type*} [CommRing S] (f : R →+* S) (g : GL n R) :
+    map f (mk g) = mk (GeneralLinearGroup.map f g) := rfl
+
+lemma map_comp {S T : Type*} [CommRing S] [CommRing T] (f : R →+* S) (g : S →+* T) :
+    map (n := n) (g.comp f) = (map g).comp (map f) := by
+  ext g
+  induction g using Matrix.ProjGenLinGroup.induction_on with | mk g => simp
+
 variable [Fact (Even (Fintype.card n))] [LinearOrder R] [IsStrictOrderedRing R]
 
 /-- In case of an even dimension, the sign of the determinant of `g : PGL(n, R)` is well-defined. -/

Mathlib/LinearAlgebra/Projectivization/Action.lean

@@ -11,7 +11,7 @@ public import Mathlib.LinearAlgebra.Projectivization.Basic
 public import Mathlib.LinearAlgebra.SpecialLinearGroup
 public import Mathlib.LinearAlgebra.Transvection.Basic
 public import Mathlib.LinearAlgebra.Matrix.IsDiag
-public import Mathlib.LinearAlgebra.Matrix.ProjectiveSpecialLinearGroup
+public import Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Projective
 public import Mathlib.LinearAlgebra.Center
 
 /-!
@@ -240,6 +240,17 @@ instance : IsPreprimitive (Matrix.ProjectiveSpecialLinearGroup ι K) (ℙ K (ι
     {toFun := id, map_smul' := by intros; simp; rfl} (prePrimitive_SL (ι := ι) (K := K))
     Function.surjective_id
 
+open MatrixGroups Matrix.ProjGenLinGroup
+
+instance : MulAction PGL(ι, K) (ℙ K (ι → K)) :=
+  mulActionOfGL fun u ↦ ind fun v hv ↦ by
+    simp only [smul_mk, mk_eq_mk_iff]
+    exact ⟨u, by simp [Units.smul_def]⟩
+
+@[simp]
+lemma PGL.mk_smul_mk (g : GL ι K) {v : ι → K} (hv : v ≠ 0) :
+    (.mk g : PGL(ι, K)) • mk K v hv = mk K (g • v) (smul_ne_zero_iff_ne g|>.2 hv) := rfl
+
 end Field
 
 end Projectivization