Conservative

📁 Source: Mathlib/CategoryTheory/Sites/Point/Conservative.lean

Statistics

Metric	Count
Definitions HasEnoughPoints, IsConservativeFamilyOfPoints	2
Theorems exists_objectProperty, W_iff, jointlyFaithful, jointlyReflectEpimorphisms, jointlyReflectIsomorphisms, jointlyReflectIsomorphisms_type, jointlyReflectMonomorphisms, jointly_reflect_isLocallySurjective, jointly_reflect_ofArrows_mem, jointly_reflect_ofArrows_mem_of_small, mk'	11
Total	13

CategoryTheory.GrothendieckTopology

Definitions

Name	Category	Theorems
HasEnoughPoints 📖	CompData	3 math math: instHasEnoughPointsOverOverOfWEqualsLocallyBijectiveHomOfHasSheafifyType, Opens.instHasEnoughPointsOpensGrothendieckTopology, instHasEnoughPointsBot

CategoryTheory.GrothendieckTopology.HasEnoughPoints

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_objectProperty 📖	mathematical	—	CategoryTheory.ObjectProperty CategoryTheory.GrothendieckTopology.Point CategoryTheory.Category.toCategoryStruct CategoryTheory.GrothendieckTopology.Point.instCategory CategoryTheory.ObjectProperty.Small CategoryTheory.ObjectProperty.IsConservativeFamilyOfPoints	—	—

CategoryTheory.ObjectProperty

Definitions

Name	Category	Theorems
IsConservativeFamilyOfPoints 📖	CompData	5 math math: CategoryTheory.GrothendieckTopology.HasEnoughPoints.exists_objectProperty, IsConservativeFamilyOfPoints.over, Opens.isConservativeFamilyOfPoints_pointsGrothendieckTopology, CategoryTheory.GrothendieckTopology.isConservative_pointsBot, IsConservativeFamilyOfPoints.mk'

