Theorems · Theorem · category theory

CategoryTheory.MorphismProperty.of_zeroHypercover_target

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

Defined in

Mathlib.CategoryTheory.MorphismProperty.Local

Cited by

2 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.Precoverage.HasPullbacksCategoryTheory.MorphismProperty.IsLocalAtTargetCategoryTheory.Precoverage.ZeroHypercover.Small