LocallySurjective

📁 Source: Mathlib/CategoryTheory/Sites/LocallySurjective.lean

Statistics

Metric	Count
Definitions IsLocallySurjective, imageSieve, localPreimage, sheafificationIsoImagePresheaf, localPreimage, IsLocallySurjective	6
Theorems ofArrows_mem_iff_isLocallySurjective_cofanIsColimitDesc_shrinkYoneda_map, ofArrows_mem_iff_isLocallySurjective_cofanIsColimitDesc_uliftYoneda_map, ofArrows_mem_iff_isLocallySurjective_sigmaDesc_shrinkYoneda_map, ofArrows_mem_iff_isLocallySurjective_sigmaDesc_uliftYoneda_map, imageSieve_mem, app_localPreimage, comp_isLocallyInjective_iff, comp_isLocallySurjective_iff, imageSieve_app, imageSieve_apply, imageSieve_cofanIsColimitDesc_shrinkYoneda_map, imageSieve_eq_sieveOfSection, imageSieve_mem, imageSieve_whisker_forget, instIsLocallySurjectiveHomToRangeSheafify, instIsLocallySurjectiveHomWhiskerRightOppositeForget, isLocallyInjective_of_isLocallyInjective_of_isLocallySurjective, isLocallyInjective_of_isLocallyInjective_of_isLocallySurjective_fac, isLocallySurjective_comp, isLocallySurjective_comp_iff, isLocallySurjective_iff_of_fac, isLocallySurjective_iff_range_sheafify_eq_top, isLocallySurjective_iff_range_sheafify_eq_top', isLocallySurjective_iff_whisker_forget, isLocallySurjective_of_isLocallySurjective, isLocallySurjective_of_isLocallySurjective_fac, isLocallySurjective_of_isLocallySurjective_of_isLocallyInjective, isLocallySurjective_of_isLocallySurjective_of_isLocallyInjective_fac, isLocallySurjective_of_iso, isLocallySurjective_of_le, isLocallySurjective_of_surjective, isLocallySurjective_toPlus, isLocallySurjective_toSheafify, isLocallySurjective_toSheafify', pullback_imageSieve, isAmalgamation_map_localPreimage, epi_of_isLocallySurjective, epi_of_isLocallySurjective', instIsLocallySurjectiveHomMapTypeSheafComposeForget, instIsLocallySurjectiveHomToImage, isLocallySurjective_comp, isLocallySurjective_iff_epi, isLocallySurjective_iff_isIso, isLocallySurjective_of_iso, isLocallySurjective_sheafToPresheaf_map_iff	45
Total	51

