Lean4
/-- Mapping a Grothendieck construction along the whiskering of any natural transformation
`α : F ⟶ G` with the functor `asSmallFunctor : Cat ⥤ Cat` is naturally isomorphic to conjugating
`map α` with the equivalence between `Grothendieck (F ⋙ asSmallFunctor)` and `Grothendieck F`. -/
def mapWhiskerRightAsSmallFunctor (α : F ⟶ G) :
map (whiskerRight α Cat.asSmallFunctor.{w}) ≅
(compAsSmallFunctorEquivalence F).functor ⋙ map α ⋙ (compAsSmallFunctorEquivalence G).inverse :=
NatIso.ofComponents (fun X => Iso.refl _)
(fun f => by
fapply Grothendieck.ext
· simp [compAsSmallFunctorEquivalenceInverse]
· simp only [compAsSmallFunctorEquivalence_functor, compAsSmallFunctorEquivalence_inverse, Functor.comp_obj,
compAsSmallFunctorEquivalenceInverse_obj_base, map_obj_base, compAsSmallFunctorEquivalenceFunctor_obj_base,
Cat.asSmallFunctor_obj, Cat.of_α, Iso.refl_hom, Functor.comp_map, comp_base, id_base,
compAsSmallFunctorEquivalenceInverse_map_base, map_map_base, compAsSmallFunctorEquivalenceFunctor_map_base,
Cat.asSmallFunctor_map, map_obj_fiber, whiskerRight_app, AsSmall.down_obj, AsSmall.up_obj_down,
compAsSmallFunctorEquivalenceInverse_obj_fiber, compAsSmallFunctorEquivalenceFunctor_obj_fiber, comp_fiber,
map_map_fiber, AsSmall.down_map, down_comp, eqToHom_down, AsSmall.up_map_down, Functor.map_comp, eqToHom_map,
id_fiber, Category.assoc, eqToHom_trans_assoc, compAsSmallFunctorEquivalenceInverse_map_fiber,
compAsSmallFunctorEquivalenceFunctor_map_fiber, eqToHom_comp_iff, comp_eqToHom_iff]
simp only [conj_eqToHom_iff_heq']
rw [G.map_id]
simp)
