commBialgCatEquivComonCommAlgCat_functor_map_unop_hom

English

Under the equivalence between CommBialgCat R and ComonCommAlgCat R, the functorial map on morphisms corresponds to the opposite of the corresponding AlgHom; i.e., mapping respects the opposite picture.

Русский

При эквивалентности между CommBialgCat R и ComonCommAlgCat R отображение функторов по морфизмам соответствует противоположному отображению AlgHom; отображение сохраняет противоположную схему.

LaTeX

$$$((commBialgCatEquivComonCommAlgCat R).functor.map f).unop.hom = (CommAlgCat.ofHom (AlgHomClass.toAlgHom f.hom)).op$$$

Lean4

@[simp]
theorem commBialgCatEquivComonCommAlgCat_functor_map_unop_hom {A B : CommBialgCat R} (f : A ⟶ B) :
    ((commBialgCatEquivComonCommAlgCat R).functor.map f).unop.hom =
      (CommAlgCat.ofHom (AlgHomClass.toAlgHom f.hom)).op :=
  rfl

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