English
The center of GL_n(R) is the image of the units R^× under the natural embedding a ↦ aI_n.
Русский
Центр GL_n(R) является образом единиц R^× при естественном отображении a ↦ aI_n.
LaTeX
$$Center(GL_n(R)) = { a I_n : a ∈ R^× }$$
Lean4
/-- The center of `GL n R` is the image of `Rˣ`. -/
theorem center_eq_range_units : Subgroup.center (GL n R) = (Units.map (algebraMap R _).toMonoidHom).range :=
by
ext g
rcases isEmpty_or_nonempty n
· simpa [Subsingleton.elim (Subgroup.center _) ⊤] using ⟨1, Subsingleton.elim _ _⟩
constructor
· -- previous lemma shows the underlying matrix is scalar, but now need to show
-- the scalar is a unit; so we apply argument both to `g` and `g⁻¹`
intro hg
obtain ⟨a, ha⟩ := mem_center_iff_val_eq_scalar.mp hg
obtain ⟨b, hb⟩ := mem_center_iff_val_eq_scalar.mp (Subgroup.inv_mem _ hg)
have hab : a * b = 1 := by simpa [-mul_inv_cancel, ← ha, ← hb, ← diagonal_one, Units.ext_iff] using mul_inv_cancel g
refine ⟨⟨a, b, hab, mul_comm a b ▸ hab⟩, ?_⟩
simp [Units.ext_iff, ← ha, algebraMap_eq_diagonal]
· rintro ⟨a, rfl⟩
exact mem_center_iff_val_eq_scalar.mpr ⟨a, rfl⟩
