Commit 2026-06-01 14:37 8dd7853d

View on Github →

perf(AlgebraicGeometry): specialize index type in AffineSpace to Type u (#39970) The AffineSpace file is notoriously slow and making the index type be in the same universe as the base scheme cuts instructions in half. In case it is necessary, we can still ULift to obtain the old functionality.

Estimated changes

Modified Mathlib/AlgebraicGeometry/AffineSpace.lean

modified def AlgebraicGeometry.AffineSpace.SpecIso

modified theorem AlgebraicGeometry.AffineSpace.SpecIso_hom_appTop

modified theorem AlgebraicGeometry.AffineSpace.SpecIso_inv_appTop_coord

modified theorem AlgebraicGeometry.AffineSpace.SpecIso_inv_over

modified def AlgebraicGeometry.AffineSpace.functor

modified theorem AlgebraicGeometry.AffineSpace.isPullback_map

modified def AlgebraicGeometry.AffineSpace.map

modified def AlgebraicGeometry.AffineSpace.mapSpecMap

modified theorem AlgebraicGeometry.AffineSpace.map_SpecMap

modified theorem AlgebraicGeometry.AffineSpace.map_appTop_coord

modified theorem AlgebraicGeometry.AffineSpace.map_over

modified theorem AlgebraicGeometry.AffineSpace.map_reindex

modified theorem AlgebraicGeometry.AffineSpace.map_toSpecMvPoly

modified def AlgebraicGeometry.AffineSpace.reindex

modified theorem AlgebraicGeometry.AffineSpace.reindex_appTop_coord

modified theorem AlgebraicGeometry.AffineSpace.reindex_comp

modified theorem AlgebraicGeometry.AffineSpace.reindex_over

modified def AlgebraicGeometry.AffineSpace.toSpecMvPoly

modified def AlgebraicGeometry.AffineSpace