isRepresentation — Mathlib

English

There is a canonical algebra map from the matrix representation to the endomorphism ring M.

Русский

Существует каноническое алгебраическое отображение из матричного представления в кольцо эндоморфизмов.

LaTeX

$$Matrix.isRepresentation.toEnd R b hb A = f$$

Lean4

/-- The subalgebra of `Matrix ι ι R` that consists of matrices that actually represent
endomorphisms on `M`. -/
def isRepresentation : Subalgebra R (Matrix ι ι R)
    where
  carrier := {A | ∃ f : Module.End R M, A.Represents b f}
  mul_mem' := fun ⟨f₁, e₁⟩ ⟨f₂, e₂⟩ => ⟨f₁ * f₂, e₁.mul e₂⟩
  one_mem' := ⟨1, Matrix.Represents.one⟩
  add_mem' := fun ⟨f₁, e₁⟩ ⟨f₂, e₂⟩ => ⟨f₁ + f₂, e₁.add e₂⟩
  zero_mem' := ⟨0, Matrix.Represents.zero⟩
  algebraMap_mem' r := ⟨algebraMap _ _ r, .algebraMap _⟩

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