SheafComparison

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

Statistics

Metric	Count
Definitions coherentExtensiveEquivalence, equivalence, equivalence', equivalence	4
Theorems coherentExtensiveEquivalence_counitIso, coherentExtensiveEquivalence_functor_map_val, coherentExtensiveEquivalence_functor_obj_val, coherentExtensiveEquivalence_inverse_map_val, coherentExtensiveEquivalence_inverse_obj_val, coherentExtensiveEquivalence_unitIso, instHasSheafComposeCoherentTopologyOfForallEffectiveEpiHasPullbackOfPreservesFiniteLimits, instHasSheafComposeCoherentTopologyOfProjectiveOfPreservesFiniteProducts, instPreservesFiniteProductsOppositeVal, isSheaf_coherent_iff_regular_and_extensive, isSheaf_coherent_of_hasPullbacks_comp, isSheaf_coherent_of_hasPullbacks_of_comp, isSheaf_coherent_of_projective_comp, isSheaf_coherent_of_projective_of_comp, isSheaf_iff_extensiveSheaf_of_projective, isSheaf_iff_preservesFiniteProducts_and_equalizerCondition, isSheaf_iff_preservesFiniteProducts_of_projective, coverPreserving, eq_induced, exists_effectiveEpiFamily_iff_mem_induced, instIsCoverDense, instIsDenseSubsite, coverPreserving, eq_induced, exists_effectiveEpi_iff_mem_induced, instIsCoverDense, instIsDenseSubsite	27
Total	31

CategoryTheory.Presheaf

Definitions

