Commit 2026-05-27 15:58 8d95dbc1

View on Github →

feat(AlgebraicGeometry/Restrict): a few more restriction lemmas (#39442) These will be used later to define composition of rational maps in #39445.

Estimated changes

Modified Mathlib/AlgebraicGeometry/Restrict.lean

added theorem AlgebraicGeometry.Scheme.Hom.isoImage_hom_homOfLE

added theorem AlgebraicGeometry.Scheme.Hom.isoImage_inv_homOfLE

added theorem AlgebraicGeometry.Scheme.Hom.isoImage_preimage_hom_homOfLE

added theorem AlgebraicGeometry.Scheme.Opens.isoImage_ι_inv_ι

added theorem AlgebraicGeometry.isoImage_ι_inv_morphismRestrict_homOfLE

added theorem AlgebraicGeometry.morphismRestrict_homOfLE

added theorem AlgebraicGeometry.morphismRestrict_homOfLE_isoImage_ι_hom

added theorem AlgebraicGeometry.morphismRestrict_morphismRestrict_ι_isoImage_hom

added theorem AlgebraicGeometry.morphismRestrict_ι_image_ι_isoImage_inv