From 20da194e4df878faae6a6fd14a07c9a4e30e6e25 Mon Sep 17 00:00:00 2001 From: tb65536 Date: Thu, 9 Jul 2026 23:55:26 +0100 Subject: [PATCH] fix --- Mathlib/CategoryTheory/Sites/Descent/Precoverage.lean | 2 +- Mathlib/CategoryTheory/Sites/Sieves.lean | 1 + 2 files changed, 2 insertions(+), 1 deletion(-) diff --git a/Mathlib/CategoryTheory/Sites/Descent/Precoverage.lean b/Mathlib/CategoryTheory/Sites/Descent/Precoverage.lean index cfb85be4edb1c8..79b9cb7a7cedaf 100644 --- a/Mathlib/CategoryTheory/Sites/Descent/Precoverage.lean +++ b/Mathlib/CategoryTheory/Sites/Descent/Precoverage.lean @@ -397,7 +397,7 @@ lemma IsPrestack.of_precoverage obtain ⟨R', hR'⟩ := (Sieve.overEquiv _).symm.surjective (Sieve.generate R) rw [Presieve.isSheafFor_iff_generate] apply IsPrestackFor.isSheafFor' - simpa [Sieve.overEquiv_generate, Presieve.functorPushforward_overForget] + simpa [Sieve.overEquiv_generate, ← Sieve.arrows_generate_map_eq_functorPushforward] using hF _ _ hR /-- If a precoverage satisfies `HasIsos`, `IsStableUnderBaseChange` and diff --git a/Mathlib/CategoryTheory/Sites/Sieves.lean b/Mathlib/CategoryTheory/Sites/Sieves.lean index 81bf60530d4028..3af74da41626a2 100644 --- a/Mathlib/CategoryTheory/Sites/Sieves.lean +++ b/Mathlib/CategoryTheory/Sites/Sieves.lean @@ -1485,6 +1485,7 @@ lemma Presieve.bind_ofArrows_le_bindOfArrows {ι : Type*} {X : C} (Z : ι → C) rw [← Sieve.ofArrows.fac hv', ← reassoc_of% hu] exact ⟨S, u, u' ≫ f _, ⟨_, _, h⟩, rfl⟩ +@[deprecated "Use Sieve.arrows_generate_map_eq_functorPushforward instead." (since := "2026-07-09")] lemma Presieve.functorPushforward_overForget {S : C} {X : Over S} (R : Presieve X) : Presieve.functorPushforward (Over.forget S) R =