instIsComonHomInvOfHom — Mathlib

English

If f: M ≅ N is an isomorphism and f.hom is a comonoid morphism, then f.inv is also a comonoid morphism.

Русский

Если f: M ≅ N — изоморфизм и f.hom — морфизм комоноида, то и f.inv является комоноидным морфизмом.

LaTeX

$$$\text{If } f: M \cong N \text{ with } IsComonHom(f.hom),\; IsComonHom(f.inv).$$$

Lean4

instance (f : M ≅ N) [IsComonHom f.hom] : IsComonHom f.inv
    where
  hom_counit := by simp [Iso.inv_comp_eq]
  hom_comul := by simp [Iso.inv_comp_eq]

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