RegularEpi

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

Statistics

Metric	Count
Definitions RegularEpi	1
Theorems instIsRegularEpiCategorySheafTypeOfHasSheafify, isRegularEpiCategory_sheaf	2
Total	3

CategoryTheory

Definitions

Name	Category	Theorems
RegularEpi 📖	CompData	1 math math: IsRegularEpi.regularEpi

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsRegularEpiCategorySheafTypeOfHasSheafify 📖	mathematical	—	IsRegularEpiCategory Sheaf types Sheaf.instCategorySheaf	—	isRegularEpiCategory_sheaf Limits.Types.instHasPullbacksType Limits.hasColimitsOfShape_widePushoutShape Finite.of_fintype Limits.hasFiniteWidePushouts_of_has_finite_limits Limits.hasFiniteColimits_of_hasColimits Limits.Types.hasColimitsOfSize UnivLE.self regularEpiCategoryOfSplitEpiCategory instSplitEpiCategoryType Limits.HasImages.has_image FunctorToTypes.instHasImagesFunctorType Limits.instEpiFactorThruImageOfHasLimitWalkingParallelPairParallelPair Limits.functorCategoryHasLimit Limits.Types.hasLimit UnivLE.small univLE_of_max Limits.instMonoι Limits.image.fac SheafOfTypes.balanced
isRegularEpiCategory_sheaf 📖	mathematical	Epi Functor Opposite Category.opposite Functor.category Sheaf.val Mono CategoryStruct.comp Category.toCategoryStruct Sheaf.Hom.val	IsRegularEpiCategory Sheaf Sheaf.instCategorySheaf	—	instHasWeakSheafifyOfHasSheafify isIso_sheafificationAdjunction_counit Adjunction.counit_naturality Category.assoc IsIso.inv_hom_id Category.comp_id IsIso.inv_hom_id_assoc epi_comp Sheaf.Hom.epi_of_presheaf_epi epi_of_effectiveEpi IsSplitEpi.EffectiveEpi IsSplitEpi.of_iso instIsIsoFunctorOppositeValAppSheafCounitSheafificationAdjunction IsIso.inv_isIso epi_of_epi Functor.map_comp Balanced.isIso_of_mono_of_epi Functor.map_mono preservesMonomorphisms_of_preservesLimitsOfShape Limits.PreservesFiniteLimits.preservesFiniteLimits instPreservesFiniteLimitsFunctorOppositeSheafPresheafToSheaf isRegularEpi_iff_effectiveEpi Limits.hasPullbackHorizPaste Limits.hasPullbackVertPaste Limits.has_kernel_pair_of_mono instMonoAppOfFunctor Sheaf.instHasLimitsOfShape mono_of_strongMono instStrongMonoOfIsRegularMono instIsRegularMonoOfIsSplitMono IsSplitMono.of_iso sheafification_reflective Limits.hasLimitOfHasLimitsOfShape IsPullback.instHasPullbackFst Presieve.instHasPullbackOfHasPairwisePullbacksOfArrows Presieve.instHasPairwisePullbacksOfHasPullbacks cancel_mono Limits.pullback.condition IsRegularEpiCategory.regularEpiOfEpi Functor.instIsRegularEpiCategoryOfForallEpiHasPullbackOfHasPushouts Limits.PullbackCone.condition Limits.PreservesColimitsOfShape.preservesColimit Limits.PreservesFiniteColimits.preservesFiniteColimits Limits.PreservesColimits.preservesFiniteColimits Functor.instPreservesColimitsOfSizeOfIsLeftAdjoint instIsLeftAdjointFunctorOppositeSheafPresheafToSheaf instEffectiveEpiOfIsRegularEpi preservesLimit_of_createsLimit_and_hasLimit Limits.functorCategoryHasLimit instEffectiveEpiOfEffectiveEpiFamily instEffectiveEpiFamilyComp instEffectiveEpiFamily instEffectiveEpiFamilyCompOfIsSplitEpi

---

← Back to Index