Theorems · Theorem · category theory
CategoryTheory.epi_of_epi_fac
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} {f : X ⟶ Y} {g : Y ⟶ Z} {h : X ⟶ Z}
[CategoryTheory.Epi h], CategoryTheory.CategoryStruct.comp f g = h → CategoryTheory.Epi g- Defined in
- Mathlib.CategoryTheory.Category.Basic
- Cited by
- 13 results in Mathlib
- Foundations
- Depth 7 from the axioms · uses propext
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CategoryTheory.Categorystatement and proof · cited by 32,673
- Quiver.Homstatement and proof · cited by 32,603
- CategoryTheory.CategoryStruct.compstatement and proof · cited by 17,999
- CategoryTheory.Epistatement and proof · cited by 688
- CategoryTheory.epi_of_epiproof · cited by 10
Cited by13
Results whose statement or proof uses this declaration.
- CategoryTheory.epi_iff_surjective_up_to_refinementsproof · cited by 5
- CategoryTheory.Sheaf.isLocallySurjective_iff_epi'proof · cited by 5
- CategoryTheory.ShortComplex.exact_iff_epi_imageToKernel'proof · cited by 2
- CategoryTheory.Sheaf.isLocallySurjective_iff_epiproof · cited by 2
- HomologicalComplex.HomologySequence.epi_homologyMap_τ₃proof · cited by 1
- CategoryTheory.ShortComplex.Exact.isIso_g'proof · cited by 1
- CategoryTheory.Abelian.epi_fst_of_isLimitproof · cited by 1
- CategoryTheory.Abelian.SpectralObject.epi_mapproof · cited by 0
- CategoryTheory.ComposableArrows.IsComplex.epi_cokerToKer'proof · cited by 0
- CategoryTheory.Abelian.Pseudoelement.epi_of_pseudo_surjectiveproof · cited by 0
- CategoryTheory.Abelian.epi_snd_of_isLimitproof · cited by 0