RegularMono

📁 Source: Mathlib/CategoryTheory/Limits/Shapes/RegularMono.lean

Statistics

Metric	Count
Definitions `isColimitCoforkOfIsPullback`, `IsRegularEpi`, `desc`, `getStruct`, `isColimit`, `left`, `right`, `IsRegularEpiCategory`, `IsRegularMono`, `Z`, `getStruct`, `isLimit`, `left`, `right`, `IsRegularMonoCategory`, `regularEpi`, `regularMono`, `desc'`, `isColimit`, `left`, `ofArrowIso`, `ofIso`, `ofSplitEpi`, `op`, `right`, `unop`, `RegularMono`, `Z`, `equalizer`, `isLimit`, `left`, `lift'`, `ofArrowIso`, `ofIsSplitMono`, `ofIso`, `op`, `right`, `unop`, `coequalizerRegular`, `effectiveEpiStructOfRegularEpi`, `isColimitCoforkOfEffectiveEpi`, `regularEpiOfEffectiveEpi`, `regularEpiOfEpi`, `regularEpiOfIsRegularEpi`, `regularEpiOfKernelPair`, `regularMonoOfIsRegularMono`, `regularMonoOfMono`, `regularOfIsPullbackFstOfRegular`, `regularOfIsPullbackSndOfRegular`, `regularOfIsPushoutFstOfRegular`, `regularOfIsPushoutSndOfRegular`	51
Theorems `fac`, `fac_assoc`, `of_epi_of_exists`, `regularEpi`, `uniq`, `w`, `regularEpiOfEpi`, `fac`, `fac_assoc`, `regularMono`, `uniq`, `w`, `regularMonoOfMono`, `containsIdentities`, `respectsIso`, `regularEpi_iff`, `containsIdentities`, `respectsIso`, `regularMono_iff`, `effectiveEpi`, `epi`, `w`, `w_assoc`, `mono`, `strongMono`, `w`, `w_assoc`, `effectiveEpiOfKernelPair`, `effectiveEpi_of_kernelPair`, `instEffectiveEpiOfIsRegularEpi`, `instIsRegularEpiOfIsSplitEpi`, `instIsRegularEpiOppositeOpOfIsRegularMono`, `instIsRegularEpiUnopOfIsRegularMonoOpposite`, `instIsRegularEpiπ`, `instIsRegularMonoOfIsSplitMono`, `instIsRegularMonoOppositeOpOfIsRegularEpi`, `instIsRegularMonoUnopOfIsRegularEpiOpposite`, `instIsRegularMonoι`, `instStrongMonoOfIsRegularMono`, `isIso_of_regularEpi_of_mono`, `isIso_of_regularMono_of_epi`, `isRegularEpi_iff_effectiveEpi`, `isRegularEpi_of_EffectiveEpi`, `isRegularEpi_of_regularEpi`, `isRegularEpi_op_iff_isRegularMono`, `isRegularEpi_unop_iff_isRegularMono`, `isRegularMono_of_regularMono`, `isRegularMono_op_iff_isRegularEpi`, `isRegularMono_unop_iff_isRegularEpi`, `regularEpiCategoryOfSplitEpiCategory`, `regularMonoCategoryOfSplitMonoCategory`, `strongEpiCategory_of_regularEpiCategory`, `strongEpi_of_regularEpi`, `strongMonoCategory_of_regularMonoCategory`	54
Total	105

CategoryTheory

Definitions

