coe_copy — Mathlib

English

The mapping from bialg homs to linear maps is injective, factoring through coalg-hom then linear maps.

Русский

Отображение из биналгомов в линейные отображения инъективно через коалгомы и линейные отображения.

LaTeX

$$$\\mathrm{Injective}\\bigl((\\uparrow) : (A \\to_{R}^{\\!c} B) \\to (A \\to_{R}^{\\!L} B)\\bigr)$$$

Lean4

@[simp]
theorem coe_copy (f : A →ₗc[R] B) (f' : A → B) (h : f' = ⇑f) : ⇑(f.copy f' h) = f' :=
  rfl

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