Lean4
/-- A functor taking a colimit on each fiber of a functor `G : Grothendieck F ⥤ H`. -/
@[simps]
def fiberwiseColimit : C ⥤ H where
obj X := colimit (Grothendieck.ι F X ⋙ G)
map {X Y}
f :=
colimMap (whiskerRight (Grothendieck.ιNatTrans f) G ≫ (associator _ _ _).hom) ≫
colimit.pre (Grothendieck.ι F Y ⋙ G) (F.map f)
map_id
X := by
ext d
simp only [Functor.comp_obj, Grothendieck.ιNatTrans, Grothendieck.ι_obj, ι_colimMap_assoc, NatTrans.comp_app,
whiskerRight_app, Functor.associator_hom_app, Category.comp_id, colimit.ι_pre]
conv_rhs => rw [← colimit.eqToHom_comp_ι (Grothendieck.ι F X ⋙ G) (j := (F.map (𝟙 X)).obj d) (by simp)]
rw [← eqToHom_map G (by simp), Grothendieck.eqToHom_eq]
rfl
map_comp {X Y Z} f
g := by
ext d
simp only [Functor.comp_obj, Grothendieck.ιNatTrans, ι_colimMap_assoc, NatTrans.comp_app, whiskerRight_app,
Functor.associator_hom_app, Category.comp_id, colimit.ι_pre, Category.assoc, colimit.ι_pre_assoc]
rw [← Category.assoc, ← G.map_comp]
conv_rhs => rw [← colimit.eqToHom_comp_ι (Grothendieck.ι F Z ⋙ G) (j := (F.map (f ≫ g)).obj d) (by simp)]
rw [← Category.assoc, ← eqToHom_map G (by simp), ← G.map_comp, Grothendieck.eqToHom_eq]
congr 2
fapply Grothendieck.ext
· simp only [eqToHom_refl, Category.assoc, Grothendieck.comp_base, Category.comp_id]
· simp only [Grothendieck.ι_obj, eqToHom_refl, Grothendieck.comp_base, Category.comp_id, Grothendieck.comp_fiber,
Functor.map_id]
conv_rhs => enter [2, 1]; rw [eqToHom_map (F.map (𝟙 Z))]
conv_rhs => rw [eqToHom_trans, eqToHom_trans]
