feat: port Topology.Sheaves.Operations (#4731)

Co-authored-by: Jujian Zhang <jujian.zhang1998@outlook.com>
Co-authored-by: Scott Morrison <scott.morrison@anu.edu.au>
Co-authored-by: Parcly Taxel <reddeloostw@gmail.com>

Mathlib.lean

@@ -2957,6 +2957,7 @@ import Mathlib.Topology.Sheaves.Init
 import Mathlib.Topology.Sheaves.Limits
 import Mathlib.Topology.Sheaves.LocalPredicate
 import Mathlib.Topology.Sheaves.LocallySurjective
+import Mathlib.Topology.Sheaves.Operations
 import Mathlib.Topology.Sheaves.PUnit
 import Mathlib.Topology.Sheaves.Presheaf
 import Mathlib.Topology.Sheaves.PresheafOfFunctions

Mathlib/Algebra/Category/Ring/Adjunctions.lean

@@ -47,7 +47,9 @@ theorem free_obj_coe {α : Type u} : (free.obj α : Type u) = MvPolynomial α 
   rfl
 #align CommRing.free_obj_coe CommRingCat.free_obj_coe
 
-@[simp]
+-- Porting note: `simpNF` should not trigger on `rfl` lemmas.
+-- see https://github.com/leanprover-community/mathlib4/issues/5081
+@[simp, nolint simpNF]
 theorem free_map_coe {α β : Type u} {f : α → β} : ⇑(free.map f) = ⇑(rename f) :=
   rfl
 #align CommRing.free_map_coe CommRingCat.free_map_coe

Mathlib/Algebra/Category/Ring/Basic.lean

@@ -69,11 +69,17 @@ instance : ConcreteCategory SemiRingCat := by
 instance : CoeSort SemiRingCat (Type _) where
   coe X := X.α
 
-instance (X : SemiRingCat) : Semiring X := X.str
+-- Porting note : Hinting to Lean that `forget R` and `R` are the same
+unif_hint forget_obj_eq_coe (R : SemiRingCat) where ⊢
+  (forget SemiRingCat).obj R ≟ R
 
--- porting note: this instance was not necessary in mathlib
-instance {X Y : SemiRingCat} : CoeFun (X ⟶ Y) fun _ => X → Y where
-  coe (f : X →+* Y) := f
+instance instSemiring (X : SemiRingCat) : Semiring X := X.str
+
+instance instSemiring' (X : SemiRingCat) : Semiring <| (forget SemiRingCat).obj X := X.str
+
+-- Porting note: added
+instance instRingHomClass {X Y : SemiRingCat} : RingHomClass (X ⟶ Y) X Y :=
+  RingHom.instRingHomClass
 
 -- porting note: added
 lemma coe_id {X : SemiRingCat} : (𝟙 X : X → X) = id := rfl
@@ -131,7 +137,9 @@ def ofHom {R S : Type u} [Semiring R] [Semiring S] (f : R →+* S) : of R ⟶ of
 set_option linter.uppercaseLean3 false in
 #align SemiRing.of_hom SemiRingCat.ofHom
 
-@[simp]
+-- Porting note: `simpNF` should not trigger on `rfl` lemmas.
+-- see https://github.com/leanprover-community/mathlib4/issues/5081
+@[simp, nolint simpNF]
 theorem ofHom_apply {R S : Type u} [Semiring R] [Semiring S] (f : R →+* S) (x : R) :
     ofHom f x = f x :=
   rfl
@@ -181,9 +189,17 @@ instance : CoeSort RingCat (Type _) where
 
 instance (X : RingCat) : Ring X := X.str
 
--- porting note: this instance was not necessary in mathlib
-instance {X Y : RingCat} : CoeFun (X ⟶ Y) fun _ => X → Y where
-  coe (f : X →+* Y) := f
+-- Porting note : Hinting to Lean that `forget R` and `R` are the same
+unif_hint forget_obj_eq_coe (R : RingCat) where ⊢
+  (forget RingCat).obj R ≟ R
+
+instance instRing (X : RingCat) : Ring X := X.str
+
+instance instRing' (X : RingCat) : Ring <| (forget RingCat).obj X := X.str
+
+-- Porting note: added
+instance instRingHomClass {X Y : RingCat} : RingHomClass (X ⟶ Y) X Y :=
+  RingHom.instRingHomClass
 
 -- porting note: added
 lemma coe_id {X : RingCat} : (𝟙 X : X → X) = id := rfl
@@ -274,9 +290,18 @@ instance : CoeSort CommSemiRingCat (Type _) where
 
 instance (X : CommSemiRingCat) : CommSemiring X := X.str
 
--- porting note: this instance was not necessary in mathlib
-instance {X Y : CommSemiRingCat} : CoeFun (X ⟶ Y) fun _ => X → Y where
-  coe (f : X →+* Y) := f
+-- Porting note : Hinting to Lean that `forget R` and `R` are the same
+unif_hint forget_obj_eq_coe (R : CommSemiRingCat) where ⊢
+  (forget CommSemiRingCat).obj R ≟ R
+
+instance instCommSemiring (X : CommSemiRingCat) : CommSemiring X := X.str
+
+instance instCommSemiring' (X : CommSemiRingCat) : CommSemiring <| (forget CommSemiRingCat).obj X :=
+  X.str
+
+-- Porting note: added
+instance instRingHomClass {X Y : CommSemiRingCat} : RingHomClass (X ⟶ Y) X Y :=
+  RingHom.instRingHomClass
 
 -- porting note: added
 lemma coe_id {X : CommSemiRingCat} : (𝟙 X : X → X) = id := rfl
@@ -382,11 +407,17 @@ instance : ConcreteCategory CommRingCat := by
 instance : CoeSort CommRingCat (Type _) where
   coe X := X.α
 
-instance (X : CommRingCat) : CommRing X := X.str
+-- Porting note : Hinting to Lean that `forget R` and `R` are the same
+unif_hint forget_obj_eq_coe (R : CommRingCat) where ⊢
+  (forget CommRingCat).obj R ≟ R
+
+instance instCommRing (X : CommRingCat) : CommRing X := X.str
+
+instance instCommRing' (X : CommRingCat) : CommRing <| (forget CommRingCat).obj X := X.str
 
--- porting note: this instance was not necessary in mathlib
-instance {X Y : CommRingCat} : CoeFun (X ⟶ Y) fun _ => X → Y where
-  coe (f : X →+* Y) := f
+-- Porting note: added
+instance instRingHomClass {X Y : CommRingCat} : RingHomClass (X ⟶ Y) X Y :=
+  RingHom.instRingHomClass
 
 -- porting note: added
 lemma coe_id {X : CommRingCat} : (𝟙 X : X → X) = id := rfl

Mathlib/Algebra/Hom/Ring.lean

@@ -418,7 +418,7 @@ See note [implicit instance arguments].
 
 variable {_ : NonAssocSemiring α} {_ : NonAssocSemiring β}
 
-instance : RingHomClass (α →+* β) α β where
+instance instRingHomClass : RingHomClass (α →+* β) α β where
   coe f := f.toFun
   coe_injective' f g h := by
     cases f

Mathlib/Topology/Sheaves/Operations.lean

@@ -0,0 +1,145 @@
+/-
+Copyright (c) 2022 Andrew Yang. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Andrew Yang
+
+! This file was ported from Lean 3 source module topology.sheaves.operations
+! leanprover-community/mathlib commit 70fd9563a21e7b963887c9360bd29b2393e6225a
+! Please do not edit these lines, except to modify the commit id
+! if you have ported upstream changes.
+-/
+import Mathlib.Algebra.Category.Ring.Instances
+import Mathlib.Algebra.Category.Ring.FilteredColimits
+import Mathlib.RingTheory.Localization.Basic
+import Mathlib.Topology.Sheaves.Stalks
+
+/-!
+
+# Operations on sheaves
+
+## Main definition
+
+- `SubmonoidPresheaf` : A subpresheaf with a submonoid structure on each of the components.
+- `LocalizationPresheaf` : The localization of a presheaf of commrings at a `SubmonoidPresheaf`.
+- `TotalQuotientPresheaf` : The presheaf of total quotient rings.
+
+-/
+
+-- Porting note: all aligns here start with `Top.`
+set_option linter.uppercaseLean3 false
+
+open scoped nonZeroDivisors
+
+open TopologicalSpace Opposite CategoryTheory
+
+universe v u w
+
+namespace TopCat
+
+namespace Presheaf
+
+variable {X : TopCat.{w}} {C : Type u} [Category.{v} C] [ConcreteCategory C]
+
+attribute [local instance 1000] ConcreteCategory.hasCoeToSort
+
+/-- A subpresheaf with a submonoid structure on each of the components. -/
+structure SubmonoidPresheaf [∀ X : C, MulOneClass X] [∀ X Y : C, MonoidHomClass (X ⟶ Y) X Y]
+    (F : X.Presheaf C) where
+  obj : ∀ U, Submonoid (F.obj U)
+  map : ∀ {U V : (Opens X)ᵒᵖ} (i : U ⟶ V), obj U ≤ (obj V).comap (F.map i)
+#align Top.presheaf.submonoid_presheaf TopCat.Presheaf.SubmonoidPresheaf
+
+variable {F : X.Presheaf CommRingCat.{w}} (G : F.SubmonoidPresheaf)
+
+/-- The localization of a presheaf of `CommRing`s with respect to a `SubmonoidPresheaf`. -/
+protected noncomputable def SubmonoidPresheaf.localizationPresheaf : X.Presheaf CommRingCat where
+  obj U := CommRingCat.of <| Localization (G.obj U)
+  map {U V} i := CommRingCat.ofHom <| IsLocalization.map _ (F.map i) (G.map i)
+  map_id U := by
+    simp_rw [F.map_id]
+    ext x
+    -- Porting note : `M` and `S` needs to be specified manually
+    exact IsLocalization.map_id (M := G.obj U) (S := Localization (G.obj U)) x
+  map_comp {U V W} i j := by
+    delta CommRingCat.ofHom CommRingCat.of Bundled.of
+    simp_rw [F.map_comp, CommRingCat.comp_eq_ring_hom_comp]
+    rw [IsLocalization.map_comp_map]
+#align Top.presheaf.submonoid_presheaf.localization_presheaf TopCat.Presheaf.SubmonoidPresheaf.localizationPresheaf
+
+-- Porting note : this is instance can't be synthesized
+instance (U) : Algebra ((forget CommRingCat).obj (F.obj U)) (G.localizationPresheaf.obj U) :=
+  show Algebra _ (Localization (G.obj U)) from inferInstance
+
+-- Porting note : this is instance can't be synthesized
+instance (U) : IsLocalization (G.obj U) (G.localizationPresheaf.obj U) :=
+  show IsLocalization (G.obj U) (Localization (G.obj U)) from inferInstance
+
+/-- The map into the localization presheaf. -/
+@[simps app]
+def SubmonoidPresheaf.toLocalizationPresheaf : F ⟶ G.localizationPresheaf where
+  app U := CommRingCat.ofHom <| algebraMap (F.obj U) (Localization <| G.obj U)
+  naturality {_ _} i := (IsLocalization.map_comp (G.map i)).symm
+#align Top.presheaf.submonoid_presheaf.to_localization_presheaf TopCat.Presheaf.SubmonoidPresheaf.toLocalizationPresheaf
+
+instance epi_toLocalizationPresheaf : Epi G.toLocalizationPresheaf :=
+  @NatTrans.epi_of_epi_app _ _ _ _ _ _ G.toLocalizationPresheaf fun U => Localization.epi' (G.obj U)
+
+variable (F)
+
+/-- Given a submonoid at each of the stalks, we may define a submonoid presheaf consisting of
+sections whose restriction onto each stalk falls in the given submonoid. -/
+@[simps]
+noncomputable def submonoidPresheafOfStalk (S : ∀ x : X, Submonoid (F.stalk x)) :
+    F.SubmonoidPresheaf where
+  obj U := ⨅ x : U.unop, Submonoid.comap (F.germ x) (S x)
+  map {U V} i := by
+    intro s hs
+    simp only [Submonoid.mem_comap, Submonoid.mem_iInf] at hs ⊢
+    intro x
+    change (F.map i.unop.op ≫ F.germ x) s ∈ _
+    rw [F.germ_res]
+    exact hs _
+#align Top.presheaf.submonoid_presheaf_of_stalk TopCat.Presheaf.submonoidPresheafOfStalk
+
+noncomputable instance : Inhabited F.SubmonoidPresheaf :=
+  ⟨F.submonoidPresheafOfStalk fun _ => ⊥⟩
+
+/-- The localization of a presheaf of `CommRing`s at locally non-zero-divisor sections. -/
+noncomputable def totalQuotientPresheaf : X.Presheaf CommRingCat.{w} :=
+  (F.submonoidPresheafOfStalk fun x => (F.stalk x)⁰).localizationPresheaf
+#align Top.presheaf.total_quotient_presheaf TopCat.Presheaf.totalQuotientPresheaf
+
+/-- The map into the presheaf of total quotient rings -/
+noncomputable def toTotalQuotientPresheaf : F ⟶ F.totalQuotientPresheaf :=
+  SubmonoidPresheaf.toLocalizationPresheaf _
+#align Top.presheaf.to_total_quotient_presheaf TopCat.Presheaf.toTotalQuotientPresheaf
+
+-- Porting note : deriving `Epi` failed
+instance : Epi (toTotalQuotientPresheaf F) := epi_toLocalizationPresheaf _
+
+instance (F : X.Sheaf CommRingCat.{w}) : Mono F.presheaf.toTotalQuotientPresheaf := by
+  -- Porting note : was an `apply (config := { synthAssignedInstances := false })`
+  suffices : ∀ (U : (Opens ↑X)ᵒᵖ), Mono (F.presheaf.toTotalQuotientPresheaf.app U)
+  . apply NatTrans.mono_of_mono_app
+  intro U
+  apply ConcreteCategory.mono_of_injective
+  dsimp [toTotalQuotientPresheaf, CommRingCat.ofHom]
+  -- Porting note : this is a hack to make the `refine` below works
+  set m := _
+  change Function.Injective (algebraMap _ (Localization m))
+  change Function.Injective (algebraMap (F.presheaf.obj U) _)
+  haveI : IsLocalization _ (Localization m) := Localization.isLocalization
+  -- Porting note : `M` and `S` need to be specified manually, so used a hack to save some typing
+  refine IsLocalization.injective (M := m) (S := Localization m) ?_
+  intro s hs t e
+  apply section_ext F (unop U)
+  intro x
+  rw [map_zero]
+  apply Submonoid.mem_iInf.mp hs x
+  -- Porting note : added `dsimp` to make `rw ←map_mul` work
+  dsimp
+  rw [←map_mul, e, map_zero]
+
+end Presheaf
+
+end TopCat