[GOAL]
X : TopCat
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ConcreteCategory C
F : Presheaf CommRingCat X
G : SubmonoidPresheaf F
U : (Opens ↑X)ᵒᵖ
⊢ { obj := fun U => CommRingCat.of (Localization (obj G U)),
          map := fun {U V} i =>
            CommRingCat.ofHom
              (IsLocalization.map (Localization (obj G V)) (F.map i)
                (_ : obj G U ≤ Submonoid.comap (F.map i) (obj G V))) }.map
      (𝟙 U) =
    𝟙
      ({ obj := fun U => CommRingCat.of (Localization (obj G U)),
            map := fun {U V} i =>
              CommRingCat.ofHom
                (IsLocalization.map (Localization (obj G V)) (F.map i)
                  (_ : obj G U ≤ Submonoid.comap (F.map i) (obj G V))) }.obj
        U)
[PROOFSTEP]
simp_rw [F.map_id]
[GOAL]
X : TopCat
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ConcreteCategory C
F : Presheaf CommRingCat X
G : SubmonoidPresheaf F
U : (Opens ↑X)ᵒᵖ
⊢ CommRingCat.ofHom
      (IsLocalization.map (Localization (obj G U)) (𝟙 (F.obj U))
        (_ : obj G U ≤ Submonoid.comap (𝟙 (F.obj U)) (obj G U))) =
    𝟙 (CommRingCat.of (Localization (obj G U)))
[PROOFSTEP]
ext x
[GOAL]
case w
X : TopCat
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ConcreteCategory C
F : Presheaf CommRingCat X
G : SubmonoidPresheaf F
U : (Opens ↑X)ᵒᵖ
x : (forget CommRingCat).obj (CommRingCat.of (Localization (obj G U)))
⊢ ↑(CommRingCat.ofHom
          (IsLocalization.map (Localization (obj G U)) (𝟙 (F.obj U))
            (_ : obj G U ≤ Submonoid.comap (𝟙 (F.obj U)) (obj G U))))
      x =
    ↑(𝟙 (CommRingCat.of (Localization (obj G U)))) x
[PROOFSTEP]
exact IsLocalization.map_id (M := G.obj U) (S := Localization (G.obj U)) x
[GOAL]
X : TopCat
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ConcreteCategory C
F : Presheaf CommRingCat X
G : SubmonoidPresheaf F
U V W : (Opens ↑X)ᵒᵖ
i : U ⟶ V
j : V ⟶ W
⊢ { obj := fun U => CommRingCat.of (Localization (obj G U)),
          map := fun {U V} i =>
            CommRingCat.ofHom
              (IsLocalization.map (Localization (obj G V)) (F.map i)
                (_ : obj G U ≤ Submonoid.comap (F.map i) (obj G V))) }.map
      (i ≫ j) =
    { obj := fun U => CommRingCat.of (Localization (obj G U)),
            map := fun {U V} i =>
              CommRingCat.ofHom
                (IsLocalization.map (Localization (obj G V)) (F.map i)
                  (_ : obj G U ≤ Submonoid.comap (F.map i) (obj G V))) }.map
        i ≫
      { obj := fun U => CommRingCat.of (Localization (obj G U)),
            map := fun {U V} i =>
              CommRingCat.ofHom
                (IsLocalization.map (Localization (obj G V)) (F.map i)
                  (_ : obj G U ≤ Submonoid.comap (F.map i) (obj G V))) }.map
        j
[PROOFSTEP]
delta CommRingCat.ofHom CommRingCat.of Bundled.of
[GOAL]
X : TopCat
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ConcreteCategory C
F : Presheaf CommRingCat X
G : SubmonoidPresheaf F
U V W : (Opens ↑X)ᵒᵖ
i : U ⟶ V
j : V ⟶ W
⊢ { obj := fun U => Bundled.mk (Localization (obj G U)),
          map := fun {U V} i =>
            IsLocalization.map (Localization (obj G V)) (F.map i)
              (_ : obj G U ≤ Submonoid.comap (F.map i) (obj G V)) }.map
      (i ≫ j) =
    { obj := fun U => Bundled.mk (Localization (obj G U)),
            map := fun {U V} i =>
              IsLocalization.map (Localization (obj G V)) (F.map i)
                (_ : obj G U ≤ Submonoid.comap (F.map i) (obj G V)) }.map
        i ≫
      { obj := fun U => Bundled.mk (Localization (obj G U)),
            map := fun {U V} i =>
              IsLocalization.map (Localization (obj G V)) (F.map i)
                (_ : obj G U ≤ Submonoid.comap (F.map i) (obj G V)) }.map
        j