Name	Category	Theorems
coherentExtensiveEquivalence 📖	CompOp	6 math math: coherentExtensiveEquivalence_functor_map_val, coherentExtensiveEquivalence_counitIso, coherentExtensiveEquivalence_inverse_map_val, coherentExtensiveEquivalence_unitIso, coherentExtensiveEquivalence_functor_obj_val, coherentExtensiveEquivalence_inverse_obj_val

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coherentExtensiveEquivalence_counitIso 📖	mathematical	CategoryTheory.Projective	CategoryTheory.Equivalence.counitIso CategoryTheory.Sheaf CategoryTheory.coherentTopology CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive CategoryTheory.extensiveTopology CategoryTheory.Sheaf.instCategorySheaf coherentExtensiveEquivalence CategoryTheory.Iso.refl CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.comp CategoryTheory.Sheaf.val CategoryTheory.Sheaf.Hom.val	—	CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular
coherentExtensiveEquivalence_functor_map_val 📖	mathematical	CategoryTheory.Projective	CategoryTheory.Sheaf.Hom.val CategoryTheory.extensiveTopology CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive CategoryTheory.Sheaf.val CategoryTheory.coherentTopology CategoryTheory.Functor.map CategoryTheory.Sheaf CategoryTheory.Sheaf.instCategorySheaf CategoryTheory.Equivalence.functor CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular coherentExtensiveEquivalence	—	CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular
coherentExtensiveEquivalence_functor_obj_val 📖	mathematical	CategoryTheory.Projective	CategoryTheory.Sheaf.val CategoryTheory.extensiveTopology CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive CategoryTheory.Functor.obj CategoryTheory.Sheaf CategoryTheory.coherentTopology CategoryTheory.Sheaf.instCategorySheaf CategoryTheory.Equivalence.functor CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular coherentExtensiveEquivalence	—	CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular
coherentExtensiveEquivalence_inverse_map_val 📖	mathematical	CategoryTheory.Projective	CategoryTheory.Sheaf.Hom.val CategoryTheory.coherentTopology CategoryTheory.Sheaf.val CategoryTheory.extensiveTopology CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive CategoryTheory.Functor.map CategoryTheory.Sheaf CategoryTheory.Sheaf.instCategorySheaf CategoryTheory.Equivalence.inverse CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular coherentExtensiveEquivalence	—	CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular
coherentExtensiveEquivalence_inverse_obj_val 📖	mathematical	CategoryTheory.Projective	CategoryTheory.Sheaf.val CategoryTheory.coherentTopology CategoryTheory.Functor.obj CategoryTheory.Sheaf CategoryTheory.extensiveTopology CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive CategoryTheory.Sheaf.instCategorySheaf CategoryTheory.Equivalence.inverse CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular coherentExtensiveEquivalence	—	CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular
coherentExtensiveEquivalence_unitIso 📖	mathematical	CategoryTheory.Projective	CategoryTheory.Equivalence.unitIso CategoryTheory.Sheaf CategoryTheory.coherentTopology CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive CategoryTheory.extensiveTopology CategoryTheory.Sheaf.instCategorySheaf coherentExtensiveEquivalence CategoryTheory.Iso.refl CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.id	—	CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive
instHasSheafComposeCoherentTopologyOfForallEffectiveEpiHasPullbackOfPreservesFiniteLimits 📖	mathematical	CategoryTheory.Limits.HasPullback	CategoryTheory.GrothendieckTopology.HasSheafCompose CategoryTheory.coherentTopology CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive	—	CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive isSheaf_coherent_of_hasPullbacks_comp
instHasSheafComposeCoherentTopologyOfProjectiveOfPreservesFiniteProducts 📖	mathematical	CategoryTheory.Projective	CategoryTheory.GrothendieckTopology.HasSheafCompose CategoryTheory.coherentTopology CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive	—	CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive isSheaf_coherent_of_projective_comp
instPreservesFiniteProductsOppositeVal 📖	mathematical	—	CategoryTheory.Limits.PreservesFiniteProducts Opposite CategoryTheory.Category.opposite CategoryTheory.Sheaf.val CategoryTheory.coherentTopology CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive	—	CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive isSheaf_iff_preservesFiniteProducts isSheaf_coherent_iff_regular_and_extensive CategoryTheory.Sheaf.cond
isSheaf_coherent_iff_regular_and_extensive 📖	mathematical	—	IsSheaf CategoryTheory.coherentTopology CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular CategoryTheory.extensiveTopology CategoryTheory.regularTopology	—	CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular CategoryTheory.extensive_regular_generate_coherent isSheaf_sup
isSheaf_coherent_of_hasPullbacks_comp 📖	mathematical	CategoryTheory.Limits.HasPullback IsSheaf CategoryTheory.coherentTopology CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive	CategoryTheory.Functor.comp Opposite CategoryTheory.Category.opposite	—	CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive isSheaf_iff_preservesFiniteProducts_and_equalizerCondition CategoryTheory.Limits.comp_preservesFiniteProducts CategoryTheory.Limits.instPreservesFiniteProductsOfPreservesFiniteLimits CategoryTheory.regularTopology.equalizerCondition_w CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit CategoryTheory.Limits.PreservesFiniteLimits.preservesFiniteLimits
isSheaf_coherent_of_hasPullbacks_of_comp 📖	—	CategoryTheory.Limits.HasPullback IsSheaf CategoryTheory.coherentTopology CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive CategoryTheory.Functor.comp Opposite CategoryTheory.Category.opposite	—	—	CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive isSheaf_iff_preservesFiniteProducts_and_equalizerCondition CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit CategoryTheory.Limits.instPreservesLimitsOfShapeDiscreteOfFiniteOfPreservesFiniteProducts Finite.of_fintype CategoryTheory.Limits.reflectsLimit_of_reflectsLimitsOfShape CategoryTheory.Limits.ReflectsFiniteLimits.reflects CategoryTheory.regularTopology.equalizerCondition_w
isSheaf_coherent_of_projective_comp 📖	mathematical	CategoryTheory.Projective IsSheaf CategoryTheory.coherentTopology CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive	CategoryTheory.Functor.comp Opposite CategoryTheory.Category.opposite	—	CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive isSheaf_iff_preservesFiniteProducts_of_projective CategoryTheory.Limits.comp_preservesFiniteProducts
isSheaf_coherent_of_projective_of_comp 📖	—	CategoryTheory.Projective IsSheaf CategoryTheory.coherentTopology CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive CategoryTheory.Functor.comp Opposite CategoryTheory.Category.opposite	—	—	CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive isSheaf_iff_preservesFiniteProducts_of_projective CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit CategoryTheory.Limits.instPreservesLimitsOfShapeDiscreteOfFiniteOfPreservesFiniteProducts Finite.of_fintype CategoryTheory.Limits.reflectsLimit_of_reflectsLimitsOfShape CategoryTheory.Limits.instReflectsLimitsOfShapeDiscreteOfReflectsFiniteProductsOfFinite
isSheaf_iff_extensiveSheaf_of_projective 📖	mathematical	CategoryTheory.Projective	IsSheaf CategoryTheory.coherentTopology CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive CategoryTheory.extensiveTopology	—	CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive isSheaf_iff_preservesFiniteProducts_of_projective isSheaf_iff_preservesFiniteProducts
isSheaf_iff_preservesFiniteProducts_and_equalizerCondition 📖	mathematical	CategoryTheory.Limits.HasPullback	IsSheaf CategoryTheory.coherentTopology CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive CategoryTheory.Limits.PreservesFiniteProducts Opposite CategoryTheory.Category.opposite CategoryTheory.regularTopology.EqualizerCondition	—	CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive isSheaf_coherent_iff_regular_and_extensive isSheaf_iff_preservesFiniteProducts CategoryTheory.regularTopology.equalizerCondition_iff_isSheaf
isSheaf_iff_preservesFiniteProducts_of_projective 📖	mathematical	CategoryTheory.Projective	IsSheaf CategoryTheory.coherentTopology CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive CategoryTheory.Limits.PreservesFiniteProducts Opposite CategoryTheory.Category.opposite	—	CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive isSheaf_coherent_iff_regular_and_extensive CategoryTheory.regularTopology.isSheaf_of_projective isSheaf_iff_preservesFiniteProducts

