Commit 2023-06-15 03:08 8183aac8

View on Github →

feat: relax universe constraint in AlgebraicGeometry/SheafedSpace and AlgebraicGeometry/RingedSpace (#5047)

Estimated changes

Modified Mathlib/AlgebraicGeometry/LocallyRingedSpace.lean

modified structure AlgebraicGeometry.LocallyRingedSpace.Hom

modified theorem AlgebraicGeometry.LocallyRingedSpace.comp_val_c

Modified Mathlib/AlgebraicGeometry/RingedSpace.lean

Modified Mathlib/AlgebraicGeometry/SheafedSpace.lean

modified def AlgebraicGeometry.SheafedSpace.forgetToPresheafedSpace

modified theorem AlgebraicGeometry.SheafedSpace.id_base

modified def AlgebraicGeometry.SheafedSpace.restrict

modified def AlgebraicGeometry.SheafedSpace.sheaf

modified structure AlgebraicGeometry.SheafedSpace