isSheaf_of_projective — Mathlib

English

Same as 79606: the equalizer condition is equivalent to the isomorphism property of the equalizer lift

Русский

То же, что и 79606: условие равнозначителя эквивалентно свойству изоморфизма подъема равнозначителя

LaTeX

$$equalizerCondition_iff_isIso_lift P$$

Lean4

/-- Every presheaf is a sheaf for the regular topology if every object of `C` is projective. -/
theorem isSheaf_of_projective (F : Cᵒᵖ ⥤ D) [Preregular C] [∀ (X : C), Projective X] :
    Presheaf.IsSheaf (regularTopology C) F := fun _ ↦
  (isSheaf_coverage _ _).mpr fun S ⟨_, h⟩ ↦
    have : S.regular := ⟨_, h⟩
    isSheafFor_regular_of_projective _ _

Похожие утверждения