Documentation Verification Report

StrongEpi

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

Statistics

Metric	Count
Definitions `StrongEpi`, `StrongEpiCategory`, `StrongMono`, `StrongMonoCategory`	4
Theorems `epi`, `iff_of_arrow_iso`, `llp`, `mk'`, `of_arrow_iso`, `strongEpi_of_epi`, `iff_of_arrow_iso`, `mk'`, `mono`, `of_arrow_iso`, `rlp`, `strongMono_of_mono`, `balanced_of_strongEpiCategory`, `balanced_of_strongMonoCategory`, `epi_of_strongEpi`, `isIso_of_epi_of_strongMono`, `isIso_of_mono_of_strongEpi`, `mono_of_strongMono`, `strongEpi_comp`, `strongEpi_of_epi`, `strongEpi_of_isIso`, `strongEpi_of_strongEpi`, `strongMono_comp`, `strongMono_of_isIso`, `strongMono_of_mono`, `strongMono_of_strongMono`	26
Total	30

CategoryTheory

Definitions

Name	Category	Theorems
`StrongEpi` 📖	CompData	18 math math: `strongEpi_of_epi`, `strongEpi_of_effectiveEpi`, `Limits.strongEpi_of_strongEpiMonoFactorisation`, `StrongEpi.mk'`, `Functor.strongEpi_map_iff_strongEpi_of_isEquivalence`, `StrongEpi.of_arrow_iso`, `Limits.StrongEpiMonoFactorisation.e_strong_epi`, `Limits.HasStrongEpiImages.strong_factorThruImage`, `Adjunction.strongEpi_map_of_strongEpi`, `strongEpi_of_strongEpi`, `extremalEpi_iff_strongEpi_of_hasPullbacks`, `StrongEpi.iff_of_arrow_iso`, `strongEpi_comp`, `Limits.strongEpi_factorThruImage_of_strongEpiMonoFactorisation`, `strongEpi_of_isIso`, `StrongEpiCategory.strongEpi_of_epi`, `Adjunction.strongEpi_map_of_isEquivalence`, `strongEpi_of_regularEpi`
`StrongEpiCategory` 📖	CompData	1 math math: `strongEpiCategory_of_regularEpiCategory`
`StrongMono` 📖	CompData	10 math math: `StrongMono.of_arrow_iso`, `strongMono_comp`, `RegularMono.strongMono`, `strongMono_of_strongMono`, `strongMono_of_mono`, `StrongMono.iff_of_arrow_iso`, `strongMono_of_isIso`, `StrongMono.mk'`, `StrongMonoCategory.strongMono_of_mono`, `instStrongMonoOfIsRegularMono`
`StrongMonoCategory` 📖	CompData	1 math math: `strongMonoCategory_of_regularMonoCategory`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`balanced_of_strongEpiCategory` 📖	mathematical	—	`Balanced`	—	`isIso_of_mono_of_strongEpi` `strongEpi_of_epi`
`balanced_of_strongMonoCategory` 📖	mathematical	—	`Balanced`	—	`isIso_of_epi_of_strongMono` `strongMono_of_mono`
`epi_of_strongEpi` 📖	mathematical	—	`Epi`	—	`StrongEpi.epi`
`isIso_of_epi_of_strongMono` 📖	mathematical	—	`IsIso`	—	`Category.id_comp` `Category.comp_id` `sq_hasLift_of_hasLiftingProperty` `StrongMono.rlp` `CommSq.fac_left` `CommSq.fac_right`
`isIso_of_mono_of_strongEpi` 📖	mathematical	—	`IsIso`	—	`Category.id_comp` `Category.comp_id` `sq_hasLift_of_hasLiftingProperty` `StrongEpi.llp` `CommSq.fac_left` `CommSq.fac_right`
`mono_of_strongMono` 📖	mathematical	—	`Mono`	—	`StrongMono.mono`
`strongEpi_comp` 📖	mathematical	—	`StrongEpi` `CategoryStruct.comp` `Category.toCategoryStruct`	—	`epi_comp` `epi_of_strongEpi` `HasLiftingProperty.of_comp_left` `StrongEpi.llp`
`strongEpi_of_epi` 📖	mathematical	—	`StrongEpi`	—	`StrongEpiCategory.strongEpi_of_epi`
`strongEpi_of_isIso` 📖	mathematical	—	`StrongEpi`	—	`IsSplitEpi.epi` `IsSplitEpi.of_iso` `HasLiftingProperty.of_left_iso`
`strongEpi_of_strongEpi` 📖	mathematical	—	`StrongEpi`	—	`epi_of_epi` `epi_of_strongEpi` `Category.assoc` `CommSq.w` `CommSq.HasLift.mk'` `sq_hasLift_of_hasLiftingProperty` `StrongEpi.llp` `cancel_mono` `CommSq.fac_right`
`strongMono_comp` 📖	mathematical	—	`StrongMono` `CategoryStruct.comp` `Category.toCategoryStruct`	—	`mono_comp` `mono_of_strongMono` `HasLiftingProperty.of_comp_right` `StrongMono.rlp`
`strongMono_of_isIso` 📖	mathematical	—	`StrongMono`	—	`IsSplitMono.mono` `IsSplitMono.of_iso` `HasLiftingProperty.of_right_iso`
`strongMono_of_mono` 📖	mathematical	—	`StrongMono`	—	`StrongMonoCategory.strongMono_of_mono`
`strongMono_of_strongMono` 📖	mathematical	—	`StrongMono`	—	`mono_of_mono` `mono_of_strongMono` `Category.assoc` `eq_whisker` `CommSq.w` `CommSq.HasLift.mk'` `sq_hasLift_of_hasLiftingProperty` `StrongMono.rlp` `CommSq.fac_left` `cancel_epi` `CommSq.fac_left_assoc`

