LocallyInjective

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

Statistics

Metric	Count
Definitions IsLocallyInjective, equalizerSieve, IsLocallyInjective	3
Theorems equalizerSieve_mem, equalizerSieve_apply, equalizerSieve_eq_top_iff, equalizerSieve_mem, equalizerSieve_mem_of_equalizerSieve_app_mem, equalizerSieve_self_eq_top, instIsLocallyInjectiveHomιOpposite, instIsLocallyInjectiveOfIsIsoFunctorOpposite, isLocallyInjective_comp, isLocallyInjective_comp_iff, isLocallyInjective_forget, isLocallyInjective_forget_iff, isLocallyInjective_iff_equalizerSieve_mem_imp, isLocallyInjective_iff_injective_of_separated, isLocallyInjective_iff_of_fac, isLocallyInjective_of_injective, isLocallyInjective_of_isLocallyInjective, isLocallyInjective_of_isLocallyInjective_fac, isLocallyInjective_toPlus, isLocallyInjective_toSheafify, isLocallyInjective_toSheafify', instIsLocallyInjectiveHomImageι, isLocallyInjective_forget, isLocallyInjective_iff_injective, isLocallyInjective_of_iso, isLocallyInjective_sheafToPresheaf_map_iff, mono_of_injective, mono_of_isLocallyInjective	28
Total	31

CategoryTheory.Presheaf

Definitions