Name	Category	Theorems
`IsRegularEpi` 📖	CompData	22 math math: `instIsRegularEpiOppositeOpOfIsRegularMono`, `Regular.isRegularEpi_of_extremalEpi`, `isRegularEpi_of_regularEpi`, `instIsRegularEpiOfIsSplitEpi`, `isRegularEpi_of_EffectiveEpi`, `instIsRegularEpiOfNormalEpi`, `isRegularEpi_unop_iff_isRegularMono`, `IsRegularEpi.of_epi_of_exists`, `isRegularEpi_iff_effectiveEpi`, `Regular.instIsRegularEpiFrobeniusMorphism`, `AlgebraicGeometry.isRegularEpi_of_flat_of_surjective_of_isAffine`, `instIsRegularEpiSnd`, `IsRegularEpiCategory.regularEpiOfEpi`, `CommRingCat.Opposite.regularEpiOfFaithfullyFlat`, `isRegularMono_op_iff_isRegularEpi`, `MorphismProperty.regularEpi_iff`, `instIsRegularEpiFst`, `Regular.instIsRegularEpiEStrongEpiMonoFactorisation`, `instIsRegularEpiUnopOfIsRegularMonoOpposite`, `isRegularMono_unop_iff_isRegularEpi`, `isRegularEpi_op_iff_isRegularMono`, `instIsRegularEpiπ`
`IsRegularEpiCategory` 📖	CompData	8 math math: `instIsRegularEpiCategoryLightCondSet`, `instIsRegularEpiCategoryCondensedSet`, `regularEpiCategoryOfNormalEpiCategory`, `isRegularEpiCategory_sheaf`, `regularEpiCategoryOfSplitEpiCategory`, `Functor.instIsRegularEpiCategoryOfForallEpiHasPullbackOfHasPushouts`, `instIsRegularEpiCategorySheafTypeOfHasSheafify`, `SSet.instIsRegularEpiCategory`
`IsRegularMono` 📖	CompData	14 math math: `isRegularMono_of_regularMono`, `CommRingCat.isRegularMono_of_faithfullyFlat`, `instIsRegularMonoι`, `instIsRegularMonoOfIsSplitMono`, `IsRegularMonoCategory.regularMonoOfMono`, `instIsRegularMonoUnopOfIsRegularEpiOpposite`, `isRegularEpi_unop_iff_isRegularMono`, `instIsRegularMonoOppositeOpOfIsRegularEpi`, `HasSubobjectClassifier.instIsRegularMonoTruth`, `isRegularMono_op_iff_isRegularEpi`, `MorphismProperty.regularMono_iff`, `instIsRegularMonoOfNormalMono`, `isRegularMono_unop_iff_isRegularEpi`, `isRegularEpi_op_iff_isRegularMono`
`IsRegularMonoCategory` 📖	CompData	5 math math: `HasSubobjectClassifier.isRegularMonoCategory`, `regularMonoCategoryOfSplitMonoCategory`, `HasClassifier.isRegularMonoCategory`, `regularMonoCategoryOfNormalMonoCategory`, `Adhesive.toRegularMonoCategory`
`RegularMono` 📖	CompData	1 math math: `IsRegularMono.regularMono`
`coequalizerRegular` 📖	CompOp	—
`effectiveEpiStructOfRegularEpi` 📖	CompOp	—
`isColimitCoforkOfEffectiveEpi` 📖	CompOp	—
`regularEpiOfEffectiveEpi` 📖	CompOp	—
`regularEpiOfEpi` 📖	CompOp	—
`regularEpiOfIsRegularEpi` 📖	CompOp	—
`regularEpiOfKernelPair` 📖	CompOp	—
`regularMonoOfIsRegularMono` 📖	CompOp	—
`regularMonoOfMono` 📖	CompOp	—
`regularOfIsPullbackFstOfRegular` 📖	CompOp	—
`regularOfIsPullbackSndOfRegular` 📖	CompOp	—
`regularOfIsPushoutFstOfRegular` 📖	CompOp	—
`regularOfIsPushoutSndOfRegular` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`effectiveEpiOfKernelPair` 📖	mathematical	—	`EffectiveEpi`	—	`effectiveEpi_of_kernelPair`
`effectiveEpi_of_kernelPair` 📖	mathematical	—	`EffectiveEpi`	—	`Limits.pullback.condition` `RegularEpi.effectiveEpi`
`instEffectiveEpiOfIsRegularEpi` 📖	mathematical	—	`EffectiveEpi`	—	`RegularEpi.effectiveEpi`
`instIsRegularEpiOfIsSplitEpi` 📖	mathematical	—	`IsRegularEpi`	—	`isRegularEpi_of_regularEpi`
`instIsRegularEpiOppositeOpOfIsRegularMono` 📖	mathematical	—	`IsRegularEpi` `Opposite` `Category.opposite` `Opposite.op` `Quiver.Hom.op` `CategoryStruct.toQuiver` `Category.toCategoryStruct`	—	—
`instIsRegularEpiUnopOfIsRegularMonoOpposite` 📖	mathematical	—	`IsRegularEpi` `Opposite.unop` `Quiver.Hom.unop` `CategoryStruct.toQuiver` `Category.toCategoryStruct`	—	—
`instIsRegularEpiπ` 📖	mathematical	—	`IsRegularEpi` `Limits.coequalizer` `Limits.coequalizer.π`	—	—
`instIsRegularMonoOfIsSplitMono` 📖	mathematical	—	`IsRegularMono`	—	`isRegularMono_of_regularMono`
`instIsRegularMonoOppositeOpOfIsRegularEpi` 📖	mathematical	—	`IsRegularMono` `Opposite` `Category.opposite` `Opposite.op` `Quiver.Hom.op` `CategoryStruct.toQuiver` `Category.toCategoryStruct`	—	—
`instIsRegularMonoUnopOfIsRegularEpiOpposite` 📖	mathematical	—	`IsRegularMono` `Opposite.unop` `Quiver.Hom.unop` `CategoryStruct.toQuiver` `Category.toCategoryStruct`	—	—
`instIsRegularMonoι` 📖	mathematical	—	`IsRegularMono` `Limits.equalizer` `Limits.equalizer.ι`	—	`isRegularMono_of_regularMono`
`instStrongMonoOfIsRegularMono` 📖	mathematical	—	`StrongMono`	—	`RegularMono.strongMono`
`isIso_of_regularEpi_of_mono` 📖	mathematical	—	`IsIso`	—	`isRegularEpi_of_regularEpi` `isIso_of_mono_of_strongEpi` `strongEpi_of_effectiveEpi` `instEffectiveEpiOfIsRegularEpi`
`isIso_of_regularMono_of_epi` 📖	mathematical	—	`IsIso`	—	`RegularMono.strongMono` `isIso_of_epi_of_strongMono`
`isRegularEpi_iff_effectiveEpi` 📖	mathematical	—	`IsRegularEpi` `EffectiveEpi`	—	`instEffectiveEpiOfIsRegularEpi` `isRegularEpi_of_EffectiveEpi`
`isRegularEpi_of_EffectiveEpi` 📖	mathematical	—	`IsRegularEpi`	—	`isRegularEpi_of_regularEpi`
`isRegularEpi_of_regularEpi` 📖	mathematical	—	`IsRegularEpi`	—	—
`isRegularEpi_op_iff_isRegularMono` 📖	mathematical	—	`IsRegularEpi` `Opposite` `Category.opposite` `Opposite.op` `Quiver.Hom.op` `CategoryStruct.toQuiver` `Category.toCategoryStruct` `IsRegularMono`	—	`IsRegularEpi.regularEpi` `IsRegularMono.regularMono`
`isRegularEpi_unop_iff_isRegularMono` 📖	mathematical	—	`IsRegularEpi` `Opposite.unop` `Quiver.Hom.unop` `CategoryStruct.toQuiver` `Category.toCategoryStruct` `IsRegularMono` `Opposite` `Category.opposite`	—	`IsRegularEpi.regularEpi` `IsRegularMono.regularMono`
`isRegularMono_of_regularMono` 📖	mathematical	—	`IsRegularMono`	—	—
`isRegularMono_op_iff_isRegularEpi` 📖	mathematical	—	`IsRegularMono` `Opposite` `Category.opposite` `Opposite.op` `Quiver.Hom.op` `CategoryStruct.toQuiver` `Category.toCategoryStruct` `IsRegularEpi`	—	`IsRegularMono.regularMono` `IsRegularEpi.regularEpi`
`isRegularMono_unop_iff_isRegularEpi` 📖	mathematical	—	`IsRegularMono` `Opposite.unop` `Quiver.Hom.unop` `CategoryStruct.toQuiver` `Category.toCategoryStruct` `IsRegularEpi` `Opposite` `Category.opposite`	—	`IsRegularMono.regularMono` `IsRegularEpi.regularEpi`
`regularEpiCategoryOfSplitEpiCategory` 📖	mathematical	—	`IsRegularEpiCategory`	—	`instIsRegularEpiOfIsSplitEpi` `isSplitEpi_of_epi`
`regularMonoCategoryOfSplitMonoCategory` 📖	mathematical	—	`IsRegularMonoCategory`	—	`isRegularMono_of_regularMono` `isSplitMono_of_mono`
`strongEpiCategory_of_regularEpiCategory` 📖	mathematical	—	`StrongEpiCategory`	—	`strongEpi_of_effectiveEpi` `instEffectiveEpiOfIsRegularEpi` `isRegularEpi_of_regularEpi`
`strongEpi_of_regularEpi` 📖	mathematical	—	`StrongEpi`	—	`isRegularEpi_of_regularEpi` `strongEpi_of_effectiveEpi` `instEffectiveEpiOfIsRegularEpi`
`strongMonoCategory_of_regularMonoCategory` 📖	mathematical	—	`StrongMonoCategory`	—	`RegularMono.strongMono`