CategoryTheory.GrothendieckTopology

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ofArrows_mem_iff_isLocallySurjective_cofanIsColimitDesc_shrinkYoneda_map 📖	mathematical	—	CategoryTheory.Sieve Set Set.instMembership DFunLike.coe CategoryTheory.GrothendieckTopology instDFunLikeSetSieve CategoryTheory.Sieve.ofArrows CategoryTheory.Presheaf.IsLocallySurjective CategoryTheory.types Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Types.instFunLike CategoryTheory.Types.instConcreteCategory CategoryTheory.Limits.Cocone.pt CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.Discrete.functor CategoryTheory.Functor.obj CategoryTheory.shrinkYoneda CategoryTheory.Limits.Cofan.IsColimit.desc CategoryTheory.Functor.map	—	Equiv.surjective pullback_stable CategoryTheory.Presheaf.imageSieve_cofanIsColimitDesc_shrinkYoneda_map CategoryTheory.Sieve.pullback_id CategoryTheory.Presheaf.imageSieve_mem
ofArrows_mem_iff_isLocallySurjective_cofanIsColimitDesc_uliftYoneda_map 📖	mathematical	—	CategoryTheory.Sieve Set Set.instMembership DFunLike.coe CategoryTheory.GrothendieckTopology instDFunLikeSetSieve CategoryTheory.Sieve.ofArrows CategoryTheory.Presheaf.IsLocallySurjective CategoryTheory.types Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Types.instFunLike CategoryTheory.Types.instConcreteCategory CategoryTheory.Limits.Cocone.pt CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.Discrete.functor CategoryTheory.Functor.obj CategoryTheory.uliftYoneda CategoryTheory.Limits.Cofan.IsColimit.desc CategoryTheory.Functor.map	—	CategoryTheory.locallySmall_of_univLE univLE_of_max UnivLE.self ofArrows_mem_iff_isLocallySurjective_cofanIsColimitDesc_shrinkYoneda_map CategoryTheory.Limits.Cofan.IsColimit.hom_ext CategoryTheory.Limits.Cofan.IsColimit.fac_assoc CategoryTheory.NatTrans.naturality CategoryTheory.Limits.Cofan.IsColimit.fac CategoryTheory.Category.assoc CategoryTheory.Iso.hom_inv_id_app_assoc CategoryTheory.Presheaf.isLocallySurjective_comp_iff CategoryTheory.Presheaf.instIsLocallyInjectiveOfIsIsoFunctorOpposite CategoryTheory.NatIso.hom_app_isIso CategoryTheory.Presheaf.isLocallySurjective_of_iso
ofArrows_mem_iff_isLocallySurjective_sigmaDesc_shrinkYoneda_map 📖	mathematical	—	CategoryTheory.Sieve Set Set.instMembership DFunLike.coe CategoryTheory.GrothendieckTopology instDFunLikeSetSieve CategoryTheory.Sieve.ofArrows CategoryTheory.Presheaf.IsLocallySurjective CategoryTheory.types Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Types.instFunLike CategoryTheory.Types.instConcreteCategory CategoryTheory.Limits.sigmaObj CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.Functor.obj CategoryTheory.shrinkYoneda CategoryTheory.Limits.functorCategoryHasColimit CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Discrete.functor CategoryTheory.Limits.Types.hasColimit CategoryTheory.instSmallDiscrete CategoryTheory.Functor.flip CategoryTheory.Limits.Sigma.desc CategoryTheory.Functor.map	—	ofArrows_mem_iff_isLocallySurjective_cofanIsColimitDesc_shrinkYoneda_map CategoryTheory.Limits.functorCategoryHasColimit CategoryTheory.Limits.Types.hasColimit CategoryTheory.instSmallDiscrete
ofArrows_mem_iff_isLocallySurjective_sigmaDesc_uliftYoneda_map 📖	mathematical	—	CategoryTheory.Sieve Set Set.instMembership DFunLike.coe CategoryTheory.GrothendieckTopology instDFunLikeSetSieve CategoryTheory.Sieve.ofArrows CategoryTheory.Presheaf.IsLocallySurjective CategoryTheory.types Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Types.instFunLike CategoryTheory.Types.instConcreteCategory CategoryTheory.Limits.sigmaObj CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.Functor.obj CategoryTheory.uliftYoneda CategoryTheory.Limits.functorCategoryHasColimit CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Discrete.functor CategoryTheory.Limits.Types.hasColimit CategoryTheory.instSmallDiscrete CategoryTheory.Functor.flip CategoryTheory.Limits.Sigma.desc CategoryTheory.Functor.map	—	ofArrows_mem_iff_isLocallySurjective_cofanIsColimitDesc_uliftYoneda_map CategoryTheory.Limits.functorCategoryHasColimit CategoryTheory.Limits.Types.hasColimit CategoryTheory.instSmallDiscrete

CategoryTheory.Presheaf

Definitions

