LocallySurjective

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

Statistics

Metric	Count
Definitions	0
Theorems isLocallySurjective_iff, presheafIsLocallySurjective_iff, isLocallySurjective_iff, presheafIsLocallySurjective_iff, surjective_of_isLocallySurjective_sheaf_of_types, isLocallySurjective_iff, isLocallySurjective_sheaf_of_types	7
Total	7

CategoryTheory.coherentTopology

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isLocallySurjective_iff 📖	mathematical	—	CategoryTheory.Sheaf.IsLocallySurjective CategoryTheory.coherentTopology CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive CategoryTheory.Presheaf.IsLocallySurjective CategoryTheory.regularTopology CategoryTheory.Sheaf.val CategoryTheory.Sheaf.Hom.val	—	CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive presheafIsLocallySurjective_iff CategoryTheory.Presheaf.instPreservesFiniteProductsOppositeVal
presheafIsLocallySurjective_iff 📖	mathematical	—	CategoryTheory.Presheaf.IsLocallySurjective CategoryTheory.coherentTopology CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular CategoryTheory.regularTopology	—	CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular CategoryTheory.Presheaf.isLocallySurjective_iff_whisker_forget CategoryTheory.regularTopology.isLocallySurjective_sheaf_of_types CategoryTheory.Limits.comp_preservesFiniteProducts CategoryTheory.Presheaf.isLocallySurjective_of_le CategoryTheory.extensive_regular_generate_coherent GaloisConnection.monotone_l GaloisInsertion.gc le_sup_right

CategoryTheory.extensiveTopology

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isLocallySurjective_iff 📖	mathematical	—	CategoryTheory.Sheaf.IsLocallySurjective CategoryTheory.extensiveTopology CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.Sheaf.val Opposite.op DFunLike.coe CategoryTheory.ConcreteCategory.hom CategoryTheory.NatTrans.app CategoryTheory.Sheaf.Hom.val	—	CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive presheafIsLocallySurjective_iff CategoryTheory.instPreservesFiniteProductsOppositeVal
presheafIsLocallySurjective_iff 📖	mathematical	—	CategoryTheory.Presheaf.IsLocallySurjective CategoryTheory.extensiveTopology CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Opposite.op DFunLike.coe CategoryTheory.ConcreteCategory.hom CategoryTheory.NatTrans.app	—	CategoryTheory.Presheaf.isLocallySurjective_iff_whisker_forget surjective_of_isLocallySurjective_sheaf_of_types CategoryTheory.Limits.comp_preservesFiniteProducts CategoryTheory.Sieve.id_mem_iff_eq_top CategoryTheory.Functor.map_id CategoryTheory.id_apply CategoryTheory.GrothendieckTopology.top_mem'
surjective_of_isLocallySurjective_sheaf_of_types 📖	mathematical	—	CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.types Opposite.op CategoryTheory.NatTrans.app	—	CategoryTheory.Presheaf.IsLocallySurjective.imageSieve_mem mem_sieves_iff_contains_colimit_cofan CategoryTheory.Functor.initial_of_isLeftAdjoint CategoryTheory.Functor.isLeftAdjoint_of_isEquivalence CategoryTheory.Equivalence.isEquivalence_inverse CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit CategoryTheory.Limits.instPreservesLimitsOfShapeDiscreteOfFiniteOfPreservesFiniteProducts CategoryTheory.Limits.Concrete.isLimit_ext CategoryTheory.Functor.corepresentable_preservesLimit CategoryTheory.Types.instIsCorepresentableForgetTypeHom CategoryTheory.NatTrans.naturality_apply CategoryTheory.Limits.IsLimit.map_π

CategoryTheory.regularTopology

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isLocallySurjective_iff 📖	mathematical	—	CategoryTheory.Presheaf.IsLocallySurjective CategoryTheory.regularTopology DFunLike.coe CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Opposite.op CategoryTheory.ConcreteCategory.hom CategoryTheory.NatTrans.app CategoryTheory.Functor.map Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Opposite.unop	—	mem_sieves_iff_hasEffectiveEpi
isLocallySurjective_sheaf_of_types 📖	mathematical	—	CategoryTheory.Presheaf.IsLocallySurjective CategoryTheory.regularTopology CategoryTheory.types Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Types.instFunLike CategoryTheory.Types.instConcreteCategory	—	CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular CategoryTheory.Presheaf.IsLocallySurjective.imageSieve_mem CategoryTheory.coherentTopology.mem_sieves_iff_hasEffectiveEpiFamily mem_sieves_iff_hasEffectiveEpi CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.hasColimitsOfShape_discrete CategoryTheory.FinitaryPreExtensive.hasFiniteCoproducts CategoryTheory.Limits.Types.hasLimit CategoryTheory.instSmallDiscrete UnivLE.small univLE_of_max UnivLE.self CategoryTheory.Limits.instHasProductOppositeOp CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit CategoryTheory.Limits.instPreservesLimitsOfShapeDiscreteOfFiniteOfPreservesFiniteProducts CategoryTheory.instEffectiveEpiDescOfEffectiveEpiFamily CategoryTheory.Limits.preservesLimitsOfShape_of_equiv CategoryTheory.Limits.Concrete.isLimit_ext CategoryTheory.Functor.corepresentable_preservesLimit CategoryTheory.Types.instIsCorepresentableForgetTypeHom CategoryTheory.NatTrans.naturality_apply CategoryTheory.FunctorToTypes.map_comp_apply CategoryTheory.Limits.opCoproductIsoProduct_inv_comp_ι CategoryTheory.Limits.piComparison_comp_π CategoryTheory.Limits.Types.productIso_hom_comp_eval CategoryTheory.inv_hom_id_apply CategoryTheory.Iso.eq_inv_comp CategoryTheory.Limits.Sigma.ι_desc

---

← Back to Index