feat(algebraic_geometry/Spec): (f∗ 𝒪ₛ)ₚ is just the localization Sₚ for affine f : Spec S ⟶ Spec R (#17471)

Author: erdOne

src/algebra/module/localized_module.lean

@@ -964,6 +964,31 @@ begin
   exact ⟨⟨m, s⟩, mk'_eq_iff.mpr e.symm⟩
 end
 
+section algebra
+
+lemma mk_of_algebra {R S S' : Type*} [comm_ring R] [comm_ring S] [comm_ring S']
+  [algebra R S] [algebra R S'] (M : submonoid R) (f : S →ₐ[R] S')
+  (h₁ : ∀ x ∈ M, is_unit (algebra_map R S' x))
+  (h₂ : ∀ y, ∃ (x : S × M), x.2 • y = f x.1)
+  (h₃ : ∀ x, f x = 0 → ∃ m : M, m • x = 0) :
+  is_localized_module M f.to_linear_map :=
+begin
+  replace h₃ := λ x, iff.intro (h₃ x) (λ ⟨⟨m, hm⟩, e⟩, (h₁ m hm).mul_left_cancel $
+    by { rw ← algebra.smul_def, simpa [submonoid.smul_def] using f.congr_arg e }),
+  constructor,
+  { intro x,
+    rw module.End_is_unit_iff,
+    split,
+    { rintros a b (e : x • a = x • b), simp_rw [submonoid.smul_def, algebra.smul_def] at e,
+      exact (h₁ x x.2).mul_left_cancel e },
+    { intro a, refine ⟨((h₁ x x.2).unit⁻¹ : _) * a, _⟩, change (x : R) • (_ * a) = _,
+      rw [algebra.smul_def, ← mul_assoc, is_unit.mul_coe_inv, one_mul] } },
+  { exact h₂ },
+  { intros, dsimp, rw [eq_comm, ← sub_eq_zero, ← map_sub, h₃], simp_rw [smul_sub, sub_eq_zero] },
+end
+
+end algebra
+
 end is_localized_module
 
 end is_localized_module

src/algebraic_geometry/Spec.lean

@@ -9,6 +9,7 @@ import logic.equiv.transfer_instance
 import ring_theory.localization.localization_localization
 import topology.sheaves.sheaf_condition.sites
 import topology.sheaves.functors
+import algebra.module.localized_module
 
 /-!
 # $Spec$ as a functor to locally ringed spaces.
@@ -257,5 +258,104 @@ begin
   apply_instance
 end
 
+namespace structure_sheaf
+
+variables {R S : CommRing.{u}} (f : R ⟶ S) (p : prime_spectrum R)
+
+/--
+For an algebra `f : R →+* S`, this is the ring homomorphism `S →+* (f∗ 𝒪ₛ)ₚ` for a `p : Spec R`.
+This is shown to be the localization at `p` in `is_localized_module_to_pushforward_stalk_alg_hom`.
+-/
+def to_pushforward_stalk :
+  S ⟶ (Spec.Top_map f _* (structure_sheaf S).1).stalk p :=
+structure_sheaf.to_open S ⊤ ≫
+  @Top.presheaf.germ _ _ _ _ (Spec.Top_map f _* (structure_sheaf S).1) ⊤ ⟨p, trivial⟩
+
+@[reassoc]
+lemma to_pushforward_stalk_comp :
+  f ≫ structure_sheaf.to_pushforward_stalk f p =
+  structure_sheaf.to_stalk R p ≫
+    (Top.presheaf.stalk_functor _ _).map (Spec.SheafedSpace_map f).c :=
+begin
+  rw structure_sheaf.to_stalk,
+  erw category.assoc,
+  rw Top.presheaf.stalk_functor_map_germ,
+  exact Spec_Γ_naturality_assoc f _,
+end
+
+instance : algebra R ((Spec.Top_map f _* (structure_sheaf S).1).stalk p) :=
+(f ≫ structure_sheaf.to_pushforward_stalk f p).to_algebra
+
+lemma algebra_map_pushforward_stalk :
+  algebra_map R ((Spec.Top_map f _* (structure_sheaf S).1).stalk p) =
+    f ≫ structure_sheaf.to_pushforward_stalk f p := rfl
+
+variables (R S) [algebra R S]
+
+/--
+This is the `alg_hom` version of `to_pushforward_stalk`, which is the map `S ⟶ (f∗ 𝒪ₛ)ₚ` for some
+algebra `R ⟶ S` and some `p : Spec R`.
+-/
+@[simps]
+def to_pushforward_stalk_alg_hom :
+  S →ₐ[R] (Spec.Top_map (algebra_map R S) _* (structure_sheaf S).1).stalk p :=
+{ commutes' := λ _, rfl, ..(structure_sheaf.to_pushforward_stalk (algebra_map R S) p) }
+
+.
+lemma is_localized_module_to_pushforward_stalk_alg_hom_aux (y) :
+  ∃ (x : S × p.as_ideal.prime_compl), x.2 • y = to_pushforward_stalk_alg_hom R S p x.1 :=
+begin
+  obtain ⟨U, hp, s, e⟩ := Top.presheaf.germ_exist _ _ y,
+  obtain ⟨_, ⟨r, rfl⟩, hpr, hrU⟩ := prime_spectrum.is_topological_basis_basic_opens
+    .exists_subset_of_mem_open (show p ∈ U.1, from hp) U.2,
+  change prime_spectrum.basic_open r ≤ U at hrU,
+  replace e := ((Spec.Top_map (algebra_map R S) _* (structure_sheaf S).1)
+    .germ_res_apply (hom_of_le hrU) ⟨p, hpr⟩ _).trans e,
+  set s' := (Spec.Top_map (algebra_map R S) _* (structure_sheaf S).1).map (hom_of_le hrU).op s
+    with h,
+  rw ← h at e,
+  clear_value s', clear_dependent U,
+  obtain ⟨⟨s, ⟨_, n, rfl⟩⟩, hsn⟩ := @is_localization.surj _ _ _
+    _ _ _ (structure_sheaf.is_localization.to_basic_open S $ algebra_map R S r) s',
+  refine ⟨⟨s, ⟨r, hpr⟩ ^ n⟩, _⟩,
+  rw [submonoid.smul_def, algebra.smul_def, algebra_map_pushforward_stalk, to_pushforward_stalk,
+    comp_apply, comp_apply],
+  iterate 2 { erw ← (Spec.Top_map (algebra_map R S) _* (structure_sheaf S).1).germ_res_apply
+    (hom_of_le le_top) ⟨p, hpr⟩ },
+  rw [← e, ← map_mul, mul_comm],
+  dsimp only [subtype.coe_mk] at hsn,
+  rw ← map_pow (algebra_map R S) at hsn,
+  congr' 1
+end
+
+instance is_localized_module_to_pushforward_stalk_alg_hom :
+  is_localized_module p.as_ideal.prime_compl (to_pushforward_stalk_alg_hom R S p).to_linear_map :=
+begin
+  apply is_localized_module.mk_of_algebra,
+  { intros x hx, rw [algebra_map_pushforward_stalk, to_pushforward_stalk_comp, comp_apply],
+    exact (is_localization.map_units ((structure_sheaf R).presheaf.stalk p) ⟨x, hx⟩).map _ },
+  { apply is_localized_module_to_pushforward_stalk_alg_hom_aux },
+  { intros x hx,
+    rw [to_pushforward_stalk_alg_hom_apply, ring_hom.to_fun_eq_coe,
+      ← (to_pushforward_stalk (algebra_map R S) p).map_zero, to_pushforward_stalk, comp_apply,
+      comp_apply, map_zero] at hx,
+    obtain ⟨U, hpU, i₁, i₂, e⟩ := Top.presheaf.germ_eq _ _ _ _ _ _ hx,
+    obtain ⟨_, ⟨r, rfl⟩, hpr, hrU⟩ := prime_spectrum.is_topological_basis_basic_opens
+      .exists_subset_of_mem_open (show p ∈ U.1, from hpU) U.2,
+    change prime_spectrum.basic_open r ≤ U at hrU,
+    apply_fun (Spec.Top_map (algebra_map R S) _* (structure_sheaf S).1).map (hom_of_le hrU).op at e,
+    simp only [Top.presheaf.pushforward_obj_map, functor.op_map, map_zero, ← comp_apply,
+      to_open_res] at e,
+    have : to_open S (prime_spectrum.basic_open $ algebra_map R S r) x = 0,
+    { refine eq.trans _ e, refl },
+    have := (@is_localization.mk'_one _ _ _
+      _ _ _ (structure_sheaf.is_localization.to_basic_open S $ algebra_map R S r) x).trans this,
+    obtain ⟨⟨_, n, rfl⟩, e⟩ := (is_localization.mk'_eq_zero_iff _ _).mp this,
+    refine ⟨⟨r, hpr⟩ ^ n, _⟩,
+    rw [submonoid.smul_def, algebra.smul_def, submonoid.coe_pow, subtype.coe_mk, mul_comm, map_pow],
+    exact e },
+end
+
+end structure_sheaf
 
 end algebraic_geometry