Documentation Verification Report

EpiMono

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

Statistics

Metric	Count
Definitions `functorialSurjectiveInjectiveFactorizationData`	1
Theorems `bijective_of_isIso`, `epi_iff_surjective_of_preservesPushout`, `epi_of_surjective`, `forget₂_preservesEpimorphisms`, `forget₂_preservesMonomorphisms`, `injective_eq_monomorphisms`, `injective_eq_monomorphisms_iff`, `injective_le_monomorphisms`, `injective_of_mono_of_preservesPullback`, `instHasFunctorialSurjectiveInjectiveFactorization`, `isIso_iff_bijective`, `mono_iff_injective_of_preservesPullback`, `mono_of_injective`, `surjective_eq_epimorphisms`, `surjective_eq_epimorphisms_iff`, `surjective_le_epimorphisms`, `surjective_of_epi_of_preservesPushout`	17
Total	18

CategoryTheory.ConcreteCategory

Definitions

Name	Category	Theorems
`functorialSurjectiveInjectiveFactorizationData` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`bijective_of_isIso` 📖	mathematical	—	`Function.Bijective` `DFunLike.coe` `hom`	—	`CategoryTheory.isIso_iff_bijective` `CategoryTheory.hom_isIso`
`epi_iff_surjective_of_preservesPushout` 📖	mathematical	—	`CategoryTheory.Epi` `DFunLike.coe` `hom`	—	`CategoryTheory.Functor.epi_map_iff_epi` `CategoryTheory.preservesEpimorphisms_of_preservesColimitsOfShape` `CategoryTheory.Functor.reflectsEpimorphisms_of_faithful` `CategoryTheory.instFaithfulForget` `CategoryTheory.epi_iff_surjective`
`epi_of_surjective` 📖	mathematical	`DFunLike.coe` `hom`	`CategoryTheory.Epi`	—	`CategoryTheory.Functor.epi_of_epi_map` `CategoryTheory.Functor.reflectsEpimorphisms_of_faithful` `CategoryTheory.instFaithfulForget` `CategoryTheory.epi_iff_surjective`
`forget₂_preservesEpimorphisms` 📖	mathematical	—	`CategoryTheory.Functor.PreservesEpimorphisms` `CategoryTheory.forget₂`	—	`CategoryTheory.HasForget₂.forget_comp` `CategoryTheory.Functor.preservesEpimorphisms_of_preserves_of_reflects` `CategoryTheory.Functor.reflectsEpimorphisms_of_faithful` `CategoryTheory.instFaithfulForget`
`forget₂_preservesMonomorphisms` 📖	mathematical	—	`CategoryTheory.Functor.PreservesMonomorphisms` `CategoryTheory.forget₂`	—	`CategoryTheory.HasForget₂.forget_comp` `CategoryTheory.Functor.preservesMonomorphisms_of_preserves_of_reflects` `CategoryTheory.Functor.reflectsMonomorphisms_of_faithful` `CategoryTheory.instFaithfulForget`
`injective_eq_monomorphisms` 📖	mathematical	—	`CategoryTheory.MorphismProperty.injective` `CategoryTheory.MorphismProperty.monomorphisms`	—	`injective_eq_monomorphisms_iff`
`injective_eq_monomorphisms_iff` 📖	mathematical	—	`CategoryTheory.MorphismProperty.injective` `CategoryTheory.MorphismProperty.monomorphisms` `CategoryTheory.Functor.PreservesMonomorphisms` `CategoryTheory.types` `CategoryTheory.forget`	—	`CategoryTheory.mono_iff_injective` `le_antisymm` `injective_le_monomorphisms` `CategoryTheory.Functor.map_mono`
`injective_le_monomorphisms` 📖	mathematical	—	`CategoryTheory.MorphismProperty` `CategoryTheory.Category.toCategoryStruct` `Preorder.toLE` `PartialOrder.toPreorder` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `CompleteBooleanAlgebra.toCompleteLattice` `CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra` `CategoryTheory.MorphismProperty.injective` `CategoryTheory.MorphismProperty.monomorphisms`	—	`CategoryTheory.Functor.mono_of_mono_map` `CategoryTheory.Functor.reflectsMonomorphisms_of_faithful` `CategoryTheory.instFaithfulForget` `CategoryTheory.mono_iff_injective`
`injective_of_mono_of_preservesPullback` 📖	mathematical	—	`DFunLike.coe` `hom`	—	`CategoryTheory.mono_iff_injective` `CategoryTheory.Functor.map_mono` `CategoryTheory.preservesMonomorphisms_of_preservesLimitsOfShape`
`instHasFunctorialSurjectiveInjectiveFactorization` 📖	mathematical	—	`HasFunctorialSurjectiveInjectiveFactorization`	—	—
`isIso_iff_bijective` 📖	mathematical	—	`CategoryTheory.IsIso` `Function.Bijective` `DFunLike.coe` `hom`	—	`CategoryTheory.isIso_iff_bijective` `CategoryTheory.hom_isIso` `CategoryTheory.isIso_of_reflects_iso`
`mono_iff_injective_of_preservesPullback` 📖	mathematical	—	`CategoryTheory.Mono` `DFunLike.coe` `hom`	—	`CategoryTheory.Functor.mono_map_iff_mono` `CategoryTheory.preservesMonomorphisms_of_preservesLimitsOfShape` `CategoryTheory.Functor.reflectsMonomorphisms_of_faithful` `CategoryTheory.instFaithfulForget` `CategoryTheory.mono_iff_injective`
`mono_of_injective` 📖	mathematical	`DFunLike.coe` `hom`	`CategoryTheory.Mono`	—	`CategoryTheory.Functor.mono_of_mono_map` `CategoryTheory.Functor.reflectsMonomorphisms_of_faithful` `CategoryTheory.instFaithfulForget` `CategoryTheory.mono_iff_injective`
`surjective_eq_epimorphisms` 📖	mathematical	—	`CategoryTheory.MorphismProperty.surjective` `CategoryTheory.MorphismProperty.epimorphisms`	—	`surjective_eq_epimorphisms_iff`
`surjective_eq_epimorphisms_iff` 📖	mathematical	—	`CategoryTheory.MorphismProperty.surjective` `CategoryTheory.MorphismProperty.epimorphisms` `CategoryTheory.Functor.PreservesEpimorphisms` `CategoryTheory.types` `CategoryTheory.forget`	—	`CategoryTheory.epi_iff_surjective` `le_antisymm` `surjective_le_epimorphisms` `CategoryTheory.Functor.map_epi`
`surjective_le_epimorphisms` 📖	mathematical	—	`CategoryTheory.MorphismProperty` `CategoryTheory.Category.toCategoryStruct` `Preorder.toLE` `PartialOrder.toPreorder` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `CompleteBooleanAlgebra.toCompleteLattice` `CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra` `CategoryTheory.MorphismProperty.surjective` `CategoryTheory.MorphismProperty.epimorphisms`	—	`CategoryTheory.Functor.epi_of_epi_map` `CategoryTheory.Functor.reflectsEpimorphisms_of_faithful` `CategoryTheory.instFaithfulForget` `CategoryTheory.epi_iff_surjective`
`surjective_of_epi_of_preservesPushout` 📖	mathematical	—	`DFunLike.coe` `hom`	—	`CategoryTheory.epi_iff_surjective` `CategoryTheory.Functor.map_epi` `CategoryTheory.preservesEpimorphisms_of_preservesColimitsOfShape`

---

← Back to Index