Commit 2024-11-11 17:19 1881327c

View on Github →

feat(AlgebraicGeometry): the diagonal map is an immersion (#18726) Also shows that injective on points => separated partially from the valuation criterion project

Estimated changes

Modified Mathlib/AlgebraicGeometry/Morphisms/Immersion.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/Separated.lean

added theorem AlgebraicGeometry.Scheme.Pullback.diagonalCoverDiagonalRange_eq_top_of_injective

added theorem AlgebraicGeometry.Scheme.Pullback.range_diagonal_subset_diagonalCoverDiagonalRange

added theorem AlgebraicGeometry.isClosedImmersion_diagonal_restrict_diagonalCoverDiagonalRange

added theorem AlgebraicGeometry.isSeparated_of_injective

Modified Mathlib/AlgebraicGeometry/Pullbacks.lean

added def AlgebraicGeometry.Scheme.Pullback.diagonalCover

added def AlgebraicGeometry.Scheme.Pullback.diagonalCoverDiagonalRange

added theorem AlgebraicGeometry.Scheme.Pullback.diagonalCover_map

added def AlgebraicGeometry.Scheme.Pullback.diagonalRestrictIsoDiagonal