English
If F ≅ G, then the fork for F is isomorphic to the fork for G after postcomposition with the diagram isomorphism.
Русский
Если F ≅ G, то форк для F эквивалентен форку для G после композиции с изоморфизмом диаграммы.
LaTeX
$$$\mathrm{fork}(F,U) \cong (\mathrm{Cones.postcompose}(\mathrm{diagram.isoOfIso}(U,\alpha)^{-1}).\mathrmobj\;\mathrm{fork}(G,U))$$$
Lean4
/-- If `F G : Presheaf C X` are isomorphic presheaves,
then the `fork F U`, the canonical cone of the sheaf condition diagram for `F`,
is isomorphic to `fork F G` postcomposed with the corresponding isomorphism between
sheaf condition diagrams.
-/
def isoOfIso (α : F ≅ G) : fork F U ≅ (Cones.postcompose (diagram.isoOfIso U α).inv).obj (fork G U) :=
by
fapply Fork.ext
· apply α.app
· dsimp
ext
dsimp only [Fork.ι]
-- Ugh, `simp` can't unfold abbreviations.
simp only [res, diagram.isoOfIso, piOpens.isoOfIso, Cones.postcompose_obj_π, NatTrans.comp_app,
fork_π_app_walkingParallelPair_zero, NatIso.ofComponents_inv_app, Functor.mapIso_inv, lim_map, limit.lift_map,
Category.assoc, limit.lift_π, Fan.mk_π_app, Discrete.natIso_inv_app, Iso.app_inv, NatTrans.naturality,
Iso.hom_inv_id_app_assoc]
