ExtensiveSheaves

📁 Source: Mathlib/CategoryTheory/Sites/Coherent/ExtensiveSheaves.lean

Statistics

Metric	Count
Definitions	0
Theorems isSheaf_iff_preservesFiniteProducts, arrows_nonempty_isColimit, isSheaf_iff_preservesFiniteProducts, isSheaf_yoneda_obj, subcanonical, instExtensiveOfArrowsι, instHasPairwisePullbacksOfExtensive, instPreservesFiniteProductsOppositeVal, isSheafFor_extensive_of_preservesFiniteProducts	9
Total	9

CategoryTheory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instExtensiveOfArrowsι 📖	mathematical	—	Presieve.Extensive Limits.sigmaObj Limits.hasColimitOfHasColimitsOfShape Discrete discreteCategory Limits.hasColimitsOfShape_discrete FinitaryPreExtensive.hasFiniteCoproducts Discrete.functor Presieve.ofArrows Limits.Sigma.ι	—	Limits.hasColimitOfHasColimitsOfShape Limits.hasColimitsOfShape_discrete FinitaryPreExtensive.hasFiniteCoproducts
instHasPairwisePullbacksOfExtensive 📖	mathematical	—	Presieve.HasPairwisePullbacks	—	Presieve.Extensive.arrows_nonempty_isColimit FinitaryPreExtensive.hasPullbacks_of_is_coproduct
instPreservesFiniteProductsOppositeVal 📖	mathematical	—	Limits.PreservesFiniteProducts Opposite Category.opposite Sheaf.val extensiveTopology	—	Presheaf.isSheaf_iff_preservesFiniteProducts Sheaf.cond
isSheafFor_extensive_of_preservesFiniteProducts 📖	mathematical	—	Presieve.IsSheafFor	—	Presieve.Extensive.arrows_nonempty_isColimit instHasPairwisePullbacksOfExtensive nonempty_fintype Presieve.isSheafFor_of_preservesProduct UnivLE.small univLE_of_max UnivLE.self Limits.PreservesLimitsOfShape.preservesLimit Limits.instPreservesLimitsOfShapeDiscreteOfFiniteOfPreservesFiniteProducts

CategoryTheory.Presheaf

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isSheaf_iff_preservesFiniteProducts 📖	mathematical	—	IsSheaf CategoryTheory.extensiveTopology CategoryTheory.Limits.PreservesFiniteProducts Opposite CategoryTheory.Category.opposite	—	CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit CategoryTheory.Limits.instPreservesLimitsOfShapeDiscreteOfFiniteOfPreservesFiniteProducts Finite.of_fintype CategoryTheory.Presieve.isSheaf_iff_preservesFiniteProducts IsSheaf.eq_1 CategoryTheory.Limits.comp_preservesLimitsOfShape CategoryTheory.coyonedaPreservesLimitsOfShape

CategoryTheory.Presieve

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isSheaf_iff_preservesFiniteProducts 📖	mathematical	—	IsSheaf CategoryTheory.extensiveTopology CategoryTheory.Limits.PreservesFiniteProducts Opposite CategoryTheory.Category.opposite CategoryTheory.types	—	CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.hasColimitsOfShape_discrete CategoryTheory.FinitaryExtensive.hasFiniteCoproducts Finite.of_fintype CategoryTheory.instHasPairwisePullbacksOfExtensive CategoryTheory.instExtensiveOfArrowsι CategoryTheory.instMonoι preservesProduct_of_isSheafFor isSheaf_coverage CategoryTheory.extensiveTopology.eq_1 Empty.instIsEmpty CategoryTheory.Limits.Sigma.hom_ext Unique.instSubsingleton UnivLE.small univLE_of_max UnivLE.self CategoryTheory.FinitaryExtensive.isPullback_initial_to_sigma_ι CategoryTheory.Limits.colimit.ι_desc CategoryTheory.Category.comp_id CategoryTheory.IsIso.id CategoryTheory.Limits.preservesLimit_of_iso_diagram CategoryTheory.isSheafFor_extensive_of_preservesFiniteProducts

CategoryTheory.Presieve.Extensive

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
arrows_nonempty_isColimit 📖	mathematical	—	CategoryTheory.Presieve.ofArrows CategoryTheory.Limits.IsColimit CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Discrete.functor	—	—

CategoryTheory.extensiveTopology

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isSheaf_yoneda_obj 📖	mathematical	—	CategoryTheory.Presieve.IsSheaf CategoryTheory.extensiveTopology CategoryTheory.Functor.obj CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.category CategoryTheory.yoneda	—	eq_1 CategoryTheory.Presieve.isSheaf_coverage CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.hasColimitsOfShape_discrete CategoryTheory.FinitaryPreExtensive.hasFiniteCoproducts CategoryTheory.isSheafFor_extensive_of_preservesFiniteProducts CategoryTheory.Limits.instPreservesFiniteProductsOfPreservesFiniteLimits CategoryTheory.Limits.PreservesLimits.preservesFiniteLimits CategoryTheory.yoneda_preservesLimits
subcanonical 📖	mathematical	—	CategoryTheory.GrothendieckTopology.Subcanonical CategoryTheory.extensiveTopology	—	CategoryTheory.GrothendieckTopology.Subcanonical.of_isSheaf_yoneda_obj isSheaf_yoneda_obj

---

← Back to Index