Commit 2025-05-31 08:21 3f45597c

View on Github →

chore(AlgebraicGeometry/Gluing): generalize universes in glueMorphisms (#25130)

Estimated changes

Modified Mathlib/AlgebraicGeometry/Cover/MorphismProperty.lean

added def AlgebraicGeometry.Scheme.Cover.reindex

added def AlgebraicGeometry.Scheme.Cover.ulift

Modified Mathlib/AlgebraicGeometry/Gluing.lean

modified def AlgebraicGeometry.Scheme.Cover.glueMorphisms

modified theorem AlgebraicGeometry.Scheme.Cover.hom_ext

modified theorem AlgebraicGeometry.Scheme.Cover.ι_glueMorphisms