English
The forgetful functor from comonoids reflects isomorphisms; equivalently, if forgetful map is an iso then the morphism is iso in Comon.
Русский
Функтор забывания от комоноидов отражает изоморфизмы; эквивалентно: если образ функтором гомоморфизма является изоморфизм, то сам морфизм изоморфизм.
LaTeX
$$$\text{Forget}(C).ReflectsIsomorphisms$$$
Lean4
/-- Auxiliary definition for `ComonToMonOpOpObj`. -/
abbrev ComonToMonOpOpObjMon (A : Comon C) : MonObj (op A.X)
where
one := ε[A.X].op
mul := Δ[A.X].op
one_mul := by
rw [← op_whiskerRight, ← op_comp, counit_comul]
rfl
mul_one := by
rw [← op_whiskerLeft, ← op_comp, comul_counit]
rfl
mul_assoc :=
by
rw [← op_inv_associator, ← op_whiskerRight, ← op_comp, ← op_whiskerLeft, ← op_comp, comul_assoc_flip, op_comp,
op_comp_assoc]
rfl