CategoryTheory.EffectiveEpiStruct

Definitions

Name	Category	Theorems
`isColimitCoforkOfIsPullback` 📖	CompOp	—

CategoryTheory.IsRegularEpi

Definitions

Name	Category	Theorems
`desc` 📖	CompOp	3 math math: `uniq`, `fac`, `fac_assoc`
`getStruct` 📖	CompOp	—
`isColimit` 📖	CompOp	—
`left` 📖	CompOp	1 math math: `w`
`right` 📖	CompOp	1 math math: `w`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`fac` 📖	mathematical	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `W` `left` `right`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `desc`	—	`CategoryTheory.Limits.Cofork.IsColimit.π_desc` `w`
`fac_assoc` 📖	mathematical	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `W` `left` `right`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `desc`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `fac`
`of_epi_of_exists` 📖	mathematical	`Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.CategoryStruct.comp`	`CategoryTheory.IsRegularEpi`	—	`CategoryTheory.Limits.pullback.condition` `CategoryTheory.cancel_epi` `CategoryTheory.Limits.Cofork.condition`
`regularEpi` 📖	mathematical	—	`CategoryTheory.RegularEpi`	—	—
`uniq` 📖	mathematical	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `W` `left` `right`	`desc`	—	`ExistsUnique.unique` `w` `CategoryTheory.Limits.Cofork.IsColimit.existsUnique` `fac`
`w` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `W` `left` `right`	—	`CategoryTheory.RegularEpi.w`

