Commit 2024-11-06 12:25 89c20f6a

View on Github →

feat(AlgebraicGeometry): typeclasses for S-schemes (#18321)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/AlgebraicGeometry/Limits.lean

Created Mathlib/AlgebraicGeometry/Over.lean

Modified Mathlib/AlgebraicGeometry/ResidueField.lean

Modified Mathlib/AlgebraicGeometry/Restrict.lean

Modified Mathlib/AlgebraicGeometry/Stalk.lean

Created Mathlib/CategoryTheory/Comma/OverClass.lean

added def CategoryTheory.CanonicallyOverClass.Simps.over

added def CategoryTheory.OverClass.Simps.over

added def CategoryTheory.OverClass.asOver

added theorem CategoryTheory.comp_over

added theorem CategoryTheory.homIsOver_of_isOverTower

added def CategoryTheory.over

Modified Mathlib/RingTheory/LocalRing/ResidueField/Basic.lean

added theorem LocalRing.residue_surjective