Commit 2025-09-13 23:10 6b226223

View on Github →

feat(CategoryTheory): The finite pretopology on a category (#28614) We define CategoryTheory.Pretopology.finite, the finite pretopology on a category, which consists of presieves that contain only finitely many arrows.

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Sites/Finite.lean

added def CategoryTheory.Precoverage.finite

added theorem CategoryTheory.Precoverage.mem_finite_iff

added theorem CategoryTheory.Precoverage.ofArrows_mem_finite

added def CategoryTheory.Pretopology.finite

added theorem CategoryTheory.Pretopology.ofArrows_mem_finite

Modified Mathlib/CategoryTheory/Sites/Sieves.lean

added inductive CategoryTheory.Presieve.map

added def CategoryTheory.Presieve.uncurry

added theorem CategoryTheory.Presieve.uncurry_bind

added theorem CategoryTheory.Presieve.uncurry_ofArrows

added theorem CategoryTheory.Presieve.uncurry_pullbackArrows

added theorem CategoryTheory.Presieve.uncurry_singleton

added theorem CategoryTheory.Sieve.arrows_generate_map_eq_functorPushforward

added theorem CategoryTheory.Sieve.generate_map_eq_functorPushforward