Theorems · Theorem · category theory

CategoryTheory.MorphismProperty.IsLocalAtTarget.iff_of_zeroHypercover

∀ {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)
  [inst_2 : K.HasPullbacks], P f ↔ ∀ (i : 𝒰.I₀), P (CategoryTheory.Limits.pullback.snd f (𝒰.f i))

Defined in

Mathlib.CategoryTheory.MorphismProperty.Local

Cited by

3 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.MorphismProperty.IsLocalAtTargetCategoryTheory.Precoverage.HasPullbacks