Commit 2025-08-21 08:45 b37bb2f3

View on Github →

feat(AlgebraicGeometry): jointly surjective topology (#28617) We define jointlySurjectiveTopology to have the same condition as jointlySurjectivePretopology, which is the new name of the former surjectiveFamiliesPretopology.

Estimated changes

Modified Mathlib/AlgebraicGeometry/Sites/MorphismProperty.lean

added def AlgebraicGeometry.Scheme.jointlySurjectivePretopology

added def AlgebraicGeometry.Scheme.jointlySurjectiveTopology

added theorem AlgebraicGeometry.Scheme.jointlySurjectiveTopology_eq_toGrothendieck_jointlySurjectivePretopology

added theorem AlgebraicGeometry.Scheme.mem_jointlySurjectiveTopology_iff_jointlySurjectivePretopology

deleted def AlgebraicGeometry.Scheme.surjectiveFamiliesPretopology

Modified Mathlib/CategoryTheory/Sites/Grothendieck.lean

added theorem CategoryTheory.GrothendieckTopology.coe_copy

added def CategoryTheory.GrothendieckTopology.copy

added theorem CategoryTheory.GrothendieckTopology.copy_eq

added theorem CategoryTheory.GrothendieckTopology.sieves_copy