feat(AlgebraicGeometry): Add global preorder instance for schemes (#26204)

In this PR we added a default preorder instance for schemes, defined to be the specialization order as discussed here: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/dimension.20function.20for.20schemes/near/524997376 for discussion 



Co-authored-by: Raph-DG <77658801+Raph-DG@users.noreply.github.com>

Author: Raph-DG

Mathlib/AlgebraicGeometry/AffineSpace.lean

@@ -457,6 +457,17 @@ lemma isIntegralHom_over_iff_isEmpty : IsIntegralHom (𝔸(n; S) ↘ S) ↔ IsEm
 lemma not_isIntegralHom [Nonempty S] [Nonempty n] : ¬ IsIntegralHom (𝔸(n; S) ↘ S) := by
   simp [isIntegralHom_over_iff_isEmpty]
 
+lemma spec_le_iff (R : CommRingCat) (p q : Spec R) :
+   p ≤ q ↔ q.asIdeal ≤ p.asIdeal := by aesop (add simp PrimeSpectrum.le_iff_specializes)
+
+/--
+One should bear this equality in mind when breaking the `Spec R/ PrimeSpectrum R` abstraction
+boundary, since these instances are not definitionally equal.
+-/
+example (R : CommRingCat) :
+  inferInstance (α := Preorder (Spec R)) =
+  inferInstance (α := Preorder (PrimeSpectrum R)ᵒᵈ) := by aesop (add simp spec_le_iff)
+
 end instances
 
 end AffineSpace

Mathlib/AlgebraicGeometry/Scheme.lean

@@ -125,6 +125,13 @@ lemma Hom.continuous {X Y : Scheme} (f : X.Hom Y) : Continuous f.base := f.base.
 protected abbrev sheaf (X : Scheme) :=
   X.toSheafedSpace.sheaf
 
+/--
+We give schemes the specialization preorder by default.
+-/
+instance {X : Scheme.{u}} : Preorder X := specializationPreorder X
+
+lemma le_iff_specializes {X : Scheme.{u}} {a b : X} : a ≤ b ↔ b ⤳ a := by rfl
+
 namespace Hom
 
 variable {X Y : Scheme.{u}} (f : Hom X Y) {U U' : Y.Opens} {V V' : X.Opens}