Precoverage

📁 Source: Mathlib/CategoryTheory/Sites/Descent/Precoverage.lean

Statistics

Metric	Count
Definitions fullyFaithfulPullFunctor	1
Theorems faithful_pullFunctor, full_pullFunctor, isEquivalence_toDescentData_of_sieve_le, of_precoverage, of_precoverage, of_le, of_le'	7
Total	8

CategoryTheory.Pseudofunctor.DescentData

Definitions

Name	Category	Theorems
fullyFaithfulPullFunctor 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
faithful_pullFunctor 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Sieve Set Set.instMembership DFunLike.coe CategoryTheory.GrothendieckTopology CategoryTheory.GrothendieckTopology.instDFunLikeSetSieve CategoryTheory.Sieve.ofArrows	CategoryTheory.Functor.Faithful CategoryTheory.Pseudofunctor.DescentData instCategory pullFunctor CategoryTheory.CategoryStruct.id	—	hom_ext Equiv.injective CategoryTheory.GrothendieckTopology.mem_over_iff Equiv.apply_symm_apply CategoryTheory.GrothendieckTopology.pullback_stable CategoryTheory.Presieve.IsSeparatedFor.ext CategoryTheory.Presieve.IsSheaf.isSeparated CategoryTheory.isSheaf_iff_isSheaf_of_type CategoryTheory.Pseudofunctor.IsPrestack.isSheaf CategoryTheory.Category.comp_id CategoryTheory.Over.w CategoryTheory.Category.assoc Hom.comm CategoryTheory.Pseudofunctor.mapComp'_id_comp_inv_app CategoryTheory.locallyDiscreteBicategory.strict CategoryTheory.Cat.Hom.inv_hom_id_toNatTrans_app CategoryTheory.Pseudofunctor.mapComp'_id_comp_hom_app_assoc CategoryTheory.Cat.Hom.inv_hom_id_toNatTrans_app_assoc CategoryTheory.Pseudofunctor.mapComp'_inv_naturality CategoryTheory.Cat.Hom.hom_inv_id_toNatTrans_app_assoc Mathlib.Tactic.Reassoc.eq_whisker' hom_comp hom_self CategoryTheory.Over.OverMorphism.ext CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat.pullHom.congr_simp
full_pullFunctor 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Sieve Set Set.instMembership DFunLike.coe CategoryTheory.GrothendieckTopology CategoryTheory.GrothendieckTopology.instDFunLikeSetSieve CategoryTheory.Sieve.ofArrows	CategoryTheory.Functor.Full CategoryTheory.Pseudofunctor.DescentData instCategory pullFunctor CategoryTheory.CategoryStruct.id	—	hom_ext CategoryTheory.Category.id_comp CategoryTheory.Category.assoc CategoryTheory.Category.comp_id CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat.pullHom_id hom_self
isEquivalence_toDescentData_of_sieve_le 📖	mathematical	CategoryTheory.Sieve Set Set.instMembership DFunLike.coe CategoryTheory.GrothendieckTopology CategoryTheory.GrothendieckTopology.instDFunLikeSetSieve CategoryTheory.Sieve.ofArrows Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CategoryTheory.Sieve.instCompleteLattice	CategoryTheory.Functor.IsEquivalence CategoryTheory.Bundled.α CategoryTheory.Category Prefunctor.obj CategoryTheory.LocallyDiscrete Opposite CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.locallyDiscreteBicategory CategoryTheory.Category.opposite CategoryTheory.Cat CategoryTheory.Cat.bicategory CategoryTheory.PrelaxFunctorStruct.toPrefunctor Quiver.Hom CategoryTheory.Category.toCategoryStruct CategoryTheory.Bicategory.homCategory CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct CategoryTheory.Pseudofunctor.toPrelaxFunctor Opposite.op CategoryTheory.Cat.str CategoryTheory.Pseudofunctor.DescentData instCategory CategoryTheory.Pseudofunctor.toDescentData	—	CategoryTheory.Category.comp_id CategoryTheory.Functor.FullyFaithful.faithful CategoryTheory.GrothendieckTopology.superset_covering CategoryTheory.Functor.FullyFaithful.full CategoryTheory.Functor.IsEquivalence.essSurj

CategoryTheory.Pseudofunctor.IsPrestack

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_precoverage 📖	mathematical	CategoryTheory.Pseudofunctor.IsPrestackFor	CategoryTheory.Pseudofunctor.IsPrestack CategoryTheory.Precoverage.toGrothendieck	—	CategoryTheory.isSheaf_iff_isSheaf_of_type CategoryTheory.over_toGrothendieck_eq_toGrothendieck_comap_forget CategoryTheory.Precoverage.instHasPullbacksOfHasPullbacks CategoryTheory.Over.hasLimitsOfShape_of_isConnected CategoryTheory.instIsConnectedWidePullbackShape CategoryTheory.Precoverage.instHasIsosComap CategoryTheory.Precoverage.instIsStableUnderBaseChangeComapOfPreservesLimitsOfShapeWalkingCospan CategoryTheory.Over.preservesLimitsOfShape_forget_of_isConnected CategoryTheory.Precoverage.instIsStableUnderCompositionComap CategoryTheory.Precoverage.toGrothendieck_toPretopology_eq_toGrothendieck CategoryTheory.Presieve.isSheaf_pretopology Equiv.surjective CategoryTheory.Presieve.isSheafFor_iff_generate CategoryTheory.Pseudofunctor.IsPrestackFor.isSheafFor' CategoryTheory.Sieve.overEquiv_generate CategoryTheory.Presieve.functorPushforward_overForget CategoryTheory.Sieve.generate_sieve

CategoryTheory.Pseudofunctor.IsStack

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_precoverage 📖	mathematical	CategoryTheory.Pseudofunctor.IsStackFor	CategoryTheory.Pseudofunctor.IsStack CategoryTheory.Precoverage.toGrothendieck	—	CategoryTheory.Pseudofunctor.IsPrestack.of_precoverage CategoryTheory.Pseudofunctor.IsStackFor.isPrestackFor CategoryTheory.Pseudofunctor.IsStackFor.essSurj CategoryTheory.Precoverage.toGrothendieck_toPretopology_eq_toGrothendieck CategoryTheory.Pseudofunctor.IsStackFor.of_le CategoryTheory.Precoverage.generate_mem_toGrothendieck

CategoryTheory.Pseudofunctor.IsStackFor

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_le 📖	—	CategoryTheory.Pseudofunctor.IsStackFor CategoryTheory.Sieve Set Set.instMembership DFunLike.coe CategoryTheory.GrothendieckTopology CategoryTheory.GrothendieckTopology.instDFunLikeSetSieve CategoryTheory.Sieve.generate CategoryTheory.Presieve Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CategoryTheory.instCompleteLatticePresieve	—	—	CategoryTheory.Presieve.exists_eq_ofArrows CategoryTheory.Pseudofunctor.isStackFor_ofArrows_iff CategoryTheory.Pseudofunctor.DescentData.isEquivalence_toDescentData_of_sieve_le CategoryTheory.Sieve.generate_mono
of_le' 📖	—	CategoryTheory.Pseudofunctor.IsStackFor CategoryTheory.Sieve.arrows CategoryTheory.Sieve Set Set.instMembership DFunLike.coe CategoryTheory.GrothendieckTopology CategoryTheory.GrothendieckTopology.instDFunLikeSetSieve Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CategoryTheory.Sieve.instCompleteLattice	—	—	of_le CategoryTheory.Sieve.generate_sieve

---

← Back to Index