Documentation Verification Report

ExtremalEpi

📁 Source: Mathlib/CategoryTheory/ExtremalEpi.lean

Statistics

Metric	Count
Definitions `ExtremalEpi`	1
Theorems `isIso`, `mk_of_hasEqualizers`, `subobject_eq_top`, `toEpi`, `extremalEpi_iff_strongEpi_of_hasPullbacks`, `instExtremalEpiOfStrongEpi`	6
Total	7

CategoryTheory

Definitions

Name	Category	Theorems
`ExtremalEpi` 📖	CompData	5 math math: `instExtremalEpiOfStrongEpi`, `ObjectProperty.isStrongGenerator_iff_exists_extremalEpi`, `extremalEpi_iff_strongEpi_of_hasPullbacks`, `ObjectProperty.IsStrongGenerator.extremalEpi_coproductFrom`, `ExtremalEpi.mk_of_hasEqualizers`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`extremalEpi_iff_strongEpi_of_hasPullbacks` 📖	mathematical	—	`ExtremalEpi` `StrongEpi`	—	`ExtremalEpi.toEpi` `Limits.hasLimitOfHasLimitsOfShape` `ExtremalEpi.isIso` `CommSq.w` `Limits.limit.lift_π` `Limits.pullback.snd_of_mono` `cancel_mono` `Category.assoc` `cancel_epi` `instExtremalEpiOfStrongEpi` `strongEpi_of_isIso` `IsIso.hom_inv_id_assoc` `Limits.pullback.condition` `IsIso.inv_hom_id_assoc`
`instExtremalEpiOfStrongEpi` 📖	mathematical	—	`ExtremalEpi`	—	`epi_of_strongEpi` `Category.comp_id` `sq_hasLift_of_hasLiftingProperty` `StrongEpi.llp` `cancel_mono` `Category.assoc` `CommSq.fac_right` `Category.id_comp`

CategoryTheory.ExtremalEpi

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isIso` 📖	mathematical	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct`	`CategoryTheory.IsIso`	—	—
`mk_of_hasEqualizers` 📖	mathematical	`CategoryTheory.IsIso`	`CategoryTheory.ExtremalEpi`	—	`CategoryTheory.Limits.hasLimitOfHasLimitsOfShape` `CategoryTheory.Limits.limit.lift_π` `CategoryTheory.Limits.equalizer.ι_mono` `CategoryTheory.cancel_epi` `CategoryTheory.epi_of_strongEpi` `CategoryTheory.strongEpi_of_isIso` `CategoryTheory.Limits.equalizer.condition`
`subobject_eq_top` 📖	mathematical	`CategoryTheory.Subobject.Factors`	`Top.top` `CategoryTheory.Subobject` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `CategoryTheory.instPartialOrderSubobject` `CategoryTheory.Subobject.orderTop`	—	`CategoryTheory.Subobject.isIso_arrow_iff_eq_top` `isIso` `CategoryTheory.Subobject.factorThru_arrow` `CategoryTheory.Subobject.arrow_mono`
`toEpi` 📖	mathematical	—	`CategoryTheory.Epi`	—	—

---

← Back to Index