Lean4
/-- Given a cone over `F ⋙ G`, we can construct a `Cone G` with the same cocone point.
-/
@[simps]
def extendCone : Cone (F ⋙ G) ⥤ Cone G
where
obj
c :=
{ pt := c.pt
π :=
{ app := fun d => c.π.app (lift F d) ≫ G.map (homToLift F d)
naturality := fun X Y f => by
dsimp;
simp only [Category.id_comp, Category.assoc]
-- This would be true if we'd chosen `lift F Y` to be `lift F X`
-- and `homToLift F Y` to be `homToLift F X ≫ f`.
apply
induction F fun Z k =>
(c.π.app Z ≫ G.map k : c.pt ⟶ _) = c.π.app (lift F X) ≫ G.map (homToLift F X) ≫ G.map f
· intro Z₁ Z₂ k₁ k₂ g a z
rw [← a, Functor.map_comp, ← Functor.comp_map, ← Category.assoc, ← Category.assoc, c.w] at z
rw [z, Category.assoc]
· intro Z₁ Z₂ k₁ k₂ g a z
rw [← a, Functor.map_comp, ← Functor.comp_map, ← Category.assoc, ← Category.assoc, c.w, z, Category.assoc]
· rw [← Functor.map_comp] } }
map f := { hom := f.hom }
