Epi

📁 Source: Mathlib/Condensed/Epi.lean

Statistics

Metric	Count
Definitions	0
Theorems epi_iff_locallySurjective_on_compHaus, epi_iff_surjective_on_stonean, epi_iff_locallySurjective_on_compHaus, epi_iff_surjective_on_stonean, epi_iff_locallySurjective_on_compHaus, epi_iff_surjective_on_stonean	6
Total	6

Condensed

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
epi_iff_locallySurjective_on_compHaus 📖	mathematical	—	CategoryTheory.Epi Condensed instCategoryCondensed CompHaus Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CompHausLike.category DFunLike.coe CategoryTheory.ConcreteCategory.hom ContinuousMap TopCat.carrier CompHausLike.toTop TopCat.str ContinuousMap.instFunLike CompHausLike.concreteCategory CategoryTheory.ToType CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf CategoryTheory.coherentTopology Opposite.op CategoryTheory.NatTrans.app CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory CategoryTheory.Functor.map Opposite.unop	—	CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive CompHausLike.instFinitaryExtensiveOfHasExplicitPullbacksOfInclusions CompHaus.instHasExplicitFiniteCoproductsTrue CompHausLike.instHasExplicitPullbacksOfInclusionsOfHasExplicitPullbacks CompHaus.instHasExplicitPullbacksTrue CompHaus.instPreregular CategoryTheory.Sheaf.isLocallySurjective_iff_epi' CategoryTheory.coherentTopology.isLocallySurjective_iff CategoryTheory.regularTopology.isLocallySurjective_iff List.TFAE.out CompHaus.effectiveEpi_tfae
epi_iff_surjective_on_stonean 📖	mathematical	CategoryTheory.Limits.HasLimitsOfShape CategoryTheory.StructuredArrow Opposite Stonean CategoryTheory.Category.opposite CompHausLike.category ExtremallyDisconnected TopCat.carrier TopCat.str CompHaus CategoryTheory.Functor.op Stonean.toCompHaus CategoryTheory.instCategoryStructuredArrow	CategoryTheory.Epi Condensed instCategoryCondensed CategoryTheory.Functor.obj Opposite CompHaus CategoryTheory.Category.opposite CompHausLike.category CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf CategoryTheory.coherentTopology Opposite.op Stonean.compHaus DFunLike.coe CategoryTheory.ConcreteCategory.hom CategoryTheory.NatTrans.app CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory	—	CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive CompHausLike.instFinitaryExtensiveOfHasExplicitPullbacksOfInclusions Stonean.instHasExplicitFiniteCoproductsExtremallyDisconnectedCarrier Stonean.instHasExplicitPullbacksOfInclusionsExtremallyDisconnectedCarrier CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular Stonean.instPreregular CategoryTheory.Functor.epi_map_iff_epi CategoryTheory.preservesEpimorphisms_of_preservesColimitsOfShape CategoryTheory.Limits.PreservesFiniteColimits.preservesFiniteColimits CategoryTheory.Limits.PreservesColimits.preservesFiniteColimits CategoryTheory.Functor.instPreservesColimitsOfSizeOfIsLeftAdjoint CategoryTheory.Functor.isLeftAdjoint_of_isEquivalence CategoryTheory.Equivalence.isEquivalence_inverse CategoryTheory.reflectsEpimorphisms_of_reflectsColimitsOfShape CategoryTheory.Limits.ReflectsFiniteColimits.reflects CategoryTheory.Limits.instReflectsFiniteColimitsOfReflectsColimits CategoryTheory.Limits.fullyFaithful_reflectsColimits CategoryTheory.Equivalence.full_inverse CategoryTheory.Equivalence.faithful_inverse Stonean.instProjective CategoryTheory.Equivalence.isEquivalence_functor CategoryTheory.Equivalence.full_functor CategoryTheory.Equivalence.faithful_functor CategoryTheory.Sheaf.isLocallySurjective_iff_epi' CategoryTheory.extensiveTopology.isLocallySurjective_iff

