From 23a1a4bd2117e0e4a6391122bcf08d7c2edf6008 Mon Sep 17 00:00:00 2001
From: Christian Merten <christian@merten.dev>
Date: Thu, 17 Oct 2024 22:32:03 +0000
Subject: [PATCH] feat(AlgebraicGeometry): proper morphisms of schemes (#17863)

We define proper morphisms of schemes and show standard stability properties.

Partly from the valuative criterion project.

Co-authored by: Andrew Yang
---
 Mathlib.lean                                  |  1 +
 .../Morphisms/ClosedImmersion.lean            | 14 ++++
 .../Morphisms/FiniteType.lean                 |  3 +
 .../AlgebraicGeometry/Morphisms/Proper.lean   | 69 +++++++++++++++++++
 .../Morphisms/UniversallyClosed.lean          | 12 +++-
 5 files changed, 98 insertions(+), 1 deletion(-)
 create mode 100644 Mathlib/AlgebraicGeometry/Morphisms/Proper.lean

diff --git a/Mathlib.lean b/Mathlib.lean
index 721ac852ea637..6871945d645ea 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -868,6 +868,7 @@ import Mathlib.AlgebraicGeometry.Morphisms.FiniteType
 import Mathlib.AlgebraicGeometry.Morphisms.IsIso
 import Mathlib.AlgebraicGeometry.Morphisms.OpenImmersion
 import Mathlib.AlgebraicGeometry.Morphisms.Preimmersion
+import Mathlib.AlgebraicGeometry.Morphisms.Proper
 import Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
 import Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
 import Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
diff --git a/Mathlib/AlgebraicGeometry/Morphisms/ClosedImmersion.lean b/Mathlib/AlgebraicGeometry/Morphisms/ClosedImmersion.lean
index c78e3b86d608d..932325058e426 100644
--- a/Mathlib/AlgebraicGeometry/Morphisms/ClosedImmersion.lean
+++ b/Mathlib/AlgebraicGeometry/Morphisms/ClosedImmersion.lean
@@ -6,6 +6,7 @@ Authors: Amelia Livingston, Christian Merten, Jonas van der Schaaf
 import Mathlib.AlgebraicGeometry.Morphisms.Preimmersion
 import Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
 import Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
+import Mathlib.AlgebraicGeometry.Morphisms.FiniteType
 import Mathlib.AlgebraicGeometry.ResidueField
 import Mathlib.RingTheory.RingHom.Surjective
 
@@ -269,4 +270,17 @@ lemma IsClosedImmersion.stableUnderBaseChange :
   exact ⟨inferInstance, RingHom.surjective_stableUnderBaseChange.pullback_fst_app_top _
     RingHom.surjective_respectsIso f _ hsurj⟩
 
+/-- Closed immersions are locally of finite type. -/
+instance (priority := 900) {X Y : Scheme.{u}} (f : X ⟶ Y) [h : IsClosedImmersion f] :
+    LocallyOfFiniteType f := by
+  wlog hY : IsAffine Y
+  · rw [IsLocalAtTarget.iff_of_iSup_eq_top (P := @LocallyOfFiniteType) _
+      (iSup_affineOpens_eq_top Y)]
+    intro U
+    have H : IsClosedImmersion (f ∣_ U) := IsLocalAtTarget.restrict h U
+    exact this _ U.2
+  obtain ⟨_, hf⟩ := h.isAffine_surjective_of_isAffine
+  rw [HasRingHomProperty.iff_of_isAffine (P := @LocallyOfFiniteType)]
+  exact RingHom.FiniteType.of_surjective (Scheme.Hom.app f ⊤) hf
+
 end AlgebraicGeometry
diff --git a/Mathlib/AlgebraicGeometry/Morphisms/FiniteType.lean b/Mathlib/AlgebraicGeometry/Morphisms/FiniteType.lean
index def22435c69c0..a5bbcc0abb5f2 100644
--- a/Mathlib/AlgebraicGeometry/Morphisms/FiniteType.lean
+++ b/Mathlib/AlgebraicGeometry/Morphisms/FiniteType.lean
@@ -59,6 +59,9 @@ theorem locallyOfFiniteType_of_comp {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z)
     [LocallyOfFiniteType (f ≫ g)] : LocallyOfFiniteType f :=
   HasRingHomProperty.of_comp (fun _ _ ↦ RingHom.FiniteType.of_comp_finiteType) ‹_›
 
+instance : MorphismProperty.IsMultiplicative @LocallyOfFiniteType where
+  id_mem _ := inferInstance
+
 open scoped TensorProduct in
 lemma locallyOfFiniteType_stableUnderBaseChange :
     MorphismProperty.StableUnderBaseChange @LocallyOfFiniteType :=
diff --git a/Mathlib/AlgebraicGeometry/Morphisms/Proper.lean b/Mathlib/AlgebraicGeometry/Morphisms/Proper.lean
new file mode 100644
index 0000000000000..b54565bfb3af8
--- /dev/null
+++ b/Mathlib/AlgebraicGeometry/Morphisms/Proper.lean
@@ -0,0 +1,69 @@
+/-
+Copyright (c) 2024 Christian Merten, Andrew Yang. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Christian Merten, Andrew Yang
+-/
+import Mathlib.AlgebraicGeometry.Morphisms.Separated
+import Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed
+import Mathlib.AlgebraicGeometry.Morphisms.FiniteType
+
+/-!
+
+# Proper morphisms
+
+A morphism of schemes is proper if it is separated, universally closed and (locally) of finite type.
+Note that we don't require quasi-compact, since this is implied by universally closed (TODO).
+
+-/
+
+
+noncomputable section
+
+open CategoryTheory
+
+universe u
+
+namespace AlgebraicGeometry
+
+variable {X Y : Scheme.{u}} (f : X ⟶ Y)
+
+/-- A morphism is proper if it is separated, universally closed and locally of finite type. -/
+@[mk_iff]
+class IsProper extends IsSeparated f, UniversallyClosed f, LocallyOfFiniteType f : Prop where
+
+lemma isProper_eq : @IsProper =
+    (@IsSeparated ⊓ @UniversallyClosed : MorphismProperty Scheme) ⊓ @LocallyOfFiniteType := by
+  ext X Y f
+  rw [isProper_iff, ← and_assoc]
+  rfl
+
+namespace IsProper
+
+instance : MorphismProperty.RespectsIso @IsProper := by
+  rw [isProper_eq]
+  infer_instance
+
+instance stableUnderComposition : MorphismProperty.IsStableUnderComposition @IsProper := by
+  rw [isProper_eq]
+  infer_instance
+
+instance : MorphismProperty.IsMultiplicative @IsProper := by
+  rw [isProper_eq]
+  infer_instance
+
+instance (priority := 900) [IsClosedImmersion f] : IsProper f where
+
+lemma stableUnderBaseChange : MorphismProperty.StableUnderBaseChange @IsProper := by
+  rw [isProper_eq]
+  exact MorphismProperty.StableUnderBaseChange.inf
+    (MorphismProperty.StableUnderBaseChange.inf
+      IsSeparated.stableUnderBaseChange universallyClosed_stableUnderBaseChange)
+    locallyOfFiniteType_stableUnderBaseChange
+
+instance : IsLocalAtTarget @IsProper := by
+  rw [isProper_eq]
+  infer_instance
+
+end IsProper
+
+end AlgebraicGeometry
diff --git a/Mathlib/AlgebraicGeometry/Morphisms/UniversallyClosed.lean b/Mathlib/AlgebraicGeometry/Morphisms/UniversallyClosed.lean
index 6a5489d992476..166651638bcaa 100644
--- a/Mathlib/AlgebraicGeometry/Morphisms/UniversallyClosed.lean
+++ b/Mathlib/AlgebraicGeometry/Morphisms/UniversallyClosed.lean
@@ -3,7 +3,7 @@ Copyright (c) 2022 Andrew Yang. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Andrew Yang
 -/
-import Mathlib.AlgebraicGeometry.Morphisms.Constructors
+import Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
 import Mathlib.Topology.LocalAtTarget
 
 /-!
@@ -40,6 +40,13 @@ class UniversallyClosed (f : X ⟶ Y) : Prop where
 theorem universallyClosed_eq : @UniversallyClosed = universally (topologically @IsClosedMap) := by
   ext X Y f; rw [universallyClosed_iff]
 
+instance (priority := 900) [IsClosedImmersion f] : UniversallyClosed f := by
+  rw [universallyClosed_eq]
+  intro X' Y' i₁ i₂ f' hf
+  have hf' : IsClosedImmersion f' :=
+    IsClosedImmersion.stableUnderBaseChange hf.flip inferInstance
+  exact hf'.base_closed.isClosedMap
+
 theorem universallyClosed_respectsIso : RespectsIso @UniversallyClosed :=
   universallyClosed_eq.symm ▸ universally_respectsIso (topologically @IsClosedMap)
 
@@ -59,6 +66,9 @@ instance universallyClosedTypeComp {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z)
     [hf : UniversallyClosed f] [hg : UniversallyClosed g] : UniversallyClosed (f ≫ g) :=
   comp_mem _ _ _ hf hg
 
+instance : MorphismProperty.IsMultiplicative @UniversallyClosed where
+  id_mem _ := inferInstance
+
 instance universallyClosed_fst {X Y Z : Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [hg : UniversallyClosed g] :
     UniversallyClosed (pullback.fst f g) :=
   universallyClosed_stableUnderBaseChange.fst f g hg