[PROOFSTEP]
simp_rw [F.map_comp, CommRingCat.comp_eq_ring_hom_comp]
[GOAL]
X : TopCat
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ConcreteCategory C
F : Presheaf CommRingCat X
G : SubmonoidPresheaf F
U V W : (Opens ↑X)ᵒᵖ
i : U ⟶ V
j : V ⟶ W
⊢ IsLocalization.map (Localization (obj G W)) (RingHom.comp (F.map j) (F.map i))
      (_ : obj G U ≤ Submonoid.comap (RingHom.comp (F.map j) (F.map i)) (obj G W)) =
    RingHom.comp
      (IsLocalization.map (Localization (obj G W)) (F.map j) (_ : obj G V ≤ Submonoid.comap (F.map j) (obj G W)))
      (IsLocalization.map (Localization (obj G V)) (F.map i) (_ : obj G U ≤ Submonoid.comap (F.map i) (obj G V)))
[PROOFSTEP]
rw [IsLocalization.map_comp_map]
[GOAL]
X : TopCat
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ConcreteCategory C
F : Presheaf CommRingCat X
G : SubmonoidPresheaf F
S : (x : ↑X) → Submonoid ↑(stalk F x)
U V : (Opens ↑X)ᵒᵖ
i : U ⟶ V
⊢ (fun U => ⨅ (x : { x // x ∈ U.unop }), Submonoid.comap (germ F x) (S ↑x)) U ≤
    Submonoid.comap (F.map i) ((fun U => ⨅ (x : { x // x ∈ U.unop }), Submonoid.comap (germ F x) (S ↑x)) V)
[PROOFSTEP]
intro s hs
[GOAL]
X : TopCat
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ConcreteCategory C
F : Presheaf CommRingCat X
G : SubmonoidPresheaf F
S : (x : ↑X) → Submonoid ↑(stalk F x)
U V : (Opens ↑X)ᵒᵖ
i : U ⟶ V
s : (forget CommRingCat).obj (F.obj U)
hs : s ∈ (fun U => ⨅ (x : { x // x ∈ U.unop }), Submonoid.comap (germ F x) (S ↑x)) U
⊢ s ∈ Submonoid.comap (F.map i) ((fun U => ⨅ (x : { x // x ∈ U.unop }), Submonoid.comap (germ F x) (S ↑x)) V)
[PROOFSTEP]
simp only [Submonoid.mem_comap, Submonoid.mem_iInf] at hs ⊢
[GOAL]
X : TopCat
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ConcreteCategory C
F : Presheaf CommRingCat X
G : SubmonoidPresheaf F
S : (x : ↑X) → Submonoid ↑(stalk F x)
U V : (Opens ↑X)ᵒᵖ
i : U ⟶ V
s : (forget CommRingCat).obj (F.obj U)
hs : ∀ (i : { x // x ∈ U.unop }), ↑(germ F i) s ∈ S ↑i
⊢ ∀ (i_1 : { x // x ∈ V.unop }), ↑(germ F i_1) (↑(F.map i) s) ∈ S ↑i_1
[PROOFSTEP]
intro x
[GOAL]
X : TopCat
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ConcreteCategory C
F : Presheaf CommRingCat X
G : SubmonoidPresheaf F
S : (x : ↑X) → Submonoid ↑(stalk F x)
U V : (Opens ↑X)ᵒᵖ
i : U ⟶ V
s : (forget CommRingCat).obj (F.obj U)
hs : ∀ (i : { x // x ∈ U.unop }), ↑(germ F i) s ∈ S ↑i
x : { x // x ∈ V.unop }
⊢ ↑(germ F x) (↑(F.map i) s) ∈ S ↑x
[PROOFSTEP]
change (F.map i.unop.op ≫ F.germ x) s ∈ _
[GOAL]
X : TopCat
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ConcreteCategory C
F : Presheaf CommRingCat X
G : SubmonoidPresheaf F
S : (x : ↑X) → Submonoid ↑(stalk F x)
U V : (Opens ↑X)ᵒᵖ
i : U ⟶ V
s : (forget CommRingCat).obj (F.obj U)
hs : ∀ (i : { x // x ∈ U.unop }), ↑(germ F i) s ∈ S ↑i
x : { x // x ∈ V.unop }
⊢ ↑(F.map i.unop.op ≫ germ F x) s ∈ S ↑x
[PROOFSTEP]
rw [F.germ_res]
[GOAL]
X : TopCat
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ConcreteCategory C
F : Presheaf CommRingCat X
G : SubmonoidPresheaf F
S : (x : ↑X) → Submonoid ↑(stalk F x)
U V : (Opens ↑X)ᵒᵖ
i : U ⟶ V
s : (forget CommRingCat).obj (F.obj U)
hs : ∀ (i : { x // x ∈ U.unop }), ↑(germ F i) s ∈ S ↑i
x : { x // x ∈ V.unop }
⊢ ↑(germ F ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U.unop) }) x)) s ∈ S ↑x
[PROOFSTEP]
exact hs _
[GOAL]
X : TopCat
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ConcreteCategory C
F✝ : Presheaf CommRingCat X
G : SubmonoidPresheaf F✝
F : Sheaf CommRingCat X
⊢ Mono (toTotalQuotientPresheaf (Sheaf.presheaf F))
[PROOFSTEP]
suffices : ∀ (U : (Opens ↑X)ᵒᵖ), Mono (F.presheaf.toTotalQuotientPresheaf.app U)
[GOAL]
X : TopCat
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ConcreteCategory C
F✝ : Presheaf CommRingCat X
G : SubmonoidPresheaf F✝
F : Sheaf CommRingCat X
this : ∀ (U : (Opens ↑X)ᵒᵖ), Mono (NatTrans.app (toTotalQuotientPresheaf (Sheaf.presheaf F)) U)
⊢ Mono (toTotalQuotientPresheaf (Sheaf.presheaf F))
[PROOFSTEP]
apply NatTrans.mono_of_mono_app
[GOAL]
case this
X : TopCat
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ConcreteCategory C
F✝ : Presheaf CommRingCat X
G : SubmonoidPresheaf F✝
F : Sheaf CommRingCat X
⊢ ∀ (U : (Opens ↑X)ᵒᵖ), Mono (NatTrans.app (toTotalQuotientPresheaf (Sheaf.presheaf F)) U)
[PROOFSTEP]
intro U
[GOAL]
case this
X : TopCat
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ConcreteCategory C
F✝ : Presheaf CommRingCat X
G : SubmonoidPresheaf F✝
F : Sheaf CommRingCat X
U : (Opens ↑X)ᵒᵖ
⊢ Mono (NatTrans.app (toTotalQuotientPresheaf (Sheaf.presheaf F)) U)
[PROOFSTEP]
apply ConcreteCategory.mono_of_injective
[GOAL]
case this.i
X : TopCat
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ConcreteCategory C
F✝ : Presheaf CommRingCat X
G : SubmonoidPresheaf F✝
F : Sheaf CommRingCat X
U : (Opens ↑X)ᵒᵖ
⊢ Function.Injective ↑(NatTrans.app (toTotalQuotientPresheaf (Sheaf.presheaf F)) U)
[PROOFSTEP]
dsimp [toTotalQuotientPresheaf, CommRingCat.ofHom]
  -- Porting note : this is a hack to make the `refine` below works
[GOAL]
case this.i
X : TopCat
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ConcreteCategory C
F✝ : Presheaf CommRingCat X
G : SubmonoidPresheaf F✝
F : Sheaf CommRingCat X
U : (Opens ↑X)ᵒᵖ
⊢ Function.Injective
    ↑(algebraMap (↑((Sheaf.presheaf F).obj U))
        (Localization
          (⨅ (x : { x // x ∈ U.unop }), Submonoid.comap (germ (Sheaf.presheaf F) x) (↑(stalk (Sheaf.presheaf F) ↑x))⁰)))
[PROOFSTEP]
set m := _
[GOAL]
case this.i
X : TopCat
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ConcreteCategory C
F✝ : Presheaf CommRingCat X
G : SubmonoidPresheaf F✝
F : Sheaf CommRingCat X
U : (Opens ↑X)ᵒᵖ
m : ?m.65485 := ?m.65486
⊢ Function.Injective
    ↑(algebraMap (↑((Sheaf.presheaf F).obj U))
        (Localization
          (⨅ (x : { x // x ∈ U.unop }), Submonoid.comap (germ (Sheaf.presheaf F) x) (↑(stalk (Sheaf.presheaf F) ↑x))⁰)))
[PROOFSTEP]
change Function.Injective (algebraMap _ (Localization m))
[GOAL]
case this.i
X : TopCat
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ConcreteCategory C
F✝ : Presheaf CommRingCat X
G : SubmonoidPresheaf F✝
F : Sheaf CommRingCat X
U : (Opens ↑X)ᵒᵖ
m : Submonoid ((forget CommRingCat).obj ((Sheaf.presheaf F).obj U)) :=
  ⨅ (x : { x // x ∈ U.unop }), Submonoid.comap (germ (Sheaf.presheaf F) x) (↑(stalk (Sheaf.presheaf F) ↑x))⁰
⊢ Function.Injective ↑(algebraMap ((forget CommRingCat).obj ((Sheaf.presheaf F).obj U)) (Localization m))
[PROOFSTEP]
change Function.Injective (algebraMap (F.presheaf.obj U) _)
[GOAL]
case this.i
X : TopCat
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ConcreteCategory C
F✝ : Presheaf CommRingCat X
G : SubmonoidPresheaf F✝
F : Sheaf CommRingCat X
U : (Opens ↑X)ᵒᵖ
m : Submonoid ((forget CommRingCat).obj ((Sheaf.presheaf F).obj U)) :=
  ⨅ (x : { x // x ∈ U.unop }), Submonoid.comap (germ (Sheaf.presheaf F) x) (↑(stalk (Sheaf.presheaf F) ↑x))⁰
⊢ Function.Injective ↑(algebraMap (↑((Sheaf.presheaf F).obj U)) (Localization m))
[PROOFSTEP]
haveI : IsLocalization _ (Localization m) := Localization.isLocalization
[GOAL]
case this.i
X : TopCat
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ConcreteCategory C
F✝ : Presheaf CommRingCat X
G : SubmonoidPresheaf F✝
F : Sheaf CommRingCat X
U : (Opens ↑X)ᵒᵖ
m : Submonoid ((forget CommRingCat).obj ((Sheaf.presheaf F).obj U)) :=
  ⨅ (x : { x // x ∈ U.unop }), Submonoid.comap (germ (Sheaf.presheaf F) x) (↑(stalk (Sheaf.presheaf F) ↑x))⁰
this : IsLocalization m (Localization m)
⊢ Function.Injective ↑(algebraMap (↑((Sheaf.presheaf F).obj U)) (Localization m))
[PROOFSTEP]
refine IsLocalization.injective (M := m) (S := Localization m) ?_
[GOAL]
case this.i
X : TopCat
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ConcreteCategory C
F✝ : Presheaf CommRingCat X
G : SubmonoidPresheaf F✝
F : Sheaf CommRingCat X
U : (Opens ↑X)ᵒᵖ
m : Submonoid ((forget CommRingCat).obj ((Sheaf.presheaf F).obj U)) :=
  ⨅ (x : { x // x ∈ U.unop }), Submonoid.comap (germ (Sheaf.presheaf F) x) (↑(stalk (Sheaf.presheaf F) ↑x))⁰
this : IsLocalization m (Localization m)
⊢ m ≤ ((forget CommRingCat).obj ((Sheaf.presheaf F).obj U))⁰
[PROOFSTEP]
intro s hs t e
[GOAL]
case this.i
X : TopCat
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ConcreteCategory C
F✝ : Presheaf CommRingCat X
G : SubmonoidPresheaf F✝
F : Sheaf CommRingCat X
U : (Opens ↑X)ᵒᵖ
m : Submonoid ((forget CommRingCat).obj ((Sheaf.presheaf F).obj U)) :=
  ⨅ (x : { x // x ∈ U.unop }), Submonoid.comap (germ (Sheaf.presheaf F) x) (↑(stalk (Sheaf.presheaf F) ↑x))⁰
this : IsLocalization m (Localization m)
s : (forget CommRingCat).obj ((Sheaf.presheaf F).obj U)
hs : s ∈ m
t : (forget CommRingCat).obj ((Sheaf.presheaf F).obj U)
e : t * s = 0
⊢ t = 0
[PROOFSTEP]
apply section_ext F (unop U)
[GOAL]
case this.i.h
X : TopCat
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ConcreteCategory C
F✝ : Presheaf CommRingCat X
G : SubmonoidPresheaf F✝
F : Sheaf CommRingCat X
U : (Opens ↑X)ᵒᵖ
m : Submonoid ((forget CommRingCat).obj ((Sheaf.presheaf F).obj U)) :=
  ⨅ (x : { x // x ∈ U.unop }), Submonoid.comap (germ (Sheaf.presheaf F) x) (↑(stalk (Sheaf.presheaf F) ↑x))⁰
this : IsLocalization m (Localization m)
s : (forget CommRingCat).obj ((Sheaf.presheaf F).obj U)
hs : s ∈ m
t : (forget CommRingCat).obj ((Sheaf.presheaf F).obj U)
e : t * s = 0
⊢ ∀ (x : { x // x ∈ U.unop }), ↑(germ (Sheaf.presheaf F) x) t = ↑(germ (Sheaf.presheaf F) x) 0
[PROOFSTEP]
intro x
[GOAL]
case this.i.h
X : TopCat
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ConcreteCategory C
F✝ : Presheaf CommRingCat X
G : SubmonoidPresheaf F✝
F : Sheaf CommRingCat X
U : (Opens ↑X)ᵒᵖ
m : Submonoid ((forget CommRingCat).obj ((Sheaf.presheaf F).obj U)) :=
  ⨅ (x : { x // x ∈ U.unop }), Submonoid.comap (germ (Sheaf.presheaf F) x) (↑(stalk (Sheaf.presheaf F) ↑x))⁰
this : IsLocalization m (Localization m)
s : (forget CommRingCat).obj ((Sheaf.presheaf F).obj U)
hs : s ∈ m
t : (forget CommRingCat).obj ((Sheaf.presheaf F).obj U)
e : t * s = 0
x : { x // x ∈ U.unop }
⊢ ↑(germ (Sheaf.presheaf F) x) t = ↑(germ (Sheaf.presheaf F) x) 0
[PROOFSTEP]
rw [map_zero]
[GOAL]
case this.i.h
X : TopCat
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ConcreteCategory C
F✝ : Presheaf CommRingCat X
G : SubmonoidPresheaf F✝
F : Sheaf CommRingCat X
U : (Opens ↑X)ᵒᵖ
m : Submonoid ((forget CommRingCat).obj ((Sheaf.presheaf F).obj U)) :=
  ⨅ (x : { x // x ∈ U.unop }), Submonoid.comap (germ (Sheaf.presheaf F) x) (↑(stalk (Sheaf.presheaf F) ↑x))⁰
this : IsLocalization m (Localization m)
s : (forget CommRingCat).obj ((Sheaf.presheaf F).obj U)
hs : s ∈ m
t : (forget CommRingCat).obj ((Sheaf.presheaf F).obj U)
e : t * s = 0
x : { x // x ∈ U.unop }
⊢ ↑(germ (Sheaf.presheaf F) x) t = 0
[PROOFSTEP]
apply Submonoid.mem_iInf.mp hs x
[GOAL]
case this.i.h.a
X : TopCat
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ConcreteCategory C
F✝ : Presheaf CommRingCat X
G : SubmonoidPresheaf F✝
F : Sheaf CommRingCat X
U : (Opens ↑X)ᵒᵖ
m : Submonoid ((forget CommRingCat).obj ((Sheaf.presheaf F).obj U)) :=
  ⨅ (x : { x // x ∈ U.unop }), Submonoid.comap (germ (Sheaf.presheaf F) x) (↑(stalk (Sheaf.presheaf F) ↑x))⁰
this : IsLocalization m (Localization m)
s : (forget CommRingCat).obj ((Sheaf.presheaf F).obj U)
hs : s ∈ m
t : (forget CommRingCat).obj ((Sheaf.presheaf F).obj U)
e : t * s = 0
x : { x // x ∈ U.unop }
⊢ ↑(germ (Sheaf.presheaf F) x) t * ↑(germ (Sheaf.presheaf F) x) s = 0
[PROOFSTEP]
dsimp
[GOAL]
case this.i.h.a
X : TopCat
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ConcreteCategory C
F✝ : Presheaf CommRingCat X
G : SubmonoidPresheaf F✝
F : Sheaf CommRingCat X
U : (Opens ↑X)ᵒᵖ
m : Submonoid ((forget CommRingCat).obj ((Sheaf.presheaf F).obj U)) :=
  ⨅ (x : { x // x ∈ U.unop }), Submonoid.comap (germ (Sheaf.presheaf F) x) (↑(stalk (Sheaf.presheaf F) ↑x))⁰
this : IsLocalization m (Localization m)
s : (forget CommRingCat).obj ((Sheaf.presheaf F).obj U)
hs : s ∈ m
t : (forget CommRingCat).obj ((Sheaf.presheaf F).obj U)
e : t * s = 0
x : { x // x ∈ U.unop }
⊢ ↑(germ (Sheaf.presheaf F) x) t * ↑(germ (Sheaf.presheaf F) x) s = 0
[PROOFSTEP]
rw [← map_mul, e, map_zero]
