From c9c73b6ad96738467fa56cb18b75cbe4a991ef1e Mon Sep 17 00:00:00 2001
From: Andrew Yang <the.erd.one@gmail.com>
Date: Sun, 20 Oct 2024 17:51:56 +0100
Subject: [PATCH] address comments

---
 .../Morphisms/Separated.lean                  | 42 ++++++++++++-------
 1 file changed, 28 insertions(+), 14 deletions(-)

diff --git a/Mathlib/AlgebraicGeometry/Morphisms/Separated.lean b/Mathlib/AlgebraicGeometry/Morphisms/Separated.lean
index 3c07da47c9aee..7f44de364381e 100644
--- a/Mathlib/AlgebraicGeometry/Morphisms/Separated.lean
+++ b/Mathlib/AlgebraicGeometry/Morphisms/Separated.lean
@@ -15,6 +15,11 @@ import Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer
 
 A morphism of schemes is separated if its diagonal morphism is a closed immmersion.
 
+## Main definitions
+- `AlgebraicGeometry.IsSeparated`: The class of separated morphisms.
+- `AlgebraicGeometry.Scheme.IsSeparated`: The class of separated schemes.
+- `AlgebraicGeometry.IsSeparated.hasAffineProperty`:
+  A morphism is separated iff the preimage of affine opens are separated schemes.
 -/
 
 
@@ -58,7 +63,7 @@ instance stableUnderComposition : MorphismProperty.IsStableUnderComposition @IsS
   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) :=
+instance [IsSeparated f] [IsSeparated g] : IsSeparated (f ≫ g) :=
   stableUnderComposition.comp_mem f g inferInstance inferInstance
 
 instance : MorphismProperty.IsMultiplicative @IsSeparated where
@@ -97,6 +102,8 @@ instance {S T : Scheme.{u}} (f : X ⟶ S) (g : Y ⟶ S) (i : S ⟶ T) [IsSeparat
   IsClosedImmersion.stableUnderBaseChange (pullback_map_diagonal_isPullback f g i)
     inferInstance
 
+/-- Given `f : X ⟶ Y` and `g : Y ⟶ Z` such that `g` is separated, the induced map
+`X ⟶ X ×[Z] Y` is a closed immersion. -/
 instance [IsSeparated g] :
     IsClosedImmersion (pullback.lift (𝟙 _) f (Category.id_comp (f ≫ g))) := by
   rw [← MorphismProperty.cancel_left_of_respectsIso @IsClosedImmersion (pullback.fst f (𝟙 Y))]
@@ -118,37 +125,44 @@ lemma IsSeparated.of_comp [IsSeparated (f ≫ g)] : IsSeparated f := by
   rw [pullback.diagonal_comp] at this
   exact ⟨@IsClosedImmersion.of_comp _ _ _ _ _ this inferInstance⟩
 
-lemma IsSeparated.iff_of_comp [IsSeparated g] : IsSeparated (f ≫ g) ↔ IsSeparated f :=
+lemma IsSeparated.comp_iff [IsSeparated g] : IsSeparated (f ≫ g) ↔ IsSeparated f :=
   ⟨fun _ ↦ .of_comp f g, fun _ ↦ inferInstance⟩
 
 namespace Scheme
 
-/-- A scheme `X` is separated if the diagonal map `X ⟶ X × X` is a closed immersion. -/
+/-- A scheme `X` is separated if it is separated over `⊤_ Scheme`. -/
 @[mk_iff]
 protected class IsSeparated (X : Scheme.{u}) : Prop where
-  isClosedImmersion_prod_lift : IsClosedImmersion (prod.lift (𝟙 X) (𝟙 X))
+  isSeparated_terminal_from : IsSeparated (terminal.from X)
 
-attribute [instance] IsSeparated.isClosedImmersion_prod_lift
+attribute [instance] IsSeparated.isSeparated_terminal_from
 
-lemma isSeparated_iff_isSeparated_terminal {X : Scheme.{u}} :
-    X.IsSeparated ↔ IsSeparated (terminal.from X) := by
+lemma isSeparated_iff_isClosedImmersion_prod_lift {X : Scheme.{u}} :
+    X.IsSeparated ↔ IsClosedImmersion (prod.lift (𝟙 X) (𝟙 X)) := by
   rw [isSeparated_iff, AlgebraicGeometry.isSeparated_iff, iff_iff_eq,
     ← MorphismProperty.cancel_right_of_respectsIso @IsClosedImmersion _ (prodIsoPullback X X).hom]
   congr
   ext : 1 <;> simp
 
-instance (priority := 900) {X : Scheme.{u}} [IsAffine X] : X.IsSeparated := by
-  rw [isSeparated_iff_isSeparated_terminal]
-  infer_instance
+instance [X.IsSeparated] : IsClosedImmersion (prod.lift (𝟙 X) (𝟙 X)) := by
+  rwa [← isSeparated_iff_isClosedImmersion_prod_lift]
 
-instance : HasAffineProperty @IsSeparated fun X _ _ _ ↦ X.IsSeparated := by
-  convert HasAffineProperty.of_isLocalAtTarget @IsSeparated with X Y f hY
-  rw [isSeparated_iff_isSeparated_terminal, ← terminal.comp_from f, IsSeparated.iff_of_comp]
-  rfl
+instance (priority := 900) {X : Scheme.{u}} [IsAffine X] : X.IsSeparated := ⟨inferInstance⟩
+
+instance (priority := 900) [X.IsSeparated] : IsSeparated f := by
+  apply (config := { allowSynthFailures := true }) @IsSeparated.of_comp (g := terminal.from Y)
+  rw [terminal.comp_from]
+  infer_instance
 
 instance (f g : X ⟶ Y) [Y.IsSeparated] : IsClosedImmersion (Limits.equalizer.ι f g) :=
   IsClosedImmersion.stableUnderBaseChange (isPullback_equalizer_prod f g).flip inferInstance
 
 end Scheme
 
+instance IsSeparated.hasAffineProperty :
+    HasAffineProperty @IsSeparated fun X _ _ _ ↦ X.IsSeparated := by
+  convert HasAffineProperty.of_isLocalAtTarget @IsSeparated with X Y f hY
+  rw [Scheme.isSeparated_iff, ← terminal.comp_from f, IsSeparated.comp_iff]
+  rfl
+
 end AlgebraicGeometry