CondensedMod

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
epi_iff_locallySurjective_on_compHaus 📖	mathematical	—	CategoryTheory.Epi CondensedMod instCategoryCondensed ModuleCat ModuleCat.moduleCategory CompHaus Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CompHausLike.category DFunLike.coe CategoryTheory.ConcreteCategory.hom ContinuousMap TopCat.carrier CompHausLike.toTop TopCat.str ContinuousMap.instFunLike CompHausLike.concreteCategory ModuleCat.carrier CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf CategoryTheory.coherentTopology Opposite.op LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier CategoryTheory.NatTrans.app CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory CategoryTheory.Functor.map Opposite.unop	—	Condensed.epi_iff_locallySurjective_on_compHaus CategoryTheory.ConcreteCategory.instHasFunctorialSurjectiveInjectiveFactorization CategoryTheory.Abelian.instHasStrongEpiMonoFactorisations ModuleCat.forget_preservesMonomorphisms ModuleCat.forget_preservesEpimorphisms CategoryTheory.GrothendieckTopology.instWEqualsLocallyBijectiveOfHasWeakSheafifyOfHasSheafComposeOfPreservesSheafificationOfReflectsIsomorphismsForget CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive CompHausLike.instFinitaryExtensiveOfHasExplicitPullbacksOfInclusions CompHaus.instHasExplicitFiniteCoproductsTrue CompHausLike.instHasExplicitPullbacksOfInclusionsOfHasExplicitPullbacks CompHaus.instHasExplicitPullbacksTrue CompHaus.instPreregular CategoryTheory.sheafToPresheaf_isRightAdjoint CategoryTheory.Functor.instPreservesLimitsOfShapeOfIsRightAdjoint ModuleCat.instIsRightAdjointForgetLinearMapIdCarrier ModuleCat.hasLimit small_subtype small_Pi UnivLE.small UnivLE.self ModuleCat.hasColimitsOfShape AddCommGrpCat.hasColimitsOfShape Opposite.small CategoryTheory.Limits.PreservesFilteredColimitsOfSize.preserves_filtered_colimits ModuleCat.FilteredColimits.forget_preservesFilteredColimits CategoryTheory.isFiltered_op_of_isCofiltered CategoryTheory.isCofiltered_of_directed_ge_nonempty SemilatticeInf.instIsCodirectedOrder ModuleCat.instReflectsIsomorphismsForgetLinearMapIdCarrier CategoryTheory.hasSheafCompose_of_preservesMulticospan CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit CategoryTheory.GrothendieckTopology.instPreservesSheafificationForgetOfPreservesLimitsOfHasColimitsOfShapeOfPreservesColimitsOfShapeOppositeCoverOfHasLimitsOfShapeWalkingMulticospanOfReflectsIsomorphisms ModuleCat.forget_preservesLimits CategoryTheory.Limits.hasLimitsOfShapeOfHasLimits ModuleCat.hasLimits' CategoryTheory.instHasSheafifyOfPreservesLimitsForgetOfHasFiniteLimitsOfSmallOppositeCover CategoryTheory.Abelian.hasFiniteLimits CategoryTheory.balanced_of_strongMonoCategory CategoryTheory.strongMonoCategory_of_regularMonoCategory CategoryTheory.regularMonoCategoryOfNormalMonoCategory CategoryTheory.Abelian.toIsNormalMonoCategory CategoryTheory.Limits.instPreservesFiniteProductsOfPreservesFiniteLimits CategoryTheory.Limits.PreservesLimits.preservesFiniteLimits
epi_iff_surjective_on_stonean 📖	mathematical	—	CategoryTheory.Epi CondensedMod instCategoryCondensed ModuleCat ModuleCat.moduleCategory ModuleCat.carrier CategoryTheory.Functor.obj Opposite CompHaus CategoryTheory.Category.opposite CompHausLike.category CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf CategoryTheory.coherentTopology Opposite.op Stonean.compHaus DFunLike.coe CategoryTheory.ConcreteCategory.hom LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier CategoryTheory.NatTrans.app CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory	—	CategoryTheory.Limits.hasLimitsOfSizeShrink ModuleCat.hasLimits' Condensed.epi_iff_surjective_on_stonean CategoryTheory.ConcreteCategory.instHasFunctorialSurjectiveInjectiveFactorization CategoryTheory.Abelian.instHasStrongEpiMonoFactorisations ModuleCat.forget_preservesMonomorphisms ModuleCat.forget_preservesEpimorphisms CategoryTheory.Limits.instPreservesFiniteProductsOfPreservesFiniteLimits CategoryTheory.Limits.PreservesLimits.preservesFiniteLimits ModuleCat.forget_preservesLimits CategoryTheory.Limits.hasLimitsOfShapeOfHasLimits CategoryTheory.GrothendieckTopology.instWEqualsLocallyBijectiveOfHasWeakSheafifyOfHasSheafComposeOfPreservesSheafificationOfReflectsIsomorphismsForget CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive CompHausLike.instFinitaryExtensiveOfHasExplicitPullbacksOfInclusions Stonean.instHasExplicitFiniteCoproductsExtremallyDisconnectedCarrier Stonean.instHasExplicitPullbacksOfInclusionsExtremallyDisconnectedCarrier CategoryTheory.sheafToPresheaf_isRightAdjoint CategoryTheory.Functor.instPreservesLimitsOfShapeOfIsRightAdjoint ModuleCat.instIsRightAdjointForgetLinearMapIdCarrier ModuleCat.hasLimit small_subtype small_Pi UnivLE.small UnivLE.self ModuleCat.hasColimitsOfShape AddCommGrpCat.hasColimitsOfShape Opposite.small CategoryTheory.Limits.PreservesFilteredColimitsOfSize.preserves_filtered_colimits ModuleCat.FilteredColimits.forget_preservesFilteredColimits CategoryTheory.isFiltered_op_of_isCofiltered CategoryTheory.isCofiltered_of_directed_ge_nonempty SemilatticeInf.instIsCodirectedOrder ModuleCat.instReflectsIsomorphismsForgetLinearMapIdCarrier CategoryTheory.hasSheafCompose_of_preservesMulticospan CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit CategoryTheory.GrothendieckTopology.instPreservesSheafificationForgetOfPreservesLimitsOfHasColimitsOfShapeOfPreservesColimitsOfShapeOppositeCoverOfHasLimitsOfShapeWalkingMulticospanOfReflectsIsomorphisms CategoryTheory.instHasSheafifyOfPreservesLimitsForgetOfHasFiniteLimitsOfSmallOppositeCover CategoryTheory.Abelian.hasFiniteLimits CategoryTheory.balanced_of_strongMonoCategory CategoryTheory.strongMonoCategory_of_regularMonoCategory CategoryTheory.regularMonoCategoryOfNormalMonoCategory CategoryTheory.Abelian.toIsNormalMonoCategory

