LocallyFullyFaithful

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

Statistics

Metric	Count
Definitions IsLocallyFaithful, IsLocallyFull, imageSieve, equalizer	4
Theorems ext, functorPushforward_equalizer_mem, of_faithful, ext, functorPushforward_imageSieve_mem, of_full, functorPushforward_equalizer_mem, functorPushforward_imageSieve_mem, imageSieve_eq_imageSieve, imageSieve_map, equalizer_apply, equalizer_eq_equalizerSieve, equalizer_self	13
Total	17

CategoryTheory.Functor

Definitions

Name	Category	Theorems
IsLocallyFaithful 📖	CompData	3 math math: IsLocallyFaithful.of_faithful, IsDenseSubsite.isLocallyFaithful, IsDenseSubsite.isLocallyFaithful'
IsLocallyFull 📖	CompData	4 math math: IsLocallyFull.of_full, IsDenseSubsite.isLocallyFull, IsDenseSubsite.isLocallyFull', AlgebraicGeometry.Scheme.AffineZariskiSite.instIsLocallyFullOpensToOpensFunctorGrothendieckTopologyCarrierCarrierCommRingCat
imageSieve 📖	CompOp	5 math math: functorPushforward_imageSieve_mem, imageSieve_eq_imageSieve, IsLocallyFull.functorPushforward_imageSieve_mem, imageSieve_map, IsDenseSubsite.imageSieve_mem

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
functorPushforward_equalizer_mem 📖	mathematical	map	CategoryTheory.Sieve obj Set Set.instMembership DFunLike.coe CategoryTheory.GrothendieckTopology CategoryTheory.GrothendieckTopology.instDFunLikeSetSieve CategoryTheory.Sieve.functorPushforward CategoryTheory.Sieve.equalizer	—	IsLocallyFaithful.functorPushforward_equalizer_mem
functorPushforward_imageSieve_mem 📖	mathematical	—	CategoryTheory.Sieve obj Set Set.instMembership DFunLike.coe CategoryTheory.GrothendieckTopology CategoryTheory.GrothendieckTopology.instDFunLikeSetSieve CategoryTheory.Sieve.functorPushforward imageSieve	—	IsLocallyFull.functorPushforward_imageSieve_mem
imageSieve_eq_imageSieve 📖	mathematical	—	imageSieve CategoryTheory.Presheaf.imageSieve CategoryTheory.types Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Types.instFunLike CategoryTheory.Types.instConcreteCategory obj CategoryTheory.Functor Opposite CategoryTheory.Category.opposite category CategoryTheory.yoneda comp op CategoryTheory.yonedaMap	—	—
imageSieve_map 📖	mathematical	—	imageSieve map 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 map_comp

CategoryTheory.Functor.IsLocallyFaithful

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ext 📖	—	CategoryTheory.Functor.map Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Sheaf.val Opposite.op CategoryTheory.Functor.obj Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct	—	—	CategoryTheory.Presieve.IsSeparatedFor.ext CategoryTheory.Presieve.IsSheafFor.isSeparatedFor CategoryTheory.isSheaf_iff_isSheaf_of_type CategoryTheory.Sheaf.cond CategoryTheory.Functor.functorPushforward_equalizer_mem CategoryTheory.FunctorToTypes.map_comp_apply
functorPushforward_equalizer_mem 📖	mathematical	CategoryTheory.Functor.map	CategoryTheory.Sieve CategoryTheory.Functor.obj Set Set.instMembership DFunLike.coe CategoryTheory.GrothendieckTopology CategoryTheory.GrothendieckTopology.instDFunLikeSetSieve CategoryTheory.Sieve.functorPushforward CategoryTheory.Sieve.equalizer	—	—
of_faithful 📖	mathematical	—	CategoryTheory.Functor.IsLocallyFaithful	—	CategoryTheory.Sieve.equalizer_self CategoryTheory.Sieve.functorPushforward_top CategoryTheory.Functor.map_injective

CategoryTheory.Functor.IsLocallyFull

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ext 📖	—	CategoryTheory.Functor.map Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Sheaf.val Opposite.op CategoryTheory.Functor.obj Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct	—	—	CategoryTheory.Presieve.IsSeparatedFor.ext CategoryTheory.Presieve.IsSheafFor.isSeparatedFor CategoryTheory.isSheaf_iff_isSheaf_of_type CategoryTheory.Sheaf.cond CategoryTheory.Functor.functorPushforward_imageSieve_mem CategoryTheory.FunctorToTypes.map_comp_apply
functorPushforward_imageSieve_mem 📖	mathematical	—	CategoryTheory.Sieve CategoryTheory.Functor.obj Set Set.instMembership DFunLike.coe CategoryTheory.GrothendieckTopology CategoryTheory.GrothendieckTopology.instDFunLikeSetSieve CategoryTheory.Sieve.functorPushforward CategoryTheory.Functor.imageSieve	—	—
of_full 📖	mathematical	—	CategoryTheory.Functor.IsLocallyFull	—	CategoryTheory.Functor.map_preimage CategoryTheory.Functor.imageSieve_map CategoryTheory.Sieve.functorPushforward_top

CategoryTheory.Sieve

Definitions

Name	Category	Theorems
equalizer 📖	CompOp	6 math math: equalizer_apply, equalizer_self, CategoryTheory.Functor.functorPushforward_equalizer_mem, CategoryTheory.Functor.IsDenseSubsite.equalizer_mem, CategoryTheory.Functor.IsLocallyFaithful.functorPushforward_equalizer_mem, equalizer_eq_equalizerSieve

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
equalizer_apply 📖	mathematical	—	arrows equalizer Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.CategoryStruct.comp	—	—
equalizer_eq_equalizerSieve 📖	mathematical	—	equalizer CategoryTheory.Presheaf.equalizerSieve CategoryTheory.types Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Types.instFunLike CategoryTheory.Types.instConcreteCategory CategoryTheory.Functor.obj CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.yoneda Opposite.op	—	—
equalizer_self 📖	mathematical	—	equalizer Top.top CategoryTheory.Sieve OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	ext

---

← Back to Index