CategoryTheory.ObjectProperty.IsConservativeFamilyOfPoints

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
W_iff 📖	mathematical	CategoryTheory.ObjectProperty.IsConservativeFamilyOfPoints CategoryTheory.Limits.HasProducts	CategoryTheory.GrothendieckTopology.W CategoryTheory.IsIso CategoryTheory.Functor.obj CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.GrothendieckTopology.Point.presheafFiber CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.GrothendieckTopology.Point CategoryTheory.GrothendieckTopology.Point.instCategory CategoryTheory.Functor.map	—	CategoryTheory.GrothendieckTopology.W_iff CategoryTheory.JointlyReflectIsomorphisms.isIso_iff jointlyReflectIsomorphisms CategoryTheory.MorphismProperty.arrow_mk_iso_iff CategoryTheory.MorphismProperty.RespectsIso.isomorphisms
jointlyFaithful 📖	mathematical	CategoryTheory.ObjectProperty.IsConservativeFamilyOfPoints	CategoryTheory.JointlyFaithful CategoryTheory.Sheaf CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf CategoryTheory.ObjectProperty.FullSubcategory CategoryTheory.GrothendieckTopology.Point CategoryTheory.GrothendieckTopology.Point.instCategory CategoryTheory.GrothendieckTopology.Point.sheafFiber CategoryTheory.ObjectProperty.FullSubcategory.obj	—	CategoryTheory.Limits.hasFilteredColimitsOfSize_of_hasColimitsOfSize CategoryTheory.JointlyReflectIsomorphisms.jointlyFaithful jointlyReflectIsomorphisms CategoryTheory.Limits.PreservesFiniteLimits.preservesFiniteLimits CategoryTheory.GrothendieckTopology.Point.instPreservesFiniteLimitsSheafSheafFiberOfLocallySmallOfHasFiniteLimitsOfAB5OfSize CategoryTheory.Sheaf.instHasLimitsOfShape CategoryTheory.Limits.hasLimitsOfShape_of_hasFiniteLimits
jointlyReflectEpimorphisms 📖	mathematical	CategoryTheory.ObjectProperty.IsConservativeFamilyOfPoints CategoryTheory.Limits.HasProducts	CategoryTheory.JointlyReflectEpimorphisms CategoryTheory.Sheaf CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf CategoryTheory.ObjectProperty.FullSubcategory CategoryTheory.GrothendieckTopology.Point CategoryTheory.GrothendieckTopology.Point.instCategory CategoryTheory.GrothendieckTopology.Point.sheafFiber CategoryTheory.ObjectProperty.FullSubcategory.obj	—	CategoryTheory.JointlyReflectIsomorphisms.jointlyReflectEpimorphisms jointlyReflectIsomorphisms CategoryTheory.Functor.instPreservesColimitsOfShapeOfIsLeftAdjoint CategoryTheory.GrothendieckTopology.Point.instIsLeftAdjointSheafSheafFiber CategoryTheory.Sheaf.instHasColimitsOfShape CategoryTheory.Limits.hasPushouts_of_hasWidePushouts CategoryTheory.Limits.hasColimitsOfShapeOfHasColimitsOfSize
jointlyReflectIsomorphisms 📖	mathematical	CategoryTheory.ObjectProperty.IsConservativeFamilyOfPoints	CategoryTheory.JointlyReflectIsomorphisms CategoryTheory.Sheaf CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf CategoryTheory.ObjectProperty.FullSubcategory CategoryTheory.GrothendieckTopology.Point CategoryTheory.GrothendieckTopology.Point.instCategory CategoryTheory.GrothendieckTopology.Point.sheafFiber CategoryTheory.ObjectProperty.FullSubcategory.obj	—	CategoryTheory.isIso_iff_of_reflects_iso CategoryTheory.instReflectsIsomorphismsSheafSheafCompose CategoryTheory.Limits.Types.hasColimitsOfSize UnivLE.self CategoryTheory.JointlyReflectIsomorphisms.isIso_iff jointlyReflectIsomorphisms_type CategoryTheory.MorphismProperty.arrow_mk_iso_iff CategoryTheory.MorphismProperty.RespectsIso.isomorphisms
jointlyReflectIsomorphisms_type 📖	mathematical	CategoryTheory.ObjectProperty.IsConservativeFamilyOfPoints	CategoryTheory.JointlyReflectIsomorphisms CategoryTheory.Sheaf CategoryTheory.types CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf CategoryTheory.ObjectProperty.FullSubcategory CategoryTheory.GrothendieckTopology.Point CategoryTheory.GrothendieckTopology.Point.instCategory CategoryTheory.GrothendieckTopology.Point.sheafFiber CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Limits.Types.hasColimitsOfSize UnivLE.self	—	—
jointlyReflectMonomorphisms 📖	mathematical	CategoryTheory.ObjectProperty.IsConservativeFamilyOfPoints	CategoryTheory.JointlyReflectMonomorphisms CategoryTheory.Sheaf CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf CategoryTheory.ObjectProperty.FullSubcategory CategoryTheory.GrothendieckTopology.Point CategoryTheory.GrothendieckTopology.Point.instCategory CategoryTheory.GrothendieckTopology.Point.sheafFiber CategoryTheory.ObjectProperty.FullSubcategory.obj	—	CategoryTheory.Limits.hasFilteredColimitsOfSize_of_hasColimitsOfSize CategoryTheory.JointlyReflectIsomorphisms.jointlyReflectMonomorphisms jointlyReflectIsomorphisms CategoryTheory.Limits.PreservesFiniteLimits.preservesFiniteLimits CategoryTheory.GrothendieckTopology.Point.instPreservesFiniteLimitsSheafSheafFiberOfLocallySmallOfHasFiniteLimitsOfAB5OfSize CategoryTheory.Limits.hasLimitsOfShape_widePullbackShape Finite.of_fintype CategoryTheory.Limits.hasFiniteWidePullbacks_of_hasFiniteLimits CategoryTheory.Sheaf.instHasFiniteLimits
jointly_reflect_isLocallySurjective 📖	mathematical	CategoryTheory.ObjectProperty.IsConservativeFamilyOfPoints CategoryTheory.Functor.obj CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.GrothendieckTopology.Point.presheafFiber CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.GrothendieckTopology.Point CategoryTheory.GrothendieckTopology.Point.instCategory DFunLike.coe CategoryTheory.ConcreteCategory.hom CategoryTheory.Functor.map	CategoryTheory.Presheaf.IsLocallySurjective	—	CategoryTheory.Presheaf.isLocallySurjective_iff_whisker_forget CategoryTheory.instHasWeakSheafifyOfHasSheafify CategoryTheory.Presheaf.isLocallySurjective_presheafToSheaf_map_iff CategoryTheory.Sheaf.isLocallySurjective_iff_epi CategoryTheory.Limits.Types.hasColimitsOfSize UnivLE.self CategoryTheory.JointlyReflectEpimorphisms.epi_iff jointlyReflectEpimorphisms CategoryTheory.reflectsIsomorphisms_of_full_and_faithful CategoryTheory.Types.instFullForgetTypeHom CategoryTheory.instFaithfulForget CategoryTheory.Limits.PreservesColimits.preservesFilteredColimits CategoryTheory.Types.instPreservesColimitsOfSizeForgetTypeHom CategoryTheory.hasSheafCompose_of_preservesMulticospan CategoryTheory.Functor.corepresentable_preservesLimit CategoryTheory.Types.instIsCorepresentableForgetTypeHom CategoryTheory.Limits.Types.instHasProductsType CategoryTheory.preservesEpimorphisms_of_preservesColimitsOfShape CategoryTheory.Functor.instPreservesColimitsOfShapeOfIsLeftAdjoint CategoryTheory.GrothendieckTopology.Point.instIsLeftAdjointSheafSheafFiber CategoryTheory.MorphismProperty.arrow_mk_iso_iff CategoryTheory.MorphismProperty.RespectsIso.epimorphisms
jointly_reflect_ofArrows_mem 📖	mathematical	CategoryTheory.ObjectProperty.IsConservativeFamilyOfPoints	CategoryTheory.Sieve Set Set.instMembership DFunLike.coe CategoryTheory.GrothendieckTopology CategoryTheory.GrothendieckTopology.instDFunLikeSetSieve CategoryTheory.Sieve.ofArrows CategoryTheory.Functor.obj CategoryTheory.types CategoryTheory.GrothendieckTopology.Point.fiber CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.GrothendieckTopology.Point CategoryTheory.GrothendieckTopology.Point.instCategory CategoryTheory.Functor.map	—	CategoryTheory.GrothendieckTopology.Point.jointly_surjective CategoryTheory.FunctorToTypes.map_comp_apply CategoryTheory.Limits.functorCategoryHasColimit CategoryTheory.Limits.Types.hasColimit CategoryTheory.instSmallDiscrete CategoryTheory.GrothendieckTopology.ofArrows_mem_iff_isLocallySurjective_sigmaDesc_shrinkYoneda_map jointly_reflect_isLocallySurjective CategoryTheory.Limits.Types.hasColimitsOfSize UnivLE.self CategoryTheory.Limits.PreservesColimits.preservesFilteredColimits CategoryTheory.Types.instPreservesColimitsOfSizeForgetTypeHom Equiv.surjective CategoryTheory.NatTrans.naturality CategoryTheory.Limits.Sigma.ι_desc CategoryTheory.Functor.map_comp
jointly_reflect_ofArrows_mem_of_small 📖	mathematical	CategoryTheory.ObjectProperty.IsConservativeFamilyOfPoints	CategoryTheory.Sieve Set Set.instMembership DFunLike.coe CategoryTheory.GrothendieckTopology CategoryTheory.GrothendieckTopology.instDFunLikeSetSieve CategoryTheory.Sieve.ofArrows CategoryTheory.Functor.obj CategoryTheory.types CategoryTheory.GrothendieckTopology.Point.fiber CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.GrothendieckTopology.Point CategoryTheory.GrothendieckTopology.Point.instCategory CategoryTheory.Functor.map	—	CategoryTheory.GrothendieckTopology.Point.jointly_surjective CategoryTheory.FunctorToTypes.map_comp_apply CategoryTheory.GrothendieckTopology.superset_covering CategoryTheory.Sieve.generate_le_iff CategoryTheory.Presieve.ofArrows_le_iff jointly_reflect_ofArrows_mem small_sigma CategoryTheory.ObjectProperty.instSmallFullSubcategoryOfSmall UnivLE.small UnivLE.self
mk' 📖	mathematical	CategoryTheory.Sieve Set Set.instMembership DFunLike.coe CategoryTheory.GrothendieckTopology CategoryTheory.GrothendieckTopology.instDFunLikeSetSieve	CategoryTheory.ObjectProperty.IsConservativeFamilyOfPoints	—	CategoryTheory.JointlyFaithful.jointlyReflectsIsomorphisms CategoryTheory.Limits.Types.hasColimitsOfSize UnivLE.self CategoryTheory.SheafOfTypes.balanced CategoryTheory.JointlyFaithful.of_jointly_reflects_isIso_of_mono CategoryTheory.Sheaf.instHasLimitsOfShape CategoryTheory.Limits.Types.hasLimitsOfShape UnivLE.small univLE_of_max CategoryTheory.Limits.PreservesFiniteLimits.preservesFiniteLimits CategoryTheory.GrothendieckTopology.Point.instPreservesFiniteLimitsSheafSheafFiberOfLocallySmallOfHasFiniteLimitsOfAB5OfSize CategoryTheory.Limits.hasFiniteLimits_of_hasCountableLimits CategoryTheory.Limits.hasCountableLimits_of_hasLimits CategoryTheory.Limits.Types.hasLimitsOfSize CategoryTheory.Limits.instAB5Type CategoryTheory.Sheaf.isLocallySurjective_iff_epi CategoryTheory.instMonoFunctorOppositeHomFullSubcategoryIsSheafOfHasWeakSheafifyOfSheaf CategoryTheory.instHasWeakSheafifyOfHasSheafify CategoryTheory.isIso_iff_bijective CategoryTheory.Balanced.isIso_of_mono_of_epi

---

← Back to Index