Documentation Verification Report

Basic

📁 Source: Mathlib/CategoryTheory/RegularCategory/Basic.lean

Statistics

Metric	Count
Definitions `frobeniusMorphism`, `frobeniusStrongEpiMonoFactorisation`, `regularEpiOfExtremalEpi`, `strongEpiMonoFactorisation`	4
Theorems `exists_inf_pullback_eq_exists_inf`, `frobeniusMorphism_isPullback`, `frobeniusStrongEpiMonoFactorisation_I`, `frobeniusStrongEpiMonoFactorisation_e`, `frobeniusStrongEpiMonoFactorisation_m`, `hasCoequalizer_of_isKernelPair`, `hasStrongEpiMonoFactorisations`, `instHasCoequalizerFstSnd`, `instIsRegularEpiEStrongEpiMonoFactorisation`, `instIsRegularEpiFrobeniusMorphism`, `instMonoDesc`, `isRegularEpi_of_extremalEpi`, `regularEpiIsStableUnderBaseChange`, `toHasFiniteLimits`, `instIsRegularEpiFst`, `instIsRegularEpiSnd`, `instPreregular`	17
Total	21

CategoryTheory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsRegularEpiFst` 📖	mathematical	—	`IsRegularEpi` `Limits.pullback` `Limits.pullback.fst`	—	`MorphismProperty.IsStableUnderBaseChange.of_isPullback` `Regular.regularEpiIsStableUnderBaseChange` `IsPullback.flip` `IsPullback.of_hasPullback`
`instIsRegularEpiSnd` 📖	mathematical	—	`IsRegularEpi` `Limits.pullback` `Limits.pullback.snd`	—	`MorphismProperty.IsStableUnderBaseChange.of_isPullback` `Regular.regularEpiIsStableUnderBaseChange` `IsPullback.of_hasPullback`
`instPreregular` 📖	mathematical	—	`Preregular`	—	`Limits.hasLimitOfHasLimitsOfShape` `Limits.hasLimitsOfShape_widePullbackShape` `Finite.of_fintype` `Limits.hasFiniteWidePullbacks_of_hasFiniteLimits` `Regular.toHasFiniteLimits` `instEffectiveEpiOfIsRegularEpi` `instIsRegularEpiSnd` `isRegularEpi_of_EffectiveEpi` `Limits.pullback.condition`

CategoryTheory.Regular

Definitions

Name	Category	Theorems
`frobeniusMorphism` 📖	CompOp	3 math math: `instIsRegularEpiFrobeniusMorphism`, `frobeniusStrongEpiMonoFactorisation_e`, `frobeniusMorphism_isPullback`
`frobeniusStrongEpiMonoFactorisation` 📖	CompOp	3 math math: `frobeniusStrongEpiMonoFactorisation_I`, `frobeniusStrongEpiMonoFactorisation_e`, `frobeniusStrongEpiMonoFactorisation_m`
`regularEpiOfExtremalEpi` 📖	CompOp	—
`strongEpiMonoFactorisation` 📖	CompOp	1 math math: `instIsRegularEpiEStrongEpiMonoFactorisation`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_inf_pullback_eq_exists_inf` 📖	mathematical	—	`CategoryTheory.Functor.obj` `CategoryTheory.Subobject` `Preorder.smallCategory` `PartialOrder.toPreorder` `CategoryTheory.instPartialOrderSubobject` `CategoryTheory.Subobject.exists` `CategoryTheory.Limits.hasImages_of_hasStrongEpiMonoFactorisations` `hasStrongEpiMonoFactorisations` `SemilatticeInf.toMin` `CategoryTheory.Subobject.semilatticeInf` `CategoryTheory.Limits.hasLimitsOfShape_widePullbackShape` `CategoryTheory.Limits.WalkingPair` `Finite.of_fintype` `CategoryTheory.Limits.fintypeWalkingPair` `CategoryTheory.Limits.hasFiniteWidePullbacks_of_hasFiniteLimits` `toHasFiniteLimits` `CategoryTheory.Subobject.pullback`	—	`CategoryTheory.Subobject.eq_of_comm` `CategoryTheory.Limits.hasImages_of_hasStrongEpiMonoFactorisations` `hasStrongEpiMonoFactorisations` `CategoryTheory.Limits.hasLimitsOfShape_widePullbackShape` `Finite.of_fintype` `CategoryTheory.Limits.hasFiniteWidePullbacks_of_hasFiniteLimits` `toHasFiniteLimits` `CategoryTheory.Limits.IsImage.isoExt_hom_m`
`frobeniusMorphism_isPullback` 📖	mathematical	—	`CategoryTheory.IsPullback` `CategoryTheory.Functor.obj` `CategoryTheory.Subobject` `Preorder.smallCategory` `PartialOrder.toPreorder` `CategoryTheory.instPartialOrderSubobject` `CategoryTheory.Subobject.underlying` `SemilatticeInf.toMin` `CategoryTheory.Subobject.semilatticeInf` `CategoryTheory.Limits.hasLimitsOfShape_widePullbackShape` `CategoryTheory.Limits.WalkingPair` `Finite.of_fintype` `CategoryTheory.Limits.fintypeWalkingPair` `CategoryTheory.Limits.hasFiniteWidePullbacks_of_hasFiniteLimits` `toHasFiniteLimits` `CategoryTheory.Subobject.pullback` `CategoryTheory.Subobject.exists` `CategoryTheory.Limits.hasImages_of_hasStrongEpiMonoFactorisations` `hasStrongEpiMonoFactorisations` `frobeniusMorphism` `CategoryTheory.Subobject.ofLE` `CategoryTheory.Subobject.inf_le_left` `CategoryTheory.Limits.MonoFactorisation.e` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Subobject.arrow` `CategoryTheory.Limits.ImageFactorisation.F` `CategoryTheory.Subobject.imageFactorisation`	—	`CategoryTheory.Limits.hasLimitsOfShape_widePullbackShape` `Finite.of_fintype` `CategoryTheory.Limits.hasFiniteWidePullbacks_of_hasFiniteLimits` `toHasFiniteLimits` `CategoryTheory.Limits.hasImages_of_hasStrongEpiMonoFactorisations` `hasStrongEpiMonoFactorisations` `CategoryTheory.Subobject.inf_le_left` `CategoryTheory.IsPullback.of_right` `CategoryTheory.IsPullback.lift_snd` `CategoryTheory.IsPullback.flip` `CategoryTheory.Subobject.inf_isPullback` `CategoryTheory.IsPullback.lift_fst` `CategoryTheory.Limits.MonoFactorisation.fac` `CategoryTheory.IsPullback.paste_horiz_iff` `CategoryTheory.Subobject.isPullback` `CategoryTheory.Subobject.ofLE_arrow`
`frobeniusStrongEpiMonoFactorisation_I` 📖	mathematical	—	`CategoryTheory.Limits.MonoFactorisation.I` `CategoryTheory.Functor.obj` `CategoryTheory.Subobject` `Preorder.smallCategory` `PartialOrder.toPreorder` `CategoryTheory.instPartialOrderSubobject` `CategoryTheory.Subobject.underlying` `SemilatticeInf.toMin` `CategoryTheory.Subobject.semilatticeInf` `CategoryTheory.Limits.hasLimitsOfShape_widePullbackShape` `CategoryTheory.Limits.WalkingPair` `Finite.of_fintype` `CategoryTheory.Limits.fintypeWalkingPair` `CategoryTheory.Limits.hasFiniteWidePullbacks_of_hasFiniteLimits` `toHasFiniteLimits` `CategoryTheory.Subobject.pullback` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Subobject.arrow` `CategoryTheory.Limits.StrongEpiMonoFactorisation.toMonoFactorisation` `frobeniusStrongEpiMonoFactorisation` `CategoryTheory.Subobject.exists`	—	`CategoryTheory.Limits.hasLimitsOfShape_widePullbackShape` `Finite.of_fintype` `CategoryTheory.Limits.hasFiniteWidePullbacks_of_hasFiniteLimits` `toHasFiniteLimits`
`frobeniusStrongEpiMonoFactorisation_e` 📖	mathematical	—	`CategoryTheory.Limits.MonoFactorisation.e` `CategoryTheory.Functor.obj` `CategoryTheory.Subobject` `Preorder.smallCategory` `PartialOrder.toPreorder` `CategoryTheory.instPartialOrderSubobject` `CategoryTheory.Subobject.underlying` `SemilatticeInf.toMin` `CategoryTheory.Subobject.semilatticeInf` `CategoryTheory.Limits.hasLimitsOfShape_widePullbackShape` `CategoryTheory.Limits.WalkingPair` `Finite.of_fintype` `CategoryTheory.Limits.fintypeWalkingPair` `CategoryTheory.Limits.hasFiniteWidePullbacks_of_hasFiniteLimits` `toHasFiniteLimits` `CategoryTheory.Subobject.pullback` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Subobject.arrow` `CategoryTheory.Limits.StrongEpiMonoFactorisation.toMonoFactorisation` `frobeniusStrongEpiMonoFactorisation` `frobeniusMorphism`	—	`CategoryTheory.Limits.hasLimitsOfShape_widePullbackShape` `Finite.of_fintype` `CategoryTheory.Limits.hasFiniteWidePullbacks_of_hasFiniteLimits` `toHasFiniteLimits` `CategoryTheory.Limits.hasImages_of_hasStrongEpiMonoFactorisations` `hasStrongEpiMonoFactorisations`
`frobeniusStrongEpiMonoFactorisation_m` 📖	mathematical	—	`CategoryTheory.Limits.MonoFactorisation.m` `CategoryTheory.Functor.obj` `CategoryTheory.Subobject` `Preorder.smallCategory` `PartialOrder.toPreorder` `CategoryTheory.instPartialOrderSubobject` `CategoryTheory.Subobject.underlying` `SemilatticeInf.toMin` `CategoryTheory.Subobject.semilatticeInf` `CategoryTheory.Limits.hasLimitsOfShape_widePullbackShape` `CategoryTheory.Limits.WalkingPair` `Finite.of_fintype` `CategoryTheory.Limits.fintypeWalkingPair` `CategoryTheory.Limits.hasFiniteWidePullbacks_of_hasFiniteLimits` `toHasFiniteLimits` `CategoryTheory.Subobject.pullback` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Subobject.arrow` `CategoryTheory.Limits.StrongEpiMonoFactorisation.toMonoFactorisation` `frobeniusStrongEpiMonoFactorisation` `CategoryTheory.Subobject.exists`	—	`CategoryTheory.Limits.hasLimitsOfShape_widePullbackShape` `Finite.of_fintype` `CategoryTheory.Limits.hasFiniteWidePullbacks_of_hasFiniteLimits` `toHasFiniteLimits`
`hasCoequalizer_of_isKernelPair` 📖	mathematical	`CategoryTheory.IsKernelPair`	`CategoryTheory.Limits.HasCoequalizer`	—	—
`hasStrongEpiMonoFactorisations` 📖	mathematical	—	`CategoryTheory.Limits.HasStrongEpiMonoFactorisations`	—	—
`instHasCoequalizerFstSnd` 📖	mathematical	—	`CategoryTheory.Limits.HasCoequalizer` `CategoryTheory.Limits.pullback` `CategoryTheory.Limits.hasLimitOfHasLimitsOfShape` `CategoryTheory.Limits.WalkingCospan` `CategoryTheory.Limits.WidePullbackShape.category` `CategoryTheory.Limits.WalkingPair` `CategoryTheory.Limits.hasLimitsOfShape_widePullbackShape` `Finite.of_fintype` `CategoryTheory.Limits.fintypeWalkingPair` `CategoryTheory.Limits.hasFiniteWidePullbacks_of_hasFiniteLimits` `toHasFiniteLimits` `CategoryTheory.Limits.cospan` `CategoryTheory.Limits.pullback.fst` `CategoryTheory.Limits.pullback.snd`	—	`hasCoequalizer_of_isKernelPair` `CategoryTheory.Limits.hasLimitOfHasLimitsOfShape` `CategoryTheory.Limits.hasLimitsOfShape_widePullbackShape` `Finite.of_fintype` `CategoryTheory.Limits.hasFiniteWidePullbacks_of_hasFiniteLimits` `toHasFiniteLimits` `CategoryTheory.IsKernelPair.of_hasPullback`
`instIsRegularEpiEStrongEpiMonoFactorisation` 📖	mathematical	—	`CategoryTheory.IsRegularEpi` `CategoryTheory.Limits.MonoFactorisation.I` `CategoryTheory.Limits.StrongEpiMonoFactorisation.toMonoFactorisation` `strongEpiMonoFactorisation` `CategoryTheory.Limits.MonoFactorisation.e`	—	`instHasCoequalizerFstSnd` `CategoryTheory.instIsRegularEpiπ`
`instIsRegularEpiFrobeniusMorphism` 📖	mathematical	—	`CategoryTheory.IsRegularEpi` `CategoryTheory.Functor.obj` `CategoryTheory.Subobject` `Preorder.smallCategory` `PartialOrder.toPreorder` `CategoryTheory.instPartialOrderSubobject` `CategoryTheory.Subobject.underlying` `SemilatticeInf.toMin` `CategoryTheory.Subobject.semilatticeInf` `CategoryTheory.Limits.hasLimitsOfShape_widePullbackShape` `CategoryTheory.Limits.WalkingPair` `Finite.of_fintype` `CategoryTheory.Limits.fintypeWalkingPair` `CategoryTheory.Limits.hasFiniteWidePullbacks_of_hasFiniteLimits` `toHasFiniteLimits` `CategoryTheory.Subobject.pullback` `CategoryTheory.Subobject.exists` `CategoryTheory.Limits.hasImages_of_hasStrongEpiMonoFactorisations` `hasStrongEpiMonoFactorisations` `frobeniusMorphism`	—	`CategoryTheory.MorphismProperty.IsStableUnderBaseChange.of_isPullback` `regularEpiIsStableUnderBaseChange` `CategoryTheory.Limits.hasLimitsOfShape_widePullbackShape` `Finite.of_fintype` `CategoryTheory.Limits.hasFiniteWidePullbacks_of_hasFiniteLimits` `toHasFiniteLimits` `CategoryTheory.Limits.hasImages_of_hasStrongEpiMonoFactorisations` `hasStrongEpiMonoFactorisations` `CategoryTheory.Subobject.inf_le_left` `CategoryTheory.IsPullback.flip` `frobeniusMorphism_isPullback` `CategoryTheory.Limits.strongEpi_of_strongEpiMonoFactorisation` `isRegularEpi_of_extremalEpi` `CategoryTheory.instExtremalEpiOfStrongEpi`
`instMonoDesc` 📖	mathematical	—	`CategoryTheory.Mono` `CategoryTheory.Limits.coequalizer` `CategoryTheory.Limits.pullback` `CategoryTheory.Limits.hasLimitOfHasLimitsOfShape` `CategoryTheory.Limits.WalkingCospan` `CategoryTheory.Limits.WidePullbackShape.category` `CategoryTheory.Limits.WalkingPair` `CategoryTheory.Limits.hasLimitsOfShape_widePullbackShape` `Finite.of_fintype` `CategoryTheory.Limits.fintypeWalkingPair` `CategoryTheory.Limits.hasFiniteWidePullbacks_of_hasFiniteLimits` `toHasFiniteLimits` `CategoryTheory.Limits.cospan` `CategoryTheory.Limits.pullback.fst` `CategoryTheory.Limits.pullback.snd` `instHasCoequalizerFstSnd` `CategoryTheory.Limits.coequalizer.desc` `CategoryTheory.Limits.pullback.condition`	—	`CategoryTheory.IsKernelPair.mono_of_eq_fst_snd` `CategoryTheory.Limits.hasLimitOfHasLimitsOfShape` `CategoryTheory.Limits.hasLimitsOfShape_widePullbackShape` `Finite.of_fintype` `CategoryTheory.Limits.hasFiniteWidePullbacks_of_hasFiniteLimits` `toHasFiniteLimits` `instHasCoequalizerFstSnd` `CategoryTheory.Limits.pullback.condition` `CategoryTheory.IsKernelPair.of_hasPullback` `CategoryTheory.Category.assoc` `CategoryTheory.Limits.colimit.ι_desc` `CategoryTheory.IsPullback.instHasPullbackFst` `CategoryTheory.Limits.limit.lift_π` `CategoryTheory.IsPullback.of_right` `CategoryTheory.IsPullback.of_bot` `CategoryTheory.IsPullback.of_hasPullback` `CategoryTheory.Limits.limit.lift_π_assoc` `CategoryTheory.IsPullback.paste_horiz` `CategoryTheory.MorphismProperty.IsStableUnderBaseChange.of_isPullback` `regularEpiIsStableUnderBaseChange` `CategoryTheory.IsPullback.flip` `CategoryTheory.instIsRegularEpiFst` `CategoryTheory.instIsRegularEpiπ` `CategoryTheory.cancel_epi` `CategoryTheory.epi_comp` `CategoryTheory.epi_of_effectiveEpi` `CategoryTheory.instEffectiveEpiOfEffectiveEpiFamily` `CategoryTheory.instEffectiveEpiFamily` `CategoryTheory.instEffectiveEpiOfIsRegularEpi` `CategoryTheory.instIsRegularEpiSnd` `CategoryTheory.Limits.coequalizer.condition`
`isRegularEpi_of_extremalEpi` 📖	mathematical	—	`CategoryTheory.IsRegularEpi`	—	—
`regularEpiIsStableUnderBaseChange` 📖	mathematical	—	`CategoryTheory.MorphismProperty.IsStableUnderBaseChange` `CategoryTheory.MorphismProperty.regularEpi`	—	—
`toHasFiniteLimits` 📖	mathematical	—	`CategoryTheory.Limits.HasFiniteLimits`	—	—

---

← Back to Index