Commit 2024-04-30 23:37 ac466445

View on Github →

perf(AlgebraicGeometry.Spec): add explicit universe annotations (#12557) Following #12469 and #12494, we add explicit universe levels in AlgebraicGeometry.Spec to speed up the file now and forestall greater slowdowns with the next version of Lean.

Estimated changes

Modified Mathlib/AlgebraicGeometry/Spec.lean

modified def AlgebraicGeometry.Spec.locallyRingedSpaceMap

modified theorem AlgebraicGeometry.Spec.locallyRingedSpaceMap_comp

modified theorem AlgebraicGeometry.Spec.locallyRingedSpaceMap_id

modified def AlgebraicGeometry.Spec.locallyRingedSpaceObj

modified theorem AlgebraicGeometry.Spec.sheafedSpaceMap_comp

modified theorem AlgebraicGeometry.Spec.sheafedSpaceMap_id

modified def AlgebraicGeometry.Spec.sheafedSpaceObj

modified def AlgebraicGeometry.Spec.toLocallyRingedSpace

modified def AlgebraicGeometry.Spec.toPresheafedSpace

modified theorem AlgebraicGeometry.Spec.toPresheafedSpace_map

modified theorem AlgebraicGeometry.Spec.toPresheafedSpace_map_op

modified theorem AlgebraicGeometry.Spec.toPresheafedSpace_obj

modified theorem AlgebraicGeometry.Spec.toPresheafedSpace_obj_op

modified def AlgebraicGeometry.Spec.toSheafedSpace

modified def AlgebraicGeometry.Spec.toTop

modified def AlgebraicGeometry.Spec.topMap

modified theorem AlgebraicGeometry.Spec.topMap_comp

modified theorem AlgebraicGeometry.Spec.topMap_id

modified def AlgebraicGeometry.Spec.topObj

modified theorem AlgebraicGeometry.Spec_map_localization_isIso

modified theorem AlgebraicGeometry.Spec_Γ_naturality

modified theorem AlgebraicGeometry.localRingHom_comp_stalkIso

modified theorem AlgebraicGeometry.stalkMap_toStalk

modified def AlgebraicGeometry.toSpecΓ