CategoryTheory.IsRegularEpiCategory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`regularEpiOfEpi` 📖	mathematical	—	`CategoryTheory.IsRegularEpi`	—	—

CategoryTheory.IsRegularMono

Definitions

Name	Category	Theorems
`Z` 📖	CompOp	1 math math: `w`
`getStruct` 📖	CompOp	—
`isLimit` 📖	CompOp	—
`left` 📖	CompOp	1 math math: `w`
`right` 📖	CompOp	1 math math: `w`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`fac` 📖	mathematical	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `Z` `left` `right`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `lift`	—	`CategoryTheory.Limits.Fork.IsLimit.lift_ι` `w`
`fac_assoc` 📖	mathematical	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `Z` `left` `right`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `lift`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `fac`
`regularMono` 📖	mathematical	—	`CategoryTheory.RegularMono`	—	—
`uniq` 📖	mathematical	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `Z` `left` `right`	`lift`	—	`ExistsUnique.unique` `w` `CategoryTheory.Limits.Fork.IsLimit.existsUnique` `fac`
`w` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `Z` `left` `right`	—	`CategoryTheory.RegularMono.w`

CategoryTheory.IsRegularMonoCategory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`regularMonoOfMono` 📖	mathematical	—	`CategoryTheory.IsRegularMono`	—	—

