[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
