Documentation Verification Report

EpiMono

📁 Source: Mathlib/CategoryTheory/ObjectProperty/EpiMono.lean

Statistics

Metric	Count
Definitions `IsClosedUnderQuotients`, `IsClosedUnderSubobjects`	2
Theorems `prop_of_epi`, `prop_of_mono`, `instIsClosedUnderIsomorphisms`, `instIsClosedUnderIsomorphisms_1`, `instIsClosedUnderQuotientsInverseImageOfPreservesEpimorphisms`, `instIsClosedUnderQuotientsIsZeroOfHasZeroMorphisms`, `instIsClosedUnderQuotientsTop`, `instIsClosedUnderSubobjectsInverseImageOfPreservesMonomorphisms`, `instIsClosedUnderSubobjectsIsZeroOfHasZeroMorphisms`, `instIsClosedUnderSubobjectsTop`, `prop_X₁_of_shortExact`, `prop_X₃_of_shortExact`, `prop_of_epi`, `prop_of_mono`	14
Total	16

CategoryTheory.ObjectProperty

Definitions

Name	Category	Theorems
`IsClosedUnderQuotients` 📖	CompData	4 math math: `IsSerreClass.toIsClosedUnderQuotients`, `instIsClosedUnderQuotientsIsZeroOfHasZeroMorphisms`, `instIsClosedUnderQuotientsInverseImageOfPreservesEpimorphisms`, `instIsClosedUnderQuotientsTop`
`IsClosedUnderSubobjects` 📖	CompData	6 math math: `instIsClosedUnderSubobjectsIsZeroOfHasZeroMorphisms`, `instIsClosedUnderSubobjectsInverseImageOfPreservesMonomorphisms`, `CategoryTheory.instIsClosedUnderSubobjectsIsNoetherianObject`, `IsSerreClass.toIsClosedUnderSubobjects`, `instIsClosedUnderSubobjectsTop`, `CategoryTheory.instIsClosedUnderSubobjectsIsArtinianObject`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsClosedUnderIsomorphisms` 📖	mathematical	—	`IsClosedUnderIsomorphisms`	—	`prop_of_mono` `CategoryTheory.mono_of_strongMono` `CategoryTheory.instStrongMonoOfIsRegularMono` `CategoryTheory.instIsRegularMonoOfIsSplitMono` `CategoryTheory.IsSplitMono.of_iso` `CategoryTheory.Iso.isIso_inv`
`instIsClosedUnderIsomorphisms_1` 📖	mathematical	—	`IsClosedUnderIsomorphisms`	—	`prop_of_epi` `CategoryTheory.epi_of_effectiveEpi` `CategoryTheory.instEffectiveEpiOfIsIso` `CategoryTheory.Iso.isIso_hom`
`instIsClosedUnderQuotientsInverseImageOfPreservesEpimorphisms` 📖	mathematical	—	`IsClosedUnderQuotients` `inverseImage`	—	`prop_of_epi` `CategoryTheory.Functor.map_epi`
`instIsClosedUnderQuotientsIsZeroOfHasZeroMorphisms` 📖	mathematical	—	`IsClosedUnderQuotients` `CategoryTheory.Limits.IsZero`	—	`CategoryTheory.Limits.IsZero.of_epi`
`instIsClosedUnderQuotientsTop` 📖	mathematical	—	`IsClosedUnderQuotients` `Top.top` `CategoryTheory.ObjectProperty` `CategoryTheory.Category.toCategoryStruct` `Pi.instTopForall` `BooleanAlgebra.toTop` `Prop.instBooleanAlgebra`	—	—
`instIsClosedUnderSubobjectsInverseImageOfPreservesMonomorphisms` 📖	mathematical	—	`IsClosedUnderSubobjects` `inverseImage`	—	`prop_of_mono` `CategoryTheory.Functor.map_mono`
`instIsClosedUnderSubobjectsIsZeroOfHasZeroMorphisms` 📖	mathematical	—	`IsClosedUnderSubobjects` `CategoryTheory.Limits.IsZero`	—	`CategoryTheory.Limits.IsZero.of_mono`
`instIsClosedUnderSubobjectsTop` 📖	mathematical	—	`IsClosedUnderSubobjects` `Top.top` `CategoryTheory.ObjectProperty` `CategoryTheory.Category.toCategoryStruct` `Pi.instTopForall` `BooleanAlgebra.toTop` `Prop.instBooleanAlgebra`	—	—
`prop_X₁_of_shortExact` 📖	mathematical	`CategoryTheory.ShortComplex.ShortExact` `CategoryTheory.ShortComplex.X₂`	`CategoryTheory.ShortComplex.X₁`	—	`CategoryTheory.ShortComplex.ShortExact.mono_f` `prop_of_mono`
`prop_X₃_of_shortExact` 📖	mathematical	`CategoryTheory.ShortComplex.ShortExact` `CategoryTheory.ShortComplex.X₂`	`CategoryTheory.ShortComplex.X₃`	—	`CategoryTheory.ShortComplex.ShortExact.epi_g` `prop_of_epi`
`prop_of_epi` 📖	—	—	—	—	`IsClosedUnderQuotients.prop_of_epi`
`prop_of_mono` 📖	—	—	—	—	`IsClosedUnderSubobjects.prop_of_mono`

CategoryTheory.ObjectProperty.IsClosedUnderQuotients

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`prop_of_epi` 📖	—	—	—	—	—

CategoryTheory.ObjectProperty.IsClosedUnderSubobjects

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`prop_of_mono` 📖	—	—	—	—	—

---

← Back to Index