English
The hη compatibility implies equivalence-unitIso compatibility and coherent comparison with η and ε.
Русский
Совместимость hε согласуется с совместимостью η и ε в эквивалентности.
LaTeX
$$$$ h\\eta = Γ_2N_1 \\;:\\; (toKaroubiEquivalence).functor \\cong N_1 \\circ Γ_0 $$$$
Lean4
theorem hε :
Compatibility.υ (isoN₁) =
(Γ₂N₁ :
(toKaroubiEquivalence _).functor ≅ (N₁ : SimplicialObject C ⥤ _) ⋙ Preadditive.DoldKan.equivalence.inverse) :=
by
dsimp only [isoN₁]
ext1
rw [← cancel_epi Γ₂N₁.inv, Iso.inv_hom_id]
ext X : 2
rw [NatTrans.comp_app, Γ₂N₁_inv, compatibility_Γ₂N₁_Γ₂N₂_natTrans X, Compatibility.υ_hom_app,
Preadditive.DoldKan.equivalence_unitIso, Iso.app_inv, assoc]
dsimp only [Functor.comp_obj, Preadditive.DoldKan.equivalence_inverse, Preadditive.DoldKan.Γ.eq_1,
toKaroubiEquivalence, Functor.asEquivalence_functor, Preadditive.DoldKan.N.eq_1, NatTrans.id_app]
rw [← NatTrans.comp_app_assoc, ← Γ₂N₂_inv, Iso.inv_hom_id, NatTrans.id_app, id_comp, Γ₂N₂ToKaroubiIso_inv_app, ←
Γ₂.map_comp, Iso.inv_hom_id_app, Γ₂.map_id]
