[GOAL]
C : Type u_1
inst✝² : Category.{?u.1346, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
P : Karoubi (SimplicialObject C)
⊢ N.map (NatTrans.app Γ₂N₂.hom P) ≫ NatTrans.app N₂Γ₂.hom (N.obj P) = 𝟙 (N.obj P)
[PROOFSTEP]
let α := N.mapIso (Γ₂N₂.app P)
[GOAL]
C : Type u_1
inst✝² : Category.{?u.1346, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
P : Karoubi (SimplicialObject C)
α : N.obj ((𝟭 (Karoubi (SimplicialObject C))).obj P) ≅ N.obj ((N₂ ⋙ Γ₂).obj P) := N.mapIso (Γ₂N₂.app P)
⊢ N.map (NatTrans.app Γ₂N₂.hom P) ≫ NatTrans.app N₂Γ₂.hom (N.obj P) = 𝟙 (N.obj P)
[PROOFSTEP]
let β := N₂Γ₂.app (N.obj P)
[GOAL]
C : Type u_1
inst✝² : Category.{?u.1346, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
P : Karoubi (SimplicialObject C)
α : N.obj ((𝟭 (Karoubi (SimplicialObject C))).obj P) ≅ N.obj ((N₂ ⋙ Γ₂).obj P) := N.mapIso (Γ₂N₂.app P)
β : (Γ₂ ⋙ N₂).obj (N.obj P) ≅ (𝟭 (Karoubi (ChainComplex C ℕ))).obj (N.obj P) := N₂Γ₂.app (N.obj P)
⊢ N.map (NatTrans.app Γ₂N₂.hom P) ≫ NatTrans.app N₂Γ₂.hom (N.obj P) = 𝟙 (N.obj P)
[PROOFSTEP]
symm
[GOAL]
C : Type u_1
inst✝² : Category.{?u.1346, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
P : Karoubi (SimplicialObject C)
α : N.obj ((𝟭 (Karoubi (SimplicialObject C))).obj P) ≅ N.obj ((N₂ ⋙ Γ₂).obj P) := N.mapIso (Γ₂N₂.app P)
β : (Γ₂ ⋙ N₂).obj (N.obj P) ≅ (𝟭 (Karoubi (ChainComplex C ℕ))).obj (N.obj P) := N₂Γ₂.app (N.obj P)
⊢ 𝟙 (N.obj P) = N.map (NatTrans.app Γ₂N₂.hom P) ≫ NatTrans.app N₂Γ₂.hom (N.obj P)
[PROOFSTEP]
change 𝟙 _ = α.hom ≫ β.hom
[GOAL]
C : Type u_1
inst✝² : Category.{?u.1346, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
P : Karoubi (SimplicialObject C)
α : N.obj ((𝟭 (Karoubi (SimplicialObject C))).obj P) ≅ N.obj ((N₂ ⋙ Γ₂).obj P) := N.mapIso (Γ₂N₂.app P)
β : (Γ₂ ⋙ N₂).obj (N.obj P) ≅ (𝟭 (Karoubi (ChainComplex C ℕ))).obj (N.obj P) := N₂Γ₂.app (N.obj P)
⊢ 𝟙 (N.obj ((𝟭 (Karoubi (SimplicialObject C))).obj P)) = α.hom ≫ β.hom
[PROOFSTEP]
rw [← Iso.inv_comp_eq, comp_id, ← comp_id β.hom, ← Iso.inv_comp_eq]
[GOAL]
C : Type u_1
inst✝² : Category.{?u.1346, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
P : Karoubi (SimplicialObject C)
α : N.obj ((𝟭 (Karoubi (SimplicialObject C))).obj P) ≅ N.obj ((N₂ ⋙ Γ₂).obj P) := N.mapIso (Γ₂N₂.app P)
β : (Γ₂ ⋙ N₂).obj (N.obj P) ≅ (𝟭 (Karoubi (ChainComplex C ℕ))).obj (N.obj P) := N₂Γ₂.app (N.obj P)
⊢ β.inv ≫ α.inv = 𝟙 ((𝟭 (Karoubi (ChainComplex C ℕ))).obj (N.obj P))
[PROOFSTEP]
exact AlgebraicTopology.DoldKan.identity_N₂_objectwise P
