forget_reflects_iso — Mathlib

English

The forgetful functor forget_G: Coalgebra(G) → C reflects isomorphisms.

Русский

Забывающий функтор forget_G: G-коалгебр → C отражает изоморфизмы.

LaTeX

$$$\\\\forall G \\in \\text{Comonad}(C), \\\\forall A,B \\in G. Coalgebra, \\\\forall f: A \\\\to B, [IsIso f.f] \\\\Rightarrow IsIso f.$$$

Lean4

instance forget_reflects_iso : G.forget.ReflectsIsomorphisms where
  reflects {_ _} f [IsIso f.f] := coalgebra_iso_of_iso G f

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