feat(CategoryTheory/Sites): (Co)continuity of `Over.iteratedSliceEquiv`

[Shaddaaa]

Show that the Over.iteratedSliceEquiv functor is continuous and cocontinuous.

This contribution was created as part of the Heidelberg Lean workshop "Formalising algebraic geometry" in November 2025.

Co-authored-by: Ben Eltschig @peabrainiac Co-authored-by: Andrew Yang @erdOne

---

[github-actions[bot]]

✅ PR Title Formatted Correctly

The title of this PR has been updated to match our commit style conventions. Thank you!

[github-actions[bot]]

PR summary 998c33d676

Import changes exceeding 2%

%	File
+35.96%	Mathlib.CategoryTheory.Sites.Over

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.CategoryTheory.Sites.Over	623	847	+224 (+35.96%)

Import changes for all files

Files	Import difference
Mathlib.AlgebraicGeometry.Sites.Etale Mathlib.AlgebraicGeometry.Sites.Small	3
5 files Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators Mathlib.Algebra.Category.ModuleCat.Sheaf.PullbackContinuous Mathlib.Algebra.Category.ModuleCat.Sheaf.PullbackFree Mathlib.Algebra.Category.ModuleCat.Sheaf.PushforwardContinuous Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent	6
5 files Mathlib.CategoryTheory.Sites.Descent.DescentData Mathlib.CategoryTheory.Sites.Descent.IsPrestack Mathlib.CategoryTheory.Sites.Over Mathlib.CategoryTheory.Sites.PseudofunctorSheafOver Mathlib.CategoryTheory.Sites.SheafHom	224

---

Declarations diff

+ isDenseSubsite_functor_of_isCocontinuous + isDenseSubsite_inverse_of_isCocontinuous +++++ instance {X : C} (f : Over X) :

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[dagurtomas]

Actually, it seems you get everything you're proving in this PR from existing API in Sites.Equivalence together with the following:

instance {X : C} (f : Over X) : f.iteratedSliceBackward.IsEquivalence := 
  inferInstanceAs f.iteratedSliceEquiv.inverse.IsEquivalence

example {X : C} (f : Over X) : 
    (J.over f.left) = f.iteratedSliceBackward.inducedTopology ((J.over X).over f) := by
  ext Y S 
  simp [GrothendieckTopology.mem_over_iff, Sieve.overEquiv,
      ← Over.iteratedSliceBackward_forget_forget f, Sieve.functorPushforward_comp]

The example gives you that f.iteratedSliceBackward induces a dense subsite, and is thus continuous and cocontinuous. It's inverse f.iteratedSliceForward is then also a dense subsite, and thus continuous and cocontinuous.

[Shaddaaa]

Thank you, that makes everything much much nicer.

I am unsure whether my choice of name for the lemmas is sensible, I tried to adhere the naming convention but I might be missing something.

[erdOne]

Also I would be nice if you can click "resolve conversation" on the suggestions that are no longer relevant.

[Shaddaaa]

All done, thank you!

[dagurtomas]

Thanks!

maintainer delegate

[github-actions[bot]]

🚀 Pull request has been placed on the maintainer queue by dagurtomas.

[jcommelin]

@Shaddaaa when you've processed all comments, and the PR is ready for review again, please remove the awaiting-author label by typing:

-awaiting-author

[Shaddaaa]

Oh sorry, I am still getting used to how github PRs/suggestions etc work. It should be fixed now.

-awaiting-author

[dagurtomas]

I just pushed a suggestion I had forgotten to comment. No need to do anything, this is ready to be merged IMO. The suggestion was to change inv (e.unit.app _) to e.unitInv.app _. This plays better with automation

[dagurtomas]

maintainer merge

[github-actions[bot]]

🚀 Pull request has been placed on the maintainer queue by dagurtomas.

[Shaddaaa]

-awaiting-author

[github-actions[bot]]

🚀 Pull request has been placed on the maintainer queue by robin-carlier.

[mathlib-bors[bot]]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style
• Post-Build Step