Documentation Verification Report

RegularMono

πŸ“ Source: Mathlib/CategoryTheory/Limits/Shapes/RegularMono.lean

Statistics

MetricCount
DefinitionsisColimitCoforkOfIsPullback, IsRegularEpi, desc, getStruct, isColimit, left, right, IsRegularEpiCategory, IsRegularMono, Z, getStruct, isLimit, left, right, IsRegularMonoCategory, regularEpi, regularMono, desc', isColimit, left, ofArrowIso, ofIso, ofSplitEpi, right, RegularMono, Z, equalizer, isLimit, left, lift', ofArrowIso, ofIsSplitMono, ofIso, right, coequalizerRegular, effectiveEpiStructOfRegularEpi, isColimitCoforkOfEffectiveEpi, regularEpiOfEffectiveEpi, regularEpiOfEpi, regularEpiOfIsRegularEpi, regularEpiOfKernelPair, regularMonoOfIsRegularMono, regularMonoOfMono, regularOfIsPullbackFstOfRegular, regularOfIsPullbackSndOfRegular, regularOfIsPushoutFstOfRegular, regularOfIsPushoutSndOfRegular
47
Theoremsfac, fac_assoc, 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, instIsRegularEpiΟ€, instIsRegularMonoOfIsSplitMono, instIsRegularMonoΞΉ, instStrongMonoOfIsRegularMono, isIso_of_regularEpi_of_mono, isIso_of_regularMono_of_epi, isRegularEpi_iff_effectiveEpi, isRegularEpi_of_EffectiveEpi, isRegularEpi_of_regularEpi, isRegularMono_of_regularMono, regularEpiCategoryOfSplitEpiCategory, regularMonoCategoryOfSplitMonoCategory, strongEpiCategory_of_regularEpiCategory, strongEpi_of_regularEpi, strongMonoCategory_of_regularMonoCategory
45
Total92

CategoryTheory

Definitions

NameCategoryTheorems
IsRegularEpi πŸ“–CompData
13 mathmath: Regular.isRegularEpi_of_extremalEpi, isRegularEpi_of_regularEpi, instIsRegularEpiOfIsSplitEpi, isRegularEpi_of_EffectiveEpi, instIsRegularEpiOfNormalEpi, isRegularEpi_iff_effectiveEpi, Regular.instIsRegularEpiFrobeniusMorphism, instIsRegularEpiSnd, IsRegularEpiCategory.regularEpiOfEpi, MorphismProperty.regularEpi_iff, instIsRegularEpiFst, Regular.instIsRegularEpiEStrongEpiMonoFactorisation, instIsRegularEpiΟ€
IsRegularEpiCategory πŸ“–CompData
8 mathmath: instIsRegularEpiCategoryLightCondSet, instIsRegularEpiCategoryCondensedSet, regularEpiCategoryOfNormalEpiCategory, isRegularEpiCategory_sheaf, regularEpiCategoryOfSplitEpiCategory, Functor.instIsRegularEpiCategoryOfForallEpiHasPullbackOfHasPushouts, instIsRegularEpiCategorySheafTypeOfHasSheafify, SSet.instIsRegularEpiCategory
IsRegularMono πŸ“–CompData
7 mathmath: isRegularMono_of_regularMono, instIsRegularMonoΞΉ, instIsRegularMonoOfIsSplitMono, HasClassifier.instIsRegularMonoTruth, IsRegularMonoCategory.regularMonoOfMono, MorphismProperty.regularMono_iff, instIsRegularMonoOfNormalMono
IsRegularMonoCategory πŸ“–CompData
4 mathmath: regularMonoCategoryOfSplitMonoCategory, HasClassifier.isRegularMonoCategory, regularMonoCategoryOfNormalMonoCategory, Adhesive.toRegularMonoCategory
RegularMono πŸ“–CompData
1 mathmath: 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

NameKindAssumesProvesValidatesDepends 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
instIsRegularEpiΟ€ πŸ“–mathematicalβ€”IsRegularEpi
Limits.coequalizer
Limits.coequalizer.Ο€		β€”β€”
instIsRegularMonoOfIsSplitMono πŸ“–mathematicalβ€”IsRegularMonoβ€”isRegularMono_of_regularMono
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β€”β€”
isRegularMono_of_regularMono πŸ“–mathematicalβ€”IsRegularMonoβ€”β€”
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

NameCategoryTheorems
isColimitCoforkOfIsPullback πŸ“–CompOpβ€”

CategoryTheory.IsRegularEpi

Definitions

