Theorems · Theorem · category theory
CategoryTheory.Subobject.factorThru_arrow
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (P : CategoryTheory.Subobject Y) (f : X ⟶ Y)
(h : P.Factors f), CategoryTheory.CategoryStruct.comp (P.factorThru f h) P.arrow = f- Cited by
- 31 results in Mathlib
- Foundations
- Depth 40 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- CategoryTheory.Category
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites10
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.Functor.objstatement · cited by 19,642
- CategoryTheory.CategoryStruct.compstatement · cited by 17,999
- CategoryTheory.Subobjectstatement and proof · cited by 385
- CategoryTheory.Subobject.underlyingstatement · cited by 211
- CategoryTheory.Subobject.arrowstatement · cited by 175
- CategoryTheory.Subobject.Factorsstatement and proof · cited by 56
- CategoryTheory.Subobject.factorThrustatement · cited by 35
- CategoryTheory.Subobject.factors_iffproof · cited by 12
Cited by31
Results whose statement or proof uses this declaration.
- CategoryTheory.Limits.kernelSubobjectMap_arrowproof · cited by 5
- CategoryTheory.ObjectProperty.isStrongGenerator_iffproof · cited by 5
- CategoryTheory.Subobject.factorThru_arrow_assocproof · cited by 3
- CategoryTheory.Limits.factorThruKernelSubobject_comp_arrowproof · cited by 2
- CategoryTheory.Limits.pullback_factorsproof · cited by 2
- CategoryTheory.Subobject.finset_inf_arrow_factorsproof · cited by 2
- CategoryTheory.Subobject.factors_right_of_factors_addproof · cited by 1
- AlgebraicTopology.DoldKan.PInftyToNormalizedMooreComplex_naturalityproof · cited by 1
- AlgebraicTopology.DoldKan.PInfty_comp_PInftyToNormalizedMooreComplexproof · cited by 1
- CategoryTheory.Subobject.inf_isPullbackproof · cited by 1
- CategoryTheory.Subobject.eq_of_le_of_isDetectingproof · cited by 1