Commit 2024-10-24 14:10 f72cbf59

View on Github →

feat(AlgebraicGeometry): define immersions (#18154)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/ClosedImmersion.lean

deleted theorem AlgebraicGeometry.IsClosedImmersion.isClosedEmbedding

added theorem AlgebraicGeometry.Scheme.Hom.isClosedEmbedding

Created Mathlib/AlgebraicGeometry/Morphisms/Immersion.lean

added theorem AlgebraicGeometry.IsImmersion.comp_iff

added theorem AlgebraicGeometry.IsImmersion.isImmersion_iff_exists

added theorem AlgebraicGeometry.IsImmersion.of_comp

added theorem AlgebraicGeometry.IsImmersion.stableUnderBaseChange

added def AlgebraicGeometry.Scheme.Hom.coborderRange

added theorem AlgebraicGeometry.Scheme.Hom.isLocallyClosed_range

added def AlgebraicGeometry.Scheme.Hom.liftCoborder

added theorem AlgebraicGeometry.Scheme.Hom.liftCoborder_ι

added theorem AlgebraicGeometry.isImmersion_eq_inf