Theorems · Theorem · category theory

CategoryTheory.MorphismProperty.IsLocalAtTarget.of_forall_pullbackSnd

∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {P : CategoryTheory.MorphismProperty C}
  {K : CategoryTheory.Precoverage C} [self : P.IsLocalAtTarget K] {X Y : C} {f : Y ⟶ X} {R : CategoryTheory.Presieve X},
  R ∈ K.coverings X →
    (∀ {U : C} {g : U ⟶ X} [inst_1 : CategoryTheory.Limits.HasPullback f g],
        R g → P (CategoryTheory.Limits.pullback.snd f g)) →
      P f

If P holds for f restricted to Uᵢ for all i, it also holds for f : X ⟶ Y for any K-cover R of Y.

Defined in

Mathlib.CategoryTheory.MorphismProperty.Local

Cited by

2 results in Mathlib

Foundations

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

Assumes

CategoryTheory.MorphismProperty.IsLocalAtTarget