Theorems · Theorem · category theory

CategoryTheory.MorphismProperty.pullbackLift_fst_snd

∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C}
  [P.IsStableUnderBaseChange] {S S' X Y : C} (f : S' ⟶ S) {v₁₂ : X ⟶ S} {v₂₂ : Y ⟶ S} {g : X ⟶ Y}
  (hv₁₂ : v₁₂ = CategoryTheory.CategoryStruct.comp g v₂₂) [inst_2 : CategoryTheory.Limits.HasPullback v₁₂ f]
  [inst_3 : CategoryTheory.Limits.HasPullback v₂₂ f],
  P g →
    P
      (CategoryTheory.Limits.pullback.lift
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst v₁₂ f) g)
        (CategoryTheory.Limits.pullback.snd v₁₂ f) ⋯)

Defined in

Mathlib.CategoryTheory.MorphismProperty.Limits

Cited by

2 results in Mathlib

Foundations

Depth 34 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.MorphismProperty.IsStableUnderBaseChangeCategoryTheory.Limits.HasPullbackCategoryTheory.Limits.HasPullback