coe_toCoalgHom — Mathlib

English

Reconfirming that the map e ↦ e.toCoalgHom is injective: equal underlying coalgebra-homs imply equal equivalences.

Русский

Подтверждение инъективности отображения e ↦ e.toCoalgHom: равные подлежащие коалгебраические гомоморфизмы означают равенство эквивалентностей.

LaTeX

$$(\\operatorname{toCoalgHom}(e_1) = \\operatorname{toCoalgHom}(e_2)) \\iff e_1 = e_2$$

Lean4

@[simp]
theorem coe_toCoalgHom : ⇑(e : A →ₗc[R] B) = e :=
  rfl

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