Name	Category	Theorems
IsLocallyInjective 📖	CompData	27 math math: isLocallyInjective_of_isLocallyInjective, CategoryTheory.GrothendieckTopology.instIsLocallyInjectiveToSheafify, isLocallyInjective_iff_equalizerSieve_mem_imp, isLocallyInjective_presheafToSheaf_map_iff, isLocallyInjective_of_whisker, isLocallyInjective_of_isLocallyInjective_of_isLocallySurjective_fac, isLocallyInjective_toSheafify', isLocallyInjective_whisker, CategoryTheory.GrothendieckTopology.WEqualsLocallyBijective.iff, isLocallyInjective_toSheafify, instIsLocallyInjectiveOfIsIsoFunctorOpposite, isLocallyInjective_of_isLocallyInjective_of_isLocallySurjective, isLocallyInjective_whisker_iff, isLocallyInjective_forget_iff, isLocallyInjective_comp_iff, CategoryTheory.GrothendieckTopology.W.isLocallyInjective, CategoryTheory.Sheaf.isLocallyInjective_sheafToPresheaf_map_iff, isLocallyInjective_iff_of_fac, comp_isLocallyInjective_iff, instIsLocallyInjectiveHomιOpposite, isLocallyInjective_toPlus, isLocallyInjective_forget, isLocallyInjective_iff_injective_of_separated, isLocallyInjective_of_isLocallyInjective_fac, isLocallyInjective_comp, CategoryTheory.GrothendieckTopology.W_iff_isLocallyBijective, isLocallyInjective_of_injective
equalizerSieve 📖	CompOp	7 math math: isLocallyInjective_iff_equalizerSieve_mem_imp, equalizerSieve_self_eq_top, IsLocallyInjective.equalizerSieve_mem, equalizerSieve_mem, equalizerSieve_apply, equalizerSieve_eq_top_iff, CategoryTheory.Sieve.equalizer_eq_equalizerSieve

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
equalizerSieve_apply 📖	mathematical	—	CategoryTheory.Sieve.arrows Opposite.unop equalizerSieve CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Opposite.op DFunLike.coe CategoryTheory.ConcreteCategory.hom CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct	—	—
equalizerSieve_eq_top_iff 📖	mathematical	—	equalizerSieve Top.top CategoryTheory.Sieve Opposite.unop OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice CategoryTheory.Sieve.instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	CategoryTheory.Functor.map_id CategoryTheory.id_apply equalizerSieve_self_eq_top
equalizerSieve_mem 📖	mathematical	DFunLike.coe CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.ConcreteCategory.hom CategoryTheory.NatTrans.app	CategoryTheory.Sieve Opposite.unop Set Set.instMembership CategoryTheory.GrothendieckTopology CategoryTheory.GrothendieckTopology.instDFunLikeSetSieve equalizerSieve	—	IsLocallyInjective.equalizerSieve_mem
equalizerSieve_mem_of_equalizerSieve_app_mem 📖	—	CategoryTheory.Sieve Opposite.unop Set Set.instMembership DFunLike.coe CategoryTheory.GrothendieckTopology CategoryTheory.GrothendieckTopology.instDFunLikeSetSieve equalizerSieve CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.ConcreteCategory.hom CategoryTheory.NatTrans.app	—	—	isLocallyInjective_iff_equalizerSieve_mem_imp
equalizerSieve_self_eq_top 📖	mathematical	—	equalizerSieve Top.top CategoryTheory.Sieve Opposite.unop OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice CategoryTheory.Sieve.instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	CategoryTheory.Sieve.ext
instIsLocallyInjectiveHomιOpposite 📖	mathematical	—	IsLocallyInjective 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.ι	—	isLocallyInjective_of_injective
instIsLocallyInjectiveOfIsIsoFunctorOpposite 📖	mathematical	—	IsLocallyInjective	—	isLocallyInjective_of_injective Function.Bijective.injective CategoryTheory.isIso_iff_bijective CategoryTheory.Functor.map_isIso CategoryTheory.NatIso.isIso_app_of_isIso
isLocallyInjective_comp 📖	mathematical	—	IsLocallyInjective CategoryTheory.CategoryStruct.comp CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category	—	equalizerSieve_mem_of_equalizerSieve_app_mem equalizerSieve_mem CategoryTheory.comp_apply
isLocallyInjective_comp_iff 📖	mathematical	—	IsLocallyInjective CategoryTheory.CategoryStruct.comp CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category	—	isLocallyInjective_iff_of_fac
isLocallyInjective_forget 📖	mathematical	—	IsLocallyInjective 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	—	equalizerSieve_mem
isLocallyInjective_forget_iff 📖	mathematical	—	IsLocallyInjective 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	—	equalizerSieve_mem isLocallyInjective_forget
isLocallyInjective_iff_equalizerSieve_mem_imp 📖	mathematical	—	IsLocallyInjective CategoryTheory.Sieve Opposite.unop Set Set.instMembership DFunLike.coe CategoryTheory.GrothendieckTopology CategoryTheory.GrothendieckTopology.instDFunLikeSetSieve equalizerSieve	—	CategoryTheory.GrothendieckTopology.superset_covering CategoryTheory.Functor.map_comp CategoryTheory.comp_apply CategoryTheory.GrothendieckTopology.transitive CategoryTheory.Sieve.le_pullback_bind equalizerSieve_mem CategoryTheory.NatTrans.naturality_apply equalizerSieve_self_eq_top
isLocallyInjective_iff_injective_of_separated 📖	mathematical	CategoryTheory.Presieve.IsSeparated CategoryTheory.Functor.comp Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.forget	IsLocallyInjective CategoryTheory.Functor.obj DFunLike.coe CategoryTheory.ConcreteCategory.hom CategoryTheory.NatTrans.app	—	CategoryTheory.Presieve.IsSeparatedFor.ext equalizerSieve_mem isLocallyInjective_of_injective
isLocallyInjective_iff_of_fac 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category	IsLocallyInjective	—	isLocallyInjective_of_isLocallyInjective_fac isLocallyInjective_comp
isLocallyInjective_of_injective 📖	mathematical	CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite DFunLike.coe CategoryTheory.ConcreteCategory.hom CategoryTheory.NatTrans.app	IsLocallyInjective	—	CategoryTheory.Sieve.ext CategoryTheory.NatTrans.naturality_apply CategoryTheory.GrothendieckTopology.top_mem
isLocallyInjective_of_isLocallyInjective 📖	mathematical	—	IsLocallyInjective	—	equalizerSieve_mem CategoryTheory.comp_apply
isLocallyInjective_of_isLocallyInjective_fac 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category	IsLocallyInjective	—	isLocallyInjective_of_isLocallyInjective
isLocallyInjective_toPlus 📖	mathematical	—	IsLocallyInjective 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.eq_mk_iff_exists CategoryTheory.Functor.instPreservesColimitsOfShapeOfIsLeftAdjoint CategoryTheory.Functor.isLeftAdjoint_of_isEquivalence CategoryTheory.Types.instIsEquivalenceForgetTypeHom CategoryTheory.GrothendieckTopology.superset_covering
isLocallyInjective_toSheafify 📖	mathematical	—	IsLocallyInjective 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 isLocallyInjective_comp isLocallyInjective_toPlus
isLocallyInjective_toSheafify' 📖	mathematical	—	IsLocallyInjective CategoryTheory.sheafify CategoryTheory.toSheafify	—	isLocallyInjective_forget_iff CategoryTheory.sheafToPresheaf_isRightAdjoint CategoryTheory.Functor.corepresentable_preservesLimitsOfShape CategoryTheory.Types.instIsCorepresentableForgetTypeHom CategoryTheory.Limits.Types.hasLimit UnivLE.small UnivLE.self CategoryTheory.Limits.Types.hasColimitsOfShape Opposite.small CategoryTheory.Functor.instPreservesColimitsOfShapeOfIsLeftAdjoint CategoryTheory.Functor.isLeftAdjoint_of_isEquivalence CategoryTheory.Types.instIsEquivalenceForgetTypeHom CategoryTheory.reflectsIsomorphisms_of_full_and_faithful CategoryTheory.Types.instFullForgetTypeHom CategoryTheory.instFaithfulForget CategoryTheory.sheafComposeIso_hom_fac CategoryTheory.toSheafify_plusPlusIsoSheafify_hom isLocallyInjective_comp isLocallyInjective_toSheafify instIsLocallyInjectiveOfIsIsoFunctorOpposite CategoryTheory.Iso.isIso_hom

