Theorems · Definition · category theory

CategoryTheory.Sieve.pullback

{C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] → {X Y : C} → (Y ⟶ X) → CategoryTheory.Sieve X → CategoryTheory.Sieve Y

Given a morphism h : Y ⟶ X, send a sieve S on X to a sieve on Y as the inverse image of S with _ ≫ h. That is, Sieve.pullback S h := (≫ h) '⁻¹ S.

Defined in

Mathlib.CategoryTheory.Sites.Sieves

Cited by

126 results in Mathlib

Foundations

Depth 7 from the axioms, rests on 17 definitions · uses propext, Quot.sound

Assumes

CategoryTheory.Category