mem_center_iff_val_eq_scalar — Mathlib

English

For GL_n(R) with R a commutative ring, the center consists exactly of scalar matrices, i.e., matrices aI with a a unit in R.

Русский

Центр GL_n(R) состоит ровно из скаляров: матриц типа aI_n, где a — элемент-победитель (единица в R).

LaTeX

$$Center(GL_n(R)) = { a I_n : a ∈ R^× }$$

Lean4

/-- The center of `GL n R` consists of scalar matrices. -/
theorem mem_center_iff_val_eq_scalar {g : GL n R} : g ∈ Subgroup.center (GL n R) ↔ g.val ∈ Set.range (scalar _) :=
  by
  rcases isEmpty_or_nonempty n
  · simpa [Subsingleton.elim (Subgroup.center _) ⊤] using ⟨1, Subsingleton.elim _ _⟩
  constructor
  · intro hg
    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

Похожие утверждения