CondensedSet

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
epi_iff_locallySurjective_on_compHaus 📖	mathematical	—	CategoryTheory.Epi CondensedSet instCategoryCondensed CategoryTheory.types CompHaus Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CompHausLike.category DFunLike.coe CategoryTheory.ConcreteCategory.hom ContinuousMap TopCat.carrier CompHausLike.toTop TopCat.str ContinuousMap.instFunLike CompHausLike.concreteCategory CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf CategoryTheory.coherentTopology Opposite.op CategoryTheory.NatTrans.app CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory CategoryTheory.Functor.map Opposite.unop	—	Condensed.epi_iff_locallySurjective_on_compHaus CategoryTheory.instHasFunctorialSurjectiveInjectiveFactorizationTypeHom CategoryTheory.GrothendieckTopology.instWEqualsLocallyBijectiveTypeHom CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive CompHausLike.instFinitaryExtensiveOfHasExplicitPullbacksOfInclusions CompHaus.instHasExplicitFiniteCoproductsTrue CompHausLike.instHasExplicitPullbacksOfInclusionsOfHasExplicitPullbacks CompHaus.instHasExplicitPullbacksTrue CompHaus.instPreregular CategoryTheory.instHasSheafifyType CategoryTheory.hasSheafCompose_of_preservesMulticospan CategoryTheory.Functor.corepresentable_preservesLimit CategoryTheory.Types.instIsCorepresentableForgetTypeHom CategoryTheory.SheafOfTypes.balanced CategoryTheory.Limits.instPreservesFiniteProductsOfPreservesFiniteLimits CategoryTheory.Limits.PreservesLimits.preservesFiniteLimits CategoryTheory.Types.instPreservesLimitsOfSizeForgetTypeHom
epi_iff_surjective_on_stonean 📖	mathematical	—	CategoryTheory.Epi CondensedSet instCategoryCondensed CategoryTheory.types CategoryTheory.Functor.obj Opposite CompHaus CategoryTheory.Category.opposite CompHausLike.category CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf CategoryTheory.coherentTopology Opposite.op Stonean.compHaus CategoryTheory.NatTrans.app CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory	—	Condensed.epi_iff_surjective_on_stonean CategoryTheory.instHasFunctorialSurjectiveInjectiveFactorizationTypeHom CategoryTheory.Limits.instPreservesFiniteProductsOfPreservesFiniteLimits CategoryTheory.Limits.PreservesLimits.preservesFiniteLimits CategoryTheory.Types.instPreservesLimitsOfSizeForgetTypeHom CategoryTheory.Limits.Types.hasLimitsOfShape UnivLE.small UnivLE.self CategoryTheory.GrothendieckTopology.instWEqualsLocallyBijectiveTypeHom CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive CompHausLike.instFinitaryExtensiveOfHasExplicitPullbacksOfInclusions Stonean.instHasExplicitFiniteCoproductsExtremallyDisconnectedCarrier Stonean.instHasExplicitPullbacksOfInclusionsExtremallyDisconnectedCarrier CategoryTheory.instHasSheafifyType CategoryTheory.hasSheafCompose_of_preservesMulticospan CategoryTheory.Functor.corepresentable_preservesLimit CategoryTheory.Types.instIsCorepresentableForgetTypeHom CategoryTheory.SheafOfTypes.balanced

---

← Back to Index