Commit 2024-06-11 06:33 3e405812

View on Github →

feat(AlgebraicGeometry): definition of separated morphisms (#13698) Definition of separated morphisms.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/ClosedImmersion.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/QuasiSeparated.lean

Created Mathlib/AlgebraicGeometry/Morphisms/Separated.lean

added theorem AlgebraicGeometry.IsSeparated.isSeparated_eq_diagonal_isClosedImmersion

added theorem AlgebraicGeometry.IsSeparated.respectsIso