commBialgCatEquivComonCommAlgCat_inverse_map_unop_hom

English

The inverse equivalence maps an opposite-homomorphism back to the original homomorphism in the expected way: the image under inverse.map f is opposite to f, i.e. the underlying AlgHom is f.unop.hom.unop.hom.

Русский

Обратная эквивалентность переводит противоположный морфизм обратно в исходный морфизм; соответствие задаётся как f.unop.hom.unop.hom.

LaTeX

$$$\\text{AlgHomClass.toAlgHom}((\\mathrm{commBialgCatEquivComonCommAlgCat R).inverse.map f}).hom = f.unop.hom.unop.hom$$$

Lean4

@[simp]
theorem commBialgCatEquivComonCommAlgCat_inverse_map_unop_hom {A B : (Mon (CommAlgCat R)ᵒᵖ)ᵒᵖ} (f : A ⟶ B) :
    AlgHomClass.toAlgHom ((commBialgCatEquivComonCommAlgCat R).inverse.map f).hom = f.unop.hom.unop.hom :=
  rfl

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