Theorems · Theorem · category theory

CategoryTheory.MorphismProperty.IsLocalAtTarget.mk_of_isStableUnderBaseChange

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

Defined in

Mathlib.CategoryTheory.MorphismProperty.Local

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.Precoverage.HasPullbacksCategoryTheory.MorphismProperty.IsStableUnderBaseChange