Commit 2025-02-04 09:16 2dd5bb2d

View on Github →

feat(AlgebraicGeometry): the diagonal of an unramified morphism is an open immersion (#21386)

Estimated changes

Modified Mathlib/AlgebraicGeometry/Morphisms/Basic.lean

added theorem AlgebraicGeometry.IsLocalAtTarget.of_range_subset_iSup

Modified Mathlib/AlgebraicGeometry/Morphisms/FormallyUnramified.lean

added theorem AlgebraicGeometry.FormallyUnramified.AlgebraicGeometry.FormallyUnramified.isOpenImmersion_diagonal

Modified Mathlib/AlgebraicGeometry/Restrict.lean

added theorem AlgebraicGeometry.Scheme.Opens.isoOfLE_hom_ι

added theorem AlgebraicGeometry.Scheme.Opens.isoOfLE_inv_ι