CategoryTheory.StrongEpi

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`epi` 📖	mathematical	—	`CategoryTheory.Epi`	—	—
`iff_of_arrow_iso` 📖	mathematical	—	`CategoryTheory.StrongEpi`	—	`of_arrow_iso`
`llp` 📖	mathematical	—	`CategoryTheory.HasLiftingProperty`	—	—
`mk'` 📖	mathematical	`CategoryTheory.CommSq.HasLift`	`CategoryTheory.StrongEpi`	—	—
`of_arrow_iso` 📖	mathematical	—	`CategoryTheory.StrongEpi`	—	`CategoryTheory.Arrow.iso_w'` `CategoryTheory.epi_comp` `CategoryTheory.epi_of_strongEpi` `CategoryTheory.strongEpi_of_isIso` `CategoryTheory.Arrow.isIso_left` `CategoryTheory.Iso.isIso_inv` `CategoryTheory.Arrow.epi_right` `CategoryTheory.Iso.isIso_hom` `CategoryTheory.HasLiftingProperty.of_arrow_iso_left` `llp`

CategoryTheory.StrongEpiCategory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`strongEpi_of_epi` 📖	mathematical	—	`CategoryTheory.StrongEpi`	—	—

CategoryTheory.StrongMono

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`iff_of_arrow_iso` 📖	mathematical	—	`CategoryTheory.StrongMono`	—	`of_arrow_iso`
`mk'` 📖	mathematical	`CategoryTheory.CommSq.HasLift`	`CategoryTheory.StrongMono`	—	—
`mono` 📖	mathematical	—	`CategoryTheory.Mono`	—	—
`of_arrow_iso` 📖	mathematical	—	`CategoryTheory.StrongMono`	—	`CategoryTheory.Arrow.iso_w'` `CategoryTheory.mono_comp` `CategoryTheory.Arrow.mono_left` `CategoryTheory.mono_of_strongMono` `CategoryTheory.strongMono_of_isIso` `CategoryTheory.Iso.isIso_inv` `CategoryTheory.Arrow.isIso_right` `CategoryTheory.Iso.isIso_hom` `CategoryTheory.HasLiftingProperty.of_arrow_iso_right` `rlp`
`rlp` 📖	mathematical	—	`CategoryTheory.HasLiftingProperty`	—	—

CategoryTheory.StrongMonoCategory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`strongMono_of_mono` 📖	mathematical	—	`CategoryTheory.StrongMono`	—	—

---

← Back to Index