Theorems · Theorem · category theory

CategoryTheory.MorphismProperty.Over.pullback_map_left

∀ {T : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} T] (P Q : CategoryTheory.MorphismProperty T)
  [inst_1 : Q.IsMultiplicative] {X Y : T} (f : X ⟶ Y) [inst_2 : P.HasPullbacksAlong f]
  [inst_3 : P.IsStableUnderBaseChangeAlong f] [inst_4 : Q.IsStableUnderBaseChange] {A B : P.Over Q Y} (g : A ⟶ B),
  ((CategoryTheory.MorphismProperty.Over.pullback P Q f).map g).left =
    CategoryTheory.Limits.pullback.lift
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst A.hom f) g.left)
      (CategoryTheory.Limits.pullback.snd A.hom f) ⋯

Defined in

Mathlib.CategoryTheory.MorphismProperty.OverAdjunction

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.MorphismProperty.IsMultiplicativeCategoryTheory.MorphismProperty.HasPullbacksAlongCategoryTheory.MorphismProperty.IsStableUnderBaseChangeAlongCategoryTheory.MorphismProperty.IsStableUnderBaseChange