perf: speed up some algebraic geometry with explicit universes (#12494)

leanprover-community · Apr 29, 2024 · 888ba02 · 888ba02
1 parent a547a94
commit 888ba02
Show file tree

Hide file tree

Showing 3 changed files with 5 additions and 3 deletions.
diff --git a/Mathlib/AlgebraicGeometry/AffineScheme.lean b/Mathlib/AlgebraicGeometry/AffineScheme.lean
@@ -245,7 +245,7 @@ theorem isBasis_basicOpen (X : Scheme) [IsAffine X] :
 
 namespace IsAffineOpen
 
-variable {X Y : Scheme} {U : Opens X} (hU : IsAffineOpen U) (f : X.presheaf.obj (op U))
+variable {X Y : Scheme.{u}} {U : Opens X} (hU : IsAffineOpen U) (f : X.presheaf.obj (op U))
 
 local notation "𝖲𝗉𝖾𝖼 𝓞ₓ(U)" => Scheme.Spec.obj (op <| X.presheaf.obj <| op U)
 

diff --git a/Mathlib/AlgebraicGeometry/FunctionField.lean b/Mathlib/AlgebraicGeometry/FunctionField.lean
@@ -106,7 +106,7 @@ instance functionField_isScalarTower [IrreducibleSpace X.carrier] (U : Opens X.c
   rw [X.presheaf.germ_stalkSpecializes]
 #align algebraic_geometry.function_field_is_scalar_tower AlgebraicGeometry.functionField_isScalarTower
 
-noncomputable instance (R : CommRingCat) [IsDomain R] :
+noncomputable instance (R : CommRingCat.{u}) [IsDomain R] :
     Algebra R (Scheme.Spec.obj <| op R).functionField :=
   RingHom.toAlgebra <| by change CommRingCat.of R ⟶ _; apply StructureSheaf.toStalk
 

diff --git a/Mathlib/AlgebraicGeometry/Properties.lean b/Mathlib/AlgebraicGeometry/Properties.lean
@@ -23,6 +23,8 @@ We provide some basic properties of schemes
   are reduced.
 -/
 
+universe u
+
 
 open TopologicalSpace Opposite CategoryTheory CategoryTheory.Limits TopCat
 
@@ -89,7 +91,7 @@ theorem isReducedOfOpenImmersion {X Y : Scheme} (f : X ⟶ Y) [H : IsOpenImmersi
       Y.presheaf.obj _ ≅ _).symm.commRingCatIsoToRingEquiv.injective
 #align algebraic_geometry.is_reduced_of_open_immersion AlgebraicGeometry.isReducedOfOpenImmersion
 
-instance {R : CommRingCat} [H : _root_.IsReduced R] : IsReduced (Scheme.Spec.obj <| op R) := by
+instance {R : CommRingCat.{u}} [H : _root_.IsReduced R] : IsReduced (Scheme.Spec.obj <| op R) := by
   apply (config := { allowSynthFailures := true }) isReducedOfStalkIsReduced
   intro x; dsimp
   have : _root_.IsReduced (CommRingCat.of <| Localization.AtPrime (PrimeSpectrum.asIdeal x)) := by