[GOAL]
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
x : { x // x ∈ U }
h : IsUnit (↑(germ X.presheaf x) f)
⊢ ∃ V i x, IsUnit (↑(X.presheaf.map i.op) f)
[PROOFSTEP]
obtain ⟨g', heq⟩ := h.exists_right_inv
[GOAL]
case intro
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
x : { x // x ∈ U }
h : IsUnit (↑(germ X.presheaf x) f)
g' : (CategoryTheory.forget CommRingCat).obj (stalk X.presheaf ↑x)
heq : ↑(germ X.presheaf x) f * g' = 1
⊢ ∃ V i x, IsUnit (↑(X.presheaf.map i.op) f)
[PROOFSTEP]
obtain ⟨V, hxV, g, rfl⟩ := X.presheaf.germ_exist x.1 g'
[GOAL]
case intro.intro.intro.intro
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
x : { x // x ∈ U }
h : IsUnit (↑(germ X.presheaf x) f)
V : Opens ↑↑X.toPresheafedSpace
hxV : ↑x ∈ V
g : (CategoryTheory.forget CommRingCat).obj (X.presheaf.obj (op V))
heq : ↑(germ X.presheaf x) f * ↑(germ X.presheaf { val := ↑x, property := hxV }) g = 1
⊢ ∃ V i x, IsUnit (↑(X.presheaf.map i.op) f)
[PROOFSTEP]
let W := U ⊓ V
[GOAL]
case intro.intro.intro.intro
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
x : { x // x ∈ U }
h : IsUnit (↑(germ X.presheaf x) f)
V : Opens ↑↑X.toPresheafedSpace
hxV : ↑x ∈ V
g : (CategoryTheory.forget CommRingCat).obj (X.presheaf.obj (op V))
heq : ↑(germ X.presheaf x) f * ↑(germ X.presheaf { val := ↑x, property := hxV }) g = 1
W : Opens ↑↑X.toPresheafedSpace := U ⊓ V
⊢ ∃ V i x, IsUnit (↑(X.presheaf.map i.op) f)
[PROOFSTEP]
have hxW : x.1 ∈ W :=
  ⟨x.2, hxV⟩
    -- Porting note : `erw` can't write into `HEq`, so this is replaced with another `HEq` in the
      -- desired form
[GOAL]
case intro.intro.intro.intro
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
x : { x // x ∈ U }
h : IsUnit (↑(germ X.presheaf x) f)
V : Opens ↑↑X.toPresheafedSpace
hxV : ↑x ∈ V
g : (CategoryTheory.forget CommRingCat).obj (X.presheaf.obj (op V))
heq : ↑(germ X.presheaf x) f * ↑(germ X.presheaf { val := ↑x, property := hxV }) g = 1
W : Opens ↑↑X.toPresheafedSpace := U ⊓ V
hxW : ↑x ∈ W
⊢ ∃ V i x, IsUnit (↑(X.presheaf.map i.op) f)
[PROOFSTEP]
replace heq :
  (X.presheaf.germ ⟨x.val, hxW⟩) ((X.presheaf.map (U.infLELeft V).op) f * (X.presheaf.map (U.infLERight V).op) g) =
    (X.presheaf.germ ⟨x.val, hxW⟩) 1
[GOAL]
case heq
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
x : { x // x ∈ U }
h : IsUnit (↑(germ X.presheaf x) f)
V : Opens ↑↑X.toPresheafedSpace
hxV : ↑x ∈ V
g : (CategoryTheory.forget CommRingCat).obj (X.presheaf.obj (op V))
heq : ↑(germ X.presheaf x) f * ↑(germ X.presheaf { val := ↑x, property := hxV }) g = 1
W : Opens ↑↑X.toPresheafedSpace := U ⊓ V
hxW : ↑x ∈ W
⊢ ↑(germ X.presheaf { val := ↑x, property := hxW })
      (↑(X.presheaf.map (Opens.infLELeft U V).op) f * ↑(X.presheaf.map (Opens.infLERight U V).op) g) =
    ↑(germ X.presheaf { val := ↑x, property := hxW }) 1
[PROOFSTEP]
dsimp [germ]
[GOAL]
case heq
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
x : { x // x ∈ U }
h : IsUnit (↑(germ X.presheaf x) f)
V : Opens ↑↑X.toPresheafedSpace
hxV : ↑x ∈ V
g : (CategoryTheory.forget CommRingCat).obj (X.presheaf.obj (op V))
heq : ↑(germ X.presheaf x) f * ↑(germ X.presheaf { val := ↑x, property := hxV }) g = 1
W : Opens ↑↑X.toPresheafedSpace := U ⊓ V
hxW : ↑x ∈ W
⊢ ↑(Limits.colimit.ι ((OpenNhds.inclusion ↑x).op ⋙ X.presheaf)
          (op { obj := U ⊓ V, property := (_ : ↑{ val := ↑x, property := hxW } ∈ U ⊓ V) }))
      (↑(X.presheaf.map (Opens.infLELeft U V).op) f * ↑(X.presheaf.map (Opens.infLERight U V).op) g) =
    ↑(Limits.colimit.ι ((OpenNhds.inclusion ↑x).op ⋙ X.presheaf)
          (op { obj := U ⊓ V, property := (_ : ↑{ val := ↑x, property := hxW } ∈ U ⊓ V) }))
      1
[PROOFSTEP]
erw [map_mul, map_one,
  show X.presheaf.germ ⟨x, hxW⟩ ((X.presheaf.map (U.infLELeft V).op) f) = X.presheaf.germ x f from
    X.presheaf.germ_res_apply (Opens.infLELeft U V) ⟨x.1, hxW⟩ f,
  show X.presheaf.germ ⟨x, hxW⟩ (X.presheaf.map (U.infLERight V).op g) = X.presheaf.germ ⟨x, hxV⟩ g from
    X.presheaf.germ_res_apply (Opens.infLERight U V) ⟨x.1, hxW⟩ g]
[GOAL]
case heq
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
x : { x // x ∈ U }
h : IsUnit (↑(germ X.presheaf x) f)
V : Opens ↑↑X.toPresheafedSpace
hxV : ↑x ∈ V
g : (CategoryTheory.forget CommRingCat).obj (X.presheaf.obj (op V))
heq : ↑(germ X.presheaf x) f * ↑(germ X.presheaf { val := ↑x, property := hxV }) g = 1
W : Opens ↑↑X.toPresheafedSpace := U ⊓ V
hxW : ↑x ∈ W
⊢ ↑(germ X.presheaf x) f * ↑(germ X.presheaf { val := ↑x, property := hxV }) g = 1
[PROOFSTEP]
exact heq
[GOAL]
case intro.intro.intro.intro
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
x : { x // x ∈ U }
h : IsUnit (↑(germ X.presheaf x) f)
V : Opens ↑↑X.toPresheafedSpace
hxV : ↑x ∈ V
g : (CategoryTheory.forget CommRingCat).obj (X.presheaf.obj (op V))
W : Opens ↑↑X.toPresheafedSpace := U ⊓ V
hxW : ↑x ∈ W
heq :
  ↑(germ X.presheaf { val := ↑x, property := hxW })
      (↑(X.presheaf.map (Opens.infLELeft U V).op) f * ↑(X.presheaf.map (Opens.infLERight U V).op) g) =
    ↑(germ X.presheaf { val := ↑x, property := hxW }) 1
⊢ ∃ V i x, IsUnit (↑(X.presheaf.map i.op) f)
[PROOFSTEP]
obtain ⟨W', hxW', i₁, i₂, heq'⟩ := X.presheaf.germ_eq x.1 hxW hxW _ _ heq
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
x : { x // x ∈ U }
h : IsUnit (↑(germ X.presheaf x) f)
V : Opens ↑↑X.toPresheafedSpace
hxV : ↑x ∈ V
g : (CategoryTheory.forget CommRingCat).obj (X.presheaf.obj (op V))
W : Opens ↑↑X.toPresheafedSpace := U ⊓ V
hxW : ↑x ∈ W
heq :
  ↑(germ X.presheaf { val := ↑x, property := hxW })
      (↑(X.presheaf.map (Opens.infLELeft U V).op) f * ↑(X.presheaf.map (Opens.infLERight U V).op) g) =
    ↑(germ X.presheaf { val := ↑x, property := hxW }) 1
W' : Opens ↑↑X.toPresheafedSpace
hxW' : ↑x ∈ W'
i₁ i₂ : W' ⟶ W
heq' :
  ↑(X.presheaf.map i₁.op)
      (↑(X.presheaf.map (Opens.infLELeft U V).op) f * ↑(X.presheaf.map (Opens.infLERight U V).op) g) =
    ↑(X.presheaf.map i₂.op) 1
⊢ ∃ V i x, IsUnit (↑(X.presheaf.map i.op) f)
[PROOFSTEP]
use W', i₁ ≫ Opens.infLELeft U V, hxW'
[GOAL]
case h
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
x : { x // x ∈ U }
h : IsUnit (↑(germ X.presheaf x) f)
V : Opens ↑↑X.toPresheafedSpace
hxV : ↑x ∈ V
g : (CategoryTheory.forget CommRingCat).obj (X.presheaf.obj (op V))
W : Opens ↑↑X.toPresheafedSpace := U ⊓ V
hxW : ↑x ∈ W
heq :
  ↑(germ X.presheaf { val := ↑x, property := hxW })
      (↑(X.presheaf.map (Opens.infLELeft U V).op) f * ↑(X.presheaf.map (Opens.infLERight U V).op) g) =
    ↑(germ X.presheaf { val := ↑x, property := hxW }) 1
W' : Opens ↑↑X.toPresheafedSpace
hxW' : ↑x ∈ W'
i₁ i₂ : W' ⟶ W
heq' :
  ↑(X.presheaf.map i₁.op)
      (↑(X.presheaf.map (Opens.infLELeft U V).op) f * ↑(X.presheaf.map (Opens.infLERight U V).op) g) =
    ↑(X.presheaf.map i₂.op) 1
⊢ IsUnit (↑(X.presheaf.map (i₁ ≫ Opens.infLELeft U V).op) f)
[PROOFSTEP]
rw [(X.presheaf.map i₂.op).map_one, (X.presheaf.map i₁.op).map_mul] at heq'
[GOAL]
case h
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
x : { x // x ∈ U }
h : IsUnit (↑(germ X.presheaf x) f)
V : Opens ↑↑X.toPresheafedSpace
hxV : ↑x ∈ V
g : (CategoryTheory.forget CommRingCat).obj (X.presheaf.obj (op V))
W : Opens ↑↑X.toPresheafedSpace := U ⊓ V
hxW : ↑x ∈ W
heq :
  ↑(germ X.presheaf { val := ↑x, property := hxW })
      (↑(X.presheaf.map (Opens.infLELeft U V).op) f * ↑(X.presheaf.map (Opens.infLERight U V).op) g) =
    ↑(germ X.presheaf { val := ↑x, property := hxW }) 1
W' : Opens ↑↑X.toPresheafedSpace
hxW' : ↑x ∈ W'
i₁ i₂ : W' ⟶ W
heq' :
  ↑(X.presheaf.map i₁.op) (↑(X.presheaf.map (Opens.infLELeft U V).op) f) *
      ↑(X.presheaf.map i₁.op) (↑(X.presheaf.map (Opens.infLERight U V).op) g) =
    1
⊢ IsUnit (↑(X.presheaf.map (i₁ ≫ Opens.infLELeft U V).op) f)
[PROOFSTEP]
rw [← comp_apply, ← X.presheaf.map_comp, ← comp_apply, ← X.presheaf.map_comp, ← op_comp] at heq'
[GOAL]
case h
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
x : { x // x ∈ U }
h : IsUnit (↑(germ X.presheaf x) f)
V : Opens ↑↑X.toPresheafedSpace
hxV : ↑x ∈ V
g : (CategoryTheory.forget CommRingCat).obj (X.presheaf.obj (op V))
W : Opens ↑↑X.toPresheafedSpace := U ⊓ V
hxW : ↑x ∈ W
heq :
  ↑(germ X.presheaf { val := ↑x, property := hxW })
      (↑(X.presheaf.map (Opens.infLELeft U V).op) f * ↑(X.presheaf.map (Opens.infLERight U V).op) g) =
    ↑(germ X.presheaf { val := ↑x, property := hxW }) 1
W' : Opens ↑↑X.toPresheafedSpace
hxW' : ↑x ∈ W'
i₁ i₂ : W' ⟶ W
heq' : ↑(X.presheaf.map (i₁ ≫ Opens.infLELeft U V).op) f * ↑(X.presheaf.map ((Opens.infLERight U V).op ≫ i₁.op)) g = 1
⊢ IsUnit (↑(X.presheaf.map (i₁ ≫ Opens.infLELeft U V).op) f)
[PROOFSTEP]
exact isUnit_of_mul_eq_one _ _ heq'
[GOAL]
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
h : ∀ (x : { x // x ∈ U }), IsUnit (↑(germ X.presheaf x) f)
⊢ IsUnit f
[PROOFSTEP]
choose V iVU m h_unit using fun x : U => X.isUnit_res_of_isUnit_germ U f x (h x)
[GOAL]
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
h : ∀ (x : { x // x ∈ U }), IsUnit (↑(germ X.presheaf x) f)
V : { x // x ∈ U } → Opens ↑↑X.toPresheafedSpace
iVU : (x : { x // x ∈ U }) → V x ⟶ U
m : ∀ (x : { x // x ∈ U }), ↑x ∈ V x
h_unit : ∀ (x : { x // x ∈ U }), IsUnit (↑(X.presheaf.map (iVU x).op) f)
⊢ IsUnit f
[PROOFSTEP]
have hcover : U ≤ iSup V
[GOAL]
case hcover
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
h : ∀ (x : { x // x ∈ U }), IsUnit (↑(germ X.presheaf x) f)
V : { x // x ∈ U } → Opens ↑↑X.toPresheafedSpace
iVU : (x : { x // x ∈ U }) → V x ⟶ U
m : ∀ (x : { x // x ∈ U }), ↑x ∈ V x
h_unit : ∀ (x : { x // x ∈ U }), IsUnit (↑(X.presheaf.map (iVU x).op) f)
⊢ U ≤ iSup V
[PROOFSTEP]
intro x hxU
[GOAL]
case hcover
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
h : ∀ (x : { x // x ∈ U }), IsUnit (↑(germ X.presheaf x) f)
V : { x // x ∈ U } → Opens ↑↑X.toPresheafedSpace
iVU : (x : { x // x ∈ U }) → V x ⟶ U
m : ∀ (x : { x // x ∈ U }), ↑x ∈ V x
h_unit : ∀ (x : { x // x ∈ U }), IsUnit (↑(X.presheaf.map (iVU x).op) f)
x : ↑↑X.toPresheafedSpace
hxU : x ∈ ↑U
⊢ x ∈ ↑(iSup V)
[PROOFSTEP]
erw [Opens.mem_iSup]
[GOAL]
case hcover
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
h : ∀ (x : { x // x ∈ U }), IsUnit (↑(germ X.presheaf x) f)
V : { x // x ∈ U } → Opens ↑↑X.toPresheafedSpace
iVU : (x : { x // x ∈ U }) → V x ⟶ U
m : ∀ (x : { x // x ∈ U }), ↑x ∈ V x
h_unit : ∀ (x : { x // x ∈ U }), IsUnit (↑(X.presheaf.map (iVU x).op) f)
x : ↑↑X.toPresheafedSpace
hxU : x ∈ ↑U
⊢ ∃ i, x ∈ V i
[PROOFSTEP]
exact
  ⟨⟨x, hxU⟩, m ⟨x, hxU⟩⟩
    -- Let `g x` denote the inverse of `f` in `U x`.
[GOAL]
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
h : ∀ (x : { x // x ∈ U }), IsUnit (↑(germ X.presheaf x) f)
V : { x // x ∈ U } → Opens ↑↑X.toPresheafedSpace
iVU : (x : { x // x ∈ U }) → V x ⟶ U
m : ∀ (x : { x // x ∈ U }), ↑x ∈ V x
h_unit : ∀ (x : { x // x ∈ U }), IsUnit (↑(X.presheaf.map (iVU x).op) f)
hcover : U ≤ iSup V
⊢ IsUnit f
[PROOFSTEP]
choose g hg using fun x : U => IsUnit.exists_right_inv (h_unit x)
[GOAL]
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
h : ∀ (x : { x // x ∈ U }), IsUnit (↑(germ X.presheaf x) f)
V : { x // x ∈ U } → Opens ↑↑X.toPresheafedSpace
iVU : (x : { x // x ∈ U }) → V x ⟶ U
m : ∀ (x : { x // x ∈ U }), ↑x ∈ V x
h_unit : ∀ (x : { x // x ∈ U }), IsUnit (↑(X.presheaf.map (iVU x).op) f)
hcover : U ≤ iSup V
g : (x : { x // x ∈ U }) → (fun x_1 => (CategoryTheory.forget CommRingCat).obj (X.presheaf.obj (op (V x)))) f
hg : ∀ (x : { x // x ∈ U }), ↑(X.presheaf.map (iVU x).op) f * g x = 1
⊢ IsUnit f
[PROOFSTEP]
have ic : IsCompatible (sheaf X).val V g
[GOAL]
case ic
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
h : ∀ (x : { x // x ∈ U }), IsUnit (↑(germ X.presheaf x) f)
V : { x // x ∈ U } → Opens ↑↑X.toPresheafedSpace
iVU : (x : { x // x ∈ U }) → V x ⟶ U
m : ∀ (x : { x // x ∈ U }), ↑x ∈ V x
h_unit : ∀ (x : { x // x ∈ U }), IsUnit (↑(X.presheaf.map (iVU x).op) f)
hcover : U ≤ iSup V
g : (x : { x // x ∈ U }) → (fun x_1 => (CategoryTheory.forget CommRingCat).obj (X.presheaf.obj (op (V x)))) f
hg : ∀ (x : { x // x ∈ U }), ↑(X.presheaf.map (iVU x).op) f * g x = 1
⊢ IsCompatible (sheaf X).val V g
[PROOFSTEP]
intro x y
[GOAL]
case ic
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
h : ∀ (x : { x // x ∈ U }), IsUnit (↑(germ X.presheaf x) f)
V : { x // x ∈ U } → Opens ↑↑X.toPresheafedSpace
iVU : (x : { x // x ∈ U }) → V x ⟶ U
m : ∀ (x : { x // x ∈ U }), ↑x ∈ V x
h_unit : ∀ (x : { x // x ∈ U }), IsUnit (↑(X.presheaf.map (iVU x).op) f)
hcover : U ≤ iSup V
g : (x : { x // x ∈ U }) → (fun x_1 => (CategoryTheory.forget CommRingCat).obj (X.presheaf.obj (op (V x)))) f
hg : ∀ (x : { x // x ∈ U }), ↑(X.presheaf.map (iVU x).op) f * g x = 1
x y : { x // x ∈ U }
⊢ ↑((sheaf X).val.map (Opens.infLELeft (V x) (V y)).op) (g x) =
    ↑((sheaf X).val.map (Opens.infLERight (V x) (V y)).op) (g y)
[PROOFSTEP]
apply section_ext X.sheaf (V x ⊓ V y)
[GOAL]
case ic.h
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
h : ∀ (x : { x // x ∈ U }), IsUnit (↑(germ X.presheaf x) f)
V : { x // x ∈ U } → Opens ↑↑X.toPresheafedSpace
iVU : (x : { x // x ∈ U }) → V x ⟶ U
m : ∀ (x : { x // x ∈ U }), ↑x ∈ V x
h_unit : ∀ (x : { x // x ∈ U }), IsUnit (↑(X.presheaf.map (iVU x).op) f)
hcover : U ≤ iSup V
g : (x : { x // x ∈ U }) → (fun x_1 => (CategoryTheory.forget CommRingCat).obj (X.presheaf.obj (op (V x)))) f
hg : ∀ (x : { x // x ∈ U }), ↑(X.presheaf.map (iVU x).op) f * g x = 1
x y : { x // x ∈ U }
⊢ ∀ (x_1 : { x_1 // x_1 ∈ V x ⊓ V y }),
    ↑(germ (Sheaf.presheaf (sheaf X)) x_1) (↑((sheaf X).val.map (Opens.infLELeft (V x) (V y)).op) (g x)) =
      ↑(germ (Sheaf.presheaf (sheaf X)) x_1) (↑((sheaf X).val.map (Opens.infLERight (V x) (V y)).op) (g y))
[PROOFSTEP]
rintro ⟨z, hzVx, hzVy⟩
[GOAL]
case ic.h.mk.intro
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
h : ∀ (x : { x // x ∈ U }), IsUnit (↑(germ X.presheaf x) f)
V : { x // x ∈ U } → Opens ↑↑X.toPresheafedSpace
iVU : (x : { x // x ∈ U }) → V x ⟶ U
m : ∀ (x : { x // x ∈ U }), ↑x ∈ V x
h_unit : ∀ (x : { x // x ∈ U }), IsUnit (↑(X.presheaf.map (iVU x).op) f)
hcover : U ≤ iSup V
g : (x : { x // x ∈ U }) → (fun x_1 => (CategoryTheory.forget CommRingCat).obj (X.presheaf.obj (op (V x)))) f
hg : ∀ (x : { x // x ∈ U }), ↑(X.presheaf.map (iVU x).op) f * g x = 1
x y : { x // x ∈ U }
z : ↑↑X.toPresheafedSpace
hzVx : z ∈ ↑(V x)
hzVy : z ∈ ↑(V y)
⊢ ↑(germ (Sheaf.presheaf (sheaf X)) { val := z, property := (_ : z ∈ ↑(V x) ∧ z ∈ ↑(V y)) })
      (↑((sheaf X).val.map (Opens.infLELeft (V x) (V y)).op) (g x)) =
    ↑(germ (Sheaf.presheaf (sheaf X)) { val := z, property := (_ : z ∈ ↑(V x) ∧ z ∈ ↑(V y)) })
      (↑((sheaf X).val.map (Opens.infLERight (V x) (V y)).op) (g y))
[PROOFSTEP]
erw [germ_res_apply, germ_res_apply]
[GOAL]
case ic.h.mk.intro
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
h : ∀ (x : { x // x ∈ U }), IsUnit (↑(germ X.presheaf x) f)
V : { x // x ∈ U } → Opens ↑↑X.toPresheafedSpace
iVU : (x : { x // x ∈ U }) → V x ⟶ U
m : ∀ (x : { x // x ∈ U }), ↑x ∈ V x
h_unit : ∀ (x : { x // x ∈ U }), IsUnit (↑(X.presheaf.map (iVU x).op) f)
hcover : U ≤ iSup V
g : (x : { x // x ∈ U }) → (fun x_1 => (CategoryTheory.forget CommRingCat).obj (X.presheaf.obj (op (V x)))) f
hg : ∀ (x : { x // x ∈ U }), ↑(X.presheaf.map (iVU x).op) f * g x = 1
x y : { x // x ∈ U }
z : ↑↑X.toPresheafedSpace
hzVx : z ∈ ↑(V x)
hzVy : z ∈ ↑(V y)
⊢ ↑(germ (Sheaf.presheaf (sheaf X))
          ((fun x_1 => { val := ↑x_1, property := (_ : ↑x_1 ∈ ↑(V x)) })
            { val := z, property := (_ : z ∈ ↑(V x) ∧ z ∈ ↑(V y)) }))
      (g x) =
    ↑(germ (Sheaf.presheaf (sheaf X))
          ((fun x_1 => { val := ↑x_1, property := (_ : ↑x_1 ∈ ↑(V y)) })
            { val := z, property := (_ : z ∈ ↑(V x) ∧ z ∈ ↑(V y)) }))
      (g y)
[PROOFSTEP]
apply (IsUnit.mul_right_inj (h ⟨z, (iVU x).le hzVx⟩)).mp
[GOAL]
case ic.h.mk.intro
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
h : ∀ (x : { x // x ∈ U }), IsUnit (↑(germ X.presheaf x) f)
V : { x // x ∈ U } → Opens ↑↑X.toPresheafedSpace
iVU : (x : { x // x ∈ U }) → V x ⟶ U
m : ∀ (x : { x // x ∈ U }), ↑x ∈ V x
h_unit : ∀ (x : { x // x ∈ U }), IsUnit (↑(X.presheaf.map (iVU x).op) f)
hcover : U ≤ iSup V
g : (x : { x // x ∈ U }) → (fun x_1 => (CategoryTheory.forget CommRingCat).obj (X.presheaf.obj (op (V x)))) f
hg : ∀ (x : { x // x ∈ U }), ↑(X.presheaf.map (iVU x).op) f * g x = 1
x y : { x // x ∈ U }
z : ↑↑X.toPresheafedSpace
hzVx : z ∈ ↑(V x)
hzVy : z ∈ ↑(V y)
⊢ ↑(germ X.presheaf { val := z, property := (_ : z ∈ ↑U) }) f *
      ↑(germ (Sheaf.presheaf (sheaf X))
            ((fun x_1 => { val := ↑x_1, property := (_ : ↑x_1 ∈ ↑(V x)) })
              { val := z, property := (_ : z ∈ ↑(V x) ∧ z ∈ ↑(V y)) }))
        (g x) =
    ↑(germ X.presheaf { val := z, property := (_ : z ∈ ↑U) }) f *
      ↑(germ (Sheaf.presheaf (sheaf X))
            ((fun x_1 => { val := ↑x_1, property := (_ : ↑x_1 ∈ ↑(V y)) })
              { val := z, property := (_ : z ∈ ↑(V x) ∧ z ∈ ↑(V y)) }))
        (g y)
[PROOFSTEP]
rw [←
  show X.presheaf.germ ⟨z, hzVx⟩ (X.presheaf.map (iVU x).op f) = X.presheaf.germ ⟨z, ((iVU x) ⟨z, hzVx⟩).2⟩ f from
    X.presheaf.germ_res_apply (iVU x) ⟨z, hzVx⟩ f]
  -- Porting note : change was not necessary in Lean3
[GOAL]
case ic.h.mk.intro
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
h : ∀ (x : { x // x ∈ U }), IsUnit (↑(germ X.presheaf x) f)
V : { x // x ∈ U } → Opens ↑↑X.toPresheafedSpace
iVU : (x : { x // x ∈ U }) → V x ⟶ U
m : ∀ (x : { x // x ∈ U }), ↑x ∈ V x
h_unit : ∀ (x : { x // x ∈ U }), IsUnit (↑(X.presheaf.map (iVU x).op) f)
hcover : U ≤ iSup V
g : (x : { x // x ∈ U }) → (fun x_1 => (CategoryTheory.forget CommRingCat).obj (X.presheaf.obj (op (V x)))) f
hg : ∀ (x : { x // x ∈ U }), ↑(X.presheaf.map (iVU x).op) f * g x = 1
x y : { x // x ∈ U }
z : ↑↑X.toPresheafedSpace
hzVx : z ∈ ↑(V x)
hzVy : z ∈ ↑(V y)
⊢ ↑(germ X.presheaf { val := z, property := hzVx }) (↑(X.presheaf.map (iVU x).op) f) *
      ↑(germ (Sheaf.presheaf (sheaf X))
            ((fun x_1 => { val := ↑x_1, property := (_ : ↑x_1 ∈ ↑(V x)) })
              { val := z, property := (_ : z ∈ ↑(V x) ∧ z ∈ ↑(V y)) }))
        (g x) =
    ↑(germ X.presheaf { val := z, property := hzVx }) (↑(X.presheaf.map (iVU x).op) f) *
      ↑(germ (Sheaf.presheaf (sheaf X))
            ((fun x_1 => { val := ↑x_1, property := (_ : ↑x_1 ∈ ↑(V y)) })
              { val := z, property := (_ : z ∈ ↑(V x) ∧ z ∈ ↑(V y)) }))
        (g y)
[PROOFSTEP]
change
  X.presheaf.germ ⟨z, hzVx⟩ _ * (X.presheaf.germ ⟨z, hzVx⟩ _) =
    X.presheaf.germ ⟨z, hzVx⟩ _ * X.presheaf.germ ⟨z, hzVy⟩ (g y)
[GOAL]
case ic.h.mk.intro
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
h : ∀ (x : { x // x ∈ U }), IsUnit (↑(germ X.presheaf x) f)
V : { x // x ∈ U } → Opens ↑↑X.toPresheafedSpace
iVU : (x : { x // x ∈ U }) → V x ⟶ U
m : ∀ (x : { x // x ∈ U }), ↑x ∈ V x
h_unit : ∀ (x : { x // x ∈ U }), IsUnit (↑(X.presheaf.map (iVU x).op) f)
hcover : U ≤ iSup V
g : (x : { x // x ∈ U }) → (fun x_1 => (CategoryTheory.forget CommRingCat).obj (X.presheaf.obj (op (V x)))) f
hg : ∀ (x : { x // x ∈ U }), ↑(X.presheaf.map (iVU x).op) f * g x = 1
x y : { x // x ∈ U }
z : ↑↑X.toPresheafedSpace
hzVx : z ∈ ↑(V x)
hzVy : z ∈ ↑(V y)
⊢ ↑(germ X.presheaf { val := z, property := hzVx }) (↑(X.presheaf.map (iVU x).op) f) *
      ↑(germ X.presheaf { val := z, property := hzVx }) (g x) =
    ↑(germ X.presheaf { val := z, property := hzVx }) (↑(X.presheaf.map (iVU x).op) f) *
      ↑(germ X.presheaf { val := z, property := hzVy }) (g y)
[PROOFSTEP]
rw [← RingHom.map_mul, congr_arg (X.presheaf.germ (⟨z, hzVx⟩ : V x)) (hg x),
  -- Porting note : now need explicitly typing the rewritesshow
    X.presheaf.germ ⟨z, hzVx⟩ (X.presheaf.map (iVU x).op f) = X.presheaf.germ ⟨z, ((iVU x) ⟨z, hzVx⟩).2⟩ f from
    X.presheaf.germ_res_apply _ _ f,
  -- Porting note : now need explicitly typing the rewrites←
  show X.presheaf.germ ⟨z, hzVy⟩ (X.presheaf.map (iVU y).op f) = X.presheaf.germ ⟨z, ((iVU x) ⟨z, hzVx⟩).2⟩ f from
    X.presheaf.germ_res_apply (iVU y) ⟨z, hzVy⟩ f,
  ← RingHom.map_mul, congr_arg (X.presheaf.germ (⟨z, hzVy⟩ : V y)) (hg y), RingHom.map_one, RingHom.map_one]
  -- We claim that these local inverses glue together to a global inverse of `f`.
[GOAL]
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
h : ∀ (x : { x // x ∈ U }), IsUnit (↑(germ X.presheaf x) f)
V : { x // x ∈ U } → Opens ↑↑X.toPresheafedSpace
iVU : (x : { x // x ∈ U }) → V x ⟶ U
m : ∀ (x : { x // x ∈ U }), ↑x ∈ V x
h_unit : ∀ (x : { x // x ∈ U }), IsUnit (↑(X.presheaf.map (iVU x).op) f)
hcover : U ≤ iSup V
g : (x : { x // x ∈ U }) → (fun x_1 => (CategoryTheory.forget CommRingCat).obj (X.presheaf.obj (op (V x)))) f
hg : ∀ (x : { x // x ∈ U }), ↑(X.presheaf.map (iVU x).op) f * g x = 1
ic : IsCompatible (sheaf X).val V g
⊢ IsUnit f
[PROOFSTEP]
obtain ⟨gl, gl_spec, -⟩ := X.sheaf.existsUnique_gluing' V U iVU hcover g ic
[GOAL]
case intro.intro
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
h : ∀ (x : { x // x ∈ U }), IsUnit (↑(germ X.presheaf x) f)
V : { x // x ∈ U } → Opens ↑↑X.toPresheafedSpace
iVU : (x : { x // x ∈ U }) → V x ⟶ U
m : ∀ (x : { x // x ∈ U }), ↑x ∈ V x
h_unit : ∀ (x : { x // x ∈ U }), IsUnit (↑(X.presheaf.map (iVU x).op) f)
hcover : U ≤ iSup V
g : (x : { x // x ∈ U }) → (fun x_1 => (CategoryTheory.forget CommRingCat).obj (X.presheaf.obj (op (V x)))) f
hg : ∀ (x : { x // x ∈ U }), ↑(X.presheaf.map (iVU x).op) f * g x = 1
ic : IsCompatible (sheaf X).val V g
gl : (CategoryTheory.forget CommRingCat).obj ((sheaf X).val.obj (op U))
gl_spec : ∀ (i : { x // x ∈ U }), ↑((sheaf X).val.map (iVU i).op) gl = g i
⊢ IsUnit f
[PROOFSTEP]
apply isUnit_of_mul_eq_one f gl
[GOAL]
case intro.intro
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
h : ∀ (x : { x // x ∈ U }), IsUnit (↑(germ X.presheaf x) f)
V : { x // x ∈ U } → Opens ↑↑X.toPresheafedSpace
iVU : (x : { x // x ∈ U }) → V x ⟶ U
m : ∀ (x : { x // x ∈ U }), ↑x ∈ V x
h_unit : ∀ (x : { x // x ∈ U }), IsUnit (↑(X.presheaf.map (iVU x).op) f)
hcover : U ≤ iSup V
g : (x : { x // x ∈ U }) → (fun x_1 => (CategoryTheory.forget CommRingCat).obj (X.presheaf.obj (op (V x)))) f
hg : ∀ (x : { x // x ∈ U }), ↑(X.presheaf.map (iVU x).op) f * g x = 1
ic : IsCompatible (sheaf X).val V g
gl : (CategoryTheory.forget CommRingCat).obj ((sheaf X).val.obj (op U))
gl_spec : ∀ (i : { x // x ∈ U }), ↑((sheaf X).val.map (iVU i).op) gl = g i
⊢ f * gl = 1
[PROOFSTEP]
apply X.sheaf.eq_of_locally_eq' V U iVU hcover
[GOAL]
case intro.intro.h
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
h : ∀ (x : { x // x ∈ U }), IsUnit (↑(germ X.presheaf x) f)
V : { x // x ∈ U } → Opens ↑↑X.toPresheafedSpace
iVU : (x : { x // x ∈ U }) → V x ⟶ U
m : ∀ (x : { x // x ∈ U }), ↑x ∈ V x
h_unit : ∀ (x : { x // x ∈ U }), IsUnit (↑(X.presheaf.map (iVU x).op) f)
hcover : U ≤ iSup V
g : (x : { x // x ∈ U }) → (fun x_1 => (CategoryTheory.forget CommRingCat).obj (X.presheaf.obj (op (V x)))) f
hg : ∀ (x : { x // x ∈ U }), ↑(X.presheaf.map (iVU x).op) f * g x = 1
ic : IsCompatible (sheaf X).val V g
gl : (CategoryTheory.forget CommRingCat).obj ((sheaf X).val.obj (op U))
gl_spec : ∀ (i : { x // x ∈ U }), ↑((sheaf X).val.map (iVU i).op) gl = g i
⊢ ∀ (i : { x // x ∈ U }), ↑((sheaf X).val.map (iVU i).op) (f * gl) = ↑((sheaf X).val.map (iVU i).op) 1
[PROOFSTEP]
intro i
[GOAL]
case intro.intro.h
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
h : ∀ (x : { x // x ∈ U }), IsUnit (↑(germ X.presheaf x) f)
V : { x // x ∈ U } → Opens ↑↑X.toPresheafedSpace
iVU : (x : { x // x ∈ U }) → V x ⟶ U
m : ∀ (x : { x // x ∈ U }), ↑x ∈ V x
h_unit : ∀ (x : { x // x ∈ U }), IsUnit (↑(X.presheaf.map (iVU x).op) f)
hcover : U ≤ iSup V
g : (x : { x // x ∈ U }) → (fun x_1 => (CategoryTheory.forget CommRingCat).obj (X.presheaf.obj (op (V x)))) f
hg : ∀ (x : { x // x ∈ U }), ↑(X.presheaf.map (iVU x).op) f * g x = 1
ic : IsCompatible (sheaf X).val V g
gl : (CategoryTheory.forget CommRingCat).obj ((sheaf X).val.obj (op U))
gl_spec : ∀ (i : { x // x ∈ U }), ↑((sheaf X).val.map (iVU i).op) gl = g i
i : { x // x ∈ U }
⊢ ↑((sheaf X).val.map (iVU i).op) (f * gl) = ↑((sheaf X).val.map (iVU i).op) 1
[PROOFSTEP]
rw [RingHom.map_one, RingHom.map_mul, gl_spec]
[GOAL]
case intro.intro.h
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
h : ∀ (x : { x // x ∈ U }), IsUnit (↑(germ X.presheaf x) f)
V : { x // x ∈ U } → Opens ↑↑X.toPresheafedSpace
iVU : (x : { x // x ∈ U }) → V x ⟶ U
m : ∀ (x : { x // x ∈ U }), ↑x ∈ V x
h_unit : ∀ (x : { x // x ∈ U }), IsUnit (↑(X.presheaf.map (iVU x).op) f)
hcover : U ≤ iSup V
g : (x : { x // x ∈ U }) → (fun x_1 => (CategoryTheory.forget CommRingCat).obj (X.presheaf.obj (op (V x)))) f
hg : ∀ (x : { x // x ∈ U }), ↑(X.presheaf.map (iVU x).op) f * g x = 1
ic : IsCompatible (sheaf X).val V g
gl : (CategoryTheory.forget CommRingCat).obj ((sheaf X).val.obj (op U))
gl_spec : ∀ (i : { x // x ∈ U }), ↑((sheaf X).val.map (iVU i).op) gl = g i
i : { x // x ∈ U }
⊢ ↑((sheaf X).val.map (iVU i).op) f * g i = 1
[PROOFSTEP]
exact hg i
[GOAL]
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
⊢ IsOpen (Subtype.val '' {x | IsUnit (↑(germ X.presheaf x) f)})
[PROOFSTEP]
rw [isOpen_iff_forall_mem_open]
[GOAL]
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
⊢ ∀ (x : ↑↑X.toPresheafedSpace),
    x ∈ Subtype.val '' {x | IsUnit (↑(germ X.presheaf x) f)} →
      ∃ t, t ⊆ Subtype.val '' {x | IsUnit (↑(germ X.presheaf x) f)} ∧ IsOpen t ∧ x ∈ t
[PROOFSTEP]
rintro _ ⟨x, hx, rfl⟩
[GOAL]
case intro.intro
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
x : { x // x ∈ U }
hx : x ∈ {x | IsUnit (↑(germ X.presheaf x) f)}
⊢ ∃ t, t ⊆ Subtype.val '' {x | IsUnit (↑(germ X.presheaf x) f)} ∧ IsOpen t ∧ ↑x ∈ t
[PROOFSTEP]
obtain ⟨V, i, hxV, hf⟩ := X.isUnit_res_of_isUnit_germ U f x hx
[GOAL]
case intro.intro.intro.intro.intro
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
x : { x // x ∈ U }
hx : x ∈ {x | IsUnit (↑(germ X.presheaf x) f)}
V : Opens ↑↑X.toPresheafedSpace
i : V ⟶ U
hxV : ↑x ∈ V
hf : IsUnit (↑(X.presheaf.map i.op) f)
⊢ ∃ t, t ⊆ Subtype.val '' {x | IsUnit (↑(germ X.presheaf x) f)} ∧ IsOpen t ∧ ↑x ∈ t
[PROOFSTEP]
use V.1
[GOAL]
case h
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
x : { x // x ∈ U }
hx : x ∈ {x | IsUnit (↑(germ X.presheaf x) f)}
V : Opens ↑↑X.toPresheafedSpace
i : V ⟶ U
hxV : ↑x ∈ V
hf : IsUnit (↑(X.presheaf.map i.op) f)
⊢ V.carrier ⊆ Subtype.val '' {x | IsUnit (↑(germ X.presheaf x) f)} ∧ IsOpen V.carrier ∧ ↑x ∈ V.carrier
[PROOFSTEP]
refine' ⟨_, V.2, hxV⟩
[GOAL]
case h
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
x : { x // x ∈ U }
hx : x ∈ {x | IsUnit (↑(germ X.presheaf x) f)}
V : Opens ↑↑X.toPresheafedSpace
i : V ⟶ U
hxV : ↑x ∈ V
hf : IsUnit (↑(X.presheaf.map i.op) f)
⊢ V.carrier ⊆ Subtype.val '' {x | IsUnit (↑(germ X.presheaf x) f)}
[PROOFSTEP]
intro y hy
[GOAL]
case h
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
x : { x // x ∈ U }
hx : x ∈ {x | IsUnit (↑(germ X.presheaf x) f)}
V : Opens ↑↑X.toPresheafedSpace
i : V ⟶ U
hxV : ↑x ∈ V
hf : IsUnit (↑(X.presheaf.map i.op) f)
y : ↑↑X.toPresheafedSpace
hy : y ∈ V.carrier
⊢ y ∈ Subtype.val '' {x | IsUnit (↑(germ X.presheaf x) f)}
[PROOFSTEP]
use(⟨y, i.le hy⟩ : U)
[GOAL]
case h
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
x : { x // x ∈ U }
hx : x ∈ {x | IsUnit (↑(germ X.presheaf x) f)}
V : Opens ↑↑X.toPresheafedSpace
i : V ⟶ U
hxV : ↑x ∈ V
hf : IsUnit (↑(X.presheaf.map i.op) f)
y : ↑↑X.toPresheafedSpace
hy : y ∈ V.carrier
⊢ { val := y, property := (_ : y ∈ ↑U) } ∈ {x | IsUnit (↑(germ X.presheaf x) f)} ∧
    ↑{ val := y, property := (_ : y ∈ ↑U) } = y
[PROOFSTEP]
rw [Set.mem_setOf_eq]
[GOAL]
case h
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
x : { x // x ∈ U }
hx : x ∈ {x | IsUnit (↑(germ X.presheaf x) f)}
V : Opens ↑↑X.toPresheafedSpace
i : V ⟶ U
hxV : ↑x ∈ V
hf : IsUnit (↑(X.presheaf.map i.op) f)
y : ↑↑X.toPresheafedSpace
hy : y ∈ V.carrier
⊢ IsUnit (↑(germ X.presheaf { val := y, property := (_ : y ∈ ↑U) }) f) ∧ ↑{ val := y, property := (_ : y ∈ ↑U) } = y
[PROOFSTEP]
constructor
[GOAL]
case h.left
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
x : { x // x ∈ U }
hx : x ∈ {x | IsUnit (↑(germ X.presheaf x) f)}
V : Opens ↑↑X.toPresheafedSpace
i : V ⟶ U
hxV : ↑x ∈ V
hf : IsUnit (↑(X.presheaf.map i.op) f)
y : ↑↑X.toPresheafedSpace
hy : y ∈ V.carrier
⊢ IsUnit (↑(germ X.presheaf { val := y, property := (_ : y ∈ ↑U) }) f)
[PROOFSTEP]
convert RingHom.isUnit_map (X.presheaf.germ ⟨y, hy⟩) hf
[GOAL]
case h.e'_3
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
x : { x // x ∈ U }
hx : x ∈ {x | IsUnit (↑(germ X.presheaf x) f)}
V : Opens ↑↑X.toPresheafedSpace
i : V ⟶ U
hxV : ↑x ∈ V
hf : IsUnit (↑(X.presheaf.map i.op) f)
y : ↑↑X.toPresheafedSpace
hy : y ∈ V.carrier
⊢ ↑(germ X.presheaf { val := y, property := (_ : y ∈ ↑U) }) f =
    ↑(germ X.presheaf { val := y, property := hy }) (↑(X.presheaf.map i.op) f)
[PROOFSTEP]
exact (X.presheaf.germ_res_apply i ⟨y, hy⟩ f).symm
[GOAL]
case h.right
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
x : { x // x ∈ U }
hx : x ∈ {x | IsUnit (↑(germ X.presheaf x) f)}
V : Opens ↑↑X.toPresheafedSpace
i : V ⟶ U
hxV : ↑x ∈ V
hf : IsUnit (↑(X.presheaf.map i.op) f)
y : ↑↑X.toPresheafedSpace
hy : y ∈ V.carrier
⊢ ↑{ val := y, property := (_ : y ∈ ↑U) } = y
[PROOFSTEP]
rfl
[GOAL]
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
x : { x // x ∈ U }
⊢ ↑x ∈ basicOpen X f ↔ IsUnit (↑(germ X.presheaf x) f)
[PROOFSTEP]
constructor
[GOAL]
case mp
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
x : { x // x ∈ U }
⊢ ↑x ∈ basicOpen X f → IsUnit (↑(germ X.presheaf x) f)
[PROOFSTEP]
rintro ⟨x, hx, a⟩
[GOAL]
case mp.intro.intro
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
x✝ x : { x // x ∈ U }
hx : x ∈ {x | IsUnit (↑(germ X.presheaf x) f)}
a : ↑x = ↑x✝
⊢ IsUnit (↑(germ X.presheaf x✝) f)
[PROOFSTEP]
cases Subtype.eq a
[GOAL]
case mp.intro.intro.refl
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
x : { x // x ∈ U }
hx : x ∈ {x | IsUnit (↑(germ X.presheaf x) f)}
a : ↑x = ↑x
⊢ IsUnit (↑(germ X.presheaf x) f)
[PROOFSTEP]
exact hx
[GOAL]
case mpr
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
x : { x // x ∈ U }
⊢ IsUnit (↑(germ X.presheaf x) f) → ↑x ∈ basicOpen X f
[PROOFSTEP]
intro h
[GOAL]
case mpr
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
x : { x // x ∈ U }
h : IsUnit (↑(germ X.presheaf x) f)
⊢ ↑x ∈ basicOpen X f
[PROOFSTEP]
exact ⟨x, h, rfl⟩
[GOAL]
X : RingedSpace
f : ↑(X.presheaf.obj (op ⊤))
x : ↑↑X.toPresheafedSpace
⊢ x ∈ ⊤
[PROOFSTEP]
trivial
[GOAL]
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
⊢ basicOpen X f ≤ U
[PROOFSTEP]
rintro _ ⟨x, _, rfl⟩
[GOAL]
case intro.intro
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
x : { x // x ∈ U }
left✝ : x ∈ {x | IsUnit (↑(germ X.presheaf x) f)}
⊢ ↑x ∈ ↑U
[PROOFSTEP]
exact x.2
[GOAL]
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
⊢ IsUnit (↑(X.presheaf.map (homOfLE (_ : basicOpen X f ≤ U)).op) f)
[PROOFSTEP]
apply isUnit_of_isUnit_germ
[GOAL]
case h
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
⊢ ∀ (x : { x // x ∈ basicOpen X f }),
    IsUnit (↑(germ X.presheaf x) (↑(X.presheaf.map (homOfLE (_ : basicOpen X f ≤ U)).op) f))
[PROOFSTEP]
rintro ⟨_, ⟨x, (hx : IsUnit _), rfl⟩⟩
[GOAL]
case h.mk.intro.intro
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
x : { x // x ∈ U }
hx : IsUnit (↑(germ X.presheaf x) f)
⊢ IsUnit
    (↑(germ X.presheaf { val := ↑x, property := (_ : ∃ a, a ∈ {x | IsUnit (↑(germ X.presheaf x) f)} ∧ ↑a = ↑x) })
      (↑(X.presheaf.map (homOfLE (_ : basicOpen X f ≤ U)).op) f))
[PROOFSTEP]
convert hx
[GOAL]
case h.e'_3
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
x : { x // x ∈ U }
hx : IsUnit (↑(germ X.presheaf x) f)
⊢ ↑(germ X.presheaf { val := ↑x, property := (_ : ∃ a, a ∈ {x | IsUnit (↑(germ X.presheaf x) f)} ∧ ↑a = ↑x) })
      (↑(X.presheaf.map (homOfLE (_ : basicOpen X f ≤ U)).op) f) =
    ↑(germ X.presheaf x) f
[PROOFSTEP]
convert X.presheaf.germ_res_apply _ _ _
[GOAL]
X : RingedSpace
U V : (Opens ↑↑X.toPresheafedSpace)ᵒᵖ
i : U ⟶ V
f : ↑(X.presheaf.obj U)
⊢ basicOpen X (↑(X.presheaf.map i) f) = V.unop ⊓ basicOpen X f
[PROOFSTEP]
induction U using Opposite.rec'
[GOAL]
case h
X : RingedSpace
V : (Opens ↑↑X.toPresheafedSpace)ᵒᵖ
X✝ : Opens ↑↑X.toPresheafedSpace
i : op X✝ ⟶ V
f : ↑(X.presheaf.obj (op X✝))
⊢ basicOpen X (↑(X.presheaf.map i) f) = V.unop ⊓ basicOpen X f
[PROOFSTEP]
induction V using Opposite.rec'
[GOAL]
case h.h
X : RingedSpace
X✝¹ : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op X✝¹))
X✝ : Opens ↑↑X.toPresheafedSpace
i : op X✝¹ ⟶ op X✝
⊢ basicOpen X (↑(X.presheaf.map i) f) = (op X✝).unop ⊓ basicOpen X f
[PROOFSTEP]
let g := i.unop
[GOAL]
case h.h
X : RingedSpace
X✝¹ : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op X✝¹))
X✝ : Opens ↑↑X.toPresheafedSpace
i : op X✝¹ ⟶ op X✝
g : (op X✝).unop ⟶ (op X✝¹).unop := i.unop
⊢ basicOpen X (↑(X.presheaf.map i) f) = (op X✝).unop ⊓ basicOpen X f
[PROOFSTEP]
have : i = g.op := rfl
[GOAL]
case h.h
X : RingedSpace
X✝¹ : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op X✝¹))
X✝ : Opens ↑↑X.toPresheafedSpace
i : op X✝¹ ⟶ op X✝
g : (op X✝).unop ⟶ (op X✝¹).unop := i.unop
this : i = g.op
⊢ basicOpen X (↑(X.presheaf.map i) f) = (op X✝).unop ⊓ basicOpen X f
[PROOFSTEP]
clear_value g
[GOAL]
case h.h
X : RingedSpace
X✝¹ : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op X✝¹))
X✝ : Opens ↑↑X.toPresheafedSpace
i : op X✝¹ ⟶ op X✝
g : (op X✝).unop ⟶ (op X✝¹).unop
this : i = g.op
⊢ basicOpen X (↑(X.presheaf.map i) f) = (op X✝).unop ⊓ basicOpen X f
[PROOFSTEP]
subst this
[GOAL]
case h.h
X : RingedSpace
X✝¹ : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op X✝¹))
X✝ : Opens ↑↑X.toPresheafedSpace
g : (op X✝).unop ⟶ (op X✝¹).unop
⊢ basicOpen X (↑(X.presheaf.map g.op) f) = (op X✝).unop ⊓ basicOpen X f
[PROOFSTEP]
ext
[GOAL]
case h.h.h.h
X : RingedSpace
X✝¹ : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op X✝¹))
X✝ : Opens ↑↑X.toPresheafedSpace
g : (op X✝).unop ⟶ (op X✝¹).unop
x✝ : ↑↑X.toPresheafedSpace
⊢ x✝ ∈ ↑(basicOpen X (↑(X.presheaf.map g.op) f)) ↔ x✝ ∈ ↑((op X✝).unop ⊓ basicOpen X f)
[PROOFSTEP]
constructor
[GOAL]
case h.h.h.h.mp
X : RingedSpace
X✝¹ : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op X✝¹))
X✝ : Opens ↑↑X.toPresheafedSpace
g : (op X✝).unop ⟶ (op X✝¹).unop
x✝ : ↑↑X.toPresheafedSpace
⊢ x✝ ∈ ↑(basicOpen X (↑(X.presheaf.map g.op) f)) → x✝ ∈ ↑((op X✝).unop ⊓ basicOpen X f)
[PROOFSTEP]
rintro ⟨x, hx : IsUnit _, rfl⟩
[GOAL]
case h.h.h.h.mp.intro.intro
X : RingedSpace
X✝¹ : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op X✝¹))
X✝ : Opens ↑↑X.toPresheafedSpace
g : (op X✝).unop ⟶ (op X✝¹).unop
x : { x // x ∈ (op X✝).unop }
hx : IsUnit (↑(germ X.presheaf x) (↑(X.presheaf.map g.op) f))
⊢ ↑x ∈ ↑((op X✝).unop ⊓ basicOpen X f)
[PROOFSTEP]
erw [X.presheaf.germ_res_apply _ _ _] at hx
[GOAL]
case h.h.h.h.mp.intro.intro
X : RingedSpace
X✝¹ : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op X✝¹))
X✝ : Opens ↑↑X.toPresheafedSpace
g : (op X✝).unop ⟶ (op X✝¹).unop
x : { x // x ∈ (op X✝).unop }
hx : IsUnit (↑(germ X.presheaf ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑(op X✝¹).unop) }) x)) f)
⊢ ↑x ∈ ↑((op X✝).unop ⊓ basicOpen X f)
[PROOFSTEP]
exact ⟨x.2, g x, hx, rfl⟩
[GOAL]
case h.h.h.h.mpr
X : RingedSpace
X✝¹ : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op X✝¹))
X✝ : Opens ↑↑X.toPresheafedSpace
g : (op X✝).unop ⟶ (op X✝¹).unop
x✝ : ↑↑X.toPresheafedSpace
⊢ x✝ ∈ ↑((op X✝).unop ⊓ basicOpen X f) → x✝ ∈ ↑(basicOpen X (↑(X.presheaf.map g.op) f))
[PROOFSTEP]
rintro ⟨hxV, x, hx, rfl⟩
[GOAL]
case h.h.h.h.mpr.intro.intro.intro
X : RingedSpace
X✝¹ : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op X✝¹))
X✝ : Opens ↑↑X.toPresheafedSpace
g : (op X✝).unop ⟶ (op X✝¹).unop
x : { x // x ∈ (op X✝¹).unop }
hx : x ∈ {x | IsUnit (↑(germ X.presheaf x) f)}
hxV : ↑x ∈ ↑(op X✝).unop
⊢ ↑x ∈ ↑(basicOpen X (↑(X.presheaf.map g.op) f))
[PROOFSTEP]
refine' ⟨⟨x, hxV⟩, (_ : IsUnit _), rfl⟩
[GOAL]
case h.h.h.h.mpr.intro.intro.intro
X : RingedSpace
X✝¹ : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op X✝¹))
X✝ : Opens ↑↑X.toPresheafedSpace
g : (op X✝).unop ⟶ (op X✝¹).unop
x : { x // x ∈ (op X✝¹).unop }
hx : x ∈ {x | IsUnit (↑(germ X.presheaf x) f)}
hxV : ↑x ∈ ↑(op X✝).unop
⊢ IsUnit (↑(germ X.presheaf { val := ↑x, property := hxV }) (↑(X.presheaf.map g.op) f))
[PROOFSTEP]
erw [X.presheaf.germ_res_apply _ _ _]
[GOAL]
case h.h.h.h.mpr.intro.intro.intro
X : RingedSpace
X✝¹ : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op X✝¹))
X✝ : Opens ↑↑X.toPresheafedSpace
g : (op X✝).unop ⟶ (op X✝¹).unop
x : { x // x ∈ (op X✝¹).unop }
hx : x ∈ {x | IsUnit (↑(germ X.presheaf x) f)}
hxV : ↑x ∈ ↑(op X✝).unop
⊢ IsUnit
    (↑(germ X.presheaf ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑(op X✝¹).unop) }) { val := ↑x, property := hxV }))
      f)
[PROOFSTEP]
exact hx
[GOAL]
X : RingedSpace
U V : (Opens ↑↑X.toPresheafedSpace)ᵒᵖ
i : U ⟶ V
inst✝ : IsIso i
f : ↑(X.presheaf.obj U)
⊢ basicOpen X (↑(X.presheaf.map i) f) = basicOpen X f
[PROOFSTEP]
apply le_antisymm
[GOAL]
case a
X : RingedSpace
U V : (Opens ↑↑X.toPresheafedSpace)ᵒᵖ
i : U ⟶ V
inst✝ : IsIso i
f : ↑(X.presheaf.obj U)
⊢ basicOpen X (↑(X.presheaf.map i) f) ≤ basicOpen X f
[PROOFSTEP]
rw [X.basicOpen_res i f]
[GOAL]
case a
X : RingedSpace
U V : (Opens ↑↑X.toPresheafedSpace)ᵒᵖ
i : U ⟶ V
inst✝ : IsIso i
f : ↑(X.presheaf.obj U)
⊢ V.unop ⊓ basicOpen X f ≤ basicOpen X f
[PROOFSTEP]
exact inf_le_right
[GOAL]
case a
X : RingedSpace
U V : (Opens ↑↑X.toPresheafedSpace)ᵒᵖ
i : U ⟶ V
inst✝ : IsIso i
f : ↑(X.presheaf.obj U)
⊢ basicOpen X f ≤ basicOpen X (↑(X.presheaf.map i) f)
[PROOFSTEP]
have := X.basicOpen_res (inv i) (X.presheaf.map i f)
[GOAL]
case a
X : RingedSpace
U V : (Opens ↑↑X.toPresheafedSpace)ᵒᵖ
i : U ⟶ V
inst✝ : IsIso i
f : ↑(X.presheaf.obj U)
this : basicOpen X (↑(X.presheaf.map (inv i)) (↑(X.presheaf.map i) f)) = U.unop ⊓ basicOpen X (↑(X.presheaf.map i) f)
⊢ basicOpen X f ≤ basicOpen X (↑(X.presheaf.map i) f)
[PROOFSTEP]
rw [← comp_apply, ← X.presheaf.map_comp, IsIso.hom_inv_id, X.presheaf.map_id, id_apply] at this
[GOAL]
case a
X : RingedSpace
U V : (Opens ↑↑X.toPresheafedSpace)ᵒᵖ
i : U ⟶ V
inst✝ : IsIso i
f : ↑(X.presheaf.obj U)
this : basicOpen X f = U.unop ⊓ basicOpen X (↑(X.presheaf.map i) f)
⊢ basicOpen X f ≤ basicOpen X (↑(X.presheaf.map i) f)
[PROOFSTEP]
rw [this]
[GOAL]
case a
X : RingedSpace
U V : (Opens ↑↑X.toPresheafedSpace)ᵒᵖ
i : U ⟶ V
inst✝ : IsIso i
f : ↑(X.presheaf.obj U)
this : basicOpen X f = U.unop ⊓ basicOpen X (↑(X.presheaf.map i) f)
⊢ U.unop ⊓ basicOpen X (↑(X.presheaf.map i) f) ≤ basicOpen X (↑(X.presheaf.map i) f)
[PROOFSTEP]
exact inf_le_right
[GOAL]
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f g : ↑(X.presheaf.obj (op U))
⊢ basicOpen X (f * g) = basicOpen X f ⊓ basicOpen X g
[PROOFSTEP]
ext1
[GOAL]
case h
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f g : ↑(X.presheaf.obj (op U))
⊢ ↑(basicOpen X (f * g)) = ↑(basicOpen X f ⊓ basicOpen X g)
[PROOFSTEP]
dsimp [RingedSpace.basicOpen]
[GOAL]
case h
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f g : ↑(X.presheaf.obj (op U))
⊢ Subtype.val '' {x | IsUnit (↑(germ X.presheaf x) (f * g))} =
    Subtype.val '' {x | IsUnit (↑(germ X.presheaf x) f)} ∩ Subtype.val '' {x | IsUnit (↑(germ X.presheaf x) g)}
[PROOFSTEP]
rw [← Set.image_inter Subtype.coe_injective]
[GOAL]
case h
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f g : ↑(X.presheaf.obj (op U))
⊢ Subtype.val '' {x | IsUnit (↑(germ X.presheaf x) (f * g))} =
    (fun a => ↑a) '' ({x | IsUnit (↑(germ X.presheaf x) f)} ∩ {x | IsUnit (↑(germ X.presheaf x) g)})
[PROOFSTEP]
congr
[GOAL]
case h
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f g : ↑(X.presheaf.obj (op U))
⊢ Subtype.val '' {x | IsUnit (↑(germ X.presheaf x) (f * g))} =
    (fun a => ↑a) '' ({x | IsUnit (↑(germ X.presheaf x) f)} ∩ {x | IsUnit (↑(germ X.presheaf x) g)})
[PROOFSTEP]
ext x
[GOAL]
case h.h
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f g : ↑(X.presheaf.obj (op U))
x : ↑↑X.toPresheafedSpace
⊢ x ∈ Subtype.val '' {x | IsUnit (↑(germ X.presheaf x) (f * g))} ↔
    x ∈ (fun a => ↑a) '' ({x | IsUnit (↑(germ X.presheaf x) f)} ∩ {x | IsUnit (↑(germ X.presheaf x) g)})
[PROOFSTEP]
simp [map_mul, Set.mem_image]
[GOAL]
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
hf : IsUnit f
⊢ basicOpen X f = U
[PROOFSTEP]
apply le_antisymm
[GOAL]
case a
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
hf : IsUnit f
⊢ basicOpen X f ≤ U
[PROOFSTEP]
exact X.basicOpen_le f
[GOAL]
case a
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
hf : IsUnit f
⊢ U ≤ basicOpen X f
[PROOFSTEP]
intro x hx
[GOAL]
case a
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
hf : IsUnit f
x : ↑↑X.toPresheafedSpace
hx : x ∈ ↑U
⊢ x ∈ ↑(basicOpen X f)
[PROOFSTEP]
erw [X.mem_basicOpen f (⟨x, hx⟩ : U)]
[GOAL]
case a
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
hf : IsUnit f
x : ↑↑X.toPresheafedSpace
hx : x ∈ ↑U
⊢ IsUnit (↑(germ X.presheaf { val := x, property := hx }) f)
[PROOFSTEP]
exact RingHom.isUnit_map _ hf


[GOAL]
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
I : Ideal R
⊢ ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I
[PROOFSTEP]
refine'
  IsNoetherian.induction (P := fun I => ∃ Z : Multiset (PrimeSpectrum R), Multiset.prod (Z.map asIdeal) ≤ I)
    (fun (M : Ideal R) hgt => _) I
[GOAL]
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
I M : Ideal R
hgt : ∀ (J : Submodule R R), J > M → (fun I => ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I) J
⊢ (fun I => ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I) M
[PROOFSTEP]
by_cases h_prM : M.IsPrime
[GOAL]
case pos
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
I M : Ideal R
hgt : ∀ (J : Submodule R R), J > M → (fun I => ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I) J
h_prM : Ideal.IsPrime M
⊢ (fun I => ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I) M
[PROOFSTEP]
use{⟨M, h_prM⟩}
[GOAL]
case h
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
I M : Ideal R
hgt : ∀ (J : Submodule R R), J > M → (fun I => ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I) J
h_prM : Ideal.IsPrime M
⊢ Multiset.prod (Multiset.map asIdeal {{ asIdeal := M, IsPrime := h_prM }}) ≤ M
[PROOFSTEP]
rw [Multiset.map_singleton, Multiset.prod_singleton]
[GOAL]
case neg
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
I M : Ideal R
hgt : ∀ (J : Submodule R R), J > M → (fun I => ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I) J
h_prM : ¬Ideal.IsPrime M
⊢ (fun I => ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I) M
[PROOFSTEP]
by_cases htop : M = ⊤
[GOAL]
case pos
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
I M : Ideal R
hgt : ∀ (J : Submodule R R), J > M → (fun I => ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I) J
h_prM : ¬Ideal.IsPrime M
htop : M = ⊤
⊢ (fun I => ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I) M
[PROOFSTEP]
rw [htop]
[GOAL]
case pos
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
I M : Ideal R
hgt : ∀ (J : Submodule R R), J > M → (fun I => ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I) J
h_prM : ¬Ideal.IsPrime M
htop : M = ⊤
⊢ (fun I => ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I) ⊤
[PROOFSTEP]
exact ⟨0, le_top⟩
[GOAL]
case neg
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
I M : Ideal R
hgt : ∀ (J : Submodule R R), J > M → (fun I => ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I) J
h_prM : ¬Ideal.IsPrime M
htop : ¬M = ⊤
⊢ (fun I => ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I) M
[PROOFSTEP]
have lt_add : ∀ (z) (_ : z ∉ M), M < M + span R { z } :=
  by
  intro z hz
  refine' lt_of_le_of_ne le_sup_left fun m_eq => hz _
  rw [m_eq]
  exact Ideal.mem_sup_right (mem_span_singleton_self z)
[GOAL]
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
I M : Ideal R
hgt : ∀ (J : Submodule R R), J > M → (fun I => ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I) J
h_prM : ¬Ideal.IsPrime M
htop : ¬M = ⊤
⊢ ∀ (z : R), ¬z ∈ M → M < M + span R {z}
[PROOFSTEP]
intro z hz
[GOAL]
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
I M : Ideal R
hgt : ∀ (J : Submodule R R), J > M → (fun I => ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I) J
h_prM : ¬Ideal.IsPrime M
htop : ¬M = ⊤
z : R
hz : ¬z ∈ M
⊢ M < M + span R {z}
[PROOFSTEP]
refine' lt_of_le_of_ne le_sup_left fun m_eq => hz _
[GOAL]
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
I M : Ideal R
hgt : ∀ (J : Submodule R R), J > M → (fun I => ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I) J
h_prM : ¬Ideal.IsPrime M
htop : ¬M = ⊤
z : R
hz : ¬z ∈ M
m_eq : M = M + span R {z}
⊢ z ∈ M
[PROOFSTEP]
rw [m_eq]
[GOAL]
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
I M : Ideal R
hgt : ∀ (J : Submodule R R), J > M → (fun I => ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I) J
h_prM : ¬Ideal.IsPrime M
htop : ¬M = ⊤
z : R
hz : ¬z ∈ M
m_eq : M = M + span R {z}
⊢ z ∈ M + span R {z}
[PROOFSTEP]
exact Ideal.mem_sup_right (mem_span_singleton_self z)
[GOAL]
case neg
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
I M : Ideal R
hgt : ∀ (J : Submodule R R), J > M → (fun I => ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I) J
h_prM : ¬Ideal.IsPrime M
htop : ¬M = ⊤
lt_add : ∀ (z : R), ¬z ∈ M → M < M + span R {z}
⊢ (fun I => ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I) M
[PROOFSTEP]
obtain ⟨x, hx, y, hy, hxy⟩ := (Ideal.not_isPrime_iff.mp h_prM).resolve_left htop
[GOAL]
case neg.intro.intro.intro.intro
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
I M : Ideal R
hgt : ∀ (J : Submodule R R), J > M → (fun I => ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I) J
h_prM : ¬Ideal.IsPrime M
htop : ¬M = ⊤
lt_add : ∀ (z : R), ¬z ∈ M → M < M + span R {z}
x : R
hx : ¬x ∈ M
y : R
hy : ¬y ∈ M
hxy : x * y ∈ M
⊢ (fun I => ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I) M
[PROOFSTEP]
obtain ⟨Wx, h_Wx⟩ := hgt (M + span R { x }) (lt_add _ hx)
[GOAL]
case neg.intro.intro.intro.intro.intro
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
I M : Ideal R
hgt : ∀ (J : Submodule R R), J > M → (fun I => ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I) J
h_prM : ¬Ideal.IsPrime M
htop : ¬M = ⊤
lt_add : ∀ (z : R), ¬z ∈ M → M < M + span R {z}
x : R
hx : ¬x ∈ M
y : R
hy : ¬y ∈ M
hxy : x * y ∈ M
Wx : Multiset (PrimeSpectrum R)
h_Wx : Multiset.prod (Multiset.map asIdeal Wx) ≤ M + span R {x}
⊢ (fun I => ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I) M
[PROOFSTEP]
obtain ⟨Wy, h_Wy⟩ := hgt (M + span R { y }) (lt_add _ hy)
[GOAL]
case neg.intro.intro.intro.intro.intro.intro
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
I M : Ideal R
hgt : ∀ (J : Submodule R R), J > M → (fun I => ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I) J
h_prM : ¬Ideal.IsPrime M
htop : ¬M = ⊤
lt_add : ∀ (z : R), ¬z ∈ M → M < M + span R {z}
x : R
hx : ¬x ∈ M
y : R
hy : ¬y ∈ M
hxy : x * y ∈ M
Wx : Multiset (PrimeSpectrum R)
h_Wx : Multiset.prod (Multiset.map asIdeal Wx) ≤ M + span R {x}
Wy : Multiset (PrimeSpectrum R)
h_Wy : Multiset.prod (Multiset.map asIdeal Wy) ≤ M + span R {y}
⊢ (fun I => ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I) M
[PROOFSTEP]
use Wx + Wy
[GOAL]
case h
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
I M : Ideal R
hgt : ∀ (J : Submodule R R), J > M → (fun I => ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I) J
h_prM : ¬Ideal.IsPrime M
htop : ¬M = ⊤
lt_add : ∀ (z : R), ¬z ∈ M → M < M + span R {z}
x : R
hx : ¬x ∈ M
y : R
hy : ¬y ∈ M
hxy : x * y ∈ M
Wx : Multiset (PrimeSpectrum R)
h_Wx : Multiset.prod (Multiset.map asIdeal Wx) ≤ M + span R {x}
Wy : Multiset (PrimeSpectrum R)
h_Wy : Multiset.prod (Multiset.map asIdeal Wy) ≤ M + span R {y}
⊢ Multiset.prod (Multiset.map asIdeal (Wx + Wy)) ≤ M
[PROOFSTEP]
rw [Multiset.map_add, Multiset.prod_add]
[GOAL]
case h
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
I M : Ideal R
hgt : ∀ (J : Submodule R R), J > M → (fun I => ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I) J
h_prM : ¬Ideal.IsPrime M
htop : ¬M = ⊤
lt_add : ∀ (z : R), ¬z ∈ M → M < M + span R {z}
x : R
hx : ¬x ∈ M
y : R
hy : ¬y ∈ M
hxy : x * y ∈ M
Wx : Multiset (PrimeSpectrum R)
h_Wx : Multiset.prod (Multiset.map asIdeal Wx) ≤ M + span R {x}
Wy : Multiset (PrimeSpectrum R)
h_Wy : Multiset.prod (Multiset.map asIdeal Wy) ≤ M + span R {y}
⊢ Multiset.prod (Multiset.map asIdeal Wx) * Multiset.prod (Multiset.map asIdeal Wy) ≤ M
[PROOFSTEP]
apply le_trans (Submodule.mul_le_mul h_Wx h_Wy)
[GOAL]
case h
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
I M : Ideal R
hgt : ∀ (J : Submodule R R), J > M → (fun I => ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I) J
h_prM : ¬Ideal.IsPrime M
htop : ¬M = ⊤
lt_add : ∀ (z : R), ¬z ∈ M → M < M + span R {z}
x : R
hx : ¬x ∈ M
y : R
hy : ¬y ∈ M
hxy : x * y ∈ M
Wx : Multiset (PrimeSpectrum R)
h_Wx : Multiset.prod (Multiset.map asIdeal Wx) ≤ M + span R {x}
Wy : Multiset (PrimeSpectrum R)
h_Wy : Multiset.prod (Multiset.map asIdeal Wy) ≤ M + span R {y}
⊢ (M + span R {x}) * (M + span R {y}) ≤ M
[PROOFSTEP]
rw [add_mul]
[GOAL]
case h
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
I M : Ideal R
hgt : ∀ (J : Submodule R R), J > M → (fun I => ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I) J
h_prM : ¬Ideal.IsPrime M
htop : ¬M = ⊤
lt_add : ∀ (z : R), ¬z ∈ M → M < M + span R {z}
x : R
hx : ¬x ∈ M
y : R
hy : ¬y ∈ M
hxy : x * y ∈ M
Wx : Multiset (PrimeSpectrum R)
h_Wx : Multiset.prod (Multiset.map asIdeal Wx) ≤ M + span R {x}
Wy : Multiset (PrimeSpectrum R)
h_Wy : Multiset.prod (Multiset.map asIdeal Wy) ≤ M + span R {y}
⊢ M * (M + span R {y}) + span R {x} * (M + span R {y}) ≤ M
[PROOFSTEP]
apply sup_le (show M * (M + span R { y }) ≤ M from Ideal.mul_le_right)
[GOAL]
case h
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
I M : Ideal R
hgt : ∀ (J : Submodule R R), J > M → (fun I => ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I) J
h_prM : ¬Ideal.IsPrime M
htop : ¬M = ⊤
lt_add : ∀ (z : R), ¬z ∈ M → M < M + span R {z}
x : R
hx : ¬x ∈ M
y : R
hy : ¬y ∈ M
hxy : x * y ∈ M
Wx : Multiset (PrimeSpectrum R)
h_Wx : Multiset.prod (Multiset.map asIdeal Wx) ≤ M + span R {x}
Wy : Multiset (PrimeSpectrum R)
h_Wy : Multiset.prod (Multiset.map asIdeal Wy) ≤ M + span R {y}
⊢ span R {x} * (M + span R {y}) ≤ M
[PROOFSTEP]
rw [mul_add]
[GOAL]
case h
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
I M : Ideal R
hgt : ∀ (J : Submodule R R), J > M → (fun I => ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I) J
h_prM : ¬Ideal.IsPrime M
htop : ¬M = ⊤
lt_add : ∀ (z : R), ¬z ∈ M → M < M + span R {z}
x : R
hx : ¬x ∈ M
y : R
hy : ¬y ∈ M
hxy : x * y ∈ M
Wx : Multiset (PrimeSpectrum R)
h_Wx : Multiset.prod (Multiset.map asIdeal Wx) ≤ M + span R {x}
Wy : Multiset (PrimeSpectrum R)
h_Wy : Multiset.prod (Multiset.map asIdeal Wy) ≤ M + span R {y}
⊢ span R {x} * M + span R {x} * span R {y} ≤ M
[PROOFSTEP]
apply sup_le (show span R { x } * M ≤ M from Ideal.mul_le_left)
[GOAL]
case h
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
I M : Ideal R
hgt : ∀ (J : Submodule R R), J > M → (fun I => ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I) J
h_prM : ¬Ideal.IsPrime M
htop : ¬M = ⊤
lt_add : ∀ (z : R), ¬z ∈ M → M < M + span R {z}
x : R
hx : ¬x ∈ M
y : R
hy : ¬y ∈ M
hxy : x * y ∈ M
Wx : Multiset (PrimeSpectrum R)
h_Wx : Multiset.prod (Multiset.map asIdeal Wx) ≤ M + span R {x}
Wy : Multiset (PrimeSpectrum R)
h_Wy : Multiset.prod (Multiset.map asIdeal Wy) ≤ M + span R {y}
⊢ span R {x} * span R {y} ≤ M
[PROOFSTEP]
rwa [span_mul_span, Set.singleton_mul_singleton, span_singleton_le_iff_mem]
[GOAL]
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
h_fA : ¬IsField A
I : Ideal A
h_nzI : I ≠ ⊥
⊢ ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I ∧ Multiset.prod (Multiset.map asIdeal Z) ≠ ⊥
[PROOFSTEP]
revert h_nzI
[GOAL]
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
h_fA : ¬IsField A
I : Ideal A
⊢ I ≠ ⊥ → ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I ∧ Multiset.prod (Multiset.map asIdeal Z) ≠ ⊥
[PROOFSTEP]
refine'
  IsNoetherian.induction (P := fun I =>
    I ≠ ⊥ → ∃ Z : Multiset (PrimeSpectrum A), Multiset.prod (Z.map asIdeal) ≤ I ∧ Multiset.prod (Z.map asIdeal) ≠ ⊥)
    (fun (M : Ideal A) hgt => _) I
[GOAL]
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
h_fA : ¬IsField A
I M : Ideal A
hgt :
  ∀ (J : Submodule A A),
    J > M →
      (fun I => I ≠ ⊥ → ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I ∧ Multiset.prod (Multiset.map asIdeal Z) ≠ ⊥) J
⊢ (fun I => I ≠ ⊥ → ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I ∧ Multiset.prod (Multiset.map asIdeal Z) ≠ ⊥) M
[PROOFSTEP]
intro h_nzM
[GOAL]
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
h_fA : ¬IsField A
I M : Ideal A
hgt :
  ∀ (J : Submodule A A),
    J > M →
      (fun I => I ≠ ⊥ → ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I ∧ Multiset.prod (Multiset.map asIdeal Z) ≠ ⊥) J
h_nzM : M ≠ ⊥
⊢ ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ M ∧ Multiset.prod (Multiset.map asIdeal Z) ≠ ⊥
[PROOFSTEP]
have hA_nont : Nontrivial A
[GOAL]
case hA_nont
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
h_fA : ¬IsField A
I M : Ideal A
hgt :
  ∀ (J : Submodule A A),
    J > M →
      (fun I => I ≠ ⊥ → ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I ∧ Multiset.prod (Multiset.map asIdeal Z) ≠ ⊥) J
h_nzM : M ≠ ⊥
⊢ Nontrivial A
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
h_fA : ¬IsField A
I M : Ideal A
hgt :
  ∀ (J : Submodule A A),
    J > M →
      (fun I => I ≠ ⊥ → ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I ∧ Multiset.prod (Multiset.map asIdeal Z) ≠ ⊥) J
h_nzM : M ≠ ⊥
hA_nont : Nontrivial A
⊢ ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ M ∧ Multiset.prod (Multiset.map asIdeal Z) ≠ ⊥
[PROOFSTEP]
apply IsDomain.toNontrivial
[GOAL]
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
h_fA : ¬IsField A
I M : Ideal A
hgt :
  ∀ (J : Submodule A A),
    J > M →
      (fun I => I ≠ ⊥ → ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I ∧ Multiset.prod (Multiset.map asIdeal Z) ≠ ⊥) J
h_nzM : M ≠ ⊥
hA_nont : Nontrivial A
⊢ ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ M ∧ Multiset.prod (Multiset.map asIdeal Z) ≠ ⊥
[PROOFSTEP]
by_cases h_topM : M = ⊤
[GOAL]
case pos
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
h_fA : ¬IsField A
I M : Ideal A
hgt :
  ∀ (J : Submodule A A),
    J > M →
      (fun I => I ≠ ⊥ → ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I ∧ Multiset.prod (Multiset.map asIdeal Z) ≠ ⊥) J
h_nzM : M ≠ ⊥
hA_nont : Nontrivial A
h_topM : M = ⊤
⊢ ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ M ∧ Multiset.prod (Multiset.map asIdeal Z) ≠ ⊥
[PROOFSTEP]
rcases h_topM with rfl
[GOAL]
case pos
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
h_fA : ¬IsField A
I : Ideal A
hA_nont : Nontrivial A
hgt :
  ∀ (J : Submodule A A),
    J > ⊤ →
      (fun I => I ≠ ⊥ → ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I ∧ Multiset.prod (Multiset.map asIdeal Z) ≠ ⊥) J
h_nzM : ⊤ ≠ ⊥
⊢ ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ ⊤ ∧ Multiset.prod (Multiset.map asIdeal Z) ≠ ⊥
[PROOFSTEP]
obtain ⟨p_id, h_nzp, h_pp⟩ : ∃ p : Ideal A, p ≠ ⊥ ∧ p.IsPrime := by apply Ring.not_isField_iff_exists_prime.mp h_fA
[GOAL]
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
h_fA : ¬IsField A
I : Ideal A
hA_nont : Nontrivial A
hgt :
  ∀ (J : Submodule A A),
    J > ⊤ →
      (fun I => I ≠ ⊥ → ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I ∧ Multiset.prod (Multiset.map asIdeal Z) ≠ ⊥) J
h_nzM : ⊤ ≠ ⊥
⊢ ∃ p, p ≠ ⊥ ∧ Ideal.IsPrime p
[PROOFSTEP]
apply Ring.not_isField_iff_exists_prime.mp h_fA
[GOAL]
case pos.intro.intro
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
h_fA : ¬IsField A
I : Ideal A
hA_nont : Nontrivial A
hgt :
  ∀ (J : Submodule A A),
    J > ⊤ →
      (fun I => I ≠ ⊥ → ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I ∧ Multiset.prod (Multiset.map asIdeal Z) ≠ ⊥) J
h_nzM : ⊤ ≠ ⊥
p_id : Ideal A
h_nzp : p_id ≠ ⊥
h_pp : Ideal.IsPrime p_id
⊢ ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ ⊤ ∧ Multiset.prod (Multiset.map asIdeal Z) ≠ ⊥
[PROOFSTEP]
use({⟨p_id, h_pp⟩} : Multiset (PrimeSpectrum A)), le_top
[GOAL]
case right
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
h_fA : ¬IsField A
I : Ideal A
hA_nont : Nontrivial A
hgt :
  ∀ (J : Submodule A A),
    J > ⊤ →
      (fun I => I ≠ ⊥ → ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I ∧ Multiset.prod (Multiset.map asIdeal Z) ≠ ⊥) J
h_nzM : ⊤ ≠ ⊥
p_id : Ideal A
h_nzp : p_id ≠ ⊥
h_pp : Ideal.IsPrime p_id
⊢ Multiset.prod (Multiset.map asIdeal {{ asIdeal := p_id, IsPrime := h_pp }}) ≠ ⊥
[PROOFSTEP]
rwa [Multiset.map_singleton, Multiset.prod_singleton]
[GOAL]
case neg
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
h_fA : ¬IsField A
I M : Ideal A
hgt :
  ∀ (J : Submodule A A),
    J > M →
      (fun I => I ≠ ⊥ → ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I ∧ Multiset.prod (Multiset.map asIdeal Z) ≠ ⊥) J
h_nzM : M ≠ ⊥
hA_nont : Nontrivial A
h_topM : ¬M = ⊤
⊢ ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ M ∧ Multiset.prod (Multiset.map asIdeal Z) ≠ ⊥
[PROOFSTEP]
by_cases h_prM : M.IsPrime
[GOAL]
case pos
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
h_fA : ¬IsField A
I M : Ideal A
hgt :
  ∀ (J : Submodule A A),
    J > M →
      (fun I => I ≠ ⊥ → ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I ∧ Multiset.prod (Multiset.map asIdeal Z) ≠ ⊥) J
h_nzM : M ≠ ⊥
hA_nont : Nontrivial A
h_topM : ¬M = ⊤
h_prM : Ideal.IsPrime M
⊢ ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ M ∧ Multiset.prod (Multiset.map asIdeal Z) ≠ ⊥
[PROOFSTEP]
use({⟨M, h_prM⟩} : Multiset (PrimeSpectrum A))
[GOAL]
case h
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
h_fA : ¬IsField A
I M : Ideal A
hgt :
  ∀ (J : Submodule A A),
    J > M →
      (fun I => I ≠ ⊥ → ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I ∧ Multiset.prod (Multiset.map asIdeal Z) ≠ ⊥) J
h_nzM : M ≠ ⊥
hA_nont : Nontrivial A
h_topM : ¬M = ⊤
h_prM : Ideal.IsPrime M
⊢ Multiset.prod (Multiset.map asIdeal {{ asIdeal := M, IsPrime := h_prM }}) ≤ M ∧
    Multiset.prod (Multiset.map asIdeal {{ asIdeal := M, IsPrime := h_prM }}) ≠ ⊥
[PROOFSTEP]
rw [Multiset.map_singleton, Multiset.prod_singleton]
[GOAL]
case h
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
h_fA : ¬IsField A
I M : Ideal A
hgt :
  ∀ (J : Submodule A A),
    J > M →
      (fun I => I ≠ ⊥ → ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I ∧ Multiset.prod (Multiset.map asIdeal Z) ≠ ⊥) J
h_nzM : M ≠ ⊥
hA_nont : Nontrivial A
h_topM : ¬M = ⊤
h_prM : Ideal.IsPrime M
⊢ { asIdeal := M, IsPrime := h_prM }.asIdeal ≤ M ∧ { asIdeal := M, IsPrime := h_prM }.asIdeal ≠ ⊥
[PROOFSTEP]
exact ⟨le_rfl, h_nzM⟩
[GOAL]
case neg
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
h_fA : ¬IsField A
I M : Ideal A
hgt :
  ∀ (J : Submodule A A),
    J > M →
      (fun I => I ≠ ⊥ → ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I ∧ Multiset.prod (Multiset.map asIdeal Z) ≠ ⊥) J
h_nzM : M ≠ ⊥
hA_nont : Nontrivial A
h_topM : ¬M = ⊤
h_prM : ¬Ideal.IsPrime M
⊢ ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ M ∧ Multiset.prod (Multiset.map asIdeal Z) ≠ ⊥
[PROOFSTEP]
obtain ⟨x, hx, y, hy, h_xy⟩ := (Ideal.not_isPrime_iff.mp h_prM).resolve_left h_topM
[GOAL]
case neg.intro.intro.intro.intro
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
h_fA : ¬IsField A
I M : Ideal A
hgt :
  ∀ (J : Submodule A A),
    J > M →
      (fun I => I ≠ ⊥ → ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I ∧ Multiset.prod (Multiset.map asIdeal Z) ≠ ⊥) J
h_nzM : M ≠ ⊥
hA_nont : Nontrivial A
h_topM : ¬M = ⊤
h_prM : ¬Ideal.IsPrime M
x : A
hx : ¬x ∈ M
y : A
hy : ¬y ∈ M
h_xy : x * y ∈ M
⊢ ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ M ∧ Multiset.prod (Multiset.map asIdeal Z) ≠ ⊥
[PROOFSTEP]
have lt_add : ∀ (z) (_ : z ∉ M), M < M + span A { z } :=
  by
  intro z hz
  refine' lt_of_le_of_ne le_sup_left fun m_eq => hz _
  rw [m_eq]
  exact mem_sup_right (mem_span_singleton_self z)
[GOAL]
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
h_fA : ¬IsField A
I M : Ideal A
hgt :
  ∀ (J : Submodule A A),
    J > M →
      (fun I => I ≠ ⊥ → ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I ∧ Multiset.prod (Multiset.map asIdeal Z) ≠ ⊥) J
h_nzM : M ≠ ⊥
hA_nont : Nontrivial A
h_topM : ¬M = ⊤
h_prM : ¬Ideal.IsPrime M
x : A
hx : ¬x ∈ M
y : A
hy : ¬y ∈ M
h_xy : x * y ∈ M
⊢ ∀ (z : A), ¬z ∈ M → M < M + span A {z}
[PROOFSTEP]
intro z hz
[GOAL]
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
h_fA : ¬IsField A
I M : Ideal A
hgt :
  ∀ (J : Submodule A A),
    J > M →
      (fun I => I ≠ ⊥ → ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I ∧ Multiset.prod (Multiset.map asIdeal Z) ≠ ⊥) J
h_nzM : M ≠ ⊥
hA_nont : Nontrivial A
h_topM : ¬M = ⊤
h_prM : ¬Ideal.IsPrime M
x : A
hx : ¬x ∈ M
y : A
hy : ¬y ∈ M
h_xy : x * y ∈ M
z : A
hz : ¬z ∈ M
⊢ M < M + span A {z}
[PROOFSTEP]
refine' lt_of_le_of_ne le_sup_left fun m_eq => hz _
[GOAL]
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
h_fA : ¬IsField A
I M : Ideal A
hgt :
  ∀ (J : Submodule A A),
    J > M →
      (fun I => I ≠ ⊥ → ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I ∧ Multiset.prod (Multiset.map asIdeal Z) ≠ ⊥) J
h_nzM : M ≠ ⊥
hA_nont : Nontrivial A
h_topM : ¬M = ⊤
h_prM : ¬Ideal.IsPrime M
x : A
hx : ¬x ∈ M
y : A
hy : ¬y ∈ M
h_xy : x * y ∈ M
z : A
hz : ¬z ∈ M
m_eq : M = M + span A {z}
⊢ z ∈ M
[PROOFSTEP]
rw [m_eq]
[GOAL]
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
h_fA : ¬IsField A
I M : Ideal A
hgt :
  ∀ (J : Submodule A A),
    J > M →
      (fun I => I ≠ ⊥ → ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I ∧ Multiset.prod (Multiset.map asIdeal Z) ≠ ⊥) J
h_nzM : M ≠ ⊥
hA_nont : Nontrivial A
h_topM : ¬M = ⊤
h_prM : ¬Ideal.IsPrime M
x : A
hx : ¬x ∈ M
y : A
hy : ¬y ∈ M
h_xy : x * y ∈ M
z : A
hz : ¬z ∈ M
m_eq : M = M + span A {z}
⊢ z ∈ M + span A {z}
[PROOFSTEP]
exact mem_sup_right (mem_span_singleton_self z)
[GOAL]
case neg.intro.intro.intro.intro
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
h_fA : ¬IsField A
I M : Ideal A
hgt :
  ∀ (J : Submodule A A),
    J > M →
      (fun I => I ≠ ⊥ → ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I ∧ Multiset.prod (Multiset.map asIdeal Z) ≠ ⊥) J
h_nzM : M ≠ ⊥
hA_nont : Nontrivial A
h_topM : ¬M = ⊤
h_prM : ¬Ideal.IsPrime M
x : A
hx : ¬x ∈ M
y : A
hy : ¬y ∈ M
h_xy : x * y ∈ M
lt_add : ∀ (z : A), ¬z ∈ M → M < M + span A {z}
⊢ ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ M ∧ Multiset.prod (Multiset.map asIdeal Z) ≠ ⊥
[PROOFSTEP]
obtain ⟨Wx, h_Wx_le, h_Wx_ne⟩ := hgt (M + span A { x }) (lt_add _ hx) (ne_bot_of_gt (lt_add _ hx))
[GOAL]
case neg.intro.intro.intro.intro.intro.intro
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
h_fA : ¬IsField A
I M : Ideal A
hgt :
  ∀ (J : Submodule A A),
    J > M →
      (fun I => I ≠ ⊥ → ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I ∧ Multiset.prod (Multiset.map asIdeal Z) ≠ ⊥) J
h_nzM : M ≠ ⊥
hA_nont : Nontrivial A
h_topM : ¬M = ⊤
h_prM : ¬Ideal.IsPrime M
x : A
hx : ¬x ∈ M
y : A
hy : ¬y ∈ M
h_xy : x * y ∈ M
lt_add : ∀ (z : A), ¬z ∈ M → M < M + span A {z}
Wx : Multiset (PrimeSpectrum A)
h_Wx_le : Multiset.prod (Multiset.map asIdeal Wx) ≤ M + span A {x}
h_Wx_ne : Multiset.prod (Multiset.map asIdeal Wx) ≠ ⊥
⊢ ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ M ∧ Multiset.prod (Multiset.map asIdeal Z) ≠ ⊥
[PROOFSTEP]
obtain ⟨Wy, h_Wy_le, h_Wx_ne⟩ := hgt (M + span A { y }) (lt_add _ hy) (ne_bot_of_gt (lt_add _ hy))
[GOAL]
case neg.intro.intro.intro.intro.intro.intro.intro.intro
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
h_fA : ¬IsField A
I M : Ideal A
hgt :
  ∀ (J : Submodule A A),
    J > M →
      (fun I => I ≠ ⊥ → ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I ∧ Multiset.prod (Multiset.map asIdeal Z) ≠ ⊥) J
h_nzM : M ≠ ⊥
hA_nont : Nontrivial A
h_topM : ¬M = ⊤
h_prM : ¬Ideal.IsPrime M
x : A
hx : ¬x ∈ M
y : A
hy : ¬y ∈ M
h_xy : x * y ∈ M
lt_add : ∀ (z : A), ¬z ∈ M → M < M + span A {z}
Wx : Multiset (PrimeSpectrum A)
h_Wx_le : Multiset.prod (Multiset.map asIdeal Wx) ≤ M + span A {x}
h_Wx_ne✝ : Multiset.prod (Multiset.map asIdeal Wx) ≠ ⊥
Wy : Multiset (PrimeSpectrum A)
h_Wy_le : Multiset.prod (Multiset.map asIdeal Wy) ≤ M + span A {y}
h_Wx_ne : Multiset.prod (Multiset.map asIdeal Wy) ≠ ⊥
⊢ ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ M ∧ Multiset.prod (Multiset.map asIdeal Z) ≠ ⊥
[PROOFSTEP]
use Wx + Wy
[GOAL]
case h
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
h_fA : ¬IsField A
I M : Ideal A
hgt :
  ∀ (J : Submodule A A),
    J > M →
      (fun I => I ≠ ⊥ → ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I ∧ Multiset.prod (Multiset.map asIdeal Z) ≠ ⊥) J
h_nzM : M ≠ ⊥
hA_nont : Nontrivial A
h_topM : ¬M = ⊤
h_prM : ¬Ideal.IsPrime M
x : A
hx : ¬x ∈ M
y : A
hy : ¬y ∈ M
h_xy : x * y ∈ M
lt_add : ∀ (z : A), ¬z ∈ M → M < M + span A {z}
Wx : Multiset (PrimeSpectrum A)
h_Wx_le : Multiset.prod (Multiset.map asIdeal Wx) ≤ M + span A {x}
h_Wx_ne✝ : Multiset.prod (Multiset.map asIdeal Wx) ≠ ⊥
Wy : Multiset (PrimeSpectrum A)
h_Wy_le : Multiset.prod (Multiset.map asIdeal Wy) ≤ M + span A {y}
h_Wx_ne : Multiset.prod (Multiset.map asIdeal Wy) ≠ ⊥
⊢ Multiset.prod (Multiset.map asIdeal (Wx + Wy)) ≤ M ∧ Multiset.prod (Multiset.map asIdeal (Wx + Wy)) ≠ ⊥
[PROOFSTEP]
rw [Multiset.map_add, Multiset.prod_add]
[GOAL]
case h
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
h_fA : ¬IsField A
I M : Ideal A
hgt :
  ∀ (J : Submodule A A),
    J > M →
      (fun I => I ≠ ⊥ → ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I ∧ Multiset.prod (Multiset.map asIdeal Z) ≠ ⊥) J
h_nzM : M ≠ ⊥
hA_nont : Nontrivial A
h_topM : ¬M = ⊤
h_prM : ¬Ideal.IsPrime M
x : A
hx : ¬x ∈ M
y : A
hy : ¬y ∈ M
h_xy : x * y ∈ M
lt_add : ∀ (z : A), ¬z ∈ M → M < M + span A {z}
Wx : Multiset (PrimeSpectrum A)
h_Wx_le : Multiset.prod (Multiset.map asIdeal Wx) ≤ M + span A {x}
h_Wx_ne✝ : Multiset.prod (Multiset.map asIdeal Wx) ≠ ⊥
Wy : Multiset (PrimeSpectrum A)
h_Wy_le : Multiset.prod (Multiset.map asIdeal Wy) ≤ M + span A {y}
h_Wx_ne : Multiset.prod (Multiset.map asIdeal Wy) ≠ ⊥
⊢ Multiset.prod (Multiset.map asIdeal Wx) * Multiset.prod (Multiset.map asIdeal Wy) ≤ M ∧
    Multiset.prod (Multiset.map asIdeal Wx) * Multiset.prod (Multiset.map asIdeal Wy) ≠ ⊥
[PROOFSTEP]
refine' ⟨le_trans (Submodule.mul_le_mul h_Wx_le h_Wy_le) _, mt Ideal.mul_eq_bot.mp _⟩
[GOAL]
case h.refine'_1
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
h_fA : ¬IsField A
I M : Ideal A
hgt :
  ∀ (J : Submodule A A),
    J > M →
      (fun I => I ≠ ⊥ → ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I ∧ Multiset.prod (Multiset.map asIdeal Z) ≠ ⊥) J
h_nzM : M ≠ ⊥
hA_nont : Nontrivial A
h_topM : ¬M = ⊤
h_prM : ¬Ideal.IsPrime M
x : A
hx : ¬x ∈ M
y : A
hy : ¬y ∈ M
h_xy : x * y ∈ M
lt_add : ∀ (z : A), ¬z ∈ M → M < M + span A {z}
Wx : Multiset (PrimeSpectrum A)
h_Wx_le : Multiset.prod (Multiset.map asIdeal Wx) ≤ M + span A {x}
h_Wx_ne✝ : Multiset.prod (Multiset.map asIdeal Wx) ≠ ⊥
Wy : Multiset (PrimeSpectrum A)
h_Wy_le : Multiset.prod (Multiset.map asIdeal Wy) ≤ M + span A {y}
h_Wx_ne : Multiset.prod (Multiset.map asIdeal Wy) ≠ ⊥
⊢ (M + span A {x}) * (M + span A {y}) ≤ M
[PROOFSTEP]
rw [add_mul]
[GOAL]
case h.refine'_1
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
h_fA : ¬IsField A
I M : Ideal A
hgt :
  ∀ (J : Submodule A A),
    J > M →
      (fun I => I ≠ ⊥ → ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I ∧ Multiset.prod (Multiset.map asIdeal Z) ≠ ⊥) J
h_nzM : M ≠ ⊥
hA_nont : Nontrivial A
h_topM : ¬M = ⊤
h_prM : ¬Ideal.IsPrime M
x : A
hx : ¬x ∈ M
y : A
hy : ¬y ∈ M
h_xy : x * y ∈ M
lt_add : ∀ (z : A), ¬z ∈ M → M < M + span A {z}
Wx : Multiset (PrimeSpectrum A)
h_Wx_le : Multiset.prod (Multiset.map asIdeal Wx) ≤ M + span A {x}
h_Wx_ne✝ : Multiset.prod (Multiset.map asIdeal Wx) ≠ ⊥
Wy : Multiset (PrimeSpectrum A)
h_Wy_le : Multiset.prod (Multiset.map asIdeal Wy) ≤ M + span A {y}
h_Wx_ne : Multiset.prod (Multiset.map asIdeal Wy) ≠ ⊥
⊢ M * (M + span A {y}) + span A {x} * (M + span A {y}) ≤ M
[PROOFSTEP]
apply sup_le (show M * (M + span A { y }) ≤ M from Ideal.mul_le_right)
[GOAL]
case h.refine'_1
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
h_fA : ¬IsField A
I M : Ideal A
hgt :
  ∀ (J : Submodule A A),
    J > M →
      (fun I => I ≠ ⊥ → ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I ∧ Multiset.prod (Multiset.map asIdeal Z) ≠ ⊥) J
h_nzM : M ≠ ⊥
hA_nont : Nontrivial A
h_topM : ¬M = ⊤
h_prM : ¬Ideal.IsPrime M
x : A
hx : ¬x ∈ M
y : A
hy : ¬y ∈ M
h_xy : x * y ∈ M
lt_add : ∀ (z : A), ¬z ∈ M → M < M + span A {z}
Wx : Multiset (PrimeSpectrum A)
h_Wx_le : Multiset.prod (Multiset.map asIdeal Wx) ≤ M + span A {x}
h_Wx_ne✝ : Multiset.prod (Multiset.map asIdeal Wx) ≠ ⊥
Wy : Multiset (PrimeSpectrum A)
h_Wy_le : Multiset.prod (Multiset.map asIdeal Wy) ≤ M + span A {y}
h_Wx_ne : Multiset.prod (Multiset.map asIdeal Wy) ≠ ⊥
⊢ span A {x} * (M + span A {y}) ≤ M
[PROOFSTEP]
rw [mul_add]
[GOAL]
case h.refine'_1
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
h_fA : ¬IsField A
I M : Ideal A
hgt :
  ∀ (J : Submodule A A),
    J > M →
      (fun I => I ≠ ⊥ → ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I ∧ Multiset.prod (Multiset.map asIdeal Z) ≠ ⊥) J
h_nzM : M ≠ ⊥
hA_nont : Nontrivial A
h_topM : ¬M = ⊤
h_prM : ¬Ideal.IsPrime M
x : A
hx : ¬x ∈ M
y : A
hy : ¬y ∈ M
h_xy : x * y ∈ M
lt_add : ∀ (z : A), ¬z ∈ M → M < M + span A {z}
Wx : Multiset (PrimeSpectrum A)
h_Wx_le : Multiset.prod (Multiset.map asIdeal Wx) ≤ M + span A {x}
h_Wx_ne✝ : Multiset.prod (Multiset.map asIdeal Wx) ≠ ⊥
Wy : Multiset (PrimeSpectrum A)
h_Wy_le : Multiset.prod (Multiset.map asIdeal Wy) ≤ M + span A {y}
h_Wx_ne : Multiset.prod (Multiset.map asIdeal Wy) ≠ ⊥
⊢ span A {x} * M + span A {x} * span A {y} ≤ M
[PROOFSTEP]
apply sup_le (show span A { x } * M ≤ M from Ideal.mul_le_left)
[GOAL]
case h.refine'_1
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
h_fA : ¬IsField A
I M : Ideal A
hgt :
  ∀ (J : Submodule A A),
    J > M →
      (fun I => I ≠ ⊥ → ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I ∧ Multiset.prod (Multiset.map asIdeal Z) ≠ ⊥) J
h_nzM : M ≠ ⊥
hA_nont : Nontrivial A
h_topM : ¬M = ⊤
h_prM : ¬Ideal.IsPrime M
x : A
hx : ¬x ∈ M
y : A
hy : ¬y ∈ M
h_xy : x * y ∈ M
lt_add : ∀ (z : A), ¬z ∈ M → M < M + span A {z}
Wx : Multiset (PrimeSpectrum A)
h_Wx_le : Multiset.prod (Multiset.map asIdeal Wx) ≤ M + span A {x}
h_Wx_ne✝ : Multiset.prod (Multiset.map asIdeal Wx) ≠ ⊥
Wy : Multiset (PrimeSpectrum A)
h_Wy_le : Multiset.prod (Multiset.map asIdeal Wy) ≤ M + span A {y}
h_Wx_ne : Multiset.prod (Multiset.map asIdeal Wy) ≠ ⊥
⊢ span A {x} * span A {y} ≤ M
[PROOFSTEP]
rwa [span_mul_span, Set.singleton_mul_singleton, span_singleton_le_iff_mem]
[GOAL]
case h.refine'_2
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
h_fA : ¬IsField A
I M : Ideal A
hgt :
  ∀ (J : Submodule A A),
    J > M →
      (fun I => I ≠ ⊥ → ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I ∧ Multiset.prod (Multiset.map asIdeal Z) ≠ ⊥) J
h_nzM : M ≠ ⊥
hA_nont : Nontrivial A
h_topM : ¬M = ⊤
h_prM : ¬Ideal.IsPrime M
x : A
hx : ¬x ∈ M
y : A
hy : ¬y ∈ M
h_xy : x * y ∈ M
lt_add : ∀ (z : A), ¬z ∈ M → M < M + span A {z}
Wx : Multiset (PrimeSpectrum A)
h_Wx_le : Multiset.prod (Multiset.map asIdeal Wx) ≤ M + span A {x}
h_Wx_ne✝ : Multiset.prod (Multiset.map asIdeal Wx) ≠ ⊥
Wy : Multiset (PrimeSpectrum A)
h_Wy_le : Multiset.prod (Multiset.map asIdeal Wy) ≤ M + span A {y}
h_Wx_ne : Multiset.prod (Multiset.map asIdeal Wy) ≠ ⊥
⊢ ¬(Multiset.prod (Multiset.map asIdeal Wx) = ⊥ ∨ Multiset.prod (Multiset.map asIdeal Wy) = ⊥)
[PROOFSTEP]
rintro (hx | hy)
[GOAL]
case h.refine'_2.inl
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
h_fA : ¬IsField A
I M : Ideal A
hgt :
  ∀ (J : Submodule A A),
    J > M →
      (fun I => I ≠ ⊥ → ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I ∧ Multiset.prod (Multiset.map asIdeal Z) ≠ ⊥) J
h_nzM : M ≠ ⊥
hA_nont : Nontrivial A
h_topM : ¬M = ⊤
h_prM : ¬Ideal.IsPrime M
x : A
hx✝ : ¬x ∈ M
y : A
hy : ¬y ∈ M
h_xy : x * y ∈ M
lt_add : ∀ (z : A), ¬z ∈ M → M < M + span A {z}
Wx : Multiset (PrimeSpectrum A)
h_Wx_le : Multiset.prod (Multiset.map asIdeal Wx) ≤ M + span A {x}
h_Wx_ne✝ : Multiset.prod (Multiset.map asIdeal Wx) ≠ ⊥
Wy : Multiset (PrimeSpectrum A)
h_Wy_le : Multiset.prod (Multiset.map asIdeal Wy) ≤ M + span A {y}
h_Wx_ne : Multiset.prod (Multiset.map asIdeal Wy) ≠ ⊥
hx : Multiset.prod (Multiset.map asIdeal Wx) = ⊥
⊢ False
[PROOFSTEP]
contradiction
[GOAL]
case h.refine'_2.inr
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
h_fA : ¬IsField A
I M : Ideal A
hgt :
  ∀ (J : Submodule A A),
    J > M →
      (fun I => I ≠ ⊥ → ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I ∧ Multiset.prod (Multiset.map asIdeal Z) ≠ ⊥) J
h_nzM : M ≠ ⊥
hA_nont : Nontrivial A
h_topM : ¬M = ⊤
h_prM : ¬Ideal.IsPrime M
x : A
hx : ¬x ∈ M
y : A
hy✝ : ¬y ∈ M
h_xy : x * y ∈ M
lt_add : ∀ (z : A), ¬z ∈ M → M < M + span A {z}
Wx : Multiset (PrimeSpectrum A)
h_Wx_le : Multiset.prod (Multiset.map asIdeal Wx) ≤ M + span A {x}
h_Wx_ne✝ : Multiset.prod (Multiset.map asIdeal Wx) ≠ ⊥
Wy : Multiset (PrimeSpectrum A)
h_Wy_le : Multiset.prod (Multiset.map asIdeal Wy) ≤ M + span A {y}
h_Wx_ne : Multiset.prod (Multiset.map asIdeal Wy) ≠ ⊥
hy : Multiset.prod (Multiset.map asIdeal Wy) = ⊥
⊢ False
[PROOFSTEP]
contradiction
[GOAL]
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
⊢ NoetherianSpace (PrimeSpectrum R)
[PROOFSTEP]
apply ((noetherianSpace_TFAE <| PrimeSpectrum R).out 0 1).mpr
[GOAL]
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
⊢ WellFounded fun s t => s < t
[PROOFSTEP]
have H := ‹IsNoetherianRing R›
[GOAL]
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
H : IsNoetherianRing R
⊢ WellFounded fun s t => s < t
[PROOFSTEP]
rw [isNoetherianRing_iff, isNoetherian_iff_wellFounded] at H
[GOAL]
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
H : WellFounded fun x x_1 => x > x_1
⊢ WellFounded fun s t => s < t
[PROOFSTEP]
exact (closedsEmbedding R).dual.wellFounded H


[GOAL]
R : Type u_1
inst✝ : CommRing R
f : R[X]
⊢ IsOpen (imageOfDf f)
[PROOFSTEP]
rw [imageOfDf, setOf_exists fun i (x : PrimeSpectrum R) => coeff f i ∉ x.asIdeal]
[GOAL]
R : Type u_1
inst✝ : CommRing R
f : R[X]
⊢ IsOpen (⋃ (i : ℕ), {x | ¬coeff f i ∈ x.asIdeal})
[PROOFSTEP]
exact isOpen_iUnion fun i => isOpen_basicOpen
[GOAL]
R : Type u_1
inst✝ : CommRing R
f : R[X]
⊢ imageOfDf f = ↑(PrimeSpectrum.comap C) '' (zeroLocus {f})ᶜ
[PROOFSTEP]
ext x
[GOAL]
case h
R : Type u_1
inst✝ : CommRing R
f : R[X]
x : PrimeSpectrum R
⊢ x ∈ imageOfDf f ↔ x ∈ ↑(PrimeSpectrum.comap C) '' (zeroLocus {f})ᶜ
[PROOFSTEP]
refine' ⟨fun hx => ⟨⟨map C x.asIdeal, isPrime_map_C_of_isPrime x.IsPrime⟩, ⟨_, _⟩⟩, _⟩
[GOAL]
case h.refine'_1
R : Type u_1
inst✝ : CommRing R
f : R[X]
x : PrimeSpectrum R
hx : x ∈ imageOfDf f
⊢ { asIdeal := Ideal.map C x.asIdeal, IsPrime := (_ : Ideal.IsPrime (Ideal.map C x.asIdeal)) } ∈ (zeroLocus {f})ᶜ
[PROOFSTEP]
rw [mem_compl_iff, mem_zeroLocus, singleton_subset_iff]
[GOAL]
case h.refine'_1
R : Type u_1
inst✝ : CommRing R
f : R[X]
x : PrimeSpectrum R
hx : x ∈ imageOfDf f
⊢ ¬f ∈ ↑{ asIdeal := Ideal.map C x.asIdeal, IsPrime := (_ : Ideal.IsPrime (Ideal.map C x.asIdeal)) }.asIdeal
[PROOFSTEP]
cases' hx with i hi
[GOAL]
case h.refine'_1.intro
R : Type u_1
inst✝ : CommRing R
f : R[X]
x : PrimeSpectrum R
i : ℕ
hi : ¬coeff f i ∈ x.asIdeal
⊢ ¬f ∈ ↑{ asIdeal := Ideal.map C x.asIdeal, IsPrime := (_ : Ideal.IsPrime (Ideal.map C x.asIdeal)) }.asIdeal
[PROOFSTEP]
exact fun a => hi (mem_map_C_iff.mp a i)
[GOAL]
case h.refine'_2
R : Type u_1
inst✝ : CommRing R
f : R[X]
x : PrimeSpectrum R
hx : x ∈ imageOfDf f
⊢ ↑(PrimeSpectrum.comap C)
      { asIdeal := Ideal.map C x.asIdeal, IsPrime := (_ : Ideal.IsPrime (Ideal.map C x.asIdeal)) } =
    x
[PROOFSTEP]
ext x
[GOAL]
case h.refine'_2.asIdeal.h
R : Type u_1
inst✝ : CommRing R
f : R[X]
x✝ : PrimeSpectrum R
hx : x✝ ∈ imageOfDf f
x : R
⊢ x ∈
      (↑(PrimeSpectrum.comap C)
          { asIdeal := Ideal.map C x✝.asIdeal, IsPrime := (_ : Ideal.IsPrime (Ideal.map C x✝.asIdeal)) }).asIdeal ↔
    x ∈ x✝.asIdeal
[PROOFSTEP]
refine' ⟨fun h => _, fun h => subset_span (mem_image_of_mem C.1 h)⟩
[GOAL]
case h.refine'_2.asIdeal.h
R : Type u_1
inst✝ : CommRing R
f : R[X]
x✝ : PrimeSpectrum R
hx : x✝ ∈ imageOfDf f
x : R
h :
  x ∈
    (↑(PrimeSpectrum.comap C)
        { asIdeal := Ideal.map C x✝.asIdeal, IsPrime := (_ : Ideal.IsPrime (Ideal.map C x✝.asIdeal)) }).asIdeal
⊢ x ∈ x✝.asIdeal
[PROOFSTEP]
rw [← @coeff_C_zero R x _]
[GOAL]
case h.refine'_2.asIdeal.h
R : Type u_1
inst✝ : CommRing R
f : R[X]
x✝ : PrimeSpectrum R
hx : x✝ ∈ imageOfDf f
x : R
h :
  x ∈
    (↑(PrimeSpectrum.comap C)
        { asIdeal := Ideal.map C x✝.asIdeal, IsPrime := (_ : Ideal.IsPrime (Ideal.map C x✝.asIdeal)) }).asIdeal
⊢ coeff (↑C x) 0 ∈ x✝.asIdeal
[PROOFSTEP]
exact mem_map_C_iff.mp h 0
[GOAL]
case h.refine'_3
R : Type u_1
inst✝ : CommRing R
f : R[X]
x : PrimeSpectrum R
⊢ x ∈ ↑(PrimeSpectrum.comap C) '' (zeroLocus {f})ᶜ → x ∈ imageOfDf f
[PROOFSTEP]
rintro ⟨xli, complement, rfl⟩
[GOAL]
case h.refine'_3.intro.intro
R : Type u_1
inst✝ : CommRing R
f : R[X]
xli : PrimeSpectrum R[X]
complement : xli ∈ (zeroLocus {f})ᶜ
⊢ ↑(PrimeSpectrum.comap C) xli ∈ imageOfDf f
[PROOFSTEP]
exact comap_C_mem_imageOfDf complement
[GOAL]
R : Type u_1
inst✝ : CommRing R
f : R[X]
⊢ IsOpenMap ↑(PrimeSpectrum.comap C)
[PROOFSTEP]
rintro U ⟨s, z⟩
[GOAL]
case intro
R : Type u_1
inst✝ : CommRing R
f : R[X]
U : Set (PrimeSpectrum R[X])
s : Set R[X]
z : zeroLocus s = Uᶜ
⊢ IsOpen (↑(PrimeSpectrum.comap C) '' U)
[PROOFSTEP]
rw [← compl_compl U, ← z, ← iUnion_of_singleton_coe s, zeroLocus_iUnion, compl_iInter, image_iUnion]
[GOAL]
case intro
R : Type u_1
inst✝ : CommRing R
f : R[X]
U : Set (PrimeSpectrum R[X])
s : Set R[X]
z : zeroLocus s = Uᶜ
⊢ IsOpen (⋃ (i : ↑s), ↑(PrimeSpectrum.comap C) '' (zeroLocus {↑i})ᶜ)
[PROOFSTEP]
simp_rw [← imageOfDf_eq_comap_C_compl_zeroLocus]
[GOAL]
case intro
R : Type u_1
inst✝ : CommRing R
f : R[X]
U : Set (PrimeSpectrum R[X])
s : Set R[X]
z : zeroLocus s = Uᶜ
⊢ IsOpen (⋃ (i : ↑s), imageOfDf ↑i)
[PROOFSTEP]
exact isOpen_iUnion fun f => isOpen_imageOfDf


[GOAL]
X : Scheme
U : (Opens ↑↑X.toPresheafedSpace)ᵒᵖ
⊢ U = U
[PROOFSTEP]
induction' U with U
[GOAL]
case h
X : Scheme
U : Opens ↑↑X.toPresheafedSpace
⊢ op U = op U
[PROOFSTEP]
cases U
[GOAL]
case h.mk
X : Scheme
carrier✝ : Set ↑↑X.toPresheafedSpace
is_open'✝ : IsOpen carrier✝
⊢ op { carrier := carrier✝, is_open' := is_open'✝ } = op { carrier := carrier✝, is_open' := is_open'✝ }
[PROOFSTEP]
rfl
[GOAL]
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
x : ↑↑X.toPresheafedSpace
⊢ ↑(f ≫ g).val.base x = ↑g.val.base (↑f.val.base x)
[PROOFSTEP]
simp
[GOAL]
X Y : Scheme
f g : X ⟶ Y
e : f = g
U : (Opens ↑↑Y.toPresheafedSpace)ᵒᵖ
⊢ (Opens.map g.val.base).op.obj U = (Opens.map f.val.base).op.obj U
[PROOFSTEP]
subst e
[GOAL]
X Y : Scheme
f : X ⟶ Y
U : (Opens ↑↑Y.toPresheafedSpace)ᵒᵖ
⊢ (Opens.map f.val.base).op.obj U = (Opens.map f.val.base).op.obj U
[PROOFSTEP]
rfl
[GOAL]
X Y : Scheme
f g : X ⟶ Y
e : f = g
U : (Opens ↑↑Y.toPresheafedSpace)ᵒᵖ
⊢ NatTrans.app f.val.c U =
    NatTrans.app g.val.c U ≫
      X.presheaf.map (eqToHom (_ : (Opens.map g.val.base).op.obj U = (Opens.map f.val.base).op.obj U))
[PROOFSTEP]
subst e
[GOAL]
X Y : Scheme
f : X ⟶ Y
U : (Opens ↑↑Y.toPresheafedSpace)ᵒᵖ
⊢ NatTrans.app f.val.c U =
    NatTrans.app f.val.c U ≫
      X.presheaf.map (eqToHom (_ : (Opens.map f.val.base).op.obj U = (Opens.map f.val.base).op.obj U))
[PROOFSTEP]
dsimp
[GOAL]
X Y : Scheme
f : X ⟶ Y
U : (Opens ↑↑Y.toPresheafedSpace)ᵒᵖ
⊢ NatTrans.app f.val.c U = NatTrans.app f.val.c U ≫ X.presheaf.map (𝟙 (op ((Opens.map f.val.base).obj U.unop)))
[PROOFSTEP]
simp
[GOAL]
X Y : Scheme
f : X ⟶ Y
U V : Opens ↑↑Y.toPresheafedSpace
e : U = V
⊢ NatTrans.app f.val.c (op U) =
    Y.presheaf.map (eqToHom (_ : V = U)).op ≫
      NatTrans.app f.val.c (op V) ≫
        X.presheaf.map (eqToHom (_ : (Opens.map f.val.base).obj U = (Opens.map f.val.base).obj V)).op
[PROOFSTEP]
rw [← IsIso.inv_comp_eq, ← Functor.map_inv, f.val.c.naturality, Presheaf.pushforwardObj_map]
[GOAL]
X Y : Scheme
f : X ⟶ Y
U V : Opens ↑↑Y.toPresheafedSpace
e : U = V
⊢ NatTrans.app f.val.c (op V) ≫ X.presheaf.map ((Opens.map f.val.base).op.map (inv (eqToHom (_ : V = U)).op)) =
    NatTrans.app f.val.c (op V) ≫
      X.presheaf.map (eqToHom (_ : (Opens.map f.val.base).obj U = (Opens.map f.val.base).obj V)).op
[PROOFSTEP]
cases e
[GOAL]
case refl
X Y : Scheme
f : X ⟶ Y
U : Opens ↑↑Y.toPresheafedSpace
⊢ NatTrans.app f.val.c (op U) ≫ X.presheaf.map ((Opens.map f.val.base).op.map (inv (eqToHom (_ : U = U)).op)) =
    NatTrans.app f.val.c (op U) ≫
      X.presheaf.map (eqToHom (_ : (Opens.map f.val.base).obj U = (Opens.map f.val.base).obj U)).op
[PROOFSTEP]
rfl
[GOAL]
X : Scheme
U V : Opens ↑↑X.toPresheafedSpace
i : U = V
⊢ X.presheaf.map (eqToHom i).op = eqToHom (_ : X.presheaf.obj (op V) = X.presheaf.obj (op U))
[PROOFSTEP]
rw [eqToHom_op, eqToHom_map]
[GOAL]
X Y : Scheme
f : X ⟶ Y
inst✝ : IsIso f
U : Opens ↑↑X.toPresheafedSpace
⊢ (Opens.map (f ≫ inv f).val.base).obj U = U
[PROOFSTEP]
rw [IsIso.hom_inv_id]
[GOAL]
X Y : Scheme
f : X ⟶ Y
inst✝ : IsIso f
U : Opens ↑↑X.toPresheafedSpace
⊢ (Opens.map (𝟙 X).val.base).obj U = U
[PROOFSTEP]
ext1
[GOAL]
case h
X Y : Scheme
f : X ⟶ Y
inst✝ : IsIso f
U : Opens ↑↑X.toPresheafedSpace
⊢ ↑((Opens.map (𝟙 X).val.base).obj U) = ↑U
[PROOFSTEP]
rfl
[GOAL]
X Y : Scheme
f : X ⟶ Y
inst✝ : IsIso f
U : Opens ↑↑X.toPresheafedSpace
⊢ NatTrans.app (inv f).val.c (op U) =
    X.presheaf.map (eqToHom (_ : (Opens.map (f ≫ inv f).val.base).obj U = U)).op ≫
      inv (NatTrans.app f.val.c (op ((Opens.map (inv f).val.base).obj U)))
[PROOFSTEP]
rw [IsIso.eq_comp_inv]
[GOAL]
X Y : Scheme
f : X ⟶ Y
inst✝ : IsIso f
U : Opens ↑↑X.toPresheafedSpace
⊢ NatTrans.app (inv f).val.c (op U) ≫ NatTrans.app f.val.c (op ((Opens.map (inv f).val.base).obj U)) =
    X.presheaf.map (eqToHom (_ : (Opens.map (f ≫ inv f).val.base).obj U = U)).op
[PROOFSTEP]
erw [← Scheme.comp_val_c_app]
[GOAL]
X Y : Scheme
f : X ⟶ Y
inst✝ : IsIso f
U : Opens ↑↑X.toPresheafedSpace
⊢ NatTrans.app (f ≫ inv f).val.c (op U) = X.presheaf.map (eqToHom (_ : (Opens.map (f ≫ inv f).val.base).obj U = U)).op
[PROOFSTEP]
rw [Scheme.congr_app (IsIso.hom_inv_id f), Scheme.id_app, ← Functor.map_comp, eqToHom_trans, eqToHom_op]
[GOAL]
R : CommRingCatᵒᵖ
⊢ { obj := fun R => specObj R.unop, map := fun {X Y} f => specMap f.unop }.map (𝟙 R) =
    𝟙 ({ obj := fun R => specObj R.unop, map := fun {X Y} f => specMap f.unop }.obj R)
[PROOFSTEP]
simp
[GOAL]
X✝ Y✝ Z✝ : CommRingCatᵒᵖ
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ { obj := fun R => specObj R.unop, map := fun {X Y} f => specMap f.unop }.map (f ≫ g) =
    { obj := fun R => specObj R.unop, map := fun {X Y} f => specMap f.unop }.map f ≫
      { obj := fun R => specObj R.unop, map := fun {X Y} f => specMap f.unop }.map g
[PROOFSTEP]
simp [specMap_comp]
[GOAL]
X : Scheme
V U✝ : Opens ↑↑X.toPresheafedSpace
f✝ g : ↑(X.presheaf.obj (op U✝))
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
x : ↑↑X.toPresheafedSpace
⊢ x ∈ basicOpen X f ↔ ∃ m, IsUnit (↑(Presheaf.germ X.presheaf { val := x, property := m }) f)
[PROOFSTEP]
fconstructor
[GOAL]
case mp
X : Scheme
V U✝ : Opens ↑↑X.toPresheafedSpace
f✝ g : ↑(X.presheaf.obj (op U✝))
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
x : ↑↑X.toPresheafedSpace
⊢ x ∈ basicOpen X f → ∃ m, IsUnit (↑(Presheaf.germ X.presheaf { val := x, property := m }) f)
[PROOFSTEP]
rintro ⟨y, hy1, rfl⟩
[GOAL]
case mp.intro.intro
X : Scheme
V U✝ : Opens ↑↑X.toPresheafedSpace
f✝ g : ↑(X.presheaf.obj (op U✝))
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
y : { x // x ∈ U }
hy1 :
  y ∈
    {x |
      IsUnit
        (↑(Presheaf.germ (LocallyRingedSpace.toRingedSpace X.toLocallyRingedSpace).toPresheafedSpace.presheaf x) f)}
⊢ ∃ m, IsUnit (↑(Presheaf.germ X.presheaf { val := ↑y, property := m }) f)
[PROOFSTEP]
exact ⟨y.2, hy1⟩
[GOAL]
case mpr
X : Scheme
V U✝ : Opens ↑↑X.toPresheafedSpace
f✝ g : ↑(X.presheaf.obj (op U✝))
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
x : ↑↑X.toPresheafedSpace
⊢ (∃ m, IsUnit (↑(Presheaf.germ X.presheaf { val := x, property := m }) f)) → x ∈ basicOpen X f
[PROOFSTEP]
rintro ⟨m, hm⟩
[GOAL]
case mpr.intro
X : Scheme
V U✝ : Opens ↑↑X.toPresheafedSpace
f✝ g : ↑(X.presheaf.obj (op U✝))
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
x : ↑↑X.toPresheafedSpace
m : x ∈ U
hm : IsUnit (↑(Presheaf.germ X.presheaf { val := x, property := m }) f)
⊢ x ∈ basicOpen X f
[PROOFSTEP]
exact ⟨⟨x, m⟩, hm, rfl⟩
[GOAL]
R : CommRingCat
f : ↑R
⊢ Scheme.basicOpen (Scheme.Spec.obj (op R)) (↑(SpecΓIdentity.app R).inv f) = PrimeSpectrum.basicOpen f
[PROOFSTEP]
ext x
[GOAL]
case h.h
R : CommRingCat
f : ↑R
x : ↑↑(Scheme.Spec.obj (op R)).toPresheafedSpace
⊢ x ∈ ↑(Scheme.basicOpen (Scheme.Spec.obj (op R)) (↑(SpecΓIdentity.app R).inv f)) ↔ x ∈ ↑(PrimeSpectrum.basicOpen f)
[PROOFSTEP]
erw [Scheme.mem_basicOpen_top]
[GOAL]
case h.h
R : CommRingCat
f : ↑R
x : ↑↑(Scheme.Spec.obj (op R)).toPresheafedSpace
⊢ IsUnit
      (↑(Presheaf.germ (Scheme.Spec.obj (op R)).presheaf { val := x, property := _root_.trivial })
        (↑(SpecΓIdentity.app R).inv f)) ↔
    x ∈ ↑(PrimeSpectrum.basicOpen f)
[PROOFSTEP]
suffices IsUnit (StructureSheaf.toStalk R x f) ↔ f ∉ PrimeSpectrum.asIdeal x by exact this
[GOAL]
R : CommRingCat
f : ↑R
x : ↑↑(Scheme.Spec.obj (op R)).toPresheafedSpace
this : IsUnit (↑(StructureSheaf.toStalk (↑R) x) f) ↔ ¬f ∈ x.asIdeal
⊢ IsUnit
      (↑(Presheaf.germ (Scheme.Spec.obj (op R)).presheaf { val := x, property := _root_.trivial })
        (↑(SpecΓIdentity.app R).inv f)) ↔
    x ∈ ↑(PrimeSpectrum.basicOpen f)
[PROOFSTEP]
exact this
[GOAL]
case h.h
R : CommRingCat
f : ↑R
x : ↑↑(Scheme.Spec.obj (op R)).toPresheafedSpace
⊢ IsUnit (↑(StructureSheaf.toStalk (↑R) x) f) ↔ ¬f ∈ x.asIdeal
[PROOFSTEP]
erw [← isUnit_map_iff (StructureSheaf.stalkToFiberRingHom R x), StructureSheaf.stalkToFiberRingHom_toStalk]
[GOAL]
case h.h
R : CommRingCat
f : ↑R
x : ↑↑(Scheme.Spec.obj (op R)).toPresheafedSpace
⊢ IsUnit (↑(algebraMap (↑R) (Localization.AtPrime x.asIdeal)) f) ↔ ¬f ∈ x.asIdeal
[PROOFSTEP]
exact
  (IsLocalization.AtPrime.isUnit_to_map_iff (Localization.AtPrime (PrimeSpectrum.asIdeal x)) (PrimeSpectrum.asIdeal x)
      f :
    _)
[GOAL]
R : CommRingCat
f : ↑((Spec.toSheafedSpace.obj (op R)).presheaf.obj (op ⊤))
⊢ Scheme.basicOpen (Scheme.Spec.obj (op R)) f = PrimeSpectrum.basicOpen (↑(SpecΓIdentity.app R).hom f)
[PROOFSTEP]
convert basicOpen_eq_of_affine ((SpecΓIdentity.app R).hom f)
[GOAL]
case h.e'_2.h.h.e'_3.h.h
R : CommRingCat
f : ↑((Spec.toSheafedSpace.obj (op R)).presheaf.obj (op ⊤))
e_1✝¹ :
  Opens ↑↑(Scheme.Spec.obj (op R)).toPresheafedSpace =
    Opens ↑↑(Scheme.Spec.obj (op ((𝟭 CommRingCat).obj R))).toPresheafedSpace
e_1✝ : Scheme.Spec.obj (op R) = Scheme.Spec.obj (op ((𝟭 CommRingCat).obj R))
he✝ : ⊤ = ⊤
⊢ f = ↑(SpecΓIdentity.app ((𝟭 CommRingCat).obj R)).inv (↑(SpecΓIdentity.app R).hom f)
[PROOFSTEP]
exact (Iso.hom_inv_id_apply (SpecΓIdentity.app R) f).symm