Name	Category	Theorems
IsLocallySurjective 📖	CompData	38 math math: instIsLocallySurjectiveHomWhiskerRightOppositeForget, CategoryTheory.Sheaf.isLocallySurjective_sheafToPresheaf_map_iff, CategoryTheory.ObjectProperty.IsConservativeFamilyOfPoints.jointly_reflect_isLocallySurjective, isLocallySurjective_of_surjective, isLocallySurjective_whisker, comp_isLocallySurjective_iff, isLocallySurjective_toSheafify, isLocallySurjective_comp_iff, isLocallySurjective_toSheafify', CategoryTheory.GrothendieckTopology.WEqualsLocallyBijective.iff, isLocallySurjective_of_isLocallySurjective_of_isLocallyInjective_fac, isLocallySurjective_of_isLocallySurjective_fac, isLocallySurjective_of_isLocallySurjective_of_isLocallyInjective, CategoryTheory.regularTopology.isLocallySurjective_iff, isLocallySurjective_iff_range_sheafify_eq_top, CategoryTheory.regularTopology.isLocallySurjective_sheaf_of_types, isLocallySurjective_iff_range_sheafify_eq_top', isLocallySurjective_iff_whisker_forget, isLocallySurjective_of_whisker, CategoryTheory.extensiveTopology.presheafIsLocallySurjective_iff, isLocallySurjective_comp, isLocallySurjective_of_isLocallySurjective, isLocallySurjective_toPlus, instIsLocallySurjectiveHomToRangeSheafify, CategoryTheory.GrothendieckTopology.ofArrows_mem_iff_isLocallySurjective_cofanIsColimitDesc_shrinkYoneda_map, isLocallySurjective_whisker_iff, isLocallySurjective_of_le, CategoryTheory.GrothendieckTopology.instIsLocallySurjectiveToSheafify, CategoryTheory.coherentTopology.presheafIsLocallySurjective_iff, isLocallySurjective_iff_of_fac, CategoryTheory.GrothendieckTopology.ofArrows_mem_iff_isLocallySurjective_sigmaDesc_uliftYoneda_map, CategoryTheory.coherentTopology.isLocallySurjective_iff, CategoryTheory.GrothendieckTopology.ofArrows_mem_iff_isLocallySurjective_cofanIsColimitDesc_uliftYoneda_map, CategoryTheory.GrothendieckTopology.W.isLocallySurjective, isLocallySurjective_of_iso, CategoryTheory.GrothendieckTopology.W_iff_isLocallyBijective, isLocallySurjective_presheafToSheaf_map_iff, CategoryTheory.GrothendieckTopology.ofArrows_mem_iff_isLocallySurjective_sigmaDesc_shrinkYoneda_map
imageSieve 📖	CompOp	10 math math: imageSieve_app, CategoryTheory.Functor.imageSieve_eq_imageSieve, imageSieve_apply, IsLocallySurjective.imageSieve_mem, imageSieve_eq_sieveOfSection, imageSieve_cofanIsColimitDesc_shrinkYoneda_map, imageSieve_whisker_forget, CategoryTheory.Presieve.FamilyOfElements.isAmalgamation_map_localPreimage, pullback_imageSieve, imageSieve_mem
localPreimage 📖	CompOp	1 math math: app_localPreimage
sheafificationIsoImagePresheaf 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
app_localPreimage 📖	mathematical	CategoryTheory.Sieve.arrows Opposite.unop imageSieve	DFunLike.coe CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Opposite.op CategoryTheory.ConcreteCategory.hom CategoryTheory.NatTrans.app localPreimage Opposite.unop CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct	—	—
comp_isLocallyInjective_iff 📖	mathematical	—	IsLocallyInjective CategoryTheory.CategoryStruct.comp CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category	—	isLocallyInjective_of_isLocallyInjective_of_isLocallySurjective isLocallyInjective_comp
comp_isLocallySurjective_iff 📖	mathematical	—	IsLocallySurjective CategoryTheory.CategoryStruct.comp CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category	—	isLocallySurjective_iff_of_fac
imageSieve_app 📖	mathematical	—	imageSieve DFunLike.coe CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Opposite.op CategoryTheory.ConcreteCategory.hom CategoryTheory.NatTrans.app Top.top CategoryTheory.Sieve OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice CategoryTheory.Sieve.instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	CategoryTheory.Sieve.ext CategoryTheory.NatTrans.naturality_apply
imageSieve_apply 📖	mathematical	—	CategoryTheory.Sieve.arrows imageSieve CategoryTheory.ToType CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Opposite.op DFunLike.coe CategoryTheory.ConcreteCategory.hom CategoryTheory.NatTrans.app CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct	—	—
imageSieve_cofanIsColimitDesc_shrinkYoneda_map 📖	mathematical	—	imageSieve CategoryTheory.types Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Types.instFunLike CategoryTheory.Types.instConcreteCategory CategoryTheory.Limits.Cocone.pt CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.Discrete.functor CategoryTheory.Functor.obj CategoryTheory.shrinkYoneda CategoryTheory.Limits.Cofan.IsColimit.desc CategoryTheory.Functor.map DFunLike.coe Equiv Opposite.unop Opposite.op EquivLike.toFunLike Equiv.instEquivLike Equiv.symm CategoryTheory.shrinkYonedaObjObjEquiv CategoryTheory.Sieve.pullback CategoryTheory.Sieve.ofArrows	—	CategoryTheory.Sieve.ext CategoryTheory.Limits.Types.jointly_surjective_of_isColimit CategoryTheory.Limits.evaluation_preservesColimit CategoryTheory.Limits.Types.hasColimit CategoryTheory.instSmallDiscrete Equiv.surjective Equiv.injective CategoryTheory.shrinkYoneda_map_app_shrinkYonedaObjObjEquiv_symm CategoryTheory.NatTrans.congr_app CategoryTheory.Limits.Cofan.IsColimit.fac CategoryTheory.shrinkYoneda_obj_map_shrinkYonedaObjObjEquiv_symm
imageSieve_eq_sieveOfSection 📖	mathematical	—	imageSieve CategoryTheory.Subfunctor.sieveOfSection CategoryTheory.Functor.comp Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.forget CategoryTheory.Subfunctor.range CategoryTheory.Functor.whiskerRight Opposite.op	—	—
imageSieve_mem 📖	mathematical	—	CategoryTheory.Sieve Opposite.unop Set Set.instMembership DFunLike.coe CategoryTheory.GrothendieckTopology CategoryTheory.GrothendieckTopology.instDFunLikeSetSieve imageSieve	—	IsLocallySurjective.imageSieve_mem
imageSieve_whisker_forget 📖	mathematical	—	imageSieve CategoryTheory.types Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Types.instFunLike CategoryTheory.Types.instConcreteCategory CategoryTheory.Functor.comp Opposite CategoryTheory.Category.opposite CategoryTheory.forget CategoryTheory.Functor.whiskerRight	—	—
instIsLocallySurjectiveHomToRangeSheafify 📖	mathematical	—	IsLocallySurjective CategoryTheory.types Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Types.instFunLike CategoryTheory.Types.instConcreteCategory CategoryTheory.Subfunctor.toFunctor Opposite CategoryTheory.Category.opposite CategoryTheory.Subfunctor.sheafify CategoryTheory.Subfunctor.range CategoryTheory.Subfunctor.toRangeSheafify	—	CategoryTheory.GrothendieckTopology.superset_covering
instIsLocallySurjectiveHomWhiskerRightOppositeForget 📖	mathematical	—	IsLocallySurjective CategoryTheory.types Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Types.instFunLike CategoryTheory.Types.instConcreteCategory CategoryTheory.Functor.comp Opposite CategoryTheory.Category.opposite CategoryTheory.forget CategoryTheory.Functor.whiskerRight	—	imageSieve_mem
isLocallyInjective_of_isLocallyInjective_of_isLocallySurjective 📖	mathematical	—	IsLocallyInjective	—	CategoryTheory.GrothendieckTopology.intersection_covering imageSieve_mem CategoryTheory.GrothendieckTopology.superset_covering CategoryTheory.Functor.map_comp CategoryTheory.comp_apply CategoryTheory.NatTrans.naturality_apply app_localPreimage CategoryTheory.GrothendieckTopology.transitive CategoryTheory.Sieve.le_pullback_bind equalizerSieve_mem CategoryTheory.ConcreteCategory.comp_apply
isLocallyInjective_of_isLocallyInjective_of_isLocallySurjective_fac 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category	IsLocallyInjective	—	isLocallyInjective_of_isLocallyInjective_of_isLocallySurjective
isLocallySurjective_comp 📖	mathematical	—	IsLocallySurjective CategoryTheory.CategoryStruct.comp CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category	—	CategoryTheory.op_comp CategoryTheory.Functor.map_comp CategoryTheory.NatTrans.comp_app CategoryTheory.ConcreteCategory.comp_apply CategoryTheory.NatTrans.naturality_apply CategoryTheory.GrothendieckTopology.superset_covering CategoryTheory.GrothendieckTopology.bind_covering imageSieve_mem
isLocallySurjective_comp_iff 📖	mathematical	—	IsLocallySurjective CategoryTheory.CategoryStruct.comp CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category	—	isLocallySurjective_of_isLocallySurjective_of_isLocallyInjective isLocallySurjective_comp
isLocallySurjective_iff_of_fac 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category	IsLocallySurjective	—	isLocallySurjective_of_isLocallySurjective_fac isLocallySurjective_comp
isLocallySurjective_iff_range_sheafify_eq_top 📖	mathematical	—	IsLocallySurjective CategoryTheory.Subfunctor.sheafify CategoryTheory.Functor.comp Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.forget CategoryTheory.Subfunctor.range CategoryTheory.Functor.whiskerRight Top.top CategoryTheory.Subfunctor OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice CategoryTheory.instCompleteLatticeSubfunctor BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	IsLocallySurjective.imageSieve_mem
isLocallySurjective_iff_range_sheafify_eq_top' 📖	mathematical	—	IsLocallySurjective CategoryTheory.types Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Types.instFunLike CategoryTheory.Types.instConcreteCategory CategoryTheory.Subfunctor.sheafify CategoryTheory.Subfunctor.range Opposite CategoryTheory.Category.opposite Top.top CategoryTheory.Subfunctor OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice CategoryTheory.instCompleteLatticeSubfunctor BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	isLocallySurjective_iff_range_sheafify_eq_top
isLocallySurjective_iff_whisker_forget 📖	mathematical	—	IsLocallySurjective CategoryTheory.types Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Types.instFunLike CategoryTheory.Types.instConcreteCategory CategoryTheory.Functor.comp Opposite CategoryTheory.Category.opposite CategoryTheory.forget CategoryTheory.Functor.whiskerRight	—	—
isLocallySurjective_of_isLocallySurjective 📖	mathematical	—	IsLocallySurjective	—	CategoryTheory.GrothendieckTopology.superset_covering CategoryTheory.comp_apply app_localPreimage imageSieve_mem
isLocallySurjective_of_isLocallySurjective_fac 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category	IsLocallySurjective	—	isLocallySurjective_of_isLocallySurjective
isLocallySurjective_of_isLocallySurjective_of_isLocallyInjective 📖	mathematical	—	IsLocallySurjective	—	CategoryTheory.GrothendieckTopology.superset_covering CategoryTheory.NatTrans.naturality_apply CategoryTheory.Functor.map_comp CategoryTheory.comp_apply CategoryTheory.GrothendieckTopology.transitive imageSieve_mem CategoryTheory.Sieve.le_pullback_bind equalizerSieve_mem app_localPreimage CategoryTheory.NatTrans.comp_app CategoryTheory.ConcreteCategory.comp_apply
isLocallySurjective_of_isLocallySurjective_of_isLocallyInjective_fac 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category	IsLocallySurjective	—	isLocallySurjective_of_isLocallySurjective_of_isLocallyInjective
isLocallySurjective_of_iso 📖	mathematical	—	IsLocallySurjective	—	isLocallySurjective_of_surjective Function.Bijective.surjective CategoryTheory.isIso_iff_bijective CategoryTheory.ConcreteCategory.forget_map_eq_coe CategoryTheory.Functor.map_isIso CategoryTheory.NatIso.isIso_app_of_isIso
isLocallySurjective_of_le 📖	mathematical	CategoryTheory.GrothendieckTopology CategoryTheory.GrothendieckTopology.instLEGrothendieckTopology	IsLocallySurjective	—	IsLocallySurjective.imageSieve_mem
isLocallySurjective_of_surjective 📖	mathematical	CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite DFunLike.coe CategoryTheory.ConcreteCategory.hom CategoryTheory.NatTrans.app	IsLocallySurjective	—	imageSieve_app CategoryTheory.GrothendieckTopology.top_mem
isLocallySurjective_toPlus 📖	mathematical	—	IsLocallySurjective CategoryTheory.types Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Types.instFunLike CategoryTheory.Types.instConcreteCategory CategoryTheory.GrothendieckTopology.plusObj CategoryTheory.Limits.Types.hasLimit CategoryTheory.Limits.WalkingMulticospan CategoryTheory.GrothendieckTopology.Cover.shape CategoryTheory.Limits.WalkingMulticospan.instSmallCategory UnivLE.small UnivLE.self CategoryTheory.Limits.MulticospanIndex.multicospan CategoryTheory.GrothendieckTopology.Cover.index CategoryTheory.Limits.Types.hasColimitsOfShape Opposite CategoryTheory.GrothendieckTopology.Cover CategoryTheory.Category.opposite Preorder.smallCategory CategoryTheory.GrothendieckTopology.instPreorderCover Opposite.small CategoryTheory.GrothendieckTopology.toPlus	—	CategoryTheory.Limits.Types.hasLimit UnivLE.small UnivLE.self CategoryTheory.Limits.Types.hasColimitsOfShape Opposite.small CategoryTheory.Functor.corepresentable_preservesLimitsOfShape CategoryTheory.Types.instIsCorepresentableForgetTypeHom CategoryTheory.GrothendieckTopology.Plus.exists_rep CategoryTheory.Functor.instPreservesColimitsOfShapeOfIsLeftAdjoint CategoryTheory.Functor.isLeftAdjoint_of_isEquivalence CategoryTheory.Types.instIsEquivalenceForgetTypeHom CategoryTheory.GrothendieckTopology.superset_covering CategoryTheory.GrothendieckTopology.Plus.res_mk_eq_mk_pullback CategoryTheory.GrothendieckTopology.Plus.eq_mk_iff_exists le_top CategoryTheory.Meq.ext CategoryTheory.Sieve.downward_closed CategoryTheory.Category.id_comp CategoryTheory.Functor.map_id
isLocallySurjective_toSheafify 📖	mathematical	—	IsLocallySurjective CategoryTheory.types Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Types.instFunLike CategoryTheory.Types.instConcreteCategory CategoryTheory.GrothendieckTopology.sheafify CategoryTheory.Limits.Types.hasLimit CategoryTheory.Limits.WalkingMulticospan CategoryTheory.GrothendieckTopology.Cover.shape CategoryTheory.Limits.WalkingMulticospan.instSmallCategory UnivLE.small UnivLE.self CategoryTheory.Limits.MulticospanIndex.multicospan CategoryTheory.GrothendieckTopology.Cover.index CategoryTheory.Limits.Types.hasColimitsOfShape Opposite CategoryTheory.GrothendieckTopology.Cover CategoryTheory.Category.opposite Preorder.smallCategory CategoryTheory.GrothendieckTopology.instPreorderCover Opposite.small CategoryTheory.GrothendieckTopology.toSheafify	—	CategoryTheory.Limits.Types.hasLimit UnivLE.small UnivLE.self CategoryTheory.Limits.Types.hasColimitsOfShape Opposite.small CategoryTheory.GrothendieckTopology.plusMap_toPlus isLocallySurjective_comp isLocallySurjective_toPlus
isLocallySurjective_toSheafify' 📖	mathematical	—	IsLocallySurjective CategoryTheory.sheafify CategoryTheory.toSheafify	—	isLocallySurjective_iff_whisker_forget CategoryTheory.instHasWeakSheafifyOfHasSheafify CategoryTheory.instHasSheafifyType CategoryTheory.sheafComposeIso_hom_fac CategoryTheory.Limits.Types.hasLimit UnivLE.small UnivLE.self CategoryTheory.Limits.Types.hasColimitsOfShape Opposite.small CategoryTheory.sheafToPresheaf_isRightAdjoint CategoryTheory.Functor.corepresentable_preservesLimitsOfShape CategoryTheory.Types.instIsCorepresentableForgetTypeHom CategoryTheory.Functor.instPreservesColimitsOfShapeOfIsLeftAdjoint CategoryTheory.Functor.isLeftAdjoint_of_isEquivalence CategoryTheory.Types.instIsEquivalenceForgetTypeHom CategoryTheory.reflectsIsomorphisms_of_full_and_faithful CategoryTheory.Types.instFullForgetTypeHom CategoryTheory.instFaithfulForget CategoryTheory.toSheafify_plusPlusIsoSheafify_hom isLocallySurjective_comp isLocallySurjective_toSheafify isLocallySurjective_of_iso CategoryTheory.Iso.isIso_hom
pullback_imageSieve 📖	mathematical	—	CategoryTheory.Sieve.pullback imageSieve DFunLike.coe CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Opposite.op CategoryTheory.ConcreteCategory.hom CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct	—	CategoryTheory.Sieve.ext CategoryTheory.Functor.map_comp CategoryTheory.comp_apply

