feat(algebraic_geometry/structure_sheaf): Define comap on structure s…

…heaf (#7788)

Defines the comap of a ring homomorphism on the structure sheaves of the prime spectra.



Co-authored-by: justus-springer <50165510+justus-springer@users.noreply.github.com>

src/algebraic_geometry/structure_sheaf.lean

@@ -84,6 +84,15 @@ def is_fraction {U : opens (prime_spectrum.Top R)} (f : Π x : U, localizations
 ∃ (r s : R), ∀ x : U,
   ¬ (s ∈ x.1.as_ideal) ∧ f x * (localization.of _).to_map s = (localization.of _).to_map r
 
+lemma is_fraction.eq_mk' {U : opens (prime_spectrum.Top R)} {f : Π x : U, localizations R x}
+  (hf : is_fraction f) :
+  ∃ (r s : R) , ∀ x : U, ∃ (hs : s ∉ x.1.as_ideal), f x = (localization.of _).mk' r ⟨s, hs⟩ :=
+begin
+  rcases hf with ⟨r, s, h⟩,
+  refine ⟨r, s, λ x, ⟨(h x).1, ((localization_map.mk'_eq_iff_eq_mul _).mpr _).symm⟩⟩,
+  exact (h x).2.symm,
+end
+
 variables (R)
 
 /--
@@ -357,7 +366,7 @@ by rw [mul_comm, const_mul_cancel]
 
 /-- The canonical ring homomorphism interpreting an element of `R` as
 a section of the structure sheaf. -/
-def to_open (U : opens (prime_spectrum.Top R)) :
+@[simps] def to_open (U : opens (prime_spectrum.Top R)) :
   CommRing.of R ⟶ (structure_sheaf R).presheaf.obj (op U) :=
 { to_fun := λ f, ⟨λ x, (localization.of _).to_map f,
     λ x, ⟨U, x.2, 𝟙 _, f, 1, λ y, ⟨(ideal.ne_top_iff_one _).1 y.1.2.1,
@@ -371,10 +380,6 @@ def to_open (U : opens (prime_spectrum.Top R)) :
   to_open R U ≫ (structure_sheaf R).presheaf.map i.op = to_open R V :=
 rfl
 
-@[simp] lemma to_open_apply (U : opens (prime_spectrum.Top R)) (f : R) (x : U) :
-  (to_open R U f).1 x = (localization.of _).to_map f :=
-rfl
-
 lemma to_open_eq_const (U : opens (prime_spectrum.Top R)) (f : R) : to_open R U f =
   const R f 1 U (λ x _, (ideal.ne_top_iff_one _).1 x.2.1) :=
 subtype.eq $ funext $ λ x, eq.symm $ (localization.of _).mk'_one f
@@ -487,7 +492,7 @@ ring_hom.ext_iff.1 (to_stalk_comp_stalk_to_fiber_ring_hom R x) _
 
 /-- The ring isomorphism between the stalk of the structure sheaf of `R` at a point `p`
 corresponding to a prime ideal in `R` and the localization of `R` at `p`. -/
-def stalk_iso (x : prime_spectrum.Top R) :
+@[simps] def stalk_iso (x : prime_spectrum.Top R) :
   (structure_sheaf R).presheaf.stalk x ≅ CommRing.of (localization.at_prime x.as_ideal) :=
 { hom := stalk_to_fiber_ring_hom R x,
   inv := localization_to_stalk R x,
@@ -777,4 +782,161 @@ def basic_open_iso (f : R) : (structure_sheaf R).presheaf.obj (op (basic_open f)
   CommRing.of (localization.away f) :=
 (as_iso (to_basic_open R f)).symm
 
+section comap
+
+variables {R} {S : Type u} [comm_ring S] {P : Type u} [comm_ring P]
+
+/--
+Given a ring homomorphism `f : R →+* S`, an open set `U` of the prime spectrum of `R` and an open
+set `V` of the prime spectrum of `S`, such that `V ⊆ (comap f) ⁻¹' U`, we can push a section `s`
+on `U` to a section on `V`, by composing with `localization.local_ring_hom _ _ f` from the left and
+`comap f` from the right. Explicitly, if `s` evaluates on `comap f p` to `a / b`, its image on `V`
+evaluates on `p` to `f(a) / f(b)`.
+
+At the moment, we work with arbitrary dependent functions `s : Π x : U, localizations R x`. Below,
+we prove the predicate `is_locally_fraction` is preserved by this map, hence it can be extended to
+a morphism between the structure sheaves of `R` and `S`.
+-/
+def structure_sheaf.comap_fun (f : R →+* S) (U : opens (prime_spectrum.Top R))
+  (V : opens (prime_spectrum.Top S)) (hUV : V.1 ⊆ (comap f) ⁻¹' U.1)
+  (s : Π x : U, localizations R x) (y : V) : localizations S y :=
+localization.local_ring_hom (comap f y.1).as_ideal _ f rfl (s ⟨(comap f y.1), hUV y.2⟩ : _)
+
+lemma structure_sheaf.comap_fun_is_locally_fraction (f : R →+* S)
+  (U : opens (prime_spectrum.Top R)) (V : opens (prime_spectrum.Top S))
+  (hUV : V.1 ⊆ (comap f) ⁻¹' U.1) (s : Π x : U, localizations R x)
+  (hs : (is_locally_fraction R).to_prelocal_predicate.pred s) :
+  (is_locally_fraction S).to_prelocal_predicate.pred (structure_sheaf.comap_fun f U V hUV s) :=
+begin
+  rintro ⟨p, hpV⟩,
+  -- Since `s` is locally fraction, we can find a neighborhood `W` of `comap f p` in `U`, such
+  -- that `s = a / b` on `W`, for some ring elements `a, b : R`.
+  rcases hs ⟨comap f p, hUV hpV⟩ with ⟨W, m, iWU, a, b, h_frac⟩,
+  -- We claim that we can write our new section as the fraction `f a / f b` on the neighborhood
+  -- `(comap f) ⁻¹ W ⊓ V` of `p`.
+  refine ⟨opens.comap (comap_continuous f) W ⊓ V, ⟨m, hpV⟩, opens.inf_le_right _ _, f a, f b, _⟩,
+  rintro ⟨q, ⟨hqW, hqV⟩⟩,
+  specialize h_frac ⟨prime_spectrum.comap f q, hqW⟩,
+  refine ⟨h_frac.1, _⟩,
+  dsimp only [structure_sheaf.comap_fun],
+  erw [← localization.local_ring_hom_to_map ((comap f q).as_ideal), ← ring_hom.map_mul,
+    h_frac.2, localization.local_ring_hom_to_map],
+  refl,
+end
+
+/--
+For a ring homomorphism `f : R →+* S` and open sets `U` and `V` of the prime spectra of `R` and
+`S` such that `V ⊆ (comap f) ⁻¹ U`, the induced ring homomorphism from the structure sheaf of `R`
+at `U` to the structure sheaf of `S` at `V`.
+
+Explicitly, this map is given as follows: For a point `p : V`, if the section `s` evaluates on `p`
+to the fraction `a / b`, its image on `V` evaluates on `p` to the fraction `f(a) / f(b)`.
+-/
+def structure_sheaf.comap (f : R →+* S) (U : opens (prime_spectrum.Top R))
+  (V : opens (prime_spectrum.Top S)) (hUV : V.1 ⊆ (comap f) ⁻¹' U.1) :
+  (structure_sheaf R).presheaf.obj (op U) →+* (structure_sheaf S).presheaf.obj (op V) :=
+{ to_fun := λ s, ⟨structure_sheaf.comap_fun f U V hUV s.1,
+    structure_sheaf.comap_fun_is_locally_fraction f U V hUV s.1 s.2⟩,
+  map_one' := subtype.ext $ funext $ λ p, by
+    { rw [subtype.coe_mk, subtype.val_eq_coe, structure_sheaf.comap_fun,
+      (sections_subring R (op U)).coe_one, pi.one_apply, ring_hom.map_one], refl },
+  map_zero' := subtype.ext $ funext $ λ p, by
+    { rw [subtype.coe_mk, subtype.val_eq_coe, structure_sheaf.comap_fun,
+      (sections_subring R (op U)).coe_zero, pi.zero_apply, ring_hom.map_zero], refl },
+  map_add' := λ s t, subtype.ext $ funext $ λ p, by
+    { rw [subtype.coe_mk, subtype.val_eq_coe, structure_sheaf.comap_fun,
+      (sections_subring R (op U)).coe_add, pi.add_apply, ring_hom.map_add], refl },
+  map_mul' := λ s t, subtype.ext $ funext $ λ p, by
+    { rw [subtype.coe_mk, subtype.val_eq_coe, structure_sheaf.comap_fun,
+      (sections_subring R (op U)).coe_mul, pi.mul_apply, ring_hom.map_mul], refl }
+}
+
+@[simp]
+lemma structure_sheaf.comap_apply (f : R →+* S) (U : opens (prime_spectrum.Top R))
+  (V : opens (prime_spectrum.Top S)) (hUV : V.1 ⊆ (comap f) ⁻¹' U.1)
+  (s : (structure_sheaf R).presheaf.obj (op U)) (p : V) :
+  (structure_sheaf.comap f U V hUV s).1 p =
+  localization.local_ring_hom (comap f p.1).as_ideal _ f rfl (s.1 ⟨(comap f p.1), hUV p.2⟩ : _) :=
+rfl
+
+lemma structure_sheaf.comap_const (f : R →+* S) (U : opens (prime_spectrum.Top R))
+  (V : opens (prime_spectrum.Top S)) (hUV : V.1 ⊆ (comap f) ⁻¹' U.1)
+  (a b : R) (hb : ∀ x : prime_spectrum R, x ∈ U → b ∈ x.as_ideal.prime_compl) :
+  structure_sheaf.comap f U V hUV (const R a b U hb) =
+  const S (f a) (f b) V (λ p hpV, hb (comap f p) (hUV hpV)) :=
+subtype.eq $ funext $ λ p,
+begin
+  rw [structure_sheaf.comap_apply, const_apply, const_apply],
+  erw localization.local_ring_hom_mk',
+  refl,
+end
+
+/--
+For an inclusion `i : V ⟶ U` between open sets of the prime spectrum of `R`, the comap of the
+identity from OO_X(U) to OO_X(V) equals as the restriction map of the structure sheaf.
+
+This is a generalization of the fact that, for fixed `U`, the comap of the identity from OO_X(U)
+to OO_X(U) is the identity.
+-/
+lemma structure_sheaf.comap_id_eq_map (U V : opens (prime_spectrum.Top R)) (iVU : V ⟶ U) :
+  structure_sheaf.comap (ring_hom.id R) U V
+    (λ p hpV, le_of_hom iVU $ by rwa prime_spectrum.comap_id) =
+  (structure_sheaf R).presheaf.map iVU.op :=
+ring_hom.ext $ λ s, subtype.eq $ funext $ λ p,
+begin
+  rw structure_sheaf.comap_apply,
+  -- Unfortunately, we cannot use `localization.local_ring_hom_id` here, because
+  -- `comap (ring_hom.id R) p` is not *definitionally* equal to `p`. Instead, we use that we can
+  -- write `s` as a fraction `a/b` in a small neighborhood around `p`. Since
+  -- `comap (ring_hom.id R) p` equals `p`, it is also contained in the same neighborhood, hence
+  -- `s` equals `a/b` there too.
+  obtain ⟨W, hpW, iWU, h⟩ := s.2 (iVU p),
+  obtain ⟨a, b, h'⟩ := h.eq_mk',
+  obtain ⟨hb₁, s_eq₁⟩ := h' ⟨p, hpW⟩,
+  obtain ⟨hb₂, s_eq₂⟩ := h' ⟨comap (ring_hom.id _) p.1, by rwa prime_spectrum.comap_id⟩,
+  dsimp only at s_eq₁ s_eq₂,
+  erw [s_eq₂, localization.local_ring_hom_mk', ← s_eq₁, ← res_apply],
+end
+
+/--
+The comap of the identity is the identity. In this variant of the lemma, two open subsets `U` and
+`V` are given as arguments, together with a proof that `U = V`. This is be useful when `U` and `V`
+are not definitionally equal.
+-/
+lemma structure_sheaf.comap_id (U V : opens (prime_spectrum.Top R)) (hUV : U = V) :
+  structure_sheaf.comap (ring_hom.id R) U V
+    (λ p hpV, by rwa [hUV, prime_spectrum.comap_id]) =
+  eq_to_hom (show (structure_sheaf R).presheaf.obj (op U) = _, by rw hUV) :=
+by erw [structure_sheaf.comap_id_eq_map U V (eq_to_hom hUV.symm), eq_to_hom_op, eq_to_hom_map]
+
+@[simp] lemma structure_sheaf.comap_id' (U : opens (prime_spectrum.Top R)) :
+  structure_sheaf.comap (ring_hom.id R) U U (λ p hpU, by rwa prime_spectrum.comap_id) =
+  ring_hom.id _ :=
+by { rw structure_sheaf.comap_id U U rfl, refl }
+
+lemma structure_sheaf.comap_comp (f : R →+* S) (g : S →+* P) (U : opens (prime_spectrum.Top R))
+  (V : opens (prime_spectrum.Top S)) (W : opens (prime_spectrum.Top P))
+  (hUV : ∀ p ∈ V, comap f p ∈ U) (hVW : ∀ p ∈ W, comap g p ∈ V) :
+  structure_sheaf.comap (g.comp f) U W (λ p hpW, hUV (comap g p) (hVW p hpW)) =
+    (structure_sheaf.comap g V W hVW).comp (structure_sheaf.comap f U V hUV) :=
+ring_hom.ext $ λ s, subtype.eq $ funext $ λ p,
+begin
+  rw structure_sheaf.comap_apply,
+  erw localization.local_ring_hom_comp _ (comap g p.1).as_ideal,
+  -- refl works here, because `comap (g.comp f) p` is defeq to `comap f (comap g p)`
+  refl,
+end
+
+@[elementwise, reassoc] lemma to_open_comp_comap (f : R →+* S) :
+  to_open R ⊤ ≫ structure_sheaf.comap f ⊤ ⊤ (λ p hpV, trivial) =
+  @category_theory.category_struct.comp _ _ (CommRing.of R) (CommRing.of S) _ f (to_open S ⊤) :=
+ring_hom.ext $ λ s, subtype.eq $ funext $ λ p,
+begin
+  simp_rw [comp_apply, structure_sheaf.comap_apply, subtype.val_eq_coe, to_open_apply_coe],
+  erw localization.local_ring_hom_to_map,
+  refl,
+end
+
+end comap
+
 end algebraic_geometry