LocallySurjective

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

Statistics

Metric	Count
Definitions `IsLocallySurjective`, `imageSieve`, `localPreimage`, `sheafificationIsoImagePresheaf`, `localPreimage`, `IsLocallySurjective`	6
Theorems `imageSieve_mem`, `app_localPreimage`, `comp_isLocallyInjective_iff`, `comp_isLocallySurjective_iff`, `imageSieve_app`, `imageSieve_apply`, `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'`, `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`	39
Total	45

CategoryTheory.Presheaf

Definitions

Name	Category	Theorems
`IsLocallySurjective` 📖	CompData	33 math math: `instIsLocallySurjectiveHomWhiskerRightOppositeForget`, `CategoryTheory.Sheaf.isLocallySurjective_sheafToPresheaf_map_iff`, `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`, `isLocallySurjective_whisker_iff`, `isLocallySurjective_of_le`, `CategoryTheory.GrothendieckTopology.instIsLocallySurjectiveToSheafify`, `CategoryTheory.coherentTopology.presheafIsLocallySurjective_iff`, `isLocallySurjective_iff_of_fac`, `CategoryTheory.coherentTopology.isLocallySurjective_iff`, `CategoryTheory.GrothendieckTopology.W.isLocallySurjective`, `isLocallySurjective_of_iso`, `CategoryTheory.GrothendieckTopology.W_iff_isLocallyBijective`, `isLocallySurjective_presheafToSheaf_map_iff`
`imageSieve` 📖	CompOp	8 math math: `imageSieve_app`, `CategoryTheory.Functor.imageSieve_eq_imageSieve`, `imageSieve_apply`, `IsLocallySurjective.imageSieve_mem`, `imageSieve_eq_sieveOfSection`, `imageSieve_whisker_forget`, `CategoryTheory.Presieve.FamilyOfElements.isAmalgamation_map_localPreimage`, `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` `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_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`

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	15 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`, `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` `instCategorySheaf`	—	`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` `instCategorySheaf`	—	`hom_ext` `CategoryTheory.NatTrans.ext'` `CategoryTheory.types_ext` `CategoryTheory.Presieve.IsSeparatedFor.ext` `CategoryTheory.Presieve.IsSheaf.isSeparated` `CategoryTheory.isSheaf_iff_isSheaf_of_type` `cond` `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` `instCategorySheaf` `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` `instCategorySheaf`	—	`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` `instCategorySheaf`	—	`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` `instCategorySheaf` `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.instReflectsIsomorphismsSheafFunctorOppositeSheafToPresheaf`
`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` `instCategorySheaf` `CategoryTheory.Functor` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Functor.category` `CategoryTheory.sheafToPresheaf` `CategoryTheory.Functor.map` `IsLocallySurjective`	—	—

---

← Back to Index