From d951eef6bb39b3b78cbd1fba9c515c3770a9d20a Mon Sep 17 00:00:00 2001
From: Christian Merten <christian@merten.dev>
Date: Thu, 17 Oct 2024 10:54:51 +0000
Subject: [PATCH] feat(AlgebraicGeometry): stability properties of separated
 (#17861)

Separated is multiplicative, stable under base change and local at the target.
---
 .../Morphisms/Separated.lean                  | 21 ++++++++++++++++---
 1 file changed, 18 insertions(+), 3 deletions(-)

diff --git a/Mathlib/AlgebraicGeometry/Morphisms/Separated.lean b/Mathlib/AlgebraicGeometry/Morphisms/Separated.lean
index 5831774a682e8..369855b7c262d 100644
--- a/Mathlib/AlgebraicGeometry/Morphisms/Separated.lean
+++ b/Mathlib/AlgebraicGeometry/Morphisms/Separated.lean
@@ -16,9 +16,6 @@ A morphism of schemes is separated if its diagonal morphism is a closed immmersi
 
 ## TODO
 
-- Show separated is stable under composition and base change (this is immediate if
-  we show that closed immersions are stable under base change).
-- Show separated is local at the target.
 - Show affine morphisms are separated.
 
 -/
@@ -60,6 +57,24 @@ instance : MorphismProperty.RespectsIso @IsSeparated := by
 
 instance (priority := 900) [IsSeparated f] : QuasiSeparated f where
 
+instance stableUnderComposition : MorphismProperty.IsStableUnderComposition @IsSeparated := by
+  rw [isSeparated_eq_diagonal_isClosedImmersion]
+  exact MorphismProperty.diagonal_isStableUnderComposition IsClosedImmersion.stableUnderBaseChange
+
+instance {Z : Scheme.{u}} (g : Y ⟶ Z) [IsSeparated f] [IsSeparated g] : IsSeparated (f ≫ g) :=
+  stableUnderComposition.comp_mem f g inferInstance inferInstance
+
+instance : MorphismProperty.IsMultiplicative @IsSeparated where
+  id_mem _ := inferInstance
+
+lemma stableUnderBaseChange : MorphismProperty.StableUnderBaseChange @IsSeparated := by
+  rw [isSeparated_eq_diagonal_isClosedImmersion]
+  exact MorphismProperty.StableUnderBaseChange.diagonal IsClosedImmersion.stableUnderBaseChange
+
+instance : IsLocalAtTarget @IsSeparated := by
+  rw [isSeparated_eq_diagonal_isClosedImmersion]
+  infer_instance
+
 end IsSeparated
 
 end AlgebraicGeometry