CategoryTheory.Presheaf.IsLocallySurjective

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
imageSieve_mem 📖	mathematical	—	CategoryTheory.Sieve Set Set.instMembership DFunLike.coe CategoryTheory.GrothendieckTopology CategoryTheory.GrothendieckTopology.instDFunLikeSetSieve CategoryTheory.Presheaf.imageSieve	—	—

CategoryTheory.Presieve.FamilyOfElements

Definitions

Name	Category	Theorems
localPreimage 📖	CompOp	1 math math: isAmalgamation_map_localPreimage

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isAmalgamation_map_localPreimage 📖	mathematical	—	IsAmalgamation Opposite.unop CategoryTheory.Sieve.arrows CategoryTheory.Presheaf.imageSieve CategoryTheory.types Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Types.instFunLike CategoryTheory.Types.instConcreteCategory map localPreimage	—	CategoryTheory.Presheaf.app_localPreimage

CategoryTheory.Sheaf

Definitions

Name	Category	Theorems
IsLocallySurjective 📖	MathDef	16 math math: isLocallySurjective_sheafToPresheaf_map_iff, instIsLocallySurjectiveHomToImage, instIsLocallySurjectiveAppArrowILocallySurjectiveLocallyInjectiveFunctorialLocallySurjectiveInjectiveFactorization, isLocallySurjective_comp, isLocallySurjective_iff_epi, AlgebraicGeometry.Scheme.LocalRepresentability.instIsLocallySurjectiveHomYonedaGluedToSheafOfIsLocallySurjectiveZariskiTopologyDescFunctorOppositeType, isLocallySurjective_iff_epi', LightCondensed.isLocallySurjective_iff_locallySurjective_on_lightProfinite, CategoryTheory.extensiveTopology.isLocallySurjective_iff, instIsLocallySurjectiveHomMapTypeSheafComposeForget, isLocallyBijective_iff_isIso, CategoryTheory.coherentTopology.isLocallySurjective_π_app_zero_of_isLocallySurjective_map, isLocallySurjective_iff_isIso, CategoryTheory.coherentTopology.isLocallySurjective_iff, isLocallySurjective_of_iso, CategoryTheory.Presheaf.isLocallySurjective_presheafToSheaf_map_iff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
epi_of_isLocallySurjective 📖	mathematical	—	CategoryTheory.Epi CategoryTheory.Sheaf CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf	—	CategoryTheory.Functor.epi_of_epi_map CategoryTheory.Functor.reflectsEpimorphisms_of_faithful CategoryTheory.instFaithfulSheafSheafCompose CategoryTheory.instFaithfulForget epi_of_isLocallySurjective' instIsLocallySurjectiveHomMapTypeSheafComposeForget
epi_of_isLocallySurjective' 📖	mathematical	—	CategoryTheory.Epi CategoryTheory.Sheaf CategoryTheory.types CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf	—	CategoryTheory.ObjectProperty.hom_ext CategoryTheory.NatTrans.ext' CategoryTheory.types_ext CategoryTheory.Presieve.IsSeparatedFor.ext CategoryTheory.Presieve.IsSheaf.isSeparated CategoryTheory.isSheaf_iff_isSheaf_of_type CategoryTheory.ObjectProperty.FullSubcategory.property CategoryTheory.Presheaf.imageSieve_mem CategoryTheory.NatTrans.naturality CategoryTheory.congr_app CategoryTheory.Functor.congr_map
instIsLocallySurjectiveHomMapTypeSheafComposeForget 📖	mathematical	—	IsLocallySurjective CategoryTheory.types Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Types.instFunLike CategoryTheory.Types.instConcreteCategory CategoryTheory.Functor.obj CategoryTheory.Sheaf CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf CategoryTheory.sheafCompose CategoryTheory.forget CategoryTheory.Functor.map	—	CategoryTheory.Presheaf.isLocallySurjective_iff_whisker_forget
instIsLocallySurjectiveHomToImage 📖	mathematical	—	IsLocallySurjective CategoryTheory.types Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Types.instFunLike CategoryTheory.Types.instConcreteCategory image toImage	—	CategoryTheory.Presheaf.instIsLocallySurjectiveHomToRangeSheafify
isLocallySurjective_comp 📖	mathematical	—	IsLocallySurjective CategoryTheory.CategoryStruct.comp CategoryTheory.Sheaf CategoryTheory.Category.toCategoryStruct CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf	—	CategoryTheory.Presheaf.isLocallySurjective_comp
isLocallySurjective_iff_epi 📖	mathematical	—	IsLocallySurjective CategoryTheory.types Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Types.instFunLike CategoryTheory.Types.instConcreteCategory CategoryTheory.Epi CategoryTheory.Sheaf CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf	—	epi_of_isLocallySurjective' CategoryTheory.epi_of_epi_fac toImage_ι isLocallySurjective_iff_isIso CategoryTheory.isIso_of_mono_of_epi CategoryTheory.SheafOfTypes.balanced CategoryTheory.instMonoSheafTypeImageι
isLocallySurjective_iff_isIso 📖	mathematical	—	IsLocallySurjective CategoryTheory.types Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Types.instFunLike CategoryTheory.Types.instConcreteCategory CategoryTheory.IsIso CategoryTheory.Sheaf CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf image imageι	—	imageι.eq_1 CategoryTheory.Presheaf.isLocallySurjective_iff_range_sheafify_eq_top' CategoryTheory.Subfunctor.eq_top_iff_isIso CategoryTheory.isIso_iff_of_reflects_iso CategoryTheory.reflectsIsomorphisms_of_full_and_faithful CategoryTheory.ObjectProperty.full_ι CategoryTheory.ObjectProperty.faithful_ι
isLocallySurjective_of_iso 📖	mathematical	—	IsLocallySurjective	—	CategoryTheory.Functor.map_isIso CategoryTheory.Presheaf.isLocallySurjective_of_iso
isLocallySurjective_sheafToPresheaf_map_iff 📖	mathematical	—	CategoryTheory.Presheaf.IsLocallySurjective CategoryTheory.Functor.obj CategoryTheory.Sheaf CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf CategoryTheory.sheafToPresheaf CategoryTheory.Functor.map IsLocallySurjective	—	—

---

← Back to Index