English
The counit of the opposite triangle equivalence provides a natural isomorphism between the functor composing inverse and the identity on triangles in the opposite category.
Русский
Сгонка (counit) противоположной эквивалентности треугольников задаёт естественное изоморфное отображение между композициями inverse и идентичностью на треугольниках в противоположной категории.
LaTeX
$$counitIso : inverse C ⋙ functor C ≅ 𝟭 _$$
Lean4
/-- The counit isomorphism of the
equivalence `triangleOpEquivalence C : (Triangle C)ᵒᵖ ≌ Triangle Cᵒᵖ` . -/
@[simps!]
noncomputable def counitIso : inverse C ⋙ functor C ≅ 𝟭 _ :=
NatIso.ofComponents
(fun T => by
refine Triangle.isoMk _ _ (Iso.refl _) (Iso.refl _) (Iso.refl _) ?_ ?_ ?_
· simp
· simp
· dsimp
rw [Functor.map_id, comp_id, id_comp, Functor.map_comp, ←
opShiftFunctorEquivalence_counitIso_inv_naturality_assoc, opShiftFunctorEquivalence_counitIso_inv_app_shift, ←
Functor.map_comp, Iso.hom_inv_id_app, Functor.map_id]
simp only [Functor.id_obj, comp_id])
(by cat_disch)
