English
There is a canonical equivalence between Čech conerve morphisms and arrow morphisms, compatible with composition.
Русский
Существует каноническая эквиваленция между морфизмами Čech-конвервы и стрелочными морфизмами, совместимая с композициями.
LaTeX
$$$\\mathrm{cechConerveEquiv} : (F.augmentedCechConerve \\to X) \\simeq (F \\to Augmented.toArrow.obj X)$$$
Lean4
theorem equivalenceCounitIso_eq (hη : τ₀ = τ₁ hF hG η) : (equivalence hF hG).counitIso = equivalenceCounitIso η :=
by
ext1; apply NatTrans.ext; ext Y
dsimp [equivalence]
simp only [comp_id, id_comp, Functor.map_comp, equivalence₂CounitIso_eq, equivalence₂CounitIso_hom_app, assoc,
equivalenceCounitIso_hom_app]
simp only [equivalence₂_inverse, comp_obj, ← τ₀_hom_app, hη, τ₁_hom_app, ← eB.inverse.map_comp_assoc]
rw [hF.inv.naturality_assoc, hF.inv.naturality_assoc]
congr 2
simp only [← e'.functor.map_comp_assoc]
simp only [Functor.comp_map, Equivalence.fun_inv_map, comp_obj, id_obj, map_comp, assoc]
simp only [← e'.functor.map_comp_assoc]
simp only [Iso.inv_hom_id_app_assoc, Iso.inv_hom_id_app, comp_obj, comp_id, Equivalence.functor_unit_comp, map_id,
id_comp]
