English
Equality of representations yields equality on endomorphisms via toEnd.
Русский
Равенство представлений приводит к равенству эндоморфизм через toEnd.
LaTeX
$$Matrix.isRepresentation R b hb A = B implies Matrix.isRepresentation.toEnd R b hb A = Matrix.isRepresentation.toEnd R b hb B$$
Lean4
/-- The map sending a matrix to the endomorphism it represents. This is an `R`-algebra morphism. -/
noncomputable def toEnd : Matrix.isRepresentation R b →ₐ[R] Module.End R M
where
toFun A := A.2.choose
map_one' := (1 : Matrix.isRepresentation R b).2.choose_spec.eq hb Matrix.Represents.one
map_mul' A₁ A₂ := (A₁ * A₂).2.choose_spec.eq hb (A₁.2.choose_spec.mul A₂.2.choose_spec)
map_zero' := (0 : Matrix.isRepresentation R b).2.choose_spec.eq hb Matrix.Represents.zero
map_add' A₁ A₂ := (A₁ + A₂).2.choose_spec.eq hb (A₁.2.choose_spec.add A₂.2.choose_spec)
commutes' r := (algebraMap _ (Matrix.isRepresentation R b) r).2.choose_spec.eq hb (.algebraMap r)
