Theorems · Theorem · category theory

CategoryTheory.MorphismProperty.IsLocalAtSource.of_forall_comp

∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {P : CategoryTheory.MorphismProperty C}
  {K : CategoryTheory.Precoverage C} [self : P.IsLocalAtSource K] {X Y : C} {f : X ⟶ Y} {R : CategoryTheory.Presieve X},
  R ∈ K.coverings X → (∀ ⦃U : C⦄ ⦃g : U ⟶ X⦄, R g → P (CategoryTheory.CategoryStruct.comp g f)) → P f

If P holds for 𝒰.f i ≫ f for all i, it holds for f : X ⟶ Y for any K-cover R of X.

Defined in

Mathlib.CategoryTheory.MorphismProperty.Local

Cited by

4 results in Mathlib

Foundations

Depth 4 from the axioms · uses no axioms

Assumes

CategoryTheory.MorphismProperty.IsLocalAtSource