Theorems · Definition · category theory

TopCat.Presheaf.IsSheafOpensLeCover

{C : Type u_1} → [inst : CategoryTheory.Category.{v_1, u_1} C] → {X : TopCat} → TopCat.Presheaf C X → Prop

An equivalent formulation of the sheaf condition (which we prove equivalent to the usual one below as isSheaf_iff_isSheafOpensLeCover). A presheaf is a sheaf if F sends the cone (opensLeCoverCocone U).op to a limit cone. (Recall opensLeCoverCocone U, has cone point iSup U, mapping down to any V which is contained in some U i.)

Defined in

Mathlib.Topology.Sheaves.SheafCondition.OpensLeCover

Cited by

2 results in Mathlib

Foundations

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

Assumes

CategoryTheory.Category