feat(algebraic_geometry/morphisms/finite_type): Morphisms locally of finite type. (#16124)

erdOne · erdOne · commit 64fc7238fb41 · 2022-10-07T20:10:10.000Z
Co-authored-by: Andrew Yang &lt;36414270+erdOne@users.noreply.github.com&gt;
diff --git a/src/algebraic_geometry/Scheme.lean b/src/algebraic_geometry/Scheme.lean
@@ -119,6 +119,13 @@ begin
   refl
 end
 
+/-- Given a morphism of schemes `f : X ⟶ Y`, and open sets `U ⊆ Y`, `V ⊆ f ⁻¹' U`,
+this is the induced map `Γ(Y, U) ⟶ Γ(X, V)`. -/
+abbreviation hom.app_le {X Y : Scheme}
+  (f : X ⟶ Y) {V : opens X.carrier} {U : opens Y.carrier} (e : V ≤ (opens.map f.1.base).obj U) :
+    Y.presheaf.obj (op U) ⟶ X.presheaf.obj (op V) :=
+f.1.c.app (op U) ≫ X.presheaf.map (hom_of_le e).op
+
 /--
 The spectrum of a commutative ring, as a scheme.
 -/
diff --git a/src/algebraic_geometry/morphisms/finite_type.lean b/src/algebraic_geometry/morphisms/finite_type.lean
@@ -0,0 +1,101 @@
+/-
+Copyright (c) 2022 Andrew Yang. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Andrew Yang
+-/
+import algebraic_geometry.morphisms.ring_hom_properties
+import algebraic_geometry.morphisms.quasi_compact
+import ring_theory.ring_hom.finite_type
+
+/-!
+# Morphisms of finite type
+
+A morphism of schemes `f : X ⟶ Y` is locally of finite type if for each affine `U ⊆ Y` and
+`V ⊆ f ⁻¹' U`, The induced map `Γ(Y, U) ⟶ Γ(X, V)` is of finite type.
+
+A morphism of schemes is of finite type if it is both locally of finite type and quasi-compact.
+
+We show that these properties are local, and are stable under compositions.
+
+-/
+
+noncomputable theory
+
+open category_theory category_theory.limits opposite topological_space
+
+universes v u
+
+namespace algebraic_geometry
+
+variables {X Y : Scheme.{u}} (f : X ⟶ Y)
+
+/--
+A morphism of schemes `f : X ⟶ Y` is locally of finite type if for each affine `U ⊆ Y` and
+`V ⊆ f ⁻¹' U`, The induced map `Γ(Y, U) ⟶ Γ(X, V)` is of finite type.
+-/
+@[mk_iff]
+class locally_of_finite_type (f : X ⟶ Y) : Prop :=
+(finite_type_of_affine_subset :
+  ∀ (U : Y.affine_opens) (V : X.affine_opens) (e : V.1 ≤ (opens.map f.1.base).obj U.1),
+  (f.app_le e).finite_type)
+
+lemma locally_of_finite_type_eq :
+  @locally_of_finite_type = affine_locally @ring_hom.finite_type :=
+begin
+  ext X Y f,
+  rw [locally_of_finite_type_iff, affine_locally_iff_affine_opens_le],
+  exact ring_hom.finite_type_respects_iso
+end
+
+@[priority 900]
+instance locally_of_finite_type_of_is_open_immersion {X Y : Scheme} (f : X ⟶ Y)
+  [is_open_immersion f] : locally_of_finite_type f :=
+locally_of_finite_type_eq.symm ▸ ring_hom.finite_type_is_local.affine_locally_of_is_open_immersion f
+
+lemma locally_of_finite_type_stable_under_composition :
+  morphism_property.stable_under_composition @locally_of_finite_type :=
+locally_of_finite_type_eq.symm ▸
+ring_hom.finite_type_is_local.affine_locally_stable_under_composition
+
+instance locally_of_finite_type_comp {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z)
+  [hf : locally_of_finite_type f] [hg : locally_of_finite_type g] :
+  locally_of_finite_type (f ≫ g) :=
+locally_of_finite_type_stable_under_composition f g hf hg
+
+lemma locally_of_finite_type_of_comp {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z)
+  [hf : locally_of_finite_type (f ≫ g)] :
+  locally_of_finite_type f :=
+begin
+  unfreezingI { revert hf },
+  rw [locally_of_finite_type_eq],
+  apply ring_hom.finite_type_is_local.affine_locally_of_comp,
+  introv H,
+  exactI ring_hom.finite_type.of_comp_finite_type H,
+end
+
+lemma locally_of_finite_type.affine_open_cover_iff {X Y : Scheme.{u}} (f : X ⟶ Y)
+  (𝒰 : Scheme.open_cover.{u} Y) [∀ i, is_affine (𝒰.obj i)]
+  (𝒰' : ∀ i, Scheme.open_cover.{u} ((𝒰.pullback_cover f).obj i))
+  [∀ i j, is_affine ((𝒰' i).obj j)] :
+  locally_of_finite_type f ↔
+    (∀ i j, (Scheme.Γ.map ((𝒰' i).map j ≫ pullback.snd).op).finite_type) :=
+locally_of_finite_type_eq.symm ▸ ring_hom.finite_type_is_local.affine_open_cover_iff f 𝒰 𝒰'
+
+lemma locally_of_finite_type.source_open_cover_iff {X Y : Scheme.{u}} (f : X ⟶ Y)
+  (𝒰 : Scheme.open_cover.{u} X) :
+  locally_of_finite_type f ↔ (∀ i, locally_of_finite_type (𝒰.map i ≫ f)) :=
+locally_of_finite_type_eq.symm ▸ ring_hom.finite_type_is_local.source_open_cover_iff f 𝒰
+
+lemma locally_of_finite_type.open_cover_iff {X Y : Scheme.{u}} (f : X ⟶ Y)
+  (𝒰 : Scheme.open_cover.{u} Y) :
+  locally_of_finite_type f ↔
+    (∀ i, locally_of_finite_type (pullback.snd : pullback f (𝒰.map i) ⟶ _)) :=
+locally_of_finite_type_eq.symm ▸
+  ring_hom.finite_type_is_local.is_local_affine_locally.open_cover_iff f 𝒰
+
+lemma locally_of_finite_type_respects_iso :
+  morphism_property.respects_iso @locally_of_finite_type :=
+locally_of_finite_type_eq.symm ▸ target_affine_locally_respects_iso
+  (source_affine_locally_respects_iso ring_hom.finite_type_respects_iso)
+
+end algebraic_geometry
diff --git a/src/algebraic_geometry/morphisms/ring_hom_properties.lean b/src/algebraic_geometry/morphisms/ring_hom_properties.lean
@@ -175,7 +175,7 @@ lemma affine_locally_iff_affine_opens_le
   (hP : ring_hom.respects_iso @P) {X Y : Scheme} (f : X ⟶ Y) :
   affine_locally @P f ↔
   (∀ (U : Y.affine_opens) (V : X.affine_opens) (e : V.1 ≤ (opens.map f.1.base).obj U.1),
-    P (f.1.c.app (op U) ≫ X.presheaf.map (hom_of_le e).op)) :=
+    P (f.app_le e)) :=
 begin
   apply forall_congr,
   intro U,
@@ -491,6 +491,36 @@ begin
   { intro i, exact H }
 end
 
+lemma affine_locally_of_comp
+  (H : ∀ {R S T : Type.{u}} [comm_ring R] [comm_ring S] [comm_ring T], by exactI
+    ∀ (f : R →+* S) (g : S →+* T), P (g.comp f) → P g)
+  {X Y Z : Scheme} {f : X ⟶ Y} {g : Y ⟶ Z} (h : affine_locally @P (f ≫ g)) :
+  affine_locally @P f :=
+begin
+  let 𝒰 : ∀ i, ((Z.affine_cover.pullback_cover (f ≫ g)).obj i).open_cover,
+  { intro i,
+    refine Scheme.open_cover.bind _ (λ i, Scheme.affine_cover _),
+    apply Scheme.open_cover.pushforward_iso _
+    (pullback_right_pullback_fst_iso g (Z.affine_cover.map i) f).hom,
+    apply Scheme.pullback.open_cover_of_right,
+    exact (pullback g (Z.affine_cover.map i)).affine_cover },
+  haveI h𝒰 : ∀ i j, is_affine ((𝒰 i).obj j), by { dsimp, apply_instance },
+  let 𝒰' := (Z.affine_cover.pullback_cover g).bind (λ i, Scheme.affine_cover _),
+  haveI h𝒰' : ∀ i, is_affine (𝒰'.obj i), by { dsimp, apply_instance },
+  rw hP.affine_open_cover_iff f 𝒰' (λ i, Scheme.affine_cover _),
+  rw hP.affine_open_cover_iff (f ≫ g) Z.affine_cover 𝒰 at h,
+  rintros ⟨i, j⟩ k,
+  dsimp at i j k,
+  specialize h i ⟨j, k⟩,
+  dsimp only [Scheme.open_cover.bind_map, Scheme.open_cover.pushforward_iso_obj,
+    Scheme.pullback.open_cover_of_right_obj, Scheme.open_cover.pushforward_iso_map,
+    Scheme.pullback.open_cover_of_right_map, Scheme.open_cover.bind_obj,
+    Scheme.open_cover.pullback_cover_obj, Scheme.open_cover.pullback_cover_map] at h ⊢,
+  rw [category.assoc, category.assoc, pullback_right_pullback_fst_iso_hom_snd,
+    pullback.lift_snd_assoc, category.assoc, ← category.assoc, op_comp, functor.map_comp] at h,
+  exact H _ _ h,
+end
+
 lemma affine_locally_stable_under_composition :
   (affine_locally @P).stable_under_composition :=
 begin
diff --git a/src/ring_theory/ring_hom/finite_type.lean b/src/ring_theory/ring_hom/finite_type.lean
@@ -84,9 +84,12 @@ begin
     { rw ht, trivial } }
 end
 
-lemma finite_is_local :
+lemma finite_type_is_local :
   property_is_local @finite_type :=
 ⟨localization_finite_type, finite_type_of_localization_span_target,
   finite_type_stable_under_composition, finite_type_holds_for_localization_away⟩
 
+lemma finite_type_respects_iso : ring_hom.respects_iso @ring_hom.finite_type :=
+ring_hom.finite_type_is_local.respects_iso
+
 end ring_hom
