[Merged by Bors] - feat(ring_theory,algebraic_geometry): Miscellaneous lemmas/def/typo corrections

src/algebraic_geometry/locally_ringed_space.lean

@@ -13,9 +13,6 @@ import data.equiv.transfer_instance
 We define (bundled) locally ringed spaces (as `SheafedSpace CommRing` along with the fact that the
 stalks are local rings), and morphisms between these (morphisms in `SheafedSpace` with
 `is_local_ring_hom` on the stalk maps).
-
-## Future work
-* Define the restriction along an open embedding
 -/
 
 universes v u

src/algebraic_geometry/prime_spectrum/basic.lean

@@ -520,6 +520,14 @@ begin
     exact zero_locus_anti_mono (set.singleton_subset_iff.mpr hfs) }
 end
 
+lemma is_basis_basic_opens :
+  topological_space.opens.is_basis (set.range (@basic_open R _)) :=
+begin
+  unfold topological_space.opens.is_basis,
+  convert is_topological_basis_basic_opens,
+  rw ← set.range_comp,
+end
+
 lemma is_compact_basic_open (f : R) : is_compact (basic_open f : set (prime_spectrum R)) :=
 is_compact_of_finite_subfamily_closed $ λ ι Z hZc hZ,
 begin
@@ -579,3 +587,22 @@ by rw [← as_ideal_le_as_ideal, ← zero_locus_vanishing_ideal_eq_closure,
 end order
 
 end prime_spectrum
+
+
+namespace local_ring
+
+variables (R) [local_ring R]
+
+/--
+The closed point in the prime spectrum of a local ring.
+-/
+def closed_point : prime_spectrum R :=
+⟨maximal_ideal R, (maximal_ideal.is_maximal R).is_prime⟩
+
+variable {R}
+
+lemma local_hom_iff_comap_closed_point {S : Type v} [comm_ring S] [local_ring S]
+  {f : R →+* S} : is_local_ring_hom f ↔ (closed_point S).comap f = closed_point R :=
+by { rw [(local_hom_tfae f).out 0 4, subtype.ext_iff], refl }
+
+end local_ring

src/algebraic_geometry/structure_sheaf.lean

@@ -973,7 +973,7 @@ end
 @[elementwise, reassoc] lemma to_open_comp_comap (f : R →+* S)
   (U : opens (prime_spectrum.Top R)) :
   to_open R U ≫ comap f U (opens.comap (comap_continuous f) U) (λ _, id) =
-  CommRing.of_hom f ≫ (to_open S _) :=
+  CommRing.of_hom f ≫ to_open S _ :=
 ring_hom.ext $ λ s, subtype.eq $ funext $ λ p,
 begin
   simp_rw [comp_apply, comap_apply, subtype.val_eq_coe],

src/category_theory/sites/sheaf_of_types.lean

@@ -45,7 +45,7 @@ Now given a Grothendieck topology `J`, `P` is a sheaf if it is a sheaf for every
 topology. See `is_sheaf`.
 
 In the case where the topology is generated by a basis, it suffices to check `P` is a sheaf for
-every sieve in the pretopology. See `is_sheaf_pretopology`.
+every presieve in the pretopology. See `is_sheaf_pretopology`.
 
 We also provide equivalent conditions to satisfy alternate definitions given in the literature.
 

src/category_theory/structured_arrow.lean

@@ -11,7 +11,7 @@ import category_theory.limits.shapes.terminal
 # The category of "structured arrows"
 
 For `T : C ⥤ D`, a `T`-structured arrow with source `S : D`
-is just a morphism `S ⟶ T.obj Y`, for some `Y : D`.
+is just a morphism `S ⟶ T.obj Y`, for some `Y : C`.
 
 These form a category with morphisms `g : Y ⟶ Y'` making the obvious diagram commute.
 

src/ring_theory/ideal/local_ring.lean

@@ -225,6 +225,28 @@ end
 namespace local_ring
 variables [comm_ring R] [local_ring R] [comm_ring S] [local_ring S]
 
+/--
+A ring homomorphism between local rings is a local ring hom iff it reflects units,
+i.e. any preimage of a unit is still a unit. https://stacks.math.columbia.edu/tag/07BJ
+-/
+theorem local_hom_tfae (f : R →+* S) :
+  tfae [is_local_ring_hom f,
+        f '' (maximal_ideal R).1 ⊆ maximal_ideal S,
+        (maximal_ideal R).map f ≤ maximal_ideal S,
+        maximal_ideal R ≤ (maximal_ideal S).comap f,
+        (maximal_ideal S).comap f = maximal_ideal R] :=
+begin
+  tfae_have : 1 → 2, rintros _ _ ⟨a,ha,rfl⟩,
+    resetI, exact map_nonunit f a ha,
+  tfae_have : 2 → 4, exact set.image_subset_iff.1,
+  tfae_have : 3 ↔ 4, exact ideal.map_le_iff_le_comap,
+  tfae_have : 4 → 1, intro h, fsplit, exact λ x, not_imp_not.1 (@h x),
+  tfae_have : 1 → 5, intro, resetI, ext,
+    exact not_iff_not.2 (is_unit_map_iff f x),
+  tfae_have : 5 → 4, exact λ h, le_of_eq h.symm,
+  tfae_finish,
+end
+
 variable (R)
 /-- The residue field of a local ring is the quotient of the ring by its maximal ideal. -/
 def residue_field := (maximal_ideal R).quotient

src/ring_theory/localization.lean

@@ -585,6 +585,17 @@ lemma ring_equiv_of_ring_equiv_mk' {j : R ≃+* P} (H : M.map j.to_monoid_hom =
     mk' Q (j x) ⟨j y, show j y ∈ T, from H ▸ set.mem_image_of_mem j y.2⟩ :=
 map_mk' _ _ _
 
+lemma iso_comp {S T : CommRing}
+  [l : algebra R S] [h : is_localization M S] (f : S ≅ T) :
+  @is_localization _ _ M T _ (f.hom.comp l.to_ring_hom).to_algebra :=
+{ map_units := let hm := h.1 in
+    λ t, is_unit.map f.hom.to_monoid_hom (hm t),
+  surj := let hs := h.2 in λ t, let ⟨⟨r,s⟩,he⟩ := hs (f.inv t) in ⟨ ⟨r,s⟩,
+  by { convert congr_arg f.hom he, rw [ring_hom.map_mul,
+       ←category_theory.comp_apply, category_theory.iso.inv_hom_id], refl } ⟩,
+  eq_iff_exists := let he := h.3 in λ t t', by { rw ← he, split,
+    apply f.CommRing_iso_to_ring_equiv.injective, exact congr_arg f.hom } }
+
 end map
 
 section alg_equiv

