Lean4
/-- Given a functor `F : C ⥤ Cat` and an equivalence of categories `G : D ≌ C`, the functor
`pre F G.functor` is an equivalence between `Grothendieck (G.functor ⋙ F)` and `Grothendieck F`.
-/
def preEquivalence (G : D ≌ C) : Grothendieck (G.functor ⋙ F) ≌ Grothendieck F
where
functor := pre F G.functor
inverse := preInv F G
unitIso :=
by
refine
(eqToIso ?_) ≪≫
(Grothendieck.preUnitIso F G |> isoWhiskerLeft (map _)) ≪≫
(pre_comp_map_assoc G.functor _ _ |> Eq.symm |> eqToIso)
calc
_ = map (𝟙 _) := map_id_eq.symm
_ = map _ := ?_
_ = map _ ⋙ map _ := map_comp_eq _ _
congr; ext X
simp only [Functor.comp_obj, Functor.comp_map, ← Functor.map_comp, Functor.id_obj, Functor.map_id,
NatTrans.comp_app, NatTrans.id_app, whiskerLeft_app, whiskerRight_app, Equivalence.counitInv_functor_comp]
counitIso := preNatIso F G.counitIso.symm |>.symm
functor_unitIso_comp := by
intro X
simp only [preInv, Grothendieck.preUnitIso, pre_id, Iso.trans_hom, eqToIso.hom, eqToHom_app, eqToHom_refl,
isoWhiskerLeft_hom, NatTrans.comp_app]
fapply Grothendieck.ext <;> simp [preNatIso, transportIso]