CategoryTheory.Presheaf.IsLocallyInjective

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
equalizerSieve_mem 📖	mathematical	DFunLike.coe CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.ConcreteCategory.hom CategoryTheory.NatTrans.app	CategoryTheory.Sieve Opposite.unop Set Set.instMembership CategoryTheory.GrothendieckTopology CategoryTheory.GrothendieckTopology.instDFunLikeSetSieve CategoryTheory.Presheaf.equalizerSieve	—	—

CategoryTheory.Sheaf

Definitions

Name	Category	Theorems
IsLocallyInjective 📖	MathDef	9 math math: CategoryTheory.Presheaf.isLocallyInjective_presheafToSheaf_map_iff, isLocallyInjective_iff_injective, isLocallyInjective_forget, instIsLocallyInjectiveAppArrowPLocallySurjectiveLocallyInjectiveFunctorialLocallySurjectiveInjectiveFactorization, AlgebraicGeometry.Scheme.LocalRepresentability.instIsLocallyInjectiveHomYonedaGluedToSheaf, isLocallyInjective_sheafToPresheaf_map_iff, isLocallyInjective_of_iso, isLocallyBijective_iff_isIso, instIsLocallyInjectiveHomImageι

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsLocallyInjectiveHomImageι 📖	mathematical	—	IsLocallyInjective CategoryTheory.types Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Types.instFunLike CategoryTheory.Types.instConcreteCategory image imageι	—	CategoryTheory.Presheaf.instIsLocallyInjectiveHomιOpposite
isLocallyInjective_forget 📖	mathematical	—	IsLocallyInjective 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.isLocallyInjective_forget
isLocallyInjective_iff_injective 📖	mathematical	—	IsLocallyInjective CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite val DFunLike.coe CategoryTheory.ConcreteCategory.hom CategoryTheory.NatTrans.app Hom.val	—	CategoryTheory.Presheaf.isLocallyInjective_iff_injective_of_separated CategoryTheory.Presieve.IsSheaf.isSeparated CategoryTheory.isSheaf_iff_isSheaf_of_type cond
isLocallyInjective_of_iso 📖	mathematical	—	IsLocallyInjective	—	CategoryTheory.Presheaf.instIsLocallyInjectiveOfIsIsoFunctorOpposite CategoryTheory.Functor.map_isIso
isLocallyInjective_sheafToPresheaf_map_iff 📖	mathematical	—	CategoryTheory.Presheaf.IsLocallyInjective CategoryTheory.Functor.obj CategoryTheory.Sheaf instCategorySheaf CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.sheafToPresheaf CategoryTheory.Functor.map IsLocallyInjective	—	—
mono_of_injective 📖	mathematical	CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite val DFunLike.coe CategoryTheory.ConcreteCategory.hom CategoryTheory.NatTrans.app Hom.val	CategoryTheory.Mono CategoryTheory.Sheaf instCategorySheaf	—	CategoryTheory.ConcreteCategory.mono_of_injective CategoryTheory.Functor.mono_of_mono_map CategoryTheory.reflectsMonomorphisms_of_reflectsLimitsOfShape CategoryTheory.Limits.ReflectsFiniteLimits.reflects CategoryTheory.Limits.instReflectsFiniteLimitsOfReflectsLimits CategoryTheory.Limits.fullyFaithful_reflectsLimits CategoryTheory.instFullSheafFunctorOppositeSheafToPresheaf CategoryTheory.instFaithfulSheafFunctorOppositeSheafToPresheaf CategoryTheory.NatTrans.mono_of_mono_app
mono_of_isLocallyInjective 📖	mathematical	—	CategoryTheory.Mono CategoryTheory.Sheaf instCategorySheaf	—	mono_of_injective isLocallyInjective_iff_injective

---

← Back to Index