isSheaf_iff_isSheafEqualizerProducts

English

For any presheaf F and cover U, the equalizer condition fork F U is a limit iff the map cone F.mapCone (cocone U)ᵒᵖ is a limit cone.

Русский

Для прешейфа F и покрытия U равноселение условия fork F U эквивалентно тому, что конус отображения F.mapCone (cocone U)ᵒᵖ является пределом.

LaTeX

$$$\text{IsLimit}\bigl(\mathrm{SheafConditionEqualizerProducts.fork}\,F\,U\bigr) \iff \text{IsLimit}\bigl(F.mapCone(\mathrm{cocone}\,U)^{op}\bigr).$$$

Lean4

/-- The sheaf condition in terms of an equalizer diagram is equivalent
to the default sheaf condition.
-/
theorem isSheaf_iff_isSheafEqualizerProducts (F : Presheaf C X) : F.IsSheaf ↔ F.IsSheafEqualizerProducts :=
  (isSheaf_iff_isSheafPairwiseIntersections F).trans <|
    Iff.intro (fun h _ U => ⟨isLimitSheafConditionForkOfIsLimitMapCone F U (h U).some⟩) fun h _ U =>
      ⟨isLimitMapConeOfIsLimitSheafConditionFork F U (h U).some⟩

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