English
The transport of HasSheafCompose along an equivalence yields HasSheafCompose for the transported functor.
Русский
Перенос HasSheafCompose вдоль эквивалентности даёт HasSheafCompose для перенесенного функторa.
LaTeX
$$$HasSheafCompose F$ transported$$
Lean4
theorem transport [Functor.IsContinuous.{v₄} G K J] [Functor.IsContinuous.{v₃} G K J]
[(G.sheafPushforwardContinuous B K J).EssSurj] [(G.sheafPushforwardContinuous A K J).EssSurj]
[K.PreservesSheafification F] : J.PreservesSheafification F where
le P Q f
hf := by
rw [← J.W_whiskerLeft_iff (G := G) (K := K)] at hf
have := K.W_of_preservesSheafification F (whiskerLeft G.op f) hf
rw [whiskerRight_left] at this
haveI :=
K.W.of_postcomp (W' := MorphismProperty.isomorphisms _) _ _ (Iso.isIso_inv _) <|
K.W.of_precomp (W' := MorphismProperty.isomorphisms _) _ _ (Iso.isIso_hom _) this
rwa [K.W_whiskerLeft_iff (G := G) (J := J) (f := whiskerRight f F)] at this
