Theorems · Theorem · category theory

CategoryTheory.MorphismProperty.pullback_map

Deprecated since 2026-03-20Use CategoryTheory.MorphismProperty.pullbackMap instead.

∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C}
  [P.IsStableUnderBaseChange] [P.IsStableUnderComposition] {S X X' Y Y' : C} {f : X ⟶ S}
  [inst_3 : CategoryTheory.Limits.HasPullbacksAlong f] {g : Y ⟶ S} {f' : X' ⟶ S} {g' : Y' ⟶ S} {i₁ : X ⟶ X'}
  [inst_4 : CategoryTheory.Limits.HasPullbacksAlong g'] {i₂ : Y ⟶ Y'},
  P i₁ →
    P i₂ →
      ∀ (e₁ : f = CategoryTheory.CategoryStruct.comp i₁ f') (e₂ : g = CategoryTheory.CategoryStruct.comp i₂ g'),
        P (CategoryTheory.Limits.pullback.map f g f' g' i₁ i₂ (CategoryTheory.CategoryStruct.id S) ⋯ ⋯)

Alias of CategoryTheory.MorphismProperty.pullbackMap.

Defined in

Mathlib.CategoryTheory.MorphismProperty.Limits

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.MorphismProperty.IsStableUnderBaseChangeCategoryTheory.MorphismProperty.IsStableUnderCompositionCategoryTheory.Limits.HasPullbacksAlongCategoryTheory.Limits.HasPullbacksAlong