Commit 2024-10-04 20:24 a0785003

View on Github →

feat(AlgebraicGeometry): add resLE (#17264) Adds a shortcut Scheme.Hom.resLE for the restriction of a morphism of schemes to opens on the source and the target.

Estimated changes

Modified Mathlib/AlgebraicGeometry/OpenImmersion.lean

added theorem AlgebraicGeometry.Scheme.Hom.image_le_image_iff

Modified Mathlib/AlgebraicGeometry/Restrict.lean

added theorem AlgebraicGeometry.Scheme.Hom.le_preimage_resLE_iff

added theorem AlgebraicGeometry.Scheme.Hom.map_resLE

added def AlgebraicGeometry.Scheme.Hom.resLE

added theorem AlgebraicGeometry.Scheme.Hom.resLE_appLE

added theorem AlgebraicGeometry.Scheme.Hom.resLE_comp_resLE

added theorem AlgebraicGeometry.Scheme.Hom.resLE_comp_ι

added theorem AlgebraicGeometry.Scheme.Hom.resLE_congr

added theorem AlgebraicGeometry.Scheme.Hom.resLE_eq_morphismRestrict

added theorem AlgebraicGeometry.Scheme.Hom.resLE_id

added theorem AlgebraicGeometry.Scheme.Hom.resLE_map

added theorem AlgebraicGeometry.Scheme.Hom.resLE_preimage

added theorem AlgebraicGeometry.Scheme.Opens.ι_image_le

modified theorem AlgebraicGeometry.Scheme.restrictFunctor_map_left

Modified Mathlib/AlgebraicGeometry/Scheme.lean

added theorem AlgebraicGeometry.Scheme.Hom.preimage_le_preimage_of_le

Modified Mathlib/CategoryTheory/Comma/Over.lean