toCoalgHom_inj — Mathlib

English

The map sending a coalgebra equivalence e to its underlying coalgebra homomorphism e.toCoalgHom is injective; i.e., e1 and e2 are equal whenever their corresponding homomorphisms coincide.

Русский

Отображение, отправляющее коалгебраическую эквивалентность e в соответствующий коалгебраический гомоморфизм e.toCoalgHom, инъективно; то есть e1 = e2 тогда и только если их соответствующие гомоморфизмы совпадают.

LaTeX

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

Lean4

@[simp, norm_cast]
theorem toCoalgHom_inj {e₁ e₂ : A ≃ₗc[R] B} : (↑e₁ : A →ₗc[R] B) = e₂ ↔ e₁ = e₂ :=
  toCoalgHom_injective.eq_iff

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