Theorems · Definition · category theory
CategoryTheory.Limits.weakEqualizer.lift
{C : Type u_1} →
[inst : CategoryTheory.Category.{v_1, u_1} C] →
{X Y : C} →
{f g : X ⟶ Y} →
[inst_1 : CategoryTheory.Limits.HasWeakEqualizer f g] →
{W : C} →
(k : W ⟶ X) →
CategoryTheory.CategoryStruct.comp k f = CategoryTheory.CategoryStruct.comp k g →
(W ⟶ CategoryTheory.Limits.weakEqualizer f g)A morphism k : W ⟶ X satisfying k ≫ f = k ≫ g factors through the weak equalizer of
f and g via weakEqualizer.lift : W ⟶ weakEqualizer f g.
- Cited by
- 4 results in Mathlib
- Foundations
- Depth 24 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites8
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.Limits.parallelPairproof · cited by 766
- CategoryTheory.Limits.Fork.ofιproof · cited by 66
- CategoryTheory.Limits.HasWeakEqualizerstatement and proof · cited by 10
- CategoryTheory.Limits.weakEqualizerstatement · cited by 7
- CategoryTheory.Limits.weakLimit.liftproof · cited by 3
Cited by5
Results whose statement or proof uses this declaration.
- CategoryTheory.Limits.weakEqualizer.lift_ιstatement · cited by 1
- CategoryTheory.Limits.weakEqualizer.lift.congr_simpstatement and proof · cited by 0
- CategoryTheory.Limits.weakEqualizer.lift'proof · cited by 0
- CategoryTheory.Limits.weakEqualizer.lift_ι_assocstatement and proof · cited by 0