English
The center of the matrix submonoid is the image of the center of the base semiring via the scalar embedding.
Русский
Центр подмножества матриц равен изображению центра базового полузаметного кольца через скалярное вложение.
LaTeX
$$$$\\mathrm{Submonoid}.\\mathrm{center}(\\\\mathrm{Matrix}(n,n,\\\\alpha)) = \\mathrm{Submonoid}.\\mathrm{map}(\\\\mathrm{Matrix}.\\\\mathrm{scalar}(n)).$$$$
Lean4
/-- `M` is a scalar matrix if it commutes with every non-diagonal `single`. -/
theorem mem_range_scalar_of_commute_single {M : Matrix n n α} (hM : Pairwise fun i j => Commute (single i j 1) M) :
M ∈ Set.range (Matrix.scalar n) := by
cases isEmpty_or_nonempty n
· exact ⟨0, Subsingleton.elim _ _⟩
obtain ⟨i⟩ := ‹Nonempty n›
refine ⟨M i i, Matrix.ext fun j k => ?_⟩
simp only [scalar_apply]
obtain rfl | hkl := Decidable.eq_or_ne j k
· rw [diagonal_apply_eq]
obtain rfl | hij := Decidable.eq_or_ne i j
· rfl
· exact diag_eq_of_commute_single (hM hij)
· rw [diagonal_apply_ne _ hkl]
obtain rfl | hij := Decidable.eq_or_ne i j
· rw [col_eq_zero_of_commute_single (hM hkl.symm) hkl]
· rw [row_eq_zero_of_commute_single (hM hij) hkl.symm]
