SequentialLimit

📁 Source: Mathlib/CategoryTheory/Sites/Coherent/SequentialLimit.lean

Statistics

Metric	Count
Definitions	0
Theorems epi_π_app_zero_of_epi, isLocallySurjective_π_app_zero_of_isLocallySurjective_map	2
Total	2

CategoryTheory.coherentTopology

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
epi_π_app_zero_of_epi 📖	mathematical	CategoryTheory.EffectiveEpi CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Preorder.smallCategory Nat.instPreorder Opposite.op CategoryTheory.Limits.limit CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.limit.π CategoryTheory.Epi CategoryTheory.Sheaf CategoryTheory.coherentTopology CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive CategoryTheory.types CategoryTheory.Sheaf.instCategorySheaf CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.homOfLE	CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cone.pt CategoryTheory.NatTrans.app CategoryTheory.Limits.Cone.π	—	CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive CategoryTheory.instHasFunctorialSurjectiveInjectiveFactorizationTypeHom CategoryTheory.hasSheafCompose_of_preservesMulticospan CategoryTheory.Functor.corepresentable_preservesLimit CategoryTheory.Types.instIsCorepresentableForgetTypeHom isLocallySurjective_π_app_zero_of_isLocallySurjective_map
isLocallySurjective_π_app_zero_of_isLocallySurjective_map 📖	mathematical	CategoryTheory.Sheaf.IsLocallySurjective CategoryTheory.coherentTopology CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive CategoryTheory.types Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Types.instFunLike CategoryTheory.Types.instConcreteCategory CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Preorder.smallCategory Nat.instPreorder CategoryTheory.Sheaf CategoryTheory.Sheaf.instCategorySheaf Opposite.op CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.homOfLE CategoryTheory.EffectiveEpi CategoryTheory.Limits.limit CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.limit.π	CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cone.pt CategoryTheory.NatTrans.app CategoryTheory.Limits.Cone.π	—	CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive CategoryTheory.Limits.hasLimitOfHasLimitsOfShape isLocallySurjective_iff CategoryTheory.Limits.instPreservesFiniteProductsOfPreservesFiniteLimits CategoryTheory.Limits.PreservesLimits.preservesFiniteLimits CategoryTheory.Types.instPreservesLimitsOfSizeForgetTypeHom CategoryTheory.regularTopology.isLocallySurjective_iff CategoryTheory.Functor.ofOpSequence_map_homOfLE_succ subcanonical CategoryTheory.GrothendieckTopology.yonedaEquiv_comp CategoryTheory.Limits.IsLimit.fac CategoryTheory.GrothendieckTopology.yonedaEquiv_yoneda_map

---

← Back to Index