Documentation

Mathlib.CategoryTheory.Sites.Sieves.Functoriality

Functoriality of presieves and sieves #

Given a functor F : C ⥤ D, presieves and sieves can be transported between corresponding objects of C and D. This file develops these functorial pullback and pushforward operations.

For presieves, it defines preimage under F, the presieve generated by images of arrows, and the inductive image operation Presieve.map. The latter is left adjoint to functorial pullback. For sieves, it shows that functorial pullback is again a sieve and defines functorial pushforward by closing the image under precomposition. These operations likewise form a Galois connection.

The file records compatibility with lattice operations, composition of functors, fully faithful functors, equivalences of categories, and the corresponding constructions for arrow families.

Tags #

presieve, sieve, functor, pullback, pushforward

def CategoryTheory.Presieve.functorPullback {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) {X : C} (R : Presieve (F.obj X)) :

Given a presieve on F(X), we can define a presieve on X by taking the preimage via F.

Equations

CategoryTheory.Presieve.functorPullback F R f = R (F.map f)

Instances For

@[simp]

theorem CategoryTheory.Presieve.functorPullback_mem {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) {X : C} (R : Presieve (F.obj X)) {Y : C} (f : Y ⟶ X) :

functorPullback F R f ↔ R (F.map f)

@[simp]

theorem CategoryTheory.Presieve.functorPullback_id {C : Type u₁} [Category.{v₁, u₁} C] {X : C} (R : Presieve X) :

functorPullback (Functor.id C) R = R

def CategoryTheory.Presieve.functorPushforward {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) {X : C} (S : Presieve X) :

Presieve (F.obj X)

Given a presieve on X, we can define a presieve on F(X) (which is actually a sieve) by taking the sieve generated by the image via F.

Equations

CategoryTheory.Presieve.functorPushforward F S f = ∃ (Z : C) (g : Z ⟶ X) (h : Y ⟶ F.obj Z), S g ∧ f = CategoryTheory.CategoryStruct.comp h (F.map g)

Instances For

theorem CategoryTheory.Presieve.functorPushforward_monotone {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor C D} {X : C} :

Monotone (functorPushforward F)

structure CategoryTheory.Presieve.FunctorPushforwardStructure {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) {X : C} (S : Presieve X) {Y : D} (f : Y ⟶ F.obj X) :

Type (max (max u₁ v₁) v₂)

An auxiliary definition in order to fix the choice of the preimages between various definitions.

preobj : C
an object in the source category
premap : self.preobj ⟶ X
a map in the source category which has to be in the presieve
lift : Y ⟶ F.obj self.preobj
the morphism which appear in the factorisation
cover : S self.premap
the condition that premap is in the presieve
fac : f = CategoryStruct.comp self.lift (F.map self.premap)
the factorisation of the morphism

Instances For

