Theorems · Theorem · category theory

TopCat.Presheaf.isSheaf_iff_isSheafOpensLeCover

∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X : TopCat} (F : TopCat.Presheaf C X),
  F.IsSheaf ↔ F.IsSheafOpensLeCover

A presheaf (opens X)ᵒᵖ ⥤ C on a topological space X is a sheaf on the site opens X iff it satisfies the IsSheafOpensLeCover sheaf condition. The latter is not the official definition of sheaves on spaces, but has the advantage that it does not require has_products C.

Defined in

Mathlib.Topology.Sheaves.SheafCondition.OpensLeCover

Cited by

2 results in Mathlib

Foundations

Depth 83 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.Category