CategoryTheory.MorphismProperty

Definitions

Name	Category	Theorems
`regularEpi` 📖	CompOp	4 math math: `regularEpi.containsIdentities`, `CategoryTheory.Regular.regularEpiIsStableUnderBaseChange`, `regularEpi.respectsIso`, `regularEpi_iff`
`regularMono` 📖	CompOp	3 math math: `regularMono.containsIdentities`, `regularMono_iff`, `regularMono.respectsIso`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`regularEpi_iff` 📖	mathematical	—	`regularEpi` `CategoryTheory.IsRegularEpi`	—	—
`regularMono_iff` 📖	mathematical	—	`regularMono` `CategoryTheory.IsRegularMono`	—	—

CategoryTheory.MorphismProperty.regularEpi

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`containsIdentities` 📖	mathematical	—	`CategoryTheory.MorphismProperty.ContainsIdentities` `CategoryTheory.MorphismProperty.regularEpi`	—	—
`respectsIso` 📖	mathematical	—	`CategoryTheory.MorphismProperty.RespectsIso` `CategoryTheory.MorphismProperty.regularEpi`	—	`CategoryTheory.MorphismProperty.RespectsIso.of_respects_arrow_iso` `CategoryTheory.IsRegularEpi.regularEpi`

CategoryTheory.MorphismProperty.regularMono

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`containsIdentities` 📖	mathematical	—	`CategoryTheory.MorphismProperty.ContainsIdentities` `CategoryTheory.MorphismProperty.regularMono`	—	—
`respectsIso` 📖	mathematical	—	`CategoryTheory.MorphismProperty.RespectsIso` `CategoryTheory.MorphismProperty.regularMono`	—	`CategoryTheory.MorphismProperty.RespectsIso.of_respects_arrow_iso` `CategoryTheory.IsRegularMono.regularMono`

CategoryTheory.RegularEpi

Definitions

Name	Category	Theorems
`desc'` 📖	CompOp	—
`isColimit` 📖	CompOp	—
`left` 📖	CompOp	2 math math: `w`, `w_assoc`
`ofArrowIso` 📖	CompOp	—
`ofIso` 📖	CompOp	—
`ofSplitEpi` 📖	CompOp	—
`op` 📖	CompOp	—
`right` 📖	CompOp	2 math math: `w`, `w_assoc`
`unop` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`effectiveEpi` 📖	mathematical	—	`CategoryTheory.EffectiveEpi`	—	—
`epi` 📖	mathematical	—	`CategoryTheory.Epi`	—	`CategoryTheory.Limits.epi_of_isColimit_cofork` `w`
`w` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `W` `left` `right`	—	—
`w_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `W` `left` `right`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `w`

CategoryTheory.RegularMono

Definitions

Name	Category	Theorems
`Z` 📖	CompOp	2 math math: `w_assoc`, `w`
`equalizer` 📖	CompOp	—
`isLimit` 📖	CompOp	—
`left` 📖	CompOp	2 math math: `w_assoc`, `w`
`lift'` 📖	CompOp	—
`ofArrowIso` 📖	CompOp	—
`ofIsSplitMono` 📖	CompOp	—
`ofIso` 📖	CompOp	—
`op` 📖	CompOp	—
`right` 📖	CompOp	2 math math: `w_assoc`, `w`
`unop` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mono` 📖	mathematical	—	`CategoryTheory.Mono`	—	`CategoryTheory.Limits.mono_of_isLimit_fork` `w`
`strongMono` 📖	mathematical	—	`CategoryTheory.StrongMono`	—	`mono` `CategoryTheory.StrongMono.mk'` `CategoryTheory.cancel_epi` `CategoryTheory.Category.assoc` `CategoryTheory.eq_whisker` `CategoryTheory.CommSq.w` `w` `CategoryTheory.CommSq.HasLift.mk'` `CategoryTheory.cancel_mono`
`w` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `Z` `left` `right`	—	—
`w_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `Z` `left` `right`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `w`

---

← Back to Index