noncomputable def CategoryTheory.Presieve.getFunctorPushforwardStructure {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {X : C} {F : Functor C D} {S : Presieve X} {Y : D} {f : Y ⟶ F.obj X} (h : functorPushforward F S f) :

FunctorPushforwardStructure F S f

The fixed choice of a preimage.

Equations

One or more equations did not get rendered due to their size.

Instances For

theorem CategoryTheory.Presieve.functorPushforward_comp {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) {X : C} {E : Type u₃} [Category.{v₃, u₃} E] (G : Functor D E) (R : Presieve X) :

functorPushforward (F.comp G) R = functorPushforward G (functorPushforward F R)

theorem CategoryTheory.Presieve.image_mem_functorPushforward {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) {X Y : C} (R : Presieve X) {f : Y ⟶ X} (h : R f) :

functorPushforward F R (F.map f)

inductive CategoryTheory.Presieve.map {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) {X : C} (s : Presieve X) :

Presieve (F.obj X)

This presieve generates functorPushforward. See arrows_generate_map_eq_functorPushforward.

of {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor C D} {X : C} {s : Presieve X} {Y : C} {u : Y ⟶ X} (h : s u) : map F s (F.map u)

Instances For

theorem CategoryTheory.Presieve.map_map {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor C D} {X Y : C} {f : Y ⟶ X} {R : Presieve X} (hf : R f) :

map F R (F.map f)

theorem CategoryTheory.Presieve.map_iff {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor C D} {X : C} {R : Presieve X} {Y : D} {f : Y ⟶ F.obj X} :

map F R f ↔ ∃ (Z : C) (h : F.obj Z = Y) (g : Z ⟶ X), R g ∧ F.map g = CategoryStruct.comp (eqToHom h) f

@[simp]

theorem CategoryTheory.Presieve.map_ofArrows {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor C D} {X : C} {ι : Type u_1} {Y : ι → C} (f : (i : ι) → Y i ⟶ X) :

map F (ofArrows Y f) = ofArrows (fun (i : ι) => F.obj (Y i)) fun (i : ι) => F.map (f i)

@[simp]

theorem CategoryTheory.Presieve.map_singleton {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor C D} {X Y : C} (f : X ⟶ Y) :

map F (singleton f) = singleton (F.map f)

theorem CategoryTheory.Presieve.map_le_iff_le_functorPullback {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor C D} {X : C} {R : Presieve X} {S : Presieve (F.obj X)} :

map F R ≤ S ↔ R ≤ functorPullback F S

theorem CategoryTheory.Presieve.galoisConnection_map_functorPullback {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) (X : C) :

GaloisConnection (map F) (functorPullback F)

theorem CategoryTheory.Presieve.map_functorPullback {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor C D} {X : C} (R : Presieve (F.obj X)) :

map F (functorPullback F R) ≤ R

theorem CategoryTheory.Presieve.le_functorPullback_map {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor C D} {X : C} (R : Presieve X) :

R ≤ functorPullback F (map F R)

@[simp]

theorem CategoryTheory.Presieve.map_functorPullback_map {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor C D} {X : C} (R : Presieve X) :

map F (functorPullback F (map F R)) = map F R

@[simp]

theorem CategoryTheory.Presieve.functorPullback_map_functorPullback {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor C D} {X : C} (R : Presieve (F.obj X)) :

functorPullback F (map F (functorPullback F R)) = functorPullback F R

@[simp]

theorem CategoryTheory.Presieve.map_id {C : Type u₁} [Category.{v₁, u₁} C] {X : C} (R : Presieve X) :

map (Functor.id C) R = R

theorem CategoryTheory.Presieve.map_monotone {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor C D} {X : C} :

Monotone (map F)

theorem CategoryTheory.Presieve.functorPullback_monotone {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor C D} {X : C} :

Monotone (functorPullback F)

@[simp]

theorem CategoryTheory.Presieve.map_bot {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor C D} {X : C} :

map F ⊥ = ⊥

theorem CategoryTheory.Sieve.arrows_generate_map_eq_functorPushforward {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) {X : C} {s : Presieve X} :

(generate (Presieve.map F s)).arrows = Presieve.functorPushforward F s

def CategoryTheory.Sieve.functorPullback {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) {X : C} (R : Sieve (F.obj X)) :

If R is a sieve, then the CategoryTheory.Presieve.functorPullback of R is actually a sieve.

Equations

CategoryTheory.Sieve.functorPullback F R = { arrows := CategoryTheory.Presieve.functorPullback F R.arrows, downward_closed := ⋯ }

Instances For

@[simp]

theorem CategoryTheory.Sieve.functorPullback_apply {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) {X : C} (R : Sieve (F.obj X)) :

(functorPullback F R).arrows = Presieve.functorPullback F R.arrows

@[simp]

theorem CategoryTheory.Sieve.functorPullback_arrows {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) {X : C} (R : Sieve (F.obj X)) :

(functorPullback F R).arrows = Presieve.functorPullback F R.arrows

@[simp]

theorem CategoryTheory.Sieve.functorPullback_id {C : Type u₁} [Category.{v₁, u₁} C] {X : C} (R : Sieve X) :

functorPullback (Functor.id C) R = R

theorem CategoryTheory.Sieve.functorPullback_comp {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) {X : C} {E : Type u₃} [Category.{v₃, u₃} E] (G : Functor D E) (R : Sieve ((F.comp G).obj X)) :

functorPullback (F.comp G) R = functorPullback F (functorPullback G R)

theorem CategoryTheory.Sieve.generate_functorPullback_le {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) {X : C} (R : Presieve (F.obj X)) :

generate (Presieve.functorPullback F R) ≤ functorPullback F (generate R)

theorem CategoryTheory.Sieve.functorPullback_pullback {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) {X Y : C} (f : X ⟶ Y) (S : Sieve (F.obj Y)) :

functorPullback F (pullback (F.map f) S) = pullback f (functorPullback F S)

theorem CategoryTheory.Sieve.functorPushforward_extend_eq {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) {X : C} {R : Presieve X} :

Presieve.functorPushforward F (generate R).arrows = Presieve.functorPushforward F R

def CategoryTheory.Sieve.functorPushforward {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) {X : C} (R : Sieve X) :

Sieve (F.obj X)

The sieve generated by the image of R under F.

Equations

CategoryTheory.Sieve.functorPushforward F R = { arrows := CategoryTheory.Presieve.functorPushforward F R.arrows, downward_closed := ⋯ }

Instances For

@[simp]

theorem CategoryTheory.Sieve.functorPushforward_apply {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) {X : C} (R : Sieve X) :

(functorPushforward F R).arrows = Presieve.functorPushforward F R.arrows

theorem CategoryTheory.Sieve.generate_map_eq_functorPushforward {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) {X : C} {s : Presieve X} :

generate (Presieve.map F s) = functorPushforward F (generate s)

theorem CategoryTheory.Sieve.functorPushforward_ofArrows {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) {X : C} {ι : Type u_1} {Y : ι → C} (f : (i : ι) → Y i ⟶ X) :

functorPushforward F (ofArrows Y f) = ofArrows (fun (i : ι) => F.obj (Y i)) fun (i : ι) => F.map (f i)

@[simp]

theorem CategoryTheory.Sieve.functorPushforward_id {C : Type u₁} [Category.{v₁, u₁} C] {X : C} (R : Sieve X) :

functorPushforward (Functor.id C) R = R

theorem CategoryTheory.Sieve.functorPushforward_comp {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) {X : C} {E : Type u₃} [Category.{v₃, u₃} E] (G : Functor D E) (R : Sieve X) :

functorPushforward (F.comp G) R = functorPushforward G (functorPushforward F R)

theorem CategoryTheory.Sieve.functor_galoisConnection {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) (X : C) :

GaloisConnection (functorPushforward F) (functorPullback F)

theorem CategoryTheory.Sieve.functorPushforward_le_iff_le_functorPullback {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) {X : C} (S : Sieve X) (R : Sieve (F.obj X)) :

functorPushforward F S ≤ R ↔ S ≤ functorPullback F R

theorem CategoryTheory.Sieve.functorPullback_monotone {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) (X : C) :

Monotone (functorPullback F)

theorem CategoryTheory.Sieve.functorPushforward_monotone {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) (X : C) :

Monotone (functorPushforward F)

theorem CategoryTheory.Sieve.le_functorPushforward_pullback {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) {X : C} (R : Sieve X) :

R ≤ functorPullback F (functorPushforward F R)

theorem CategoryTheory.Sieve.functorPullback_pushforward_le {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) {X : C} (R : Sieve (F.obj X)) :

functorPushforward F (functorPullback F R) ≤ R

theorem CategoryTheory.Sieve.functorPushforward_union {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) {X : C} (S R : Sieve X) :

functorPushforward F (S ⊔ R) = functorPushforward F S ⊔ functorPushforward F R

theorem CategoryTheory.Sieve.functorPullback_union {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) {X : C} (S R : Sieve (F.obj X)) :

functorPullback F (S ⊔ R) = functorPullback F S ⊔ functorPullback F R

theorem CategoryTheory.Sieve.functorPullback_inter {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) {X : C} (S R : Sieve (F.obj X)) :

functorPullback F (S ⊓ R) = functorPullback F S ⊓ functorPullback F R

@[simp]

theorem CategoryTheory.Sieve.functorPushforward_bot {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) (X : C) :

functorPushforward F ⊥ = ⊥

@[simp]

theorem CategoryTheory.Sieve.functorPushforward_top {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) (X : C) :

functorPushforward F ⊤ = ⊤

@[simp]

theorem CategoryTheory.Sieve.functorPullback_bot {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) (X : C) :

functorPullback F ⊥ = ⊥

@[simp]

theorem CategoryTheory.Sieve.functorPullback_top {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) (X : C) :

functorPullback F ⊤ = ⊤

theorem CategoryTheory.Sieve.image_mem_functorPushforward {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) {X : C} (R : Sieve X) {V : C} {f : V ⟶ X} (h : R.arrows f) :

(functorPushforward F R).arrows (F.map f)

theorem CategoryTheory.Sieve.functorPushforward_pullback_le {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) {X Y : C} (f : Y ⟶ X) (S : Sieve X) :

functorPushforward F (pullback f S) ≤ pullback (F.map f) (functorPushforward F S)

def CategoryTheory.Sieve.essSurjFullFunctorGaloisInsertion {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) [F.EssSurj] [F.Full] (X : C) :

GaloisInsertion (functorPushforward F) (functorPullback F)

When F is essentially surjective and full, the Galois connection is a Galois insertion.

Equations

CategoryTheory.Sieve.essSurjFullFunctorGaloisInsertion F X = ⋯.toGaloisInsertion ⋯

Instances For

def CategoryTheory.Sieve.fullyFaithfulFunctorGaloisCoinsertion {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) [F.Full] [F.Faithful] (X : C) :

GaloisCoinsertion (functorPushforward F) (functorPullback F)

When F is fully faithful, the Galois connection is a Galois coinsertion.

Equations

CategoryTheory.Sieve.fullyFaithfulFunctorGaloisCoinsertion F X = ⋯.toGaloisCoinsertion ⋯

Instances For

theorem CategoryTheory.Sieve.functorPullback_functorPushforward_eq {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) {X : C} {S : Sieve X} [F.Full] [F.Faithful] :

functorPullback F (functorPushforward F S) = S

theorem CategoryTheory.Sieve.functorPushforward_functor {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {X : C} (S : Sieve X) (e : C ≌ D) :

functorPushforward e.functor S = functorPullback e.inverse (pullback (e.unitInv.app X) S)

@[simp]

theorem CategoryTheory.Sieve.mem_functorPushforward_functor {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {X : C} {Y : D} {S : Sieve X} {e : C ≌ D} {f : Y ⟶ e.functor.obj X} :

(functorPushforward e.functor S).arrows f ↔ S.arrows (CategoryStruct.comp (e.inverse.map f) (e.unitInv.app X))

theorem CategoryTheory.Sieve.functorPushforward_inverse {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {X : D} (S : Sieve X) (e : C ≌ D) :

functorPushforward e.inverse S = functorPullback e.functor (pullback (e.counit.app X) S)

@[simp]

theorem CategoryTheory.Sieve.mem_functorPushforward_inverse {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {Y : C} {X : D} {S : Sieve X} {e : C ≌ D} {f : Y ⟶ e.inverse.obj X} :

(functorPushforward e.inverse S).arrows f ↔ S.arrows (CategoryStruct.comp (e.functor.map f) (e.counit.app X))

theorem CategoryTheory.Sieve.functorPushforward_equivalence_eq_pullback {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (e : C ≌ D) {U : C} (S : Sieve U) :

functorPushforward e.inverse (functorPushforward e.functor S) = pullback (e.unitInv.app U) S

theorem CategoryTheory.Sieve.pullback_functorPushforward_equivalence_eq {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (e : C ≌ D) {X : C} (S : Sieve X) :

pullback (e.unit.app X) (functorPushforward e.inverse (functorPushforward e.functor S)) = S

theorem CategoryTheory.Sieve.mem_functorPushforward_iff_of_full {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) [F.Full] {X Y : C} (R : Sieve X) (f : F.obj Y ⟶ F.obj X) :

Presieve.functorPushforward F R.arrows f ↔ ∃ (g : Y ⟶ X), F.map g = f ∧ R.arrows g

theorem CategoryTheory.Sieve.mem_functorPushforward_iff_of_full_of_faithful {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) [F.Full] [F.Faithful] {X Y : C} (R : Sieve X) (f : Y ⟶ X) :

Presieve.functorPushforward F R.arrows (F.map f) ↔ R.arrows f

theorem CategoryTheory.Sieve.functorPushforward_ofObjects_le {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) {I : Type u_1} (X : I → C) (Y : C) :

functorPushforward F (ofObjects X Y) ≤ ofObjects (F.obj ∘ X) (F.obj Y)

theorem CategoryTheory.Presieve.functorPullback_arrows {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) {X : C} (S : Sieve (F.obj X)) :

functorPullback F S.arrows = (Sieve.functorPullback F S).arrows

theorem CategoryTheory.Presieve.map_le_functorPushforward {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) {X : C} (S : Presieve X) :

map F S ≤ functorPushforward F S

@[deprecated "Use Sieve.arrows_generate_map_eq_functorPushforward instead." (since := "2026-07-09")]

theorem CategoryTheory.Presieve.functorPushforward_overForget {C : Type u₁} [Category.{v₁, u₁} C] {S : C} {X : Over S} (R : Presieve X) :

functorPushforward (Over.forget S) R = (Sieve.generate (map (Over.forget S) R)).arrows