English
The forgetting mechanism also reflects isomorphisms in the opposite direction; i.e., the forgetful functor reflects isomorphisms in the opposite category as well.
Русский
Забывающий функтор отражает изоморфизмы и в противоположной категории.
LaTeX
$$$$ \text{forget} (CoalgCat R) \text{ReflectsIsomorphisms (symm)}. $$$$
Lean4
theorem tensorObj_comul (K L : CoalgCat R) :
Coalgebra.comul (R := R) (A := (K ⊗ L : CoalgCat R)) =
(TensorProduct.tensorTensorTensorComm R K K L L).toLinearMap ∘ₗ
TensorProduct.map Coalgebra.comul Coalgebra.comul :=
by
rw [ofComonObjCoalgebraStruct_comul]
simp only [Comon.monoidal_tensorObj_comon_comul, Equivalence.symm_inverse, comonEquivalence_functor, toComon_obj,
toComonObj_X, ModuleCat.of_coe, MonObj.tensorObj.mul_def, unop_comp, unop_tensorObj, unop_tensorHom,
BraidedCategory.unop_tensorμ, tensorμ_eq_tensorTensorTensorComm, ModuleCat.hom_comp, ModuleCat.hom_ofHom,
LinearEquiv.comp_toLinearMap_eq_iff]
rfl
