Theorems · Theorem · category theory

CategoryTheory.GrothendieckTopology.bind_covering

∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C} (J : CategoryTheory.GrothendieckTopology C)
  {S : CategoryTheory.Sieve X} {R : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → S.arrows f → CategoryTheory.Sieve Y},
  S ∈ J X → (∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (H : S.arrows f), R H ∈ J Y) → CategoryTheory.Sieve.bind S.arrows R ∈ J X

Defined in

Mathlib.CategoryTheory.Sites.Grothendieck

Cited by

5 results in Mathlib

Foundations

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

Assumes

CategoryTheory.Category