toCoalgIso — Mathlib

English

A linear coalgebra equivalence e: X ≃ₗc[R] Y yields an isomorphism in the category CoalgCat R between CoalgCat.of R X and CoalgCat.of R Y.

Русский

Линейное коалгебраическое эквивалентное отображение e: X ≃ₗc[R] Y определяет изоморфизм в категории CoalgCat R между CoalgCat.of R X и CoalgCat.of R Y.

LaTeX

$$$$ toCoalgIso(e): CoalgCat.of R X \cong CoalgCat.of R Y. $$$$

Lean4

/-- Build an isomorphism in the category `CoalgCat R` from a
`CoalgEquiv`. -/
@[simps]
def toCoalgIso (e : X ≃ₗc[R] Y) : CoalgCat.of R X ≅ CoalgCat.of R Y
    where
  hom := CoalgCat.ofHom e
  inv := CoalgCat.ofHom e.symm
  hom_inv_id := Hom.ext <| DFunLike.ext _ _ e.left_inv
  inv_hom_id := Hom.ext <| DFunLike.ext _ _ e.right_inv

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