src/topology/sheaves/sheaf_condition/sites.lean

@@ -4,9 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Justus Springer
 -/
 
-import category_theory.sites.sheaf
 import category_theory.sites.spaces
 import topology.sheaves.sheaf
+import category_theory.sites.dense_subsite
 
 /-!
 
@@ -35,7 +35,7 @@ naturality lemmas relating the two fork diagrams to each other.
 
 noncomputable theory
 
-universes u v
+universes u v w
 
 namespace Top.presheaf
 
@@ -473,3 +473,52 @@ begin
 end
 
 end Top.presheaf
+
+namespace Top.opens
+
+open category_theory topological_space
+
+variables {X : Top} {ι : Type*}
+
+lemma cover_dense_iff_is_basis [category ι] (B : ι ⥤ opens X) :
+  cover_dense (opens.grothendieck_topology X) B ↔ opens.is_basis (set.range B.obj) :=
+begin
+  rw opens.is_basis_iff_nbhd,
+  split, intros hd U x hx, rcases hd.1 U x hx with ⟨V,f,⟨i,f₁,f₂,hc⟩,hV⟩,
+  exact ⟨B.obj i, ⟨i,rfl⟩, f₁.le hV, f₂.le⟩,
+  intro hb, split, intros U x hx, rcases hb hx with ⟨_,⟨i,rfl⟩,hx,hi⟩,
+  exact ⟨B.obj i, ⟨⟨hi⟩⟩, ⟨⟨i, 𝟙 _, ⟨⟨hi⟩⟩, rfl⟩⟩, hx⟩,
+end
+
+lemma cover_dense_induced_functor {B : ι → opens X} (h : opens.is_basis (set.range B)) :
+  cover_dense (opens.grothendieck_topology X) (induced_functor B) :=
+(cover_dense_iff_is_basis _).2 h
+
+end Top.opens
+
+namespace Top.sheaf
+
+open category_theory topological_space Top opposite
+
+variables {C : Type u} [category.{v} C] [limits.has_products C]
+variables {X : Top.{v}} {ι : Type*} {B : ι → opens X}
+variables (F : presheaf C X) (F' : sheaf C X) (h : opens.is_basis (set.range B))
+
+/-- If a family `B` of open sets forms a basis of the topology on `X`, and if `F'`
+    is a sheaf on `X`, then a homomorphism between a presheaf `F` on `X` and `F'`
+    is equivalent to a homomorphism between their restrictions to the indexing type
+    `ι` of `B`, with the induced category structure on `ι`. -/
+def restrict_hom_equiv_hom :
+  ((induced_functor B).op ⋙ F ⟶ (induced_functor B).op ⋙ F'.1) ≃ (F ⟶ F'.1) :=
+@cover_dense.restrict_hom_equiv_hom _ _ _ _ _ _ _ _ (opens.cover_dense_induced_functor h)
+  _ F ((presheaf.Sheaf_spaces_to_sheaf_sites C X).obj F')
+
+@[simp] lemma extend_hom_app (α : ((induced_functor B).op ⋙ F ⟶ (induced_functor B).op ⋙ F'.1))
+  (i : ι) : (restrict_hom_equiv_hom F F' h α).app (op (B i)) = α.app (op i) :=
+by { nth_rewrite 1 ← (restrict_hom_equiv_hom F F' h).left_inv α, refl }
+
+include h
+lemma hom_ext {α β : F ⟶ F'.1} (he : ∀ i, α.app (op (B i)) = β.app (op (B i))) : α = β :=
+by { apply (restrict_hom_equiv_hom F F' h).symm.injective, ext i, exact he i.unop }
+
+end Top.sheaf