Theorems · Theorem · category theory
AddCommGrpCat.image.lift_fac
∀ {G H : AddCommGrpCat} {f : G ⟶ H} (F' : CategoryTheory.Limits.MonoFactorisation f),
CategoryTheory.CategoryStruct.comp (AddCommGrpCat.image.lift F') F'.m = AddCommGrpCat.image.ι f- Defined in
- Mathlib.Algebra.Category.Grp.Images
- Cited by
- 0 results in Mathlib
- Foundations
- Depth 49 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites16
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- Quiver.Homstatement and proof · cited by 32,603
- CategoryTheory.CategoryStruct.compstatement · cited by 17,999
- CategoryTheory.ConcreteCategory.homproof · cited by 4,022
- AddCommGrpCatstatement and proof · cited by 462
- AddCommGrpCat.carrierproof · cited by 407
- AddMonoidHom.extproof · cited by 149
- CategoryTheory.Limits.MonoFactorisation.Istatement · cited by 83
- AddCommGrpCat.Hom.homproof · cited by 72
- CategoryTheory.Limits.MonoFactorisationstatement and proof · cited by 69
- CategoryTheory.Limits.MonoFactorisation.mstatement · cited by 45
- CategoryTheory.Limits.MonoFactorisation.facproof · cited by 13
Cited by1
Results whose statement or proof uses this declaration.
- AddCommGrpCat.isImageproof · cited by 0