NameCategoryTheorems
desc πŸ“–CompOp
3 mathmath: uniq, fac, fac_assoc
getStruct πŸ“–CompOpβ€”
isColimit πŸ“–CompOpβ€”
left πŸ“–CompOp
1 mathmath: w
right πŸ“–CompOp
1 mathmath: w

Theorems

NameKindAssumesProvesValidatesDepends On
fac πŸ“–mathematicalCategoryTheory.CategoryStruct.comp
CategoryTheory.Category.toCategoryStruct
W
left
right		descβ€”CategoryTheory.Limits.Cofork.IsColimit.Ο€_desc
w
fac_assoc πŸ“–mathematicalCategoryTheory.CategoryStruct.comp
CategoryTheory.Category.toCategoryStruct
W
left
right		descβ€”CategoryTheory.Category.assoc
Mathlib.Tactic.Reassoc.eq_whisker'
fac
regularEpi πŸ“–mathematicalβ€”CategoryTheory.RegularEpiβ€”β€”
uniq πŸ“–mathematicalCategoryTheory.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

NameKindAssumesProvesValidatesDepends On
regularEpiOfEpi πŸ“–mathematicalβ€”CategoryTheory.IsRegularEpiβ€”β€”

CategoryTheory.IsRegularMono

Definitions

NameCategoryTheorems
Z πŸ“–CompOp
1 mathmath: w
getStruct πŸ“–CompOpβ€”
isLimit πŸ“–CompOpβ€”
left πŸ“–CompOp
1 mathmath: w
right πŸ“–CompOp
1 mathmath: w

Theorems

NameKindAssumesProvesValidatesDepends On
fac πŸ“–mathematicalCategoryTheory.CategoryStruct.comp
CategoryTheory.Category.toCategoryStruct
Z
left
right		liftβ€”CategoryTheory.Limits.Fork.IsLimit.lift_ΞΉ
w
fac_assoc πŸ“–mathematicalCategoryTheory.CategoryStruct.comp
CategoryTheory.Category.toCategoryStruct
Z
left
right		liftβ€”CategoryTheory.Category.assoc
Mathlib.Tactic.Reassoc.eq_whisker'
fac
regularMono πŸ“–mathematicalβ€”CategoryTheory.RegularMonoβ€”β€”
uniq πŸ“–mathematicalCategoryTheory.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

NameKindAssumesProvesValidatesDepends On
regularMonoOfMono πŸ“–mathematicalβ€”CategoryTheory.IsRegularMonoβ€”β€”

CategoryTheory.MorphismProperty

Definitions

NameCategoryTheorems
regularEpi πŸ“–CompOp
4 mathmath: regularEpi.containsIdentities, CategoryTheory.Regular.regularEpiIsStableUnderBaseChange, regularEpi.respectsIso, regularEpi_iff
regularMono πŸ“–CompOp
3 mathmath: regularMono.containsIdentities, regularMono_iff, regularMono.respectsIso

Theorems

NameKindAssumesProvesValidatesDepends On
regularEpi_iff πŸ“–mathematicalβ€”regularEpi
CategoryTheory.IsRegularEpi		β€”β€”
regularMono_iff πŸ“–mathematicalβ€”regularMono
CategoryTheory.IsRegularMono		β€”β€”

CategoryTheory.MorphismProperty.regularEpi

Theorems

NameKindAssumesProvesValidatesDepends 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

NameKindAssumesProvesValidatesDepends 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

NameCategoryTheorems
desc' πŸ“–CompOpβ€”
isColimit πŸ“–CompOpβ€”
left πŸ“–CompOp
2 mathmath: w, w_assoc
ofArrowIso πŸ“–CompOpβ€”
ofIso πŸ“–CompOpβ€”
ofSplitEpi πŸ“–CompOpβ€”
right πŸ“–CompOp
2 mathmath: w, w_assoc

Theorems

NameKindAssumesProvesValidatesDepends 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

NameCategoryTheorems
Z πŸ“–CompOp
2 mathmath: w_assoc, w
equalizer πŸ“–CompOpβ€”
isLimit πŸ“–CompOpβ€”
left πŸ“–CompOp
2 mathmath: w_assoc, w
lift' πŸ“–CompOpβ€”
ofArrowIso πŸ“–CompOpβ€”
ofIsSplitMono πŸ“–CompOpβ€”
ofIso πŸ“–CompOpβ€”
right πŸ“–CompOp
2 mathmath: w_assoc, w

Theorems

NameKindAssumesProvesValidatesDepends 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