Commit 2025-09-08 18:25 6cf9d4e6

View on Github →

feat(CategoryTheory/Sites/MorphismProperty): add induced coverage (#28778) We add the (pre)coverage induced by a morphism property and show the induced topology is the same as the one induced by MorphismProperty.pretopology. This will be used in the upcoming refactor of Scheme.Cover, which will be built upon Precoverage.ZeroHypercover.

Estimated changes

Modified Mathlib/AlgebraicGeometry/Sites/MorphismProperty.lean

Modified Mathlib/CategoryTheory/MorphismProperty/Limits.lean

Modified Mathlib/CategoryTheory/Sites/Coverage.lean

added theorem CategoryTheory.Coverage.mem_toGrothendieck

added theorem CategoryTheory.Pretopology.mem_toCoverage

added theorem CategoryTheory.Pretopology.toGrothendieck_toCoverage

Modified Mathlib/CategoryTheory/Sites/MorphismProperty.lean

added def CategoryTheory.MorphismProperty.coverage

added theorem CategoryTheory.MorphismProperty.coverage_eq_toCoverage_pretopology

added theorem CategoryTheory.MorphismProperty.grothendieckTopology_eq_toGrothendieck_pretopology

added theorem CategoryTheory.MorphismProperty.ofArrows_mem_precoverage

added def CategoryTheory.MorphismProperty.precoverage

added theorem CategoryTheory.MorphismProperty.precoverage_inf

added theorem CategoryTheory.MorphismProperty.precoverage_monotone

modified theorem CategoryTheory.MorphismProperty.pretopology_inf

deleted theorem CategoryTheory.MorphismProperty.pretopology_le

added theorem CategoryTheory.MorphismProperty.pretopology_monotone