CategoryTheory.coherentTopology

Definitions

Name	Category	Theorems
equivalence 📖	CompOp	—
equivalence' 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coverPreserving 📖	mathematical	—	CategoryTheory.CoverPreserving CategoryTheory.coherentTopology CategoryTheory.Functor.reflects_precoherent	—	CategoryTheory.Functor.IsDenseSubsite.coverPreserving CategoryTheory.Functor.reflects_precoherent instIsDenseSubsite
eq_induced 📖	mathematical	—	CategoryTheory.coherentTopology CategoryTheory.Functor.reflects_precoherent CategoryTheory.Functor.inducedTopology CategoryTheory.Functor.locallyCoverDense_of_isCoverDense CategoryTheory.Functor.IsLocallyFull.of_full instIsCoverDense CategoryTheory.Functor.IsLocallyFaithful.of_faithful	—	CategoryTheory.GrothendieckTopology.ext CategoryTheory.Functor.reflects_precoherent CategoryTheory.Functor.locallyCoverDense_of_isCoverDense CategoryTheory.Functor.IsLocallyFull.of_full instIsCoverDense CategoryTheory.Functor.IsLocallyFaithful.of_faithful Set.ext exists_effectiveEpiFamily_iff_mem_induced mem_sieves_iff_hasEffectiveEpiFamily
exists_effectiveEpiFamily_iff_mem_induced 📖	mathematical	—	CategoryTheory.EffectiveEpiFamily CategoryTheory.Sieve.arrows CategoryTheory.Sieve Set Set.instMembership DFunLike.coe CategoryTheory.GrothendieckTopology CategoryTheory.GrothendieckTopology.instDFunLikeSetSieve CategoryTheory.Functor.inducedTopology CategoryTheory.coherentTopology CategoryTheory.Functor.locallyCoverDense_of_isCoverDense CategoryTheory.Functor.IsLocallyFull.of_full instIsCoverDense CategoryTheory.Functor.IsLocallyFaithful.of_faithful	—	CategoryTheory.Functor.locallyCoverDense_of_isCoverDense CategoryTheory.Functor.IsLocallyFull.of_full instIsCoverDense CategoryTheory.Functor.IsLocallyFaithful.of_faithful mem_sieves_iff_hasEffectiveEpiFamily CategoryTheory.Functor.map_finite_effectiveEpiFamily CategoryTheory.Sieve.image_mem_functorPushforward CategoryTheory.Functor.EffectivelyEnough.presentation CategoryTheory.precoherentEffectiveEpiFamilyCompEffectiveEpis CategoryTheory.Functor.instEffectiveEpiEffectiveEpiOver CategoryTheory.Functor.finite_effectiveEpiFamily_of_map CategoryTheory.Functor.map_preimage CategoryTheory.Functor.map_injective CategoryTheory.Functor.map_comp CategoryTheory.Category.assoc CategoryTheory.Sieve.downward_closed
instIsCoverDense 📖	mathematical	—	CategoryTheory.Functor.IsCoverDense CategoryTheory.coherentTopology	—	CategoryTheory.Functor.isCoverDense_of_generate_singleton_functor_π_mem CategoryTheory.Functor.EffectivelyEnough.presentation Finite.of_fintype CategoryTheory.effectiveEpi_iff_effectiveEpiFamily CategoryTheory.Functor.instEffectiveEpiEffectiveEpiOver
instIsDenseSubsite 📖	mathematical	—	CategoryTheory.Functor.IsDenseSubsite CategoryTheory.coherentTopology CategoryTheory.Functor.reflects_precoherent	—	CategoryTheory.Functor.reflects_precoherent instIsCoverDense CategoryTheory.Functor.IsLocallyFull.of_full CategoryTheory.Functor.IsLocallyFaithful.of_faithful CategoryTheory.Functor.locallyCoverDense_of_isCoverDense eq_induced

CategoryTheory.regularTopology

Definitions

Name	Category	Theorems
equivalence 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coverPreserving 📖	mathematical	—	CategoryTheory.CoverPreserving CategoryTheory.regularTopology CategoryTheory.Functor.reflects_preregular	—	CategoryTheory.Functor.IsDenseSubsite.coverPreserving CategoryTheory.Functor.reflects_preregular instIsDenseSubsite
eq_induced 📖	mathematical	—	CategoryTheory.regularTopology CategoryTheory.Functor.reflects_preregular CategoryTheory.Functor.inducedTopology CategoryTheory.Functor.locallyCoverDense_of_isCoverDense CategoryTheory.Functor.IsLocallyFull.of_full instIsCoverDense CategoryTheory.Functor.IsLocallyFaithful.of_faithful	—	CategoryTheory.GrothendieckTopology.ext CategoryTheory.Functor.reflects_preregular CategoryTheory.Functor.locallyCoverDense_of_isCoverDense CategoryTheory.Functor.IsLocallyFull.of_full instIsCoverDense CategoryTheory.Functor.IsLocallyFaithful.of_faithful Set.ext exists_effectiveEpi_iff_mem_induced mem_sieves_iff_hasEffectiveEpi
exists_effectiveEpi_iff_mem_induced 📖	mathematical	—	CategoryTheory.EffectiveEpi CategoryTheory.Sieve.arrows CategoryTheory.Sieve Set Set.instMembership DFunLike.coe CategoryTheory.GrothendieckTopology CategoryTheory.GrothendieckTopology.instDFunLikeSetSieve CategoryTheory.Functor.inducedTopology CategoryTheory.regularTopology CategoryTheory.Functor.locallyCoverDense_of_isCoverDense CategoryTheory.Functor.IsLocallyFull.of_full instIsCoverDense CategoryTheory.Functor.IsLocallyFaithful.of_faithful	—	CategoryTheory.Functor.locallyCoverDense_of_isCoverDense CategoryTheory.Functor.IsLocallyFull.of_full instIsCoverDense CategoryTheory.Functor.IsLocallyFaithful.of_faithful mem_sieves_iff_hasEffectiveEpi CategoryTheory.Functor.map_effectiveEpi CategoryTheory.Sieve.image_mem_functorPushforward CategoryTheory.Functor.EffectivelyEnough.presentation CategoryTheory.Functor.effectiveEpi_of_map CategoryTheory.Functor.map_preimage instEffectiveEpiComp CategoryTheory.Functor.instEffectiveEpiEffectiveEpiOver CategoryTheory.Functor.map_injective CategoryTheory.Functor.map_comp CategoryTheory.Category.assoc CategoryTheory.Sieve.downward_closed
instIsCoverDense 📖	mathematical	—	CategoryTheory.Functor.IsCoverDense CategoryTheory.regularTopology	—	CategoryTheory.Functor.isCoverDense_of_generate_singleton_functor_π_mem CategoryTheory.Functor.EffectivelyEnough.presentation CategoryTheory.Functor.instEffectiveEpiEffectiveEpiOver
instIsDenseSubsite 📖	mathematical	—	CategoryTheory.Functor.IsDenseSubsite CategoryTheory.regularTopology CategoryTheory.Functor.reflects_preregular	—	CategoryTheory.Functor.reflects_preregular instIsCoverDense CategoryTheory.Functor.IsLocallyFull.of_full CategoryTheory.Functor.IsLocallyFaithful.of_faithful CategoryTheory.Functor.locallyCoverDense_of_isCoverDense eq_induced

---

← Back to Index