[GOAL]
X : Scheme
inst✝ : IrreducibleSpace ↑↑X.toPresheafedSpace
U : Opens ↑↑X.toPresheafedSpace
h : Nonempty { x // x ∈ U }
⊢ Set.Nonempty (⊤ ∩ ↑U)
[PROOFSTEP]
simpa using h
[GOAL]
X : Scheme
inst✝ : IsIntegral X
⊢ Field ↑(Scheme.functionField X)
[PROOFSTEP]
apply fieldOfIsUnitOrEqZero
[GOAL]
case h
X : Scheme
inst✝ : IsIntegral X
⊢ ∀ (a : ↑(Scheme.functionField X)), IsUnit a ∨ a = 0
[PROOFSTEP]
intro a
[GOAL]
case h
X : Scheme
inst✝ : IsIntegral X
a : ↑(Scheme.functionField X)
⊢ IsUnit a ∨ a = 0
[PROOFSTEP]
obtain ⟨U, m, s, rfl⟩ := TopCat.Presheaf.germ_exist _ _ a
[GOAL]
case h.intro.intro.intro
X : Scheme
inst✝ : IsIntegral X
U : Opens ↑↑X.toPresheafedSpace
m : genericPoint ↑↑X.toPresheafedSpace ∈ U
s : (forget CommRingCat).obj (X.presheaf.obj (op U))
⊢ IsUnit (↑(Presheaf.germ X.presheaf { val := genericPoint ↑↑X.toPresheafedSpace, property := m }) s) ∨
    ↑(Presheaf.germ X.presheaf { val := genericPoint ↑↑X.toPresheafedSpace, property := m }) s = 0
[PROOFSTEP]
rw [or_iff_not_imp_right, ← (X.presheaf.germ ⟨_, m⟩).map_zero]
[GOAL]
case h.intro.intro.intro
X : Scheme
inst✝ : IsIntegral X
U : Opens ↑↑X.toPresheafedSpace
m : genericPoint ↑↑X.toPresheafedSpace ∈ U
s : (forget CommRingCat).obj (X.presheaf.obj (op U))
⊢ ¬↑(Presheaf.germ X.presheaf { val := genericPoint ↑↑X.toPresheafedSpace, property := m }) s =
        ↑(Presheaf.germ X.presheaf { val := genericPoint ↑↑X.toPresheafedSpace, property := m }) 0 →
    IsUnit (↑(Presheaf.germ X.presheaf { val := genericPoint ↑↑X.toPresheafedSpace, property := m }) s)
[PROOFSTEP]
intro ha
[GOAL]
case h.intro.intro.intro
X : Scheme
inst✝ : IsIntegral X
U : Opens ↑↑X.toPresheafedSpace
m : genericPoint ↑↑X.toPresheafedSpace ∈ U
s : (forget CommRingCat).obj (X.presheaf.obj (op U))
ha :
  ¬↑(Presheaf.germ X.presheaf { val := genericPoint ↑↑X.toPresheafedSpace, property := m }) s =
      ↑(Presheaf.germ X.presheaf { val := genericPoint ↑↑X.toPresheafedSpace, property := m }) 0
⊢ IsUnit (↑(Presheaf.germ X.presheaf { val := genericPoint ↑↑X.toPresheafedSpace, property := m }) s)
[PROOFSTEP]
replace ha := ne_of_apply_ne _ ha
[GOAL]
case h.intro.intro.intro
X : Scheme
inst✝ : IsIntegral X
U : Opens ↑↑X.toPresheafedSpace
m : genericPoint ↑↑X.toPresheafedSpace ∈ U
s : (forget CommRingCat).obj (X.presheaf.obj (op U))
ha : s ≠ 0
⊢ IsUnit (↑(Presheaf.germ X.presheaf { val := genericPoint ↑↑X.toPresheafedSpace, property := m }) s)
[PROOFSTEP]
have hs : genericPoint X.carrier ∈ RingedSpace.basicOpen _ s :=
  by
  rw [← SetLike.mem_coe, (genericPoint_spec X.carrier).mem_open_set_iff, Set.top_eq_univ, Set.univ_inter,
    Set.nonempty_iff_ne_empty, Ne.def, ← Opens.coe_bot, ← SetLike.ext'_iff]
  erw [basicOpen_eq_bot_iff]
  exacts [ha, (RingedSpace.basicOpen _ _).isOpen]
[GOAL]
X : Scheme
inst✝ : IsIntegral X
U : Opens ↑↑X.toPresheafedSpace
m : genericPoint ↑↑X.toPresheafedSpace ∈ U
s : (forget CommRingCat).obj (X.presheaf.obj (op U))
ha : s ≠ 0
⊢ genericPoint ↑↑X.toPresheafedSpace ∈ RingedSpace.basicOpen X.toSheafedSpace s
[PROOFSTEP]
rw [← SetLike.mem_coe, (genericPoint_spec X.carrier).mem_open_set_iff, Set.top_eq_univ, Set.univ_inter,
  Set.nonempty_iff_ne_empty, Ne.def, ← Opens.coe_bot, ← SetLike.ext'_iff]
[GOAL]
X : Scheme
inst✝ : IsIntegral X
U : Opens ↑↑X.toPresheafedSpace
m : genericPoint ↑↑X.toPresheafedSpace ∈ U
s : (forget CommRingCat).obj (X.presheaf.obj (op U))
ha : s ≠ 0
⊢ ¬RingedSpace.basicOpen X.toSheafedSpace s = ⊥
X : Scheme
inst✝ : IsIntegral X
U : Opens ↑↑X.toPresheafedSpace
m : genericPoint ↑↑X.toPresheafedSpace ∈ U
s : (forget CommRingCat).obj (X.presheaf.obj (op U))
ha : s ≠ 0
⊢ IsOpen ↑(RingedSpace.basicOpen X.toSheafedSpace s)
[PROOFSTEP]
erw [basicOpen_eq_bot_iff]
[GOAL]
X : Scheme
inst✝ : IsIntegral X
U : Opens ↑↑X.toPresheafedSpace
m : genericPoint ↑↑X.toPresheafedSpace ∈ U
s : (forget CommRingCat).obj (X.presheaf.obj (op U))
ha : s ≠ 0
⊢ ¬s = 0
X : Scheme
inst✝ : IsIntegral X
U : Opens ↑↑X.toPresheafedSpace
m : genericPoint ↑↑X.toPresheafedSpace ∈ U
s : (forget CommRingCat).obj (X.presheaf.obj (op U))
ha : s ≠ 0
⊢ IsOpen ↑(RingedSpace.basicOpen X.toSheafedSpace s)
[PROOFSTEP]
exacts [ha, (RingedSpace.basicOpen _ _).isOpen]
[GOAL]
case h.intro.intro.intro
X : Scheme
inst✝ : IsIntegral X
U : Opens ↑↑X.toPresheafedSpace
m : genericPoint ↑↑X.toPresheafedSpace ∈ U
s : (forget CommRingCat).obj (X.presheaf.obj (op U))
ha : s ≠ 0
hs : genericPoint ↑↑X.toPresheafedSpace ∈ RingedSpace.basicOpen X.toSheafedSpace s
⊢ IsUnit (↑(Presheaf.germ X.presheaf { val := genericPoint ↑↑X.toPresheafedSpace, property := m }) s)
[PROOFSTEP]
have := (X.presheaf.germ ⟨_, hs⟩).isUnit_map (RingedSpace.isUnit_res_basicOpen _ s)
[GOAL]
case h.intro.intro.intro
X : Scheme
inst✝ : IsIntegral X
U : Opens ↑↑X.toPresheafedSpace
m : genericPoint ↑↑X.toPresheafedSpace ∈ U
s : (forget CommRingCat).obj (X.presheaf.obj (op U))
ha : s ≠ 0
hs : genericPoint ↑↑X.toPresheafedSpace ∈ RingedSpace.basicOpen X.toSheafedSpace s
this :
  IsUnit
    (↑(Presheaf.germ X.presheaf { val := genericPoint ↑↑X.toPresheafedSpace, property := hs })
      (↑(X.presheaf.map (homOfLE (_ : RingedSpace.basicOpen X.toSheafedSpace s ≤ U)).op) s))
⊢ IsUnit (↑(Presheaf.germ X.presheaf { val := genericPoint ↑↑X.toPresheafedSpace, property := m }) s)
[PROOFSTEP]
rwa [TopCat.Presheaf.germ_res_apply] at this 
[GOAL]
X : Scheme
inst✝ : IsIntegral X
U : Opens ↑↑X.toPresheafedSpace
x : { x // x ∈ U }
⊢ Function.Injective ↑(Presheaf.germ X.presheaf x)
[PROOFSTEP]
rw [injective_iff_map_eq_zero]
[GOAL]
X : Scheme
inst✝ : IsIntegral X
U : Opens ↑↑X.toPresheafedSpace
x : { x // x ∈ U }
⊢ ∀ (a : (forget CommRingCat).obj (X.presheaf.obj (op U))), ↑(Presheaf.germ X.presheaf x) a = 0 → a = 0
[PROOFSTEP]
intro y hy
[GOAL]
X : Scheme
inst✝ : IsIntegral X
U : Opens ↑↑X.toPresheafedSpace
x : { x // x ∈ U }
y : (forget CommRingCat).obj (X.presheaf.obj (op U))
hy : ↑(Presheaf.germ X.presheaf x) y = 0
⊢ y = 0
[PROOFSTEP]
rw [← (X.presheaf.germ x).map_zero] at hy 
[GOAL]
X : Scheme
inst✝ : IsIntegral X
U : Opens ↑↑X.toPresheafedSpace
x : { x // x ∈ U }
y : (forget CommRingCat).obj (X.presheaf.obj (op U))
hy : ↑(Presheaf.germ X.presheaf x) y = ↑(Presheaf.germ X.presheaf x) 0
⊢ y = 0
[PROOFSTEP]
obtain ⟨W, hW, iU, iV, e⟩ := X.presheaf.germ_eq _ x.prop x.prop _ _ hy
[GOAL]
case intro.intro.intro.intro
X : Scheme
inst✝ : IsIntegral X
U : Opens ↑↑X.toPresheafedSpace
x : { x // x ∈ U }
y : (forget CommRingCat).obj (X.presheaf.obj (op U))
hy : ↑(Presheaf.germ X.presheaf x) y = ↑(Presheaf.germ X.presheaf x) 0
W : Opens ↑↑X.toPresheafedSpace
hW : ↑x ∈ W
iU iV : W ⟶ U
e : ↑(X.presheaf.map iU.op) y = ↑(X.presheaf.map iV.op) 0
⊢ y = 0
[PROOFSTEP]
cases show iU = iV from Subsingleton.elim _ _
[GOAL]
case intro.intro.intro.intro.refl
X : Scheme
inst✝ : IsIntegral X
U : Opens ↑↑X.toPresheafedSpace
x : { x // x ∈ U }
y : (forget CommRingCat).obj (X.presheaf.obj (op U))
hy : ↑(Presheaf.germ X.presheaf x) y = ↑(Presheaf.germ X.presheaf x) 0
W : Opens ↑↑X.toPresheafedSpace
hW : ↑x ∈ W
iU : W ⟶ U
e : ↑(X.presheaf.map iU.op) y = ↑(X.presheaf.map iU.op) 0
⊢ y = 0
[PROOFSTEP]
haveI : Nonempty W := ⟨⟨_, hW⟩⟩
[GOAL]
case intro.intro.intro.intro.refl
X : Scheme
inst✝ : IsIntegral X
U : Opens ↑↑X.toPresheafedSpace
x : { x // x ∈ U }
y : (forget CommRingCat).obj (X.presheaf.obj (op U))
hy : ↑(Presheaf.germ X.presheaf x) y = ↑(Presheaf.germ X.presheaf x) 0
W : Opens ↑↑X.toPresheafedSpace
hW : ↑x ∈ W
iU : W ⟶ U
e : ↑(X.presheaf.map iU.op) y = ↑(X.presheaf.map iU.op) 0
this : Nonempty { x // x ∈ W }
⊢ y = 0
[PROOFSTEP]
exact map_injective_of_isIntegral X iU e
[GOAL]
X✝ : Scheme
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
hX : IrreducibleSpace ↑↑X.toPresheafedSpace
inst✝ : IrreducibleSpace ↑↑Y.toPresheafedSpace
⊢ ↑f.val.base (genericPoint ↑↑X.toPresheafedSpace) = genericPoint ↑↑Y.toPresheafedSpace
[PROOFSTEP]
apply ((genericPoint_spec Y).eq _).symm
[GOAL]
X✝ : Scheme
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
hX : IrreducibleSpace ↑↑X.toPresheafedSpace
inst✝ : IrreducibleSpace ↑↑Y.toPresheafedSpace
⊢ IsGenericPoint (↑f.val.base (genericPoint ↑↑X.toPresheafedSpace)) ⊤
[PROOFSTEP]
convert (genericPoint_spec X.carrier).image (show Continuous f.1.base from ContinuousMap.continuous_toFun _)
[GOAL]
case h.e'_4.h
X✝ : Scheme
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
hX : IrreducibleSpace ↑↑X.toPresheafedSpace
inst✝ : IrreducibleSpace ↑↑Y.toPresheafedSpace
e_1✝ : ↑↑Y.toPresheafedSpace = (forget TopCat).obj ↑Y.toPresheafedSpace
⊢ ⊤ = closure (↑f.val.base '' ⊤)
[PROOFSTEP]
symm
[GOAL]
case h.e'_4.h
X✝ : Scheme
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
hX : IrreducibleSpace ↑↑X.toPresheafedSpace
inst✝ : IrreducibleSpace ↑↑Y.toPresheafedSpace
e_1✝ : ↑↑Y.toPresheafedSpace = (forget TopCat).obj ↑Y.toPresheafedSpace
⊢ closure (↑f.val.base '' ⊤) = ⊤
[PROOFSTEP]
rw [eq_top_iff, Set.top_eq_univ, Set.top_eq_univ]
[GOAL]
case h.e'_4.h
X✝ : Scheme
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
hX : IrreducibleSpace ↑↑X.toPresheafedSpace
inst✝ : IrreducibleSpace ↑↑Y.toPresheafedSpace
e_1✝ : ↑↑Y.toPresheafedSpace = (forget TopCat).obj ↑Y.toPresheafedSpace
⊢ Set.univ ≤ closure (↑f.val.base '' Set.univ)
[PROOFSTEP]
convert subset_closure_inter_of_isPreirreducible_of_isOpen _ H.base_open.open_range _
[GOAL]
case h.e'_2.h.e'_3
X✝ : Scheme
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
hX : IrreducibleSpace ↑↑X.toPresheafedSpace
inst✝ : IrreducibleSpace ↑↑Y.toPresheafedSpace
e_1✝ : ↑↑Y.toPresheafedSpace = (forget TopCat).obj ↑Y.toPresheafedSpace
⊢ ↑f.val.base '' Set.univ = Set.univ ∩ Set.range ↑f.val.base
case h.e'_4.h.convert_2
X✝ : Scheme
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
hX : IrreducibleSpace ↑↑X.toPresheafedSpace
inst✝ : IrreducibleSpace ↑↑Y.toPresheafedSpace
e_1✝ : ↑↑Y.toPresheafedSpace = (forget TopCat).obj ↑Y.toPresheafedSpace
⊢ IsPreirreducible Set.univ
case h.e'_4.h.convert_3
X✝ : Scheme
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
hX : IrreducibleSpace ↑↑X.toPresheafedSpace
inst✝ : IrreducibleSpace ↑↑Y.toPresheafedSpace
e_1✝ : ↑↑Y.toPresheafedSpace = (forget TopCat).obj ↑Y.toPresheafedSpace
⊢ Set.Nonempty (Set.univ ∩ Set.range ↑f.val.base)
[PROOFSTEP]
rw [Set.univ_inter, Set.image_univ]
[GOAL]
case h.e'_4.h.convert_2
X✝ : Scheme
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
hX : IrreducibleSpace ↑↑X.toPresheafedSpace
inst✝ : IrreducibleSpace ↑↑Y.toPresheafedSpace
e_1✝ : ↑↑Y.toPresheafedSpace = (forget TopCat).obj ↑Y.toPresheafedSpace
⊢ IsPreirreducible Set.univ
case h.e'_4.h.convert_3
X✝ : Scheme
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
hX : IrreducibleSpace ↑↑X.toPresheafedSpace
inst✝ : IrreducibleSpace ↑↑Y.toPresheafedSpace
e_1✝ : ↑↑Y.toPresheafedSpace = (forget TopCat).obj ↑Y.toPresheafedSpace
⊢ Set.Nonempty (Set.univ ∩ Set.range ↑f.val.base)
[PROOFSTEP]
apply PreirreducibleSpace.isPreirreducible_univ (α := Y.carrier)
[GOAL]
case h.e'_4.h.convert_3
X✝ : Scheme
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
hX : IrreducibleSpace ↑↑X.toPresheafedSpace
inst✝ : IrreducibleSpace ↑↑Y.toPresheafedSpace
e_1✝ : ↑↑Y.toPresheafedSpace = (forget TopCat).obj ↑Y.toPresheafedSpace
⊢ Set.Nonempty (Set.univ ∩ Set.range ↑f.val.base)
[PROOFSTEP]
exact ⟨_, trivial, Set.mem_range_self hX.2.some⟩
[GOAL]
X : Scheme
inst✝ : IrreducibleSpace ↑↑X.toPresheafedSpace
x : ↑↑X.toPresheafedSpace
⊢ Algebra ↑(Presheaf.stalk X.presheaf x) ↑(Scheme.functionField X)
[PROOFSTEP]
apply RingHom.toAlgebra
[GOAL]
case i
X : Scheme
inst✝ : IrreducibleSpace ↑↑X.toPresheafedSpace
x : ↑↑X.toPresheafedSpace
⊢ ↑(Presheaf.stalk X.presheaf x) →+* ↑(Scheme.functionField X)
[PROOFSTEP]
exact X.presheaf.stalkSpecializes ((genericPoint_spec X.carrier).specializes trivial)
[GOAL]
X : Scheme
inst✝¹ : IrreducibleSpace ↑↑X.toPresheafedSpace
U : Opens ↑↑X.toPresheafedSpace
x : { x // x ∈ U }
inst✝ : Nonempty { x // x ∈ U }
⊢ IsScalarTower ↑(X.presheaf.obj (op U)) ↑(Presheaf.stalk X.presheaf ↑x) ↑(Scheme.functionField X)
[PROOFSTEP]
apply IsScalarTower.of_algebraMap_eq'
[GOAL]
case h
X : Scheme
inst✝¹ : IrreducibleSpace ↑↑X.toPresheafedSpace
U : Opens ↑↑X.toPresheafedSpace
x : { x // x ∈ U }
inst✝ : Nonempty { x // x ∈ U }
⊢ algebraMap ↑(X.presheaf.obj (op U)) ↑(Scheme.functionField X) =
    RingHom.comp (algebraMap ↑(Presheaf.stalk X.presheaf ↑x) ↑(Scheme.functionField X))
      (algebraMap ↑(X.presheaf.obj (op U)) ↑(Presheaf.stalk X.presheaf ↑x))
[PROOFSTEP]
simp_rw [RingHom.algebraMap_toAlgebra]
[GOAL]
case h
X : Scheme
inst✝¹ : IrreducibleSpace ↑↑X.toPresheafedSpace
U : Opens ↑↑X.toPresheafedSpace
x : { x // x ∈ U }
inst✝ : Nonempty { x // x ∈ U }
⊢ Scheme.germToFunctionField X U =
    RingHom.comp (Presheaf.stalkSpecializes X.presheaf (_ : genericPoint ↑↑X.toPresheafedSpace ⤳ ↑x))
      (Presheaf.germ X.presheaf x)
[PROOFSTEP]
change _ = X.presheaf.germ x ≫ _
[GOAL]
case h
X : Scheme
inst✝¹ : IrreducibleSpace ↑↑X.toPresheafedSpace
U : Opens ↑↑X.toPresheafedSpace
x : { x // x ∈ U }
inst✝ : Nonempty { x // x ∈ U }
⊢ Scheme.germToFunctionField X U =
    Presheaf.germ X.presheaf x ≫ Presheaf.stalkSpecializes X.presheaf (_ : genericPoint ↑↑X.toPresheafedSpace ⤳ ↑x)
[PROOFSTEP]
rw [X.presheaf.germ_stalkSpecializes]
[GOAL]
X : Scheme
R : CommRingCat
inst✝ : IsDomain ↑R
⊢ ↑R →+* ↑(Scheme.functionField (Scheme.Spec.obj (op R)))
[PROOFSTEP]
change CommRingCat.of R ⟶ _
[GOAL]
X : Scheme
R : CommRingCat
inst✝ : IsDomain ↑R
⊢ CommRingCat.of ↑R ⟶ Scheme.functionField (Scheme.Spec.obj (op R))
[PROOFSTEP]
apply StructureSheaf.toStalk
[GOAL]
X : Scheme
R : CommRingCat
inst✝ : IsDomain ↑R
⊢ genericPoint ↑↑(Scheme.Spec.obj (op R)).toPresheafedSpace = { asIdeal := 0, IsPrime := (_ : Ideal.IsPrime ⊥) }
[PROOFSTEP]
apply (genericPoint_spec (Scheme.Spec.obj <| op R).carrier).eq
[GOAL]
X : Scheme
R : CommRingCat
inst✝ : IsDomain ↑R
⊢ IsGenericPoint { asIdeal := 0, IsPrime := (_ : Ideal.IsPrime ⊥) } ⊤
[PROOFSTEP]
rw [isGenericPoint_def]
[GOAL]
X : Scheme
R : CommRingCat
inst✝ : IsDomain ↑R
⊢ closure {{ asIdeal := 0, IsPrime := (_ : Ideal.IsPrime ⊥) }} = ⊤
[PROOFSTEP]
rw [← PrimeSpectrum.zeroLocus_vanishingIdeal_eq_closure, PrimeSpectrum.vanishingIdeal_singleton]
[GOAL]
X : Scheme
R : CommRingCat
inst✝ : IsDomain ↑R
⊢ PrimeSpectrum.zeroLocus ↑{ asIdeal := 0, IsPrime := (_ : Ideal.IsPrime ⊥) }.asIdeal = ⊤
[PROOFSTEP]
rw [Set.top_eq_univ, ← PrimeSpectrum.zeroLocus_singleton_zero]
[GOAL]
X : Scheme
R : CommRingCat
inst✝ : IsDomain ↑R
⊢ PrimeSpectrum.zeroLocus ↑{ asIdeal := 0, IsPrime := (_ : Ideal.IsPrime ⊥) }.asIdeal = PrimeSpectrum.zeroLocus {0}
[PROOFSTEP]
rfl
[GOAL]
X : Scheme
R : CommRingCat
inst✝ : IsDomain ↑R
⊢ IsFractionRing ↑R ↑(Scheme.functionField (Scheme.Spec.obj (op R)))
[PROOFSTEP]
convert StructureSheaf.IsLocalization.to_stalk R (genericPoint _)
[GOAL]
case a
X : Scheme
R : CommRingCat
inst✝ : IsDomain ↑R
⊢ IsFractionRing ↑R ↑(Scheme.functionField (Scheme.Spec.obj (op R))) ↔
    IsLocalization.AtPrime
      (↑(Presheaf.stalk (Sheaf.presheaf (Spec.structureSheaf ↑R))
          (genericPoint ↑↑(Scheme.Spec.obj (op R)).toPresheafedSpace)))
      (genericPoint ↑↑(Scheme.Spec.obj (op R)).toPresheafedSpace).asIdeal
[PROOFSTEP]
delta IsFractionRing IsLocalization.AtPrime
[GOAL]
case a
X : Scheme
R : CommRingCat
inst✝ : IsDomain ↑R
⊢ IsLocalization (nonZeroDivisors ↑R) ↑(Scheme.functionField (Scheme.Spec.obj (op R))) ↔
    IsLocalization (Ideal.primeCompl (genericPoint ↑↑(Scheme.Spec.obj (op R)).toPresheafedSpace).asIdeal)
      ↑(Presheaf.stalk (Sheaf.presheaf (Spec.structureSheaf ↑R))
          (genericPoint ↑↑(Scheme.Spec.obj (op R)).toPresheafedSpace))
[PROOFSTEP]
apply Eq.to_iff
[GOAL]
case a.a
X : Scheme
R : CommRingCat
inst✝ : IsDomain ↑R
⊢ IsLocalization (nonZeroDivisors ↑R) ↑(Scheme.functionField (Scheme.Spec.obj (op R))) =
    IsLocalization (Ideal.primeCompl (genericPoint ↑↑(Scheme.Spec.obj (op R)).toPresheafedSpace).asIdeal)
      ↑(Presheaf.stalk (Sheaf.presheaf (Spec.structureSheaf ↑R))
          (genericPoint ↑↑(Scheme.Spec.obj (op R)).toPresheafedSpace))
[PROOFSTEP]
congr 1
[GOAL]
case a.a.e_M
X : Scheme
R : CommRingCat
inst✝ : IsDomain ↑R
⊢ nonZeroDivisors ↑R = Ideal.primeCompl (genericPoint ↑↑(Scheme.Spec.obj (op R)).toPresheafedSpace).asIdeal
[PROOFSTEP]
rw [genericPoint_eq_bot_of_affine]
[GOAL]
case a.a.e_M
X : Scheme
R : CommRingCat
inst✝ : IsDomain ↑R
⊢ nonZeroDivisors ↑R = Ideal.primeCompl { asIdeal := 0, IsPrime := (_ : Ideal.IsPrime ⊥) }.asIdeal
[PROOFSTEP]
ext
[GOAL]
case a.a.e_M.h
X : Scheme
R : CommRingCat
inst✝ : IsDomain ↑R
x✝ : ↑R
⊢ x✝ ∈ nonZeroDivisors ↑R ↔ x✝ ∈ Ideal.primeCompl { asIdeal := 0, IsPrime := (_ : Ideal.IsPrime ⊥) }.asIdeal
[PROOFSTEP]
exact mem_nonZeroDivisors_iff_ne_zero
[GOAL]
X✝ : Scheme
X : Scheme
inst✝ : IsIntegral X
U : Opens ↑↑X.toPresheafedSpace
hU : IsAffineOpen U
h : Nonempty { x // x ∈ U }
⊢ Set.Nonempty (⊤ ∩ ↑U)
[PROOFSTEP]
simpa using h
[GOAL]
X✝ : Scheme
X : Scheme
inst✝ : IsIntegral X
U : Opens ↑↑X.toPresheafedSpace
hU : IsAffineOpen U
h : Nonempty { x // x ∈ U }
⊢ primeIdealOf hU
      { val := genericPoint ↑↑X.toPresheafedSpace, property := (_ : genericPoint ↑↑X.toPresheafedSpace ∈ ↑U) } =
    genericPoint ↑↑(Scheme.Spec.obj (op (X.presheaf.obj (op U)))).toPresheafedSpace
[PROOFSTEP]
haveI : IsAffine _ := hU
[GOAL]
X✝ : Scheme
X : Scheme
inst✝ : IsIntegral X
U : Opens ↑↑X.toPresheafedSpace
hU : IsAffineOpen U
h : Nonempty { x // x ∈ U }
this : IsAffine (Scheme.restrict X (_ : OpenEmbedding ↑(Opens.inclusion U)))
⊢ primeIdealOf hU
      { val := genericPoint ↑↑X.toPresheafedSpace, property := (_ : genericPoint ↑↑X.toPresheafedSpace ∈ ↑U) } =
    genericPoint ↑↑(Scheme.Spec.obj (op (X.presheaf.obj (op U)))).toPresheafedSpace
[PROOFSTEP]
have e : U.openEmbedding.isOpenMap.functor.obj ⊤ = U := by ext1; exact Set.image_univ.trans Subtype.range_coe
[GOAL]
X✝ : Scheme
X : Scheme
inst✝ : IsIntegral X
U : Opens ↑↑X.toPresheafedSpace
hU : IsAffineOpen U
h : Nonempty { x // x ∈ U }
this : IsAffine (Scheme.restrict X (_ : OpenEmbedding ↑(Opens.inclusion U)))
⊢ (IsOpenMap.functor (_ : IsOpenMap ↑(Opens.inclusion U))).obj ⊤ = U
[PROOFSTEP]
ext1
[GOAL]
case h
X✝ : Scheme
X : Scheme
inst✝ : IsIntegral X
U : Opens ↑↑X.toPresheafedSpace
hU : IsAffineOpen U
h : Nonempty { x // x ∈ U }
this : IsAffine (Scheme.restrict X (_ : OpenEmbedding ↑(Opens.inclusion U)))
⊢ ↑((IsOpenMap.functor (_ : IsOpenMap ↑(Opens.inclusion U))).obj ⊤) = ↑U
[PROOFSTEP]
exact Set.image_univ.trans Subtype.range_coe
[GOAL]
X✝ : Scheme
X : Scheme
inst✝ : IsIntegral X
U : Opens ↑↑X.toPresheafedSpace
hU : IsAffineOpen U
h : Nonempty { x // x ∈ U }
this : IsAffine (Scheme.restrict X (_ : OpenEmbedding ↑(Opens.inclusion U)))
e : (IsOpenMap.functor (_ : IsOpenMap ↑(Opens.inclusion U))).obj ⊤ = U
⊢ primeIdealOf hU
      { val := genericPoint ↑↑X.toPresheafedSpace, property := (_ : genericPoint ↑↑X.toPresheafedSpace ∈ ↑U) } =
    genericPoint ↑↑(Scheme.Spec.obj (op (X.presheaf.obj (op U)))).toPresheafedSpace
[PROOFSTEP]
delta IsAffineOpen.primeIdealOf
[GOAL]
X✝ : Scheme
X : Scheme
inst✝ : IsIntegral X
U : Opens ↑↑X.toPresheafedSpace
hU : IsAffineOpen U
h : Nonempty { x // x ∈ U }
this : IsAffine (Scheme.restrict X (_ : OpenEmbedding ↑(Opens.inclusion U)))
e : (IsOpenMap.functor (_ : IsOpenMap ↑(Opens.inclusion U))).obj ⊤ = U
⊢ ↑(Scheme.Spec.map
              (X.presheaf.map
                  (eqToHom (_ : (IsOpenMap.functor (_ : IsOpenMap ↑(Opens.inclusion U))).obj ⊤ = U)).op).op).val.base
      (↑(Scheme.isoSpec (Scheme.restrict X (_ : OpenEmbedding ↑(Opens.inclusion U)))).hom.val.base
        { val := genericPoint ↑↑X.toPresheafedSpace, property := (_ : genericPoint ↑↑X.toPresheafedSpace ∈ ↑U) }) =
    genericPoint ↑↑(Scheme.Spec.obj (op (X.presheaf.obj (op U)))).toPresheafedSpace
[PROOFSTEP]
erw [← Scheme.comp_val_base_apply]
[GOAL]
X✝ : Scheme
X : Scheme
inst✝ : IsIntegral X
U : Opens ↑↑X.toPresheafedSpace
hU : IsAffineOpen U
h : Nonempty { x // x ∈ U }
this : IsAffine (Scheme.restrict X (_ : OpenEmbedding ↑(Opens.inclusion U)))
e : (IsOpenMap.functor (_ : IsOpenMap ↑(Opens.inclusion U))).obj ⊤ = U
⊢ ↑((Scheme.isoSpec (Scheme.restrict X (_ : OpenEmbedding ↑(Opens.inclusion U)))).hom ≫
              Scheme.Spec.map
                (X.presheaf.map
                    (eqToHom (_ : (IsOpenMap.functor (_ : IsOpenMap ↑(Opens.inclusion U))).obj ⊤ = U)).op).op).val.base
      { val := genericPoint ↑↑X.toPresheafedSpace, property := (_ : genericPoint ↑↑X.toPresheafedSpace ∈ ↑U) } =
    genericPoint ↑↑(Scheme.Spec.obj (op (X.presheaf.obj (op U)))).toPresheafedSpace
[PROOFSTEP]
convert
  genericPoint_eq_of_isOpenImmersion
    ((X.restrict U.openEmbedding).isoSpec.hom ≫ Scheme.Spec.map (X.presheaf.map (eqToHom e).op).op)
      -- Porting note: this was `ext1`
[GOAL]
case h.e'_2.h.h.e'_6
X✝ : Scheme
X : Scheme
inst✝ : IsIntegral X
U : Opens ↑↑X.toPresheafedSpace
hU : IsAffineOpen U
h : Nonempty { x // x ∈ U }
this : IsAffine (Scheme.restrict X (_ : OpenEmbedding ↑(Opens.inclusion U)))
e : (IsOpenMap.functor (_ : IsOpenMap ↑(Opens.inclusion U))).obj ⊤ = U
e_1✝ :
  PrimeSpectrum ↑(X.presheaf.obj (op U)) =
    (fun x => (forget TopCat).obj ↑(Scheme.Spec.obj (op (X.presheaf.obj (op U)))).toPresheafedSpace)
      (genericPoint
        ↑↑(Scheme.restrict X
                    (_ : OpenEmbedding ↑(Opens.inclusion U))).toLocallyRingedSpace.toSheafedSpace.toPresheafedSpace)
⊢ { val := genericPoint ↑↑X.toPresheafedSpace, property := (_ : genericPoint ↑↑X.toPresheafedSpace ∈ ↑U) } =
    genericPoint
      ↑↑(Scheme.restrict X
                  (_ : OpenEmbedding ↑(Opens.inclusion U))).toLocallyRingedSpace.toSheafedSpace.toPresheafedSpace
[PROOFSTEP]
apply Subtype.ext
[GOAL]
case h.e'_2.h.h.e'_6.a
X✝ : Scheme
X : Scheme
inst✝ : IsIntegral X
U : Opens ↑↑X.toPresheafedSpace
hU : IsAffineOpen U
h : Nonempty { x // x ∈ U }
this : IsAffine (Scheme.restrict X (_ : OpenEmbedding ↑(Opens.inclusion U)))
e : (IsOpenMap.functor (_ : IsOpenMap ↑(Opens.inclusion U))).obj ⊤ = U
e_1✝ :
  PrimeSpectrum ↑(X.presheaf.obj (op U)) =
    (fun x => (forget TopCat).obj ↑(Scheme.Spec.obj (op (X.presheaf.obj (op U)))).toPresheafedSpace)
      (genericPoint
        ↑↑(Scheme.restrict X
                    (_ : OpenEmbedding ↑(Opens.inclusion U))).toLocallyRingedSpace.toSheafedSpace.toPresheafedSpace)
⊢ ↑{ val := genericPoint ↑↑X.toPresheafedSpace, property := (_ : genericPoint ↑↑X.toPresheafedSpace ∈ ↑U) } =
    ↑(genericPoint
        ↑↑(Scheme.restrict X
                    (_ : OpenEmbedding ↑(Opens.inclusion U))).toLocallyRingedSpace.toSheafedSpace.toPresheafedSpace)
[PROOFSTEP]
exact (genericPoint_eq_of_isOpenImmersion (X.ofRestrict U.openEmbedding)).symm
[GOAL]
X : Scheme
inst✝ : IsIntegral X
U : Opens ↑↑X.toPresheafedSpace
hU : IsAffineOpen U
hU' : Nonempty { x // x ∈ U }
⊢ IsFractionRing ↑(X.presheaf.obj (op U)) ↑(Scheme.functionField X)
[PROOFSTEP]
haveI : IsAffine _ := hU
[GOAL]
X : Scheme
inst✝ : IsIntegral X
U : Opens ↑↑X.toPresheafedSpace
hU : IsAffineOpen U
hU' : Nonempty { x // x ∈ U }
this : IsAffine (Scheme.restrict X (_ : OpenEmbedding ↑(Opens.inclusion U)))
⊢ IsFractionRing ↑(X.presheaf.obj (op U)) ↑(Scheme.functionField X)
[PROOFSTEP]
haveI : Nonempty (X.restrict U.openEmbedding).carrier := hU'
[GOAL]
X : Scheme
inst✝ : IsIntegral X
U : Opens ↑↑X.toPresheafedSpace
hU : IsAffineOpen U
hU' : Nonempty { x // x ∈ U }
this✝ : IsAffine (Scheme.restrict X (_ : OpenEmbedding ↑(Opens.inclusion U)))
this :
  Nonempty
    ↑↑(Scheme.restrict X (_ : OpenEmbedding ↑(Opens.inclusion U))).toLocallyRingedSpace.toSheafedSpace.toPresheafedSpace
⊢ IsFractionRing ↑(X.presheaf.obj (op U)) ↑(Scheme.functionField X)
[PROOFSTEP]
haveI : IsIntegral (X.restrict U.openEmbedding) :=
  @isIntegralOfIsAffineIsDomain _ _ _ (by dsimp; rw [Opens.openEmbedding_obj_top]; infer_instance)
[GOAL]
X : Scheme
inst✝ : IsIntegral X
U : Opens ↑↑X.toPresheafedSpace
hU : IsAffineOpen U
hU' : Nonempty { x // x ∈ U }
this✝ : IsAffine (Scheme.restrict X (_ : OpenEmbedding ↑(Opens.inclusion U)))
this :
  Nonempty
    ↑↑(Scheme.restrict X (_ : OpenEmbedding ↑(Opens.inclusion U))).toLocallyRingedSpace.toSheafedSpace.toPresheafedSpace
⊢ IsDomain
    ↑((Scheme.restrict X
                    (_ :
                      OpenEmbedding
                        ↑(Opens.inclusion U))).toLocallyRingedSpace.toSheafedSpace.toPresheafedSpace.presheaf.obj
        (op ⊤))
[PROOFSTEP]
dsimp
[GOAL]
X : Scheme
inst✝ : IsIntegral X
U : Opens ↑↑X.toPresheafedSpace
hU : IsAffineOpen U
hU' : Nonempty { x // x ∈ U }
this✝ : IsAffine (Scheme.restrict X (_ : OpenEmbedding ↑(Opens.inclusion U)))
this :
  Nonempty
    ↑↑(Scheme.restrict X (_ : OpenEmbedding ↑(Opens.inclusion U))).toLocallyRingedSpace.toSheafedSpace.toPresheafedSpace
⊢ IsDomain ↑(X.presheaf.obj (op ((IsOpenMap.functor (_ : IsOpenMap ↑(Opens.inclusion U))).obj ⊤)))
[PROOFSTEP]
rw [Opens.openEmbedding_obj_top]
[GOAL]
X : Scheme
inst✝ : IsIntegral X
U : Opens ↑↑X.toPresheafedSpace
hU : IsAffineOpen U
hU' : Nonempty { x // x ∈ U }
this✝ : IsAffine (Scheme.restrict X (_ : OpenEmbedding ↑(Opens.inclusion U)))
this :
  Nonempty
    ↑↑(Scheme.restrict X (_ : OpenEmbedding ↑(Opens.inclusion U))).toLocallyRingedSpace.toSheafedSpace.toPresheafedSpace
⊢ IsDomain ↑(X.presheaf.obj (op U))
[PROOFSTEP]
infer_instance
[GOAL]
X : Scheme
inst✝ : IsIntegral X
U : Opens ↑↑X.toPresheafedSpace
hU : IsAffineOpen U
hU' : Nonempty { x // x ∈ U }
this✝¹ : IsAffine (Scheme.restrict X (_ : OpenEmbedding ↑(Opens.inclusion U)))
this✝ :
  Nonempty
    ↑↑(Scheme.restrict X (_ : OpenEmbedding ↑(Opens.inclusion U))).toLocallyRingedSpace.toSheafedSpace.toPresheafedSpace
this : IsIntegral (Scheme.restrict X (_ : OpenEmbedding ↑(Opens.inclusion U)))
⊢ IsFractionRing ↑(X.presheaf.obj (op U)) ↑(Scheme.functionField X)
[PROOFSTEP]
delta IsFractionRing Scheme.functionField
[GOAL]
X : Scheme
inst✝ : IsIntegral X
U : Opens ↑↑X.toPresheafedSpace
hU : IsAffineOpen U
hU' : Nonempty { x // x ∈ U }
this✝¹ : IsAffine (Scheme.restrict X (_ : OpenEmbedding ↑(Opens.inclusion U)))
this✝ :
  Nonempty
    ↑↑(Scheme.restrict X (_ : OpenEmbedding ↑(Opens.inclusion U))).toLocallyRingedSpace.toSheafedSpace.toPresheafedSpace
this : IsIntegral (Scheme.restrict X (_ : OpenEmbedding ↑(Opens.inclusion U)))
⊢ IsLocalization (nonZeroDivisors ↑(X.presheaf.obj (op U)))
    ↑(Presheaf.stalk X.presheaf (genericPoint ↑↑X.toPresheafedSpace))
[PROOFSTEP]
convert hU.isLocalization_stalk ⟨genericPoint X.carrier, _⟩ using 1
[GOAL]
case h.e'_3.h
X : Scheme
inst✝ : IsIntegral X
U : Opens ↑↑X.toPresheafedSpace
hU : IsAffineOpen U
hU' : Nonempty { x // x ∈ U }
this✝¹ : IsAffine (Scheme.restrict X (_ : OpenEmbedding ↑(Opens.inclusion U)))
this✝ :
  Nonempty
    ↑↑(Scheme.restrict X (_ : OpenEmbedding ↑(Opens.inclusion U))).toLocallyRingedSpace.toSheafedSpace.toPresheafedSpace
this : IsIntegral (Scheme.restrict X (_ : OpenEmbedding ↑(Opens.inclusion U)))
⊢ nonZeroDivisors ↑(X.presheaf.obj (op U)) =
    Ideal.primeCompl
      (IsAffineOpen.primeIdealOf hU
          { val := genericPoint ↑↑X.toPresheafedSpace,
            property := (_ : genericPoint ↑↑X.toPresheafedSpace ∈ ↑U) }).asIdeal
[PROOFSTEP]
rw [hU.primeIdealOf_genericPoint, genericPoint_eq_bot_of_affine]
[GOAL]
case h.e'_3.h
X : Scheme
inst✝ : IsIntegral X
U : Opens ↑↑X.toPresheafedSpace
hU : IsAffineOpen U
hU' : Nonempty { x // x ∈ U }
this✝¹ : IsAffine (Scheme.restrict X (_ : OpenEmbedding ↑(Opens.inclusion U)))
this✝ :
  Nonempty
    ↑↑(Scheme.restrict X (_ : OpenEmbedding ↑(Opens.inclusion U))).toLocallyRingedSpace.toSheafedSpace.toPresheafedSpace
this : IsIntegral (Scheme.restrict X (_ : OpenEmbedding ↑(Opens.inclusion U)))
⊢ nonZeroDivisors ↑(X.presheaf.obj (op U)) = Ideal.primeCompl { asIdeal := 0, IsPrime := (_ : Ideal.IsPrime ⊥) }.asIdeal
[PROOFSTEP]
ext
[GOAL]
case h.e'_3.h.h
X : Scheme
inst✝ : IsIntegral X
U : Opens ↑↑X.toPresheafedSpace
hU : IsAffineOpen U
hU' : Nonempty { x // x ∈ U }
this✝¹ : IsAffine (Scheme.restrict X (_ : OpenEmbedding ↑(Opens.inclusion U)))
this✝ :
  Nonempty
    ↑↑(Scheme.restrict X (_ : OpenEmbedding ↑(Opens.inclusion U))).toLocallyRingedSpace.toSheafedSpace.toPresheafedSpace
this : IsIntegral (Scheme.restrict X (_ : OpenEmbedding ↑(Opens.inclusion U)))
x✝ : ↑(X.presheaf.obj (op U))
⊢ x✝ ∈ nonZeroDivisors ↑(X.presheaf.obj (op U)) ↔
    x✝ ∈ Ideal.primeCompl { asIdeal := 0, IsPrime := (_ : Ideal.IsPrime ⊥) }.asIdeal
[PROOFSTEP]
exact mem_nonZeroDivisors_iff_ne_zero
