Commit 2024-11-29 12:22 49652777

View on Github →

feat(AlgebraicGeometry): the small site associated to a morphism property (#18945) Given a sufficiently good morphism property P, we define the induced topologies on the category of S-schemes and on the category of S-schemes with P.

Estimated changes

Modified Mathlib.lean

Created Mathlib/AlgebraicGeometry/Sites/Small.lean

added theorem AlgebraicGeometry.Scheme.Cover.overEquiv_generate_toPresieveOver_eq_ofArrows

added def AlgebraicGeometry.Scheme.Cover.toPresieveOver

added def AlgebraicGeometry.Scheme.Cover.toPresieveOverProp

added theorem AlgebraicGeometry.Scheme.Cover.toPresieveOver_le_arrows_iff

added theorem AlgebraicGeometry.Scheme.locallyCoverDense_of_le

added theorem AlgebraicGeometry.Scheme.mem_overGrothendieckTopology

added theorem AlgebraicGeometry.Scheme.mem_smallGrothendieckTopology

added theorem AlgebraicGeometry.Scheme.mem_toGrothendieck_smallPretopology

added theorem AlgebraicGeometry.Scheme.overGrothendieckTopology_eq_toGrothendieck_overPretopology

added def AlgebraicGeometry.Scheme.overPretopology

added theorem AlgebraicGeometry.Scheme.smallGrothendieckTopologyOfLE_eq_toGrothendieck_smallPretopology

added theorem AlgebraicGeometry.Scheme.smallGrothendieckTopology_eq_toGrothendieck_smallPretopology

added def AlgebraicGeometry.Scheme.smallPretopology

Modified Mathlib/CategoryTheory/Sites/Over.lean

added theorem CategoryTheory.Sieve.overEquiv_le_overEquiv_iff

Modified Mathlib/CategoryTheory/Sites/Sieves.lean

added theorem CategoryTheory.Sieve.mem_functorPushforward_iff_of_full

added theorem CategoryTheory.Sieve.mem_functorPushforward_iff_of_full_of_faithful