English
Given X ⟶ Y and Y ⟶ X with appropriate unit and counit data, the symmetric constructor of the isomorphism equals the isomorphism obtained by swapping the two arrows.
Русский
Дано A→B и B→A с соответствующими данными единицы и counit; симметричный конструктор изоморфизма равен изоморфизму, полученному заменой стрелок местами.
LaTeX
$$$\\text{Iso.symm}\\{hom, inv, hom\\_inv\\_id, inv\\_hom\\_id\\} = \\{ hom := inv, inv := hom, hom\\_inv\\_id := inv\\_hom\\_id, inv\\_hom\\_id := hom\\_inv\\_id \\}$$$
Lean4
@[simp, grind =]
theorem symm_mk {X Y : C} (hom : X ⟶ Y) (inv : Y ⟶ X) (hom_inv_id) (inv_hom_id) :
Iso.symm { hom, inv, hom_inv_id := hom_inv_id, inv_hom_id := inv_hom_id } =
{ hom := inv, inv := hom, hom_inv_id := inv_hom_id, inv_hom_id := hom_inv_id } :=
rfl
