Commit 2024-05-24 11:14 32e6a4b3

View on Github →

feat(AlgebraicGeometry/Morphisms): define closed immersions (#12917) Defines closed immersions of schemes.

Estimated changes

Modified Mathlib.lean

Created Mathlib/AlgebraicGeometry/Morphisms/ClosedImmersion.lean

added theorem AlgebraicGeometry.IsClosedImmersion.closedEmbedding

added theorem AlgebraicGeometry.IsClosedImmersion.of_comp

added theorem AlgebraicGeometry.IsClosedImmersion.respectsIso

added theorem AlgebraicGeometry.IsClosedImmersion.spec_of_surjective

added theorem AlgebraicGeometry.IsClosedImmersion.surjective_stalkMap

Modified Mathlib/RingTheory/LocalProperties.lean

added theorem surjective_localRingHom_of_surjective