Theorems · Theorem · category theory

CategoryTheory.MorphismProperty.IsLocalAtTarget.of_isPullback

∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C}
  {K : CategoryTheory.Precoverage C} [P.IsLocalAtTarget K] {X Y : C} {f : X ⟶ Y} (𝒰 : K.ZeroHypercover Y) {X' : C}
  (i : 𝒰.I₀) {fst : X' ⟶ X} {snd : X' ⟶ 𝒰.X i}, CategoryTheory.IsPullback fst snd f (𝒰.f i) → P f → P snd

Defined in

Mathlib.CategoryTheory.MorphismProperty.Local

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.MorphismProperty.IsLocalAtTarget