English
Under preregular C, finitaryExtensive C, HasPullbacks, ReflectsFiniteLimits for s, and F presheaf on C^op, if hF is IsSheaf(coherentTopology C) F then F.comp s is also IsSheaf(coherentTopology C).
Русский
При preregular C, finitaryExtensive C, HasPullbacks и ReflectsFiniteLimits для s, и F как преснефлеска на C^op, если hF является IsSheaf(coherentTopology C) F, то F.comp s тоже является IsSheaf(coherentTopology C).
LaTeX
$$$IsSheaf(coherentTopology\, C) (F) \Rightarrow IsSheaf(coherentTopology\, C) (F \circ s)$$$
Lean4
theorem isSheaf_coherent_of_hasPullbacks_of_comp [Preregular C] [FinitaryExtensive C]
[h : ∀ {Y X : C} (f : Y ⟶ X) [EffectiveEpi f], HasPullback f f] [ReflectsFiniteLimits s]
(hF : IsSheaf (coherentTopology C) (F ⋙ s)) : IsSheaf (coherentTopology C) F :=
by
rw [isSheaf_iff_preservesFiniteProducts_and_equalizerCondition (h := h)] at hF ⊢
obtain ⟨_, hF₂⟩ := hF
refine ⟨⟨fun n ↦ ⟨fun {K} ↦ ⟨fun {c} hc ↦ ?_⟩⟩⟩, fun _ _ π _ c hc ↦ ⟨?_⟩⟩
· exact ⟨isLimitOfReflects s (isLimitOfPreserves (F ⋙ s) hc)⟩
· exact isLimitOfIsLimitForkMap s _ (hF₂ π c hc).some
