[GOAL]
X Y : Scheme
f : X ⟶ Y
x✝ : QuasiCompact f
h : ∀ (U : Set ↑↑Y.toPresheafedSpace), IsOpen U → IsCompact U → IsCompact (↑f.val.base ⁻¹' U)
⊢ Continuous ↑f.val.base
[PROOFSTEP]
continuity
[GOAL]
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
f : X ⟶ Y
inst✝ : IsIso f
⊢ QuasiCompact f
[PROOFSTEP]
constructor
[GOAL]
case isCompact_preimage
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
f : X ⟶ Y
inst✝ : IsIso f
⊢ ∀ (U : Set ↑↑Y.toPresheafedSpace), IsOpen U → IsCompact U → IsCompact (↑f.val.base ⁻¹' U)
[PROOFSTEP]
intro U _ hU'
[GOAL]
case isCompact_preimage
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
f : X ⟶ Y
inst✝ : IsIso f
U : Set ↑↑Y.toPresheafedSpace
a✝ : IsOpen U
hU' : IsCompact U
⊢ IsCompact (↑f.val.base ⁻¹' U)
[PROOFSTEP]
convert hU'.image (inv f.1.base).continuous_toFun using 1
[GOAL]
case h.e'_3.h
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
f : X ⟶ Y
inst✝ : IsIso f
U : Set ↑↑Y.toPresheafedSpace
a✝ : IsOpen U
hU' : IsCompact U
e_1✝ : (forget TopCat).obj ↑X.toPresheafedSpace = ↑↑X.toPresheafedSpace
⊢ ↑f.val.base ⁻¹' U = (inv f.val.base).toFun '' U
[PROOFSTEP]
rw [Set.image_eq_preimage_of_inverse]
[GOAL]
case h.e'_3.h.h₁
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
f : X ⟶ Y
inst✝ : IsIso f
U : Set ↑↑Y.toPresheafedSpace
a✝ : IsOpen U
hU' : IsCompact U
e_1✝ : (forget TopCat).obj ↑X.toPresheafedSpace = ↑↑X.toPresheafedSpace
⊢ Function.LeftInverse (↑f.val.base) (inv f.val.base).toFun
case h.e'_3.h.h₂
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
f : X ⟶ Y
inst✝ : IsIso f
U : Set ↑↑Y.toPresheafedSpace
a✝ : IsOpen U
hU' : IsCompact U
e_1✝ : (forget TopCat).obj ↑X.toPresheafedSpace = ↑↑X.toPresheafedSpace
⊢ Function.RightInverse (↑f.val.base) (inv f.val.base).toFun
[PROOFSTEP]
delta Function.LeftInverse
[GOAL]
case h.e'_3.h.h₁
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
f : X ⟶ Y
inst✝ : IsIso f
U : Set ↑↑Y.toPresheafedSpace
a✝ : IsOpen U
hU' : IsCompact U
e_1✝ : (forget TopCat).obj ↑X.toPresheafedSpace = ↑↑X.toPresheafedSpace
⊢ ∀ (x : ↑↑Y.toPresheafedSpace), ↑f.val.base (ContinuousMap.toFun (inv f.val.base) x) = x
case h.e'_3.h.h₂
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
f : X ⟶ Y
inst✝ : IsIso f
U : Set ↑↑Y.toPresheafedSpace
a✝ : IsOpen U
hU' : IsCompact U
e_1✝ : (forget TopCat).obj ↑X.toPresheafedSpace = ↑↑X.toPresheafedSpace
⊢ Function.RightInverse (↑f.val.base) (inv f.val.base).toFun
[PROOFSTEP]
exacts [IsIso.inv_hom_id_apply f.1.base, IsIso.hom_inv_id_apply f.1.base]
[GOAL]
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : QuasiCompact f
inst✝ : QuasiCompact g
⊢ QuasiCompact (f ≫ g)
[PROOFSTEP]
constructor
[GOAL]
case isCompact_preimage
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : QuasiCompact f
inst✝ : QuasiCompact g
⊢ ∀ (U : Set ↑↑Z.toPresheafedSpace), IsOpen U → IsCompact U → IsCompact (↑(f ≫ g).val.base ⁻¹' U)
[PROOFSTEP]
intro U hU hU'
[GOAL]
case isCompact_preimage
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : QuasiCompact f
inst✝ : QuasiCompact g
U : Set ↑↑Z.toPresheafedSpace
hU : IsOpen U
hU' : IsCompact U
⊢ IsCompact (↑(f ≫ g).val.base ⁻¹' U)
[PROOFSTEP]
rw [Scheme.comp_val_base, coe_comp, Set.preimage_comp]
[GOAL]
case isCompact_preimage
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : QuasiCompact f
inst✝ : QuasiCompact g
U : Set ↑↑Z.toPresheafedSpace
hU : IsOpen U
hU' : IsCompact U
⊢ IsCompact (↑f.val.base ⁻¹' (↑g.val.base ⁻¹' U))
[PROOFSTEP]
apply QuasiCompact.isCompact_preimage
[GOAL]
case isCompact_preimage.a
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : QuasiCompact f
inst✝ : QuasiCompact g
U : Set ↑↑Z.toPresheafedSpace
hU : IsOpen U
hU' : IsCompact U
⊢ IsOpen (↑g.val.base ⁻¹' U)
[PROOFSTEP]
exact
  Continuous.isOpen_preimage
    (by
      -- porting note: `continuity` failed
          -- see https://github.com/leanprover-community/mathlib4/issues/5030exact Scheme.Hom.continuous g)
    _ hU
[GOAL]
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : QuasiCompact f
inst✝ : QuasiCompact g
U : Set ↑↑Z.toPresheafedSpace
hU : IsOpen U
hU' : IsCompact U
⊢ Continuous ↑g.val.base
[PROOFSTEP]
exact Scheme.Hom.continuous g
[GOAL]
case isCompact_preimage.a
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : QuasiCompact f
inst✝ : QuasiCompact g
U : Set ↑↑Z.toPresheafedSpace
hU : IsOpen U
hU' : IsCompact U
⊢ IsCompact (↑g.val.base ⁻¹' U)
[PROOFSTEP]
apply QuasiCompact.isCompact_preimage
[GOAL]
case isCompact_preimage.a.a
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : QuasiCompact f
inst✝ : QuasiCompact g
U : Set ↑↑Z.toPresheafedSpace
hU : IsOpen U
hU' : IsCompact U
⊢ IsOpen U
[PROOFSTEP]
assumption
[GOAL]
case isCompact_preimage.a.a
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : QuasiCompact f
inst✝ : QuasiCompact g
U : Set ↑↑Z.toPresheafedSpace
hU : IsOpen U
hU' : IsCompact U
⊢ IsCompact U
[PROOFSTEP]
assumption
[GOAL]
X✝ Y : Scheme
f : X✝ ⟶ Y
X : Scheme
U : Set ↑↑X.toPresheafedSpace
⊢ IsCompact U ∧ IsOpen U ↔ ∃ s, Set.Finite s ∧ U = ⋃ (i : ↑(Scheme.affineOpens X)) (_ : i ∈ s), ↑↑i
[PROOFSTEP]
apply Opens.IsBasis.isCompact_open_iff_eq_finite_iUnion (fun (U : X.affineOpens) => (U : Opens X.carrier))
[GOAL]
case hb
X✝ Y : Scheme
f : X✝ ⟶ Y
X : Scheme
U : Set ↑↑X.toPresheafedSpace
⊢ Opens.IsBasis (Set.range fun U => ↑U)
[PROOFSTEP]
rw [Subtype.range_coe]
[GOAL]
case hb
X✝ Y : Scheme
f : X✝ ⟶ Y
X : Scheme
U : Set ↑↑X.toPresheafedSpace
⊢ Opens.IsBasis (Scheme.affineOpens X)
[PROOFSTEP]
exact isBasis_affine_open X
[GOAL]
case hb'
X✝ Y : Scheme
f : X✝ ⟶ Y
X : Scheme
U : Set ↑↑X.toPresheafedSpace
⊢ ∀ (i : ↑(Scheme.affineOpens X)), IsCompact ↑↑i
[PROOFSTEP]
exact fun i => i.2.isCompact
[GOAL]
X Y : Scheme
f : X ⟶ Y
⊢ QuasiCompact f ↔ ∀ (U : Opens ↑↑Y.toPresheafedSpace), IsAffineOpen U → IsCompact (↑f.val.base ⁻¹' ↑U)
[PROOFSTEP]
rw [QuasiCompact_iff]
[GOAL]
X Y : Scheme
f : X ⟶ Y
⊢ (∀ (U : Set ↑↑Y.toPresheafedSpace), IsOpen U → IsCompact U → IsCompact (↑f.val.base ⁻¹' U)) ↔
    ∀ (U : Opens ↑↑Y.toPresheafedSpace), IsAffineOpen U → IsCompact (↑f.val.base ⁻¹' ↑U)
[PROOFSTEP]
refine' ⟨fun H U hU => H U U.isOpen hU.isCompact, _⟩
[GOAL]
X Y : Scheme
f : X ⟶ Y
⊢ (∀ (U : Opens ↑↑Y.toPresheafedSpace), IsAffineOpen U → IsCompact (↑f.val.base ⁻¹' ↑U)) →
    ∀ (U : Set ↑↑Y.toPresheafedSpace), IsOpen U → IsCompact U → IsCompact (↑f.val.base ⁻¹' U)
[PROOFSTEP]
intro H U hU hU'
[GOAL]
X Y : Scheme
f : X ⟶ Y
H : ∀ (U : Opens ↑↑Y.toPresheafedSpace), IsAffineOpen U → IsCompact (↑f.val.base ⁻¹' ↑U)
U : Set ↑↑Y.toPresheafedSpace
hU : IsOpen U
hU' : IsCompact U
⊢ IsCompact (↑f.val.base ⁻¹' U)
[PROOFSTEP]
obtain ⟨S, hS, rfl⟩ := (isCompact_open_iff_eq_finset_affine_union U).mp ⟨hU', hU⟩
[GOAL]
case intro.intro
X Y : Scheme
f : X ⟶ Y
H : ∀ (U : Opens ↑↑Y.toPresheafedSpace), IsAffineOpen U → IsCompact (↑f.val.base ⁻¹' ↑U)
S : Set ↑(Scheme.affineOpens Y)
hS : Set.Finite S
hU : IsOpen (⋃ (i : ↑(Scheme.affineOpens Y)) (_ : i ∈ S), ↑↑i)
hU' : IsCompact (⋃ (i : ↑(Scheme.affineOpens Y)) (_ : i ∈ S), ↑↑i)
⊢ IsCompact (↑f.val.base ⁻¹' ⋃ (i : ↑(Scheme.affineOpens Y)) (_ : i ∈ S), ↑↑i)
[PROOFSTEP]
simp only [Set.preimage_iUnion]
[GOAL]
case intro.intro
X Y : Scheme
f : X ⟶ Y
H : ∀ (U : Opens ↑↑Y.toPresheafedSpace), IsAffineOpen U → IsCompact (↑f.val.base ⁻¹' ↑U)
S : Set ↑(Scheme.affineOpens Y)
hS : Set.Finite S
hU : IsOpen (⋃ (i : ↑(Scheme.affineOpens Y)) (_ : i ∈ S), ↑↑i)
hU' : IsCompact (⋃ (i : ↑(Scheme.affineOpens Y)) (_ : i ∈ S), ↑↑i)
⊢ IsCompact (⋃ (i : ↑(Scheme.affineOpens Y)) (_ : i ∈ S), ↑f.val.base ⁻¹' ↑↑i)
[PROOFSTEP]
exact Set.Finite.isCompact_biUnion hS (fun i _ => H i i.prop)
[GOAL]
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
f : X ⟶ Y
⊢ AffineTargetMorphismProperty.toProperty affineProperty f ↔ IsAffine Y ∧ CompactSpace ↑↑X.toPresheafedSpace
[PROOFSTEP]
delta AffineTargetMorphismProperty.toProperty QuasiCompact.affineProperty
[GOAL]
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
f : X ⟶ Y
⊢ (∃ h, CompactSpace ↑↑X.toPresheafedSpace) ↔ IsAffine Y ∧ CompactSpace ↑↑X.toPresheafedSpace
[PROOFSTEP]
simp
[GOAL]
X Y : Scheme
f : X ⟶ Y
⊢ QuasiCompact f ↔ targetAffineLocally QuasiCompact.affineProperty f
[PROOFSTEP]
rw [quasiCompact_iff_forall_affine]
[GOAL]
X Y : Scheme
f : X ⟶ Y
⊢ (∀ (U : Opens ↑↑Y.toPresheafedSpace), IsAffineOpen U → IsCompact (↑f.val.base ⁻¹' ↑U)) ↔
    targetAffineLocally QuasiCompact.affineProperty f
[PROOFSTEP]
trans ∀ U : Y.affineOpens, IsCompact (f.1.base ⁻¹' (U : Set Y.carrier))
[GOAL]
X Y : Scheme
f : X ⟶ Y
⊢ (∀ (U : Opens ↑↑Y.toPresheafedSpace), IsAffineOpen U → IsCompact (↑f.val.base ⁻¹' ↑U)) ↔
    ∀ (U : ↑(Scheme.affineOpens Y)), IsCompact (↑f.val.base ⁻¹' ↑↑U)
[PROOFSTEP]
exact ⟨fun h U => h U U.prop, fun h U hU => h ⟨U, hU⟩⟩
[GOAL]
X Y : Scheme
f : X ⟶ Y
⊢ (∀ (U : ↑(Scheme.affineOpens Y)), IsCompact (↑f.val.base ⁻¹' ↑↑U)) ↔ targetAffineLocally QuasiCompact.affineProperty f
[PROOFSTEP]
apply forall_congr'
[GOAL]
case h
X Y : Scheme
f : X ⟶ Y
⊢ ∀ (a : ↑(Scheme.affineOpens Y)), IsCompact (↑f.val.base ⁻¹' ↑↑a) ↔ QuasiCompact.affineProperty (f ∣_ ↑a)
[PROOFSTEP]
exact fun _ => isCompact_iff_compactSpace
[GOAL]
X Y : Scheme
f : X ⟶ Y
⊢ @QuasiCompact = targetAffineLocally QuasiCompact.affineProperty
[PROOFSTEP]
ext
[GOAL]
case h.h.h.a
X Y : Scheme
f : X ⟶ Y
x✝² x✝¹ : Scheme
x✝ : x✝² ⟶ x✝¹
⊢ QuasiCompact x✝ ↔ targetAffineLocally QuasiCompact.affineProperty x✝
[PROOFSTEP]
exact quasiCompact_iff_affineProperty _
[GOAL]
X✝ Y : Scheme
f✝ : X✝ ⟶ Y
X : Scheme
U : Opens ↑↑X.toPresheafedSpace
hU : IsCompact ↑U
f : ↑(X.presheaf.obj (op U))
⊢ IsCompact ↑(Scheme.basicOpen X f)
[PROOFSTEP]
classical
refine' ((isCompact_open_iff_eq_finset_affine_union _).mpr _).1
obtain ⟨s, hs, e⟩ := (isCompact_open_iff_eq_finset_affine_union _).mp ⟨hU, U.isOpen⟩
let g : s → X.affineOpens := by
  intro V
  use V.1 ⊓ X.basicOpen f
  have : V.1.1 ⟶ U := by
    apply homOfLE; change _ ⊆ (U : Set X.carrier); rw [e]
    convert @Set.subset_iUnion₂ _ _ _ (fun (U : X.affineOpens) (_ : U ∈ s) => ↑U) V V.prop using 1
  erw [← X.toLocallyRingedSpace.toRingedSpace.basicOpen_res this.op]
  exact IsAffineOpen.basicOpenIsAffine V.1.prop _
haveI : Finite s := hs.to_subtype
refine' ⟨Set.range g, Set.finite_range g, _⟩
refine' (Set.inter_eq_right_iff_subset.mpr (SetLike.coe_subset_coe.2 <| RingedSpace.basicOpen_le _ _)).symm.trans _
rw [e, Set.iUnion₂_inter]
apply le_antisymm <;> apply Set.iUnion₂_subset
· intro i hi
  exact
    Set.Subset.trans (Set.Subset.rfl : _ ≤ g ⟨i, hi⟩)
      (@Set.subset_iUnion₂ _ _ _ (fun (i : Scheme.affineOpens X) (_ : i ∈ Set.range g) => (i : Set X.toPresheafedSpace))
        _ (Set.mem_range_self ⟨i, hi⟩))
· rintro ⟨i, hi⟩ ⟨⟨j, hj⟩, hj'⟩
  rw [← hj']
  refine' Set.Subset.trans _ (Set.subset_iUnion₂ j hj)
  exact Set.Subset.rfl
[GOAL]
X✝ Y : Scheme
f✝ : X✝ ⟶ Y
X : Scheme
U : Opens ↑↑X.toPresheafedSpace
hU : IsCompact ↑U
f : ↑(X.presheaf.obj (op U))
⊢ IsCompact ↑(Scheme.basicOpen X f)
[PROOFSTEP]
refine' ((isCompact_open_iff_eq_finset_affine_union _).mpr _).1
[GOAL]
X✝ Y : Scheme
f✝ : X✝ ⟶ Y
X : Scheme
U : Opens ↑↑X.toPresheafedSpace
hU : IsCompact ↑U
f : ↑(X.presheaf.obj (op U))
⊢ ∃ s, Set.Finite s ∧ ↑(Scheme.basicOpen X f) = ⋃ (i : ↑(Scheme.affineOpens X)) (_ : i ∈ s), ↑↑i
[PROOFSTEP]
obtain ⟨s, hs, e⟩ := (isCompact_open_iff_eq_finset_affine_union _).mp ⟨hU, U.isOpen⟩
[GOAL]
case intro.intro
X✝ Y : Scheme
f✝ : X✝ ⟶ Y
X : Scheme
U : Opens ↑↑X.toPresheafedSpace
hU : IsCompact ↑U
f : ↑(X.presheaf.obj (op U))
s : Set ↑(Scheme.affineOpens X)
hs : Set.Finite s
e : ↑U = ⋃ (i : ↑(Scheme.affineOpens X)) (_ : i ∈ s), ↑↑i
⊢ ∃ s, Set.Finite s ∧ ↑(Scheme.basicOpen X f) = ⋃ (i : ↑(Scheme.affineOpens X)) (_ : i ∈ s), ↑↑i
[PROOFSTEP]
let g : s → X.affineOpens := by
  intro V
  use V.1 ⊓ X.basicOpen f
  have : V.1.1 ⟶ U := by
    apply homOfLE; change _ ⊆ (U : Set X.carrier); rw [e]
    convert @Set.subset_iUnion₂ _ _ _ (fun (U : X.affineOpens) (_ : U ∈ s) => ↑U) V V.prop using 1
  erw [← X.toLocallyRingedSpace.toRingedSpace.basicOpen_res this.op]
  exact IsAffineOpen.basicOpenIsAffine V.1.prop _
[GOAL]
X✝ Y : Scheme
f✝ : X✝ ⟶ Y
X : Scheme
U : Opens ↑↑X.toPresheafedSpace
hU : IsCompact ↑U
f : ↑(X.presheaf.obj (op U))
s : Set ↑(Scheme.affineOpens X)
hs : Set.Finite s
e : ↑U = ⋃ (i : ↑(Scheme.affineOpens X)) (_ : i ∈ s), ↑↑i
⊢ ↑s → ↑(Scheme.affineOpens X)
[PROOFSTEP]
intro V
[GOAL]
X✝ Y : Scheme
f✝ : X✝ ⟶ Y
X : Scheme
U : Opens ↑↑X.toPresheafedSpace
hU : IsCompact ↑U
f : ↑(X.presheaf.obj (op U))
s : Set ↑(Scheme.affineOpens X)
hs : Set.Finite s
e : ↑U = ⋃ (i : ↑(Scheme.affineOpens X)) (_ : i ∈ s), ↑↑i
V : ↑s
⊢ ↑(Scheme.affineOpens X)
[PROOFSTEP]
use V.1 ⊓ X.basicOpen f
[GOAL]
case property
X✝ Y : Scheme
f✝ : X✝ ⟶ Y
X : Scheme
U : Opens ↑↑X.toPresheafedSpace
hU : IsCompact ↑U
f : ↑(X.presheaf.obj (op U))
s : Set ↑(Scheme.affineOpens X)
hs : Set.Finite s
e : ↑U = ⋃ (i : ↑(Scheme.affineOpens X)) (_ : i ∈ s), ↑↑i
V : ↑s
⊢ ↑↑V ⊓ Scheme.basicOpen X f ∈ Scheme.affineOpens X
[PROOFSTEP]
have : V.1.1 ⟶ U := by
  apply homOfLE; change _ ⊆ (U : Set X.carrier); rw [e]
  convert @Set.subset_iUnion₂ _ _ _ (fun (U : X.affineOpens) (_ : U ∈ s) => ↑U) V V.prop using 1
[GOAL]
X✝ Y : Scheme
f✝ : X✝ ⟶ Y
X : Scheme
U : Opens ↑↑X.toPresheafedSpace
hU : IsCompact ↑U
f : ↑(X.presheaf.obj (op U))
s : Set ↑(Scheme.affineOpens X)
hs : Set.Finite s
e : ↑U = ⋃ (i : ↑(Scheme.affineOpens X)) (_ : i ∈ s), ↑↑i
V : ↑s
⊢ ↑↑V ⟶ U
[PROOFSTEP]
apply homOfLE
[GOAL]
case h
X✝ Y : Scheme
f✝ : X✝ ⟶ Y
X : Scheme
U : Opens ↑↑X.toPresheafedSpace
hU : IsCompact ↑U
f : ↑(X.presheaf.obj (op U))
s : Set ↑(Scheme.affineOpens X)
hs : Set.Finite s
e : ↑U = ⋃ (i : ↑(Scheme.affineOpens X)) (_ : i ∈ s), ↑↑i
V : ↑s
⊢ ↑↑V ≤ U
[PROOFSTEP]
change _ ⊆ (U : Set X.carrier)
[GOAL]
case h
X✝ Y : Scheme
f✝ : X✝ ⟶ Y
X : Scheme
U : Opens ↑↑X.toPresheafedSpace
hU : IsCompact ↑U
f : ↑(X.presheaf.obj (op U))
s : Set ↑(Scheme.affineOpens X)
hs : Set.Finite s
e : ↑U = ⋃ (i : ↑(Scheme.affineOpens X)) (_ : i ∈ s), ↑↑i
V : ↑s
⊢ ↑↑↑V ⊆ ↑U
[PROOFSTEP]
rw [e]
[GOAL]
case h
X✝ Y : Scheme
f✝ : X✝ ⟶ Y
X : Scheme
U : Opens ↑↑X.toPresheafedSpace
hU : IsCompact ↑U
f : ↑(X.presheaf.obj (op U))
s : Set ↑(Scheme.affineOpens X)
hs : Set.Finite s
e : ↑U = ⋃ (i : ↑(Scheme.affineOpens X)) (_ : i ∈ s), ↑↑i
V : ↑s
⊢ ↑↑↑V ⊆ ⋃ (i : ↑(Scheme.affineOpens X)) (_ : i ∈ s), ↑↑i
[PROOFSTEP]
convert @Set.subset_iUnion₂ _ _ _ (fun (U : X.affineOpens) (_ : U ∈ s) => ↑U) V V.prop using 1
[GOAL]
case property
X✝ Y : Scheme
f✝ : X✝ ⟶ Y
X : Scheme
U : Opens ↑↑X.toPresheafedSpace
hU : IsCompact ↑U
f : ↑(X.presheaf.obj (op U))
s : Set ↑(Scheme.affineOpens X)
hs : Set.Finite s
e : ↑U = ⋃ (i : ↑(Scheme.affineOpens X)) (_ : i ∈ s), ↑↑i
V : ↑s
this : ↑↑V ⟶ U
⊢ ↑↑V ⊓ Scheme.basicOpen X f ∈ Scheme.affineOpens X
[PROOFSTEP]
erw [← X.toLocallyRingedSpace.toRingedSpace.basicOpen_res this.op]
[GOAL]
case property
X✝ Y : Scheme
f✝ : X✝ ⟶ Y
X : Scheme
U : Opens ↑↑X.toPresheafedSpace
hU : IsCompact ↑U
f : ↑(X.presheaf.obj (op U))
s : Set ↑(Scheme.affineOpens X)
hs : Set.Finite s
e : ↑U = ⋃ (i : ↑(Scheme.affineOpens X)) (_ : i ∈ s), ↑↑i
V : ↑s
this : ↑↑V ⟶ U
⊢ RingedSpace.basicOpen (LocallyRingedSpace.toRingedSpace X.toLocallyRingedSpace)
      (↑((LocallyRingedSpace.toRingedSpace X.toLocallyRingedSpace).toPresheafedSpace.presheaf.map this.op) f) ∈
    Scheme.affineOpens X
[PROOFSTEP]
exact IsAffineOpen.basicOpenIsAffine V.1.prop _
[GOAL]
case intro.intro
X✝ Y : Scheme
f✝ : X✝ ⟶ Y
X : Scheme
U : Opens ↑↑X.toPresheafedSpace
hU : IsCompact ↑U
f : ↑(X.presheaf.obj (op U))
s : Set ↑(Scheme.affineOpens X)
hs : Set.Finite s
e : ↑U = ⋃ (i : ↑(Scheme.affineOpens X)) (_ : i ∈ s), ↑↑i
g : ↑s → ↑(Scheme.affineOpens X) :=
  fun V => { val := ↑↑V ⊓ Scheme.basicOpen X f, property := (_ : ↑↑V ⊓ Scheme.basicOpen X f ∈ Scheme.affineOpens X) }
⊢ ∃ s, Set.Finite s ∧ ↑(Scheme.basicOpen X f) = ⋃ (i : ↑(Scheme.affineOpens X)) (_ : i ∈ s), ↑↑i
[PROOFSTEP]
haveI : Finite s := hs.to_subtype
[GOAL]
case intro.intro
X✝ Y : Scheme
f✝ : X✝ ⟶ Y
X : Scheme
U : Opens ↑↑X.toPresheafedSpace
hU : IsCompact ↑U
f : ↑(X.presheaf.obj (op U))
s : Set ↑(Scheme.affineOpens X)
hs : Set.Finite s
e : ↑U = ⋃ (i : ↑(Scheme.affineOpens X)) (_ : i ∈ s), ↑↑i
g : ↑s → ↑(Scheme.affineOpens X) :=
  fun V => { val := ↑↑V ⊓ Scheme.basicOpen X f, property := (_ : ↑↑V ⊓ Scheme.basicOpen X f ∈ Scheme.affineOpens X) }
this : Finite ↑s
⊢ ∃ s, Set.Finite s ∧ ↑(Scheme.basicOpen X f) = ⋃ (i : ↑(Scheme.affineOpens X)) (_ : i ∈ s), ↑↑i
[PROOFSTEP]
refine' ⟨Set.range g, Set.finite_range g, _⟩
[GOAL]
case intro.intro
X✝ Y : Scheme
f✝ : X✝ ⟶ Y
X : Scheme
U : Opens ↑↑X.toPresheafedSpace
hU : IsCompact ↑U
f : ↑(X.presheaf.obj (op U))
s : Set ↑(Scheme.affineOpens X)
hs : Set.Finite s
e : ↑U = ⋃ (i : ↑(Scheme.affineOpens X)) (_ : i ∈ s), ↑↑i
g : ↑s → ↑(Scheme.affineOpens X) :=
  fun V => { val := ↑↑V ⊓ Scheme.basicOpen X f, property := (_ : ↑↑V ⊓ Scheme.basicOpen X f ∈ Scheme.affineOpens X) }
this : Finite ↑s
⊢ ↑(Scheme.basicOpen X f) = ⋃ (i : ↑(Scheme.affineOpens X)) (_ : i ∈ Set.range g), ↑↑i
[PROOFSTEP]
refine' (Set.inter_eq_right_iff_subset.mpr (SetLike.coe_subset_coe.2 <| RingedSpace.basicOpen_le _ _)).symm.trans _
[GOAL]
case intro.intro
X✝ Y : Scheme
f✝ : X✝ ⟶ Y
X : Scheme
U : Opens ↑↑X.toPresheafedSpace
hU : IsCompact ↑U
f : ↑(X.presheaf.obj (op U))
s : Set ↑(Scheme.affineOpens X)
hs : Set.Finite s
e : ↑U = ⋃ (i : ↑(Scheme.affineOpens X)) (_ : i ∈ s), ↑↑i
g : ↑s → ↑(Scheme.affineOpens X) :=
  fun V => { val := ↑↑V ⊓ Scheme.basicOpen X f, property := (_ : ↑↑V ⊓ Scheme.basicOpen X f ∈ Scheme.affineOpens X) }
this : Finite ↑s
⊢ ↑U ∩ ↑(RingedSpace.basicOpen (LocallyRingedSpace.toRingedSpace X.toLocallyRingedSpace) f) =
    ⋃ (i : ↑(Scheme.affineOpens X)) (_ : i ∈ Set.range g), ↑↑i
[PROOFSTEP]
rw [e, Set.iUnion₂_inter]
[GOAL]
case intro.intro
X✝ Y : Scheme
f✝ : X✝ ⟶ Y
X : Scheme
U : Opens ↑↑X.toPresheafedSpace
hU : IsCompact ↑U
f : ↑(X.presheaf.obj (op U))
s : Set ↑(Scheme.affineOpens X)
hs : Set.Finite s
e : ↑U = ⋃ (i : ↑(Scheme.affineOpens X)) (_ : i ∈ s), ↑↑i
g : ↑s → ↑(Scheme.affineOpens X) :=
  fun V => { val := ↑↑V ⊓ Scheme.basicOpen X f, property := (_ : ↑↑V ⊓ Scheme.basicOpen X f ∈ Scheme.affineOpens X) }
this : Finite ↑s
⊢ ⋃ (i : ↑(Scheme.affineOpens X)) (_ : i ∈ s),
      ↑↑i ∩ ↑(RingedSpace.basicOpen (LocallyRingedSpace.toRingedSpace X.toLocallyRingedSpace) f) =
    ⋃ (i : ↑(Scheme.affineOpens X)) (_ : i ∈ Set.range g), ↑↑i
[PROOFSTEP]
apply le_antisymm
[GOAL]
case intro.intro.a
X✝ Y : Scheme
f✝ : X✝ ⟶ Y
X : Scheme
U : Opens ↑↑X.toPresheafedSpace
hU : IsCompact ↑U
f : ↑(X.presheaf.obj (op U))
s : Set ↑(Scheme.affineOpens X)
hs : Set.Finite s
e : ↑U = ⋃ (i : ↑(Scheme.affineOpens X)) (_ : i ∈ s), ↑↑i
g : ↑s → ↑(Scheme.affineOpens X) :=
  fun V => { val := ↑↑V ⊓ Scheme.basicOpen X f, property := (_ : ↑↑V ⊓ Scheme.basicOpen X f ∈ Scheme.affineOpens X) }
this : Finite ↑s
⊢ ⋃ (i : ↑(Scheme.affineOpens X)) (_ : i ∈ s),
      ↑↑i ∩ ↑(RingedSpace.basicOpen (LocallyRingedSpace.toRingedSpace X.toLocallyRingedSpace) f) ≤
    ⋃ (i : ↑(Scheme.affineOpens X)) (_ : i ∈ Set.range g), ↑↑i
[PROOFSTEP]
apply Set.iUnion₂_subset
[GOAL]
case intro.intro.a
X✝ Y : Scheme
f✝ : X✝ ⟶ Y
X : Scheme
U : Opens ↑↑X.toPresheafedSpace
hU : IsCompact ↑U
f : ↑(X.presheaf.obj (op U))
s : Set ↑(Scheme.affineOpens X)
hs : Set.Finite s
e : ↑U = ⋃ (i : ↑(Scheme.affineOpens X)) (_ : i ∈ s), ↑↑i
g : ↑s → ↑(Scheme.affineOpens X) :=
  fun V => { val := ↑↑V ⊓ Scheme.basicOpen X f, property := (_ : ↑↑V ⊓ Scheme.basicOpen X f ∈ Scheme.affineOpens X) }
this : Finite ↑s
⊢ ⋃ (i : ↑(Scheme.affineOpens X)) (_ : i ∈ Set.range g), ↑↑i ≤
    ⋃ (i : ↑(Scheme.affineOpens X)) (_ : i ∈ s),
      ↑↑i ∩ ↑(RingedSpace.basicOpen (LocallyRingedSpace.toRingedSpace X.toLocallyRingedSpace) f)
[PROOFSTEP]
apply Set.iUnion₂_subset
[GOAL]
case intro.intro.a.h
X✝ Y : Scheme
f✝ : X✝ ⟶ Y
X : Scheme
U : Opens ↑↑X.toPresheafedSpace
hU : IsCompact ↑U
f : ↑(X.presheaf.obj (op U))
s : Set ↑(Scheme.affineOpens X)
hs : Set.Finite s
e : ↑U = ⋃ (i : ↑(Scheme.affineOpens X)) (_ : i ∈ s), ↑↑i
g : ↑s → ↑(Scheme.affineOpens X) :=
  fun V => { val := ↑↑V ⊓ Scheme.basicOpen X f, property := (_ : ↑↑V ⊓ Scheme.basicOpen X f ∈ Scheme.affineOpens X) }
this : Finite ↑s
⊢ ∀ (i : ↑(Scheme.affineOpens X)),
    i ∈ s →
      ↑↑i ∩ ↑(RingedSpace.basicOpen (LocallyRingedSpace.toRingedSpace X.toLocallyRingedSpace) f) ⊆
        ⋃ (i : ↑(Scheme.affineOpens X)) (_ : i ∈ Set.range g), ↑↑i
[PROOFSTEP]
intro i hi
[GOAL]
case intro.intro.a.h
X✝ Y : Scheme
f✝ : X✝ ⟶ Y
X : Scheme
U : Opens ↑↑X.toPresheafedSpace
hU : IsCompact ↑U
f : ↑(X.presheaf.obj (op U))
s : Set ↑(Scheme.affineOpens X)
hs : Set.Finite s
e : ↑U = ⋃ (i : ↑(Scheme.affineOpens X)) (_ : i ∈ s), ↑↑i
g : ↑s → ↑(Scheme.affineOpens X) :=
  fun V => { val := ↑↑V ⊓ Scheme.basicOpen X f, property := (_ : ↑↑V ⊓ Scheme.basicOpen X f ∈ Scheme.affineOpens X) }
this : Finite ↑s
i : ↑(Scheme.affineOpens X)
hi : i ∈ s
⊢ ↑↑i ∩ ↑(RingedSpace.basicOpen (LocallyRingedSpace.toRingedSpace X.toLocallyRingedSpace) f) ⊆
    ⋃ (i : ↑(Scheme.affineOpens X)) (_ : i ∈ Set.range g), ↑↑i
[PROOFSTEP]
exact
  Set.Subset.trans (Set.Subset.rfl : _ ≤ g ⟨i, hi⟩)
    (@Set.subset_iUnion₂ _ _ _ (fun (i : Scheme.affineOpens X) (_ : i ∈ Set.range g) => (i : Set X.toPresheafedSpace)) _
      (Set.mem_range_self ⟨i, hi⟩))
[GOAL]
case intro.intro.a.h
X✝ Y : Scheme
f✝ : X✝ ⟶ Y
X : Scheme
U : Opens ↑↑X.toPresheafedSpace
hU : IsCompact ↑U
f : ↑(X.presheaf.obj (op U))
s : Set ↑(Scheme.affineOpens X)
hs : Set.Finite s
e : ↑U = ⋃ (i : ↑(Scheme.affineOpens X)) (_ : i ∈ s), ↑↑i
g : ↑s → ↑(Scheme.affineOpens X) :=
  fun V => { val := ↑↑V ⊓ Scheme.basicOpen X f, property := (_ : ↑↑V ⊓ Scheme.basicOpen X f ∈ Scheme.affineOpens X) }
this : Finite ↑s
⊢ ∀ (i : ↑(Scheme.affineOpens X)),
    i ∈ Set.range g →
      ↑↑i ⊆
        ⋃ (i : ↑(Scheme.affineOpens X)) (_ : i ∈ s),
          ↑↑i ∩ ↑(RingedSpace.basicOpen (LocallyRingedSpace.toRingedSpace X.toLocallyRingedSpace) f)
[PROOFSTEP]
rintro ⟨i, hi⟩ ⟨⟨j, hj⟩, hj'⟩
[GOAL]
case intro.intro.a.h.mk.intro.mk
X✝ Y : Scheme
f✝ : X✝ ⟶ Y
X : Scheme
U : Opens ↑↑X.toPresheafedSpace
hU : IsCompact ↑U
f : ↑(X.presheaf.obj (op U))
s : Set ↑(Scheme.affineOpens X)
hs : Set.Finite s
e : ↑U = ⋃ (i : ↑(Scheme.affineOpens X)) (_ : i ∈ s), ↑↑i
g : ↑s → ↑(Scheme.affineOpens X) :=
  fun V => { val := ↑↑V ⊓ Scheme.basicOpen X f, property := (_ : ↑↑V ⊓ Scheme.basicOpen X f ∈ Scheme.affineOpens X) }
this : Finite ↑s
i : Opens ↑↑X.toPresheafedSpace
hi : i ∈ Scheme.affineOpens X
j : ↑(Scheme.affineOpens X)
hj : j ∈ s
hj' : g { val := j, property := hj } = { val := i, property := hi }
⊢ ↑↑{ val := i, property := hi } ⊆
    ⋃ (i : ↑(Scheme.affineOpens X)) (_ : i ∈ s),
      ↑↑i ∩ ↑(RingedSpace.basicOpen (LocallyRingedSpace.toRingedSpace X.toLocallyRingedSpace) f)
[PROOFSTEP]
rw [← hj']
[GOAL]
case intro.intro.a.h.mk.intro.mk
X✝ Y : Scheme
f✝ : X✝ ⟶ Y
X : Scheme
U : Opens ↑↑X.toPresheafedSpace
hU : IsCompact ↑U
f : ↑(X.presheaf.obj (op U))
s : Set ↑(Scheme.affineOpens X)
hs : Set.Finite s
e : ↑U = ⋃ (i : ↑(Scheme.affineOpens X)) (_ : i ∈ s), ↑↑i
g : ↑s → ↑(Scheme.affineOpens X) :=
  fun V => { val := ↑↑V ⊓ Scheme.basicOpen X f, property := (_ : ↑↑V ⊓ Scheme.basicOpen X f ∈ Scheme.affineOpens X) }
this : Finite ↑s
i : Opens ↑↑X.toPresheafedSpace
hi : i ∈ Scheme.affineOpens X
j : ↑(Scheme.affineOpens X)
hj : j ∈ s
hj' : g { val := j, property := hj } = { val := i, property := hi }
⊢ ↑↑(g { val := j, property := hj }) ⊆
    ⋃ (i : ↑(Scheme.affineOpens X)) (_ : i ∈ s),
      ↑↑i ∩ ↑(RingedSpace.basicOpen (LocallyRingedSpace.toRingedSpace X.toLocallyRingedSpace) f)
[PROOFSTEP]
refine' Set.Subset.trans _ (Set.subset_iUnion₂ j hj)
[GOAL]
case intro.intro.a.h.mk.intro.mk
X✝ Y : Scheme
f✝ : X✝ ⟶ Y
X : Scheme
U : Opens ↑↑X.toPresheafedSpace
hU : IsCompact ↑U
f : ↑(X.presheaf.obj (op U))
s : Set ↑(Scheme.affineOpens X)
hs : Set.Finite s
e : ↑U = ⋃ (i : ↑(Scheme.affineOpens X)) (_ : i ∈ s), ↑↑i
g : ↑s → ↑(Scheme.affineOpens X) :=
  fun V => { val := ↑↑V ⊓ Scheme.basicOpen X f, property := (_ : ↑↑V ⊓ Scheme.basicOpen X f ∈ Scheme.affineOpens X) }
this : Finite ↑s
i : Opens ↑↑X.toPresheafedSpace
hi : i ∈ Scheme.affineOpens X
j : ↑(Scheme.affineOpens X)
hj : j ∈ s
hj' : g { val := j, property := hj } = { val := i, property := hi }
⊢ ↑↑(g { val := j, property := hj }) ⊆
    ↑↑j ∩ ↑(RingedSpace.basicOpen (LocallyRingedSpace.toRingedSpace X.toLocallyRingedSpace) f)
[PROOFSTEP]
exact Set.Subset.rfl
[GOAL]
X Y : Scheme
f : X ⟶ Y
⊢ AffineTargetMorphismProperty.IsLocal affineProperty
[PROOFSTEP]
constructor
[GOAL]
case RespectsIso
X Y : Scheme
f : X ⟶ Y
⊢ MorphismProperty.RespectsIso (AffineTargetMorphismProperty.toProperty affineProperty)
[PROOFSTEP]
apply AffineTargetMorphismProperty.respectsIso_mk
[GOAL]
case RespectsIso.h₁
X Y : Scheme
f : X ⟶ Y
⊢ ∀ {X Y Z : Scheme} (e : X ≅ Y) (f : Y ⟶ Z) [inst : IsAffine Z], affineProperty f → affineProperty (e.hom ≫ f)
[PROOFSTEP]
rintro X Y Z e _ _ H
[GOAL]
case RespectsIso.h₂
X Y : Scheme
f : X ⟶ Y
⊢ ∀ {X Y Z : Scheme} (e : Y ≅ Z) (f : X ⟶ Y) [h : IsAffine Y], affineProperty f → affineProperty (f ≫ e.hom)
[PROOFSTEP]
rintro X Y Z e _ _ H
[GOAL]
case RespectsIso.h₁
X✝ Y✝ : Scheme
f : X✝ ⟶ Y✝
X Y Z : Scheme
e : X ≅ Y
f✝ : Y ⟶ Z
inst✝ : IsAffine Z
H : affineProperty f✝
⊢ affineProperty (e.hom ≫ f✝)
case RespectsIso.h₂
X✝ Y✝ : Scheme
f : X✝ ⟶ Y✝
X Y Z : Scheme
e : Y ≅ Z
f✝ : X ⟶ Y
h✝ : IsAffine Y
H : affineProperty f✝
⊢ affineProperty (f✝ ≫ e.hom)
[PROOFSTEP]
exacts [@Homeomorph.compactSpace _ _ _ _ H (TopCat.homeoOfIso (asIso e.inv.1.base)), H]
[GOAL]
case toBasicOpen
X Y : Scheme
f : X ⟶ Y
⊢ ∀ {X Y : Scheme} [inst : IsAffine Y] (f : X ⟶ Y) (r : ↑(Y.presheaf.obj (op ⊤))),
    affineProperty f → affineProperty (f ∣_ Scheme.basicOpen Y r)
[PROOFSTEP]
introv H
[GOAL]
case toBasicOpen
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
inst✝ : IsAffine Y
f : X ⟶ Y
r : ↑(Y.presheaf.obj (op ⊤))
H : affineProperty f
⊢ affineProperty (f ∣_ Scheme.basicOpen Y r)
[PROOFSTEP]
dsimp [affineProperty] at H ⊢
[GOAL]
case toBasicOpen
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
inst✝ : IsAffine Y
f : X ⟶ Y
r : ↑(Y.presheaf.obj (op ⊤))
H : CompactSpace ↑↑X.toPresheafedSpace
⊢ CompactSpace ↑((Opens.toTopCat ↑X.toPresheafedSpace).obj ((Opens.map f.val.base).obj (Scheme.basicOpen Y r)))
[PROOFSTEP]
change CompactSpace ((Opens.map f.val.base).obj (Y.basicOpen r))
[GOAL]
case toBasicOpen
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
inst✝ : IsAffine Y
f : X ⟶ Y
r : ↑(Y.presheaf.obj (op ⊤))
H : CompactSpace ↑↑X.toPresheafedSpace
⊢ CompactSpace { x // x ∈ (Opens.map f.val.base).obj (Scheme.basicOpen Y r) }
[PROOFSTEP]
rw [Scheme.preimage_basicOpen f r]
[GOAL]
case toBasicOpen
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
inst✝ : IsAffine Y
f : X ⟶ Y
r : ↑(Y.presheaf.obj (op ⊤))
H : CompactSpace ↑↑X.toPresheafedSpace
⊢ CompactSpace { x // x ∈ Scheme.basicOpen X (↑(NatTrans.app f.val.c (op ⊤)) r) }
[PROOFSTEP]
erw [← isCompact_iff_compactSpace]
[GOAL]
case toBasicOpen
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
inst✝ : IsAffine Y
f : X ⟶ Y
r : ↑(Y.presheaf.obj (op ⊤))
H : CompactSpace ↑↑X.toPresheafedSpace
⊢ IsCompact ↑(Scheme.basicOpen X (↑(NatTrans.app f.val.c (op ⊤)) r))
[PROOFSTEP]
rw [← isCompact_univ_iff] at H
[GOAL]
case toBasicOpen
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
inst✝ : IsAffine Y
f : X ⟶ Y
r : ↑(Y.presheaf.obj (op ⊤))
H : IsCompact Set.univ
⊢ IsCompact ↑(Scheme.basicOpen X (↑(NatTrans.app f.val.c (op ⊤)) r))
[PROOFSTEP]
apply isCompact_basicOpen
[GOAL]
case toBasicOpen.hU
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
inst✝ : IsAffine Y
f : X ⟶ Y
r : ↑(Y.presheaf.obj (op ⊤))
H : IsCompact Set.univ
⊢ IsCompact ↑((Opens.map f.val.base).obj ⊤)
[PROOFSTEP]
exact H
[GOAL]
case ofBasicOpenCover
X Y : Scheme
f : X ⟶ Y
⊢ ∀ {X Y : Scheme} [inst : IsAffine Y] (f : X ⟶ Y) (s : Finset ↑(Y.presheaf.obj (op ⊤))),
    Ideal.span ↑s = ⊤ → (∀ (r : { x // x ∈ s }), affineProperty (f ∣_ Scheme.basicOpen Y ↑r)) → affineProperty f
[PROOFSTEP]
rintro X Y H f S hS hS'
[GOAL]
case ofBasicOpenCover
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
H : IsAffine Y
f : X ⟶ Y
S : Finset ↑(Y.presheaf.obj (op ⊤))
hS : Ideal.span ↑S = ⊤
hS' : ∀ (r : { x // x ∈ S }), affineProperty (f ∣_ Scheme.basicOpen Y ↑r)
⊢ affineProperty f
[PROOFSTEP]
rw [← IsAffineOpen.basicOpen_union_eq_self_iff] at hS
[GOAL]
case ofBasicOpenCover
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
H : IsAffine Y
f : X ⟶ Y
S : Finset ↑(Y.presheaf.obj (op ⊤))
hS : ⨆ (f : ↑↑S), Scheme.basicOpen Y ↑f = ⊤
hS' : ∀ (r : { x // x ∈ S }), affineProperty (f ∣_ Scheme.basicOpen Y ↑r)
⊢ affineProperty f
case ofBasicOpenCover.hU
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
H : IsAffine Y
f : X ⟶ Y
S : Finset ↑(Y.presheaf.obj (op ⊤))
hS : Ideal.span ↑S = ⊤
hS' : ∀ (r : { x // x ∈ S }), affineProperty (f ∣_ Scheme.basicOpen Y ↑r)
⊢ IsAffineOpen ⊤
[PROOFSTEP]
delta QuasiCompact.affineProperty
[GOAL]
case ofBasicOpenCover
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
H : IsAffine Y
f : X ⟶ Y
S : Finset ↑(Y.presheaf.obj (op ⊤))
hS : ⨆ (f : ↑↑S), Scheme.basicOpen Y ↑f = ⊤
hS' : ∀ (r : { x // x ∈ S }), affineProperty (f ∣_ Scheme.basicOpen Y ↑r)
⊢ CompactSpace ↑↑X.toPresheafedSpace
case ofBasicOpenCover.hU
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
H : IsAffine Y
f : X ⟶ Y
S : Finset ↑(Y.presheaf.obj (op ⊤))
hS : Ideal.span ↑S = ⊤
hS' : ∀ (r : { x // x ∈ S }), affineProperty (f ∣_ Scheme.basicOpen Y ↑r)
⊢ IsAffineOpen ⊤
[PROOFSTEP]
rw [← isCompact_univ_iff]
[GOAL]
case ofBasicOpenCover
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
H : IsAffine Y
f : X ⟶ Y
S : Finset ↑(Y.presheaf.obj (op ⊤))
hS : ⨆ (f : ↑↑S), Scheme.basicOpen Y ↑f = ⊤
hS' : ∀ (r : { x // x ∈ S }), affineProperty (f ∣_ Scheme.basicOpen Y ↑r)
⊢ IsCompact Set.univ
case ofBasicOpenCover.hU
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
H : IsAffine Y
f : X ⟶ Y
S : Finset ↑(Y.presheaf.obj (op ⊤))
hS : Ideal.span ↑S = ⊤
hS' : ∀ (r : { x // x ∈ S }), affineProperty (f ∣_ Scheme.basicOpen Y ↑r)
⊢ IsAffineOpen ⊤
[PROOFSTEP]
change IsCompact ((Opens.map f.val.base).obj ⊤).1
[GOAL]
case ofBasicOpenCover
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
H : IsAffine Y
f : X ⟶ Y
S : Finset ↑(Y.presheaf.obj (op ⊤))
hS : ⨆ (f : ↑↑S), Scheme.basicOpen Y ↑f = ⊤
hS' : ∀ (r : { x // x ∈ S }), affineProperty (f ∣_ Scheme.basicOpen Y ↑r)
⊢ IsCompact ((Opens.map f.val.base).obj ⊤).carrier
case ofBasicOpenCover.hU
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
H : IsAffine Y
f : X ⟶ Y
S : Finset ↑(Y.presheaf.obj (op ⊤))
hS : Ideal.span ↑S = ⊤
hS' : ∀ (r : { x // x ∈ S }), affineProperty (f ∣_ Scheme.basicOpen Y ↑r)
⊢ IsAffineOpen ⊤
[PROOFSTEP]
rw [← hS]
[GOAL]
case ofBasicOpenCover
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
H : IsAffine Y
f : X ⟶ Y
S : Finset ↑(Y.presheaf.obj (op ⊤))
hS : ⨆ (f : ↑↑S), Scheme.basicOpen Y ↑f = ⊤
hS' : ∀ (r : { x // x ∈ S }), affineProperty (f ∣_ Scheme.basicOpen Y ↑r)
⊢ IsCompact ((Opens.map f.val.base).obj (⨆ (f : ↑↑S), Scheme.basicOpen Y ↑f)).carrier
case ofBasicOpenCover.hU
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
H : IsAffine Y
f : X ⟶ Y
S : Finset ↑(Y.presheaf.obj (op ⊤))
hS : Ideal.span ↑S = ⊤
hS' : ∀ (r : { x // x ∈ S }), affineProperty (f ∣_ Scheme.basicOpen Y ↑r)
⊢ IsAffineOpen ⊤
[PROOFSTEP]
dsimp [Opens.map]
[GOAL]
case ofBasicOpenCover
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
H : IsAffine Y
f : X ⟶ Y
S : Finset ↑(Y.presheaf.obj (op ⊤))
hS : ⨆ (f : ↑↑S), Scheme.basicOpen Y ↑f = ⊤
hS' : ∀ (r : { x // x ∈ S }), affineProperty (f ∣_ Scheme.basicOpen Y ↑r)
⊢ IsCompact (↑f.val.base ⁻¹' ↑(⨆ (f : { x // x ∈ S }), Scheme.basicOpen Y ↑f))
case ofBasicOpenCover.hU
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
H : IsAffine Y
f : X ⟶ Y
S : Finset ↑(Y.presheaf.obj (op ⊤))
hS : Ideal.span ↑S = ⊤
hS' : ∀ (r : { x // x ∈ S }), affineProperty (f ∣_ Scheme.basicOpen Y ↑r)
⊢ IsAffineOpen ⊤
[PROOFSTEP]
simp only [Opens.iSup_mk, Opens.carrier_eq_coe, Opens.coe_mk, Set.preimage_iUnion]
[GOAL]
case ofBasicOpenCover
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
H : IsAffine Y
f : X ⟶ Y
S : Finset ↑(Y.presheaf.obj (op ⊤))
hS : ⨆ (f : ↑↑S), Scheme.basicOpen Y ↑f = ⊤
hS' : ∀ (r : { x // x ∈ S }), affineProperty (f ∣_ Scheme.basicOpen Y ↑r)
⊢ IsCompact (⋃ (i : { x // x ∈ S }), ↑f.val.base ⁻¹' ↑(Scheme.basicOpen Y ↑i))
case ofBasicOpenCover.hU
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
H : IsAffine Y
f : X ⟶ Y
S : Finset ↑(Y.presheaf.obj (op ⊤))
hS : Ideal.span ↑S = ⊤
hS' : ∀ (r : { x // x ∈ S }), affineProperty (f ∣_ Scheme.basicOpen Y ↑r)
⊢ IsAffineOpen ⊤
[PROOFSTEP]
exacts [isCompact_iUnion fun i => isCompact_iff_compactSpace.mpr (hS' i), topIsAffineOpen _]
[GOAL]
X Y : Scheme
f : X ⟶ Y
⊢ AffineTargetMorphismProperty.StableUnderBaseChange affineProperty
[PROOFSTEP]
intro X Y S _ _ f g h
[GOAL]
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y S : Scheme
inst✝¹ : IsAffine S
inst✝ : IsAffine X
f : X ⟶ S
g : Y ⟶ S
h : affineProperty g
⊢ affineProperty pullback.fst
[PROOFSTEP]
rw [QuasiCompact.affineProperty] at h ⊢
[GOAL]
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y S : Scheme
inst✝¹ : IsAffine S
inst✝ : IsAffine X
f : X ⟶ S
g : Y ⟶ S
h : CompactSpace ↑↑Y.toPresheafedSpace
⊢ CompactSpace ↑↑(pullback f g).toLocallyRingedSpace.toSheafedSpace.toPresheafedSpace
[PROOFSTEP]
skip
[GOAL]
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y S : Scheme
inst✝¹ : IsAffine S
inst✝ : IsAffine X
f : X ⟶ S
g : Y ⟶ S
h : CompactSpace ↑↑Y.toPresheafedSpace
⊢ CompactSpace ↑↑(pullback f g).toLocallyRingedSpace.toSheafedSpace.toPresheafedSpace
[PROOFSTEP]
let 𝒰 := Scheme.Pullback.openCoverOfRight Y.affineCover.finiteSubcover f g
[GOAL]
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y S : Scheme
inst✝¹ : IsAffine S
inst✝ : IsAffine X
f : X ⟶ S
g : Y ⟶ S
h : CompactSpace ↑↑Y.toPresheafedSpace
𝒰 : Scheme.OpenCover (pullback f g) :=
  Scheme.Pullback.openCoverOfRight (Scheme.OpenCover.finiteSubcover (Scheme.affineCover Y)) f g
⊢ CompactSpace ↑↑(pullback f g).toLocallyRingedSpace.toSheafedSpace.toPresheafedSpace
[PROOFSTEP]
have : Finite 𝒰.J := by dsimp; infer_instance
[GOAL]
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y S : Scheme
inst✝¹ : IsAffine S
inst✝ : IsAffine X
f : X ⟶ S
g : Y ⟶ S
h : CompactSpace ↑↑Y.toPresheafedSpace
𝒰 : Scheme.OpenCover (pullback f g) :=
  Scheme.Pullback.openCoverOfRight (Scheme.OpenCover.finiteSubcover (Scheme.affineCover Y)) f g
⊢ Finite 𝒰.J
[PROOFSTEP]
dsimp
[GOAL]
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y S : Scheme
inst✝¹ : IsAffine S
inst✝ : IsAffine X
f : X ⟶ S
g : Y ⟶ S
h : CompactSpace ↑↑Y.toPresheafedSpace
𝒰 : Scheme.OpenCover (pullback f g) :=
  Scheme.Pullback.openCoverOfRight (Scheme.OpenCover.finiteSubcover (Scheme.affineCover Y)) f g
⊢ Finite (Scheme.OpenCover.finiteSubcover (Scheme.affineCover Y)).J
[PROOFSTEP]
infer_instance
[GOAL]
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y S : Scheme
inst✝¹ : IsAffine S
inst✝ : IsAffine X
f : X ⟶ S
g : Y ⟶ S
h : CompactSpace ↑↑Y.toPresheafedSpace
𝒰 : Scheme.OpenCover (pullback f g) :=
  Scheme.Pullback.openCoverOfRight (Scheme.OpenCover.finiteSubcover (Scheme.affineCover Y)) f g
this : Finite 𝒰.J
⊢ CompactSpace ↑↑(pullback f g).toLocallyRingedSpace.toSheafedSpace.toPresheafedSpace
[PROOFSTEP]
have : ∀ i, CompactSpace (𝒰.obj i).carrier := by intro i; dsimp; infer_instance
[GOAL]
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y S : Scheme
inst✝¹ : IsAffine S
inst✝ : IsAffine X
f : X ⟶ S
g : Y ⟶ S
h : CompactSpace ↑↑Y.toPresheafedSpace
𝒰 : Scheme.OpenCover (pullback f g) :=
  Scheme.Pullback.openCoverOfRight (Scheme.OpenCover.finiteSubcover (Scheme.affineCover Y)) f g
this : Finite 𝒰.J
⊢ ∀ (i : 𝒰.J), CompactSpace ↑↑(Scheme.OpenCover.obj 𝒰 i).toPresheafedSpace
[PROOFSTEP]
intro i
[GOAL]
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y S : Scheme
inst✝¹ : IsAffine S
inst✝ : IsAffine X
f : X ⟶ S
g : Y ⟶ S
h : CompactSpace ↑↑Y.toPresheafedSpace
𝒰 : Scheme.OpenCover (pullback f g) :=
  Scheme.Pullback.openCoverOfRight (Scheme.OpenCover.finiteSubcover (Scheme.affineCover Y)) f g
this : Finite 𝒰.J
i : 𝒰.J
⊢ CompactSpace ↑↑(Scheme.OpenCover.obj 𝒰 i).toPresheafedSpace
[PROOFSTEP]
dsimp
[GOAL]
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y S : Scheme
inst✝¹ : IsAffine S
inst✝ : IsAffine X
f : X ⟶ S
g : Y ⟶ S
h : CompactSpace ↑↑Y.toPresheafedSpace
𝒰 : Scheme.OpenCover (pullback f g) :=
  Scheme.Pullback.openCoverOfRight (Scheme.OpenCover.finiteSubcover (Scheme.affineCover Y)) f g
this : Finite 𝒰.J
i : 𝒰.J
⊢ CompactSpace
    ↑↑(pullback f
                (Scheme.OpenCover.map (Scheme.affineCover Y) (Scheme.OpenCover.f (Scheme.affineCover Y) ↑i) ≫
                  g)).toLocallyRingedSpace.toSheafedSpace.toPresheafedSpace
[PROOFSTEP]
infer_instance
[GOAL]
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y S : Scheme
inst✝¹ : IsAffine S
inst✝ : IsAffine X
f : X ⟶ S
g : Y ⟶ S
h : CompactSpace ↑↑Y.toPresheafedSpace
𝒰 : Scheme.OpenCover (pullback f g) :=
  Scheme.Pullback.openCoverOfRight (Scheme.OpenCover.finiteSubcover (Scheme.affineCover Y)) f g
this✝ : Finite 𝒰.J
this : ∀ (i : 𝒰.J), CompactSpace ↑↑(Scheme.OpenCover.obj 𝒰 i).toPresheafedSpace
⊢ CompactSpace ↑↑(pullback f g).toLocallyRingedSpace.toSheafedSpace.toPresheafedSpace
[PROOFSTEP]
exact 𝒰.compactSpace
[GOAL]
X Y : Scheme
f : X ⟶ Y
Z : Scheme
P : Opens ↑↑X.toPresheafedSpace → Prop
S : Opens ↑↑X.toPresheafedSpace
hS : IsCompact S.carrier
h₁ : P ⊥
h₂ : ∀ (S : Opens ↑↑X.toPresheafedSpace), IsCompact S.carrier → ∀ (U : ↑(Scheme.affineOpens X)), P S → P (S ⊔ ↑U)
⊢ P S
[PROOFSTEP]
classical
obtain ⟨s, hs, hs'⟩ := (isCompact_open_iff_eq_finset_affine_union S.1).mp ⟨hS, S.2⟩
replace hs' : S = iSup fun i : s => (i : Opens X.carrier) := by ext1; simpa using hs'
subst hs'
apply @Set.Finite.induction_on _ _ _ hs
· convert h₁; rw [iSup_eq_bot]; rintro ⟨_, h⟩; exact h.elim
· intro x s _ hs h₄
  have : IsCompact (⨆ i : s, (i : Opens X.carrier)).1 := by
    refine' ((isCompact_open_iff_eq_finset_affine_union _).mpr _).1; exact ⟨s, hs, by simp⟩
  convert h₂ _ this x h₄
  rw [iSup_subtype, sup_comm]
  conv_rhs => rw [iSup_subtype]
  exact iSup_insert
[GOAL]
X Y : Scheme
f : X ⟶ Y
Z : Scheme
P : Opens ↑↑X.toPresheafedSpace → Prop
S : Opens ↑↑X.toPresheafedSpace
hS : IsCompact S.carrier
h₁ : P ⊥
h₂ : ∀ (S : Opens ↑↑X.toPresheafedSpace), IsCompact S.carrier → ∀ (U : ↑(Scheme.affineOpens X)), P S → P (S ⊔ ↑U)
⊢ P S
[PROOFSTEP]
obtain ⟨s, hs, hs'⟩ := (isCompact_open_iff_eq_finset_affine_union S.1).mp ⟨hS, S.2⟩
[GOAL]
case intro.intro
X Y : Scheme
f : X ⟶ Y
Z : Scheme
P : Opens ↑↑X.toPresheafedSpace → Prop
S : Opens ↑↑X.toPresheafedSpace
hS : IsCompact S.carrier
h₁ : P ⊥
h₂ : ∀ (S : Opens ↑↑X.toPresheafedSpace), IsCompact S.carrier → ∀ (U : ↑(Scheme.affineOpens X)), P S → P (S ⊔ ↑U)
s : Set ↑(Scheme.affineOpens X)
hs : Set.Finite s
hs' : S.carrier = ⋃ (i : ↑(Scheme.affineOpens X)) (_ : i ∈ s), ↑↑i
⊢ P S
[PROOFSTEP]
replace hs' : S = iSup fun i : s => (i : Opens X.carrier) := by ext1; simpa using hs'
[GOAL]
X Y : Scheme
f : X ⟶ Y
Z : Scheme
P : Opens ↑↑X.toPresheafedSpace → Prop
S : Opens ↑↑X.toPresheafedSpace
hS : IsCompact S.carrier
h₁ : P ⊥
h₂ : ∀ (S : Opens ↑↑X.toPresheafedSpace), IsCompact S.carrier → ∀ (U : ↑(Scheme.affineOpens X)), P S → P (S ⊔ ↑U)
s : Set ↑(Scheme.affineOpens X)
hs : Set.Finite s
hs' : S.carrier = ⋃ (i : ↑(Scheme.affineOpens X)) (_ : i ∈ s), ↑↑i
⊢ S = ⨆ (i : ↑s), ↑↑i
[PROOFSTEP]
ext1
[GOAL]
case h
X Y : Scheme
f : X ⟶ Y
Z : Scheme
P : Opens ↑↑X.toPresheafedSpace → Prop
S : Opens ↑↑X.toPresheafedSpace
hS : IsCompact S.carrier
h₁ : P ⊥
h₂ : ∀ (S : Opens ↑↑X.toPresheafedSpace), IsCompact S.carrier → ∀ (U : ↑(Scheme.affineOpens X)), P S → P (S ⊔ ↑U)
s : Set ↑(Scheme.affineOpens X)
hs : Set.Finite s
hs' : S.carrier = ⋃ (i : ↑(Scheme.affineOpens X)) (_ : i ∈ s), ↑↑i
⊢ ↑S = ↑(⨆ (i : ↑s), ↑↑i)
[PROOFSTEP]
simpa using hs'
[GOAL]
case intro.intro
X Y : Scheme
f : X ⟶ Y
Z : Scheme
P : Opens ↑↑X.toPresheafedSpace → Prop
S : Opens ↑↑X.toPresheafedSpace
hS : IsCompact S.carrier
h₁ : P ⊥
h₂ : ∀ (S : Opens ↑↑X.toPresheafedSpace), IsCompact S.carrier → ∀ (U : ↑(Scheme.affineOpens X)), P S → P (S ⊔ ↑U)
s : Set ↑(Scheme.affineOpens X)
hs : Set.Finite s
hs' : S = ⨆ (i : ↑s), ↑↑i
⊢ P S
[PROOFSTEP]
subst hs'
[GOAL]
case intro.intro
X Y : Scheme
f : X ⟶ Y
Z : Scheme
P : Opens ↑↑X.toPresheafedSpace → Prop
h₁ : P ⊥
h₂ : ∀ (S : Opens ↑↑X.toPresheafedSpace), IsCompact S.carrier → ∀ (U : ↑(Scheme.affineOpens X)), P S → P (S ⊔ ↑U)
s : Set ↑(Scheme.affineOpens X)
hs : Set.Finite s
hS : IsCompact (⨆ (i : ↑s), ↑↑i).carrier
⊢ P (⨆ (i : ↑s), ↑↑i)
[PROOFSTEP]
apply @Set.Finite.induction_on _ _ _ hs
[GOAL]
case intro.intro.H0
X Y : Scheme
f : X ⟶ Y
Z : Scheme
P : Opens ↑↑X.toPresheafedSpace → Prop
h₁ : P ⊥
h₂ : ∀ (S : Opens ↑↑X.toPresheafedSpace), IsCompact S.carrier → ∀ (U : ↑(Scheme.affineOpens X)), P S → P (S ⊔ ↑U)
s : Set ↑(Scheme.affineOpens X)
hs : Set.Finite s
hS : IsCompact (⨆ (i : ↑s), ↑↑i).carrier
⊢ P (⨆ (i : ↑∅), ↑↑i)
[PROOFSTEP]
convert h₁
[GOAL]
case h.e'_1
X Y : Scheme
f : X ⟶ Y
Z : Scheme
P : Opens ↑↑X.toPresheafedSpace → Prop
h₁ : P ⊥
h₂ : ∀ (S : Opens ↑↑X.toPresheafedSpace), IsCompact S.carrier → ∀ (U : ↑(Scheme.affineOpens X)), P S → P (S ⊔ ↑U)
s : Set ↑(Scheme.affineOpens X)
hs : Set.Finite s
hS : IsCompact (⨆ (i : ↑s), ↑↑i).carrier
⊢ ⨆ (i : ↑∅), ↑↑i = ⊥
[PROOFSTEP]
rw [iSup_eq_bot]
[GOAL]
case h.e'_1
X Y : Scheme
f : X ⟶ Y
Z : Scheme
P : Opens ↑↑X.toPresheafedSpace → Prop
h₁ : P ⊥
h₂ : ∀ (S : Opens ↑↑X.toPresheafedSpace), IsCompact S.carrier → ∀ (U : ↑(Scheme.affineOpens X)), P S → P (S ⊔ ↑U)
s : Set ↑(Scheme.affineOpens X)
hs : Set.Finite s
hS : IsCompact (⨆ (i : ↑s), ↑↑i).carrier
⊢ ∀ (i : ↑∅), ↑↑i = ⊥
[PROOFSTEP]
rintro ⟨_, h⟩
[GOAL]
case h.e'_1.mk
X Y : Scheme
f : X ⟶ Y
Z : Scheme
P : Opens ↑↑X.toPresheafedSpace → Prop
h₁ : P ⊥
h₂ : ∀ (S : Opens ↑↑X.toPresheafedSpace), IsCompact S.carrier → ∀ (U : ↑(Scheme.affineOpens X)), P S → P (S ⊔ ↑U)
s : Set ↑(Scheme.affineOpens X)
hs : Set.Finite s
hS : IsCompact (⨆ (i : ↑s), ↑↑i).carrier
val✝ : ↑(Scheme.affineOpens X)
h : val✝ ∈ ∅
⊢ ↑↑{ val := val✝, property := h } = ⊥
[PROOFSTEP]
exact h.elim
[GOAL]
case intro.intro.H1
X Y : Scheme
f : X ⟶ Y
Z : Scheme
P : Opens ↑↑X.toPresheafedSpace → Prop
h₁ : P ⊥
h₂ : ∀ (S : Opens ↑↑X.toPresheafedSpace), IsCompact S.carrier → ∀ (U : ↑(Scheme.affineOpens X)), P S → P (S ⊔ ↑U)
s : Set ↑(Scheme.affineOpens X)
hs : Set.Finite s
hS : IsCompact (⨆ (i : ↑s), ↑↑i).carrier
⊢ ∀ {a : ↑(Scheme.affineOpens X)} {s : Set ↑(Scheme.affineOpens X)},
    ¬a ∈ s → Set.Finite s → P (⨆ (i : ↑s), ↑↑i) → P (⨆ (i : ↑(insert a s)), ↑↑i)
[PROOFSTEP]
intro x s _ hs h₄
[GOAL]
case intro.intro.H1
X Y : Scheme
f : X ⟶ Y
Z : Scheme
P : Opens ↑↑X.toPresheafedSpace → Prop
h₁ : P ⊥
h₂ : ∀ (S : Opens ↑↑X.toPresheafedSpace), IsCompact S.carrier → ∀ (U : ↑(Scheme.affineOpens X)), P S → P (S ⊔ ↑U)
s✝ : Set ↑(Scheme.affineOpens X)
hs✝ : Set.Finite s✝
hS : IsCompact (⨆ (i : ↑s✝), ↑↑i).carrier
x : ↑(Scheme.affineOpens X)
s : Set ↑(Scheme.affineOpens X)
a✝ : ¬x ∈ s
hs : Set.Finite s
h₄ : P (⨆ (i : ↑s), ↑↑i)
⊢ P (⨆ (i : ↑(insert x s)), ↑↑i)
[PROOFSTEP]
have : IsCompact (⨆ i : s, (i : Opens X.carrier)).1 := by
  refine' ((isCompact_open_iff_eq_finset_affine_union _).mpr _).1; exact ⟨s, hs, by simp⟩
[GOAL]
X Y : Scheme
f : X ⟶ Y
Z : Scheme
P : Opens ↑↑X.toPresheafedSpace → Prop
h₁ : P ⊥
h₂ : ∀ (S : Opens ↑↑X.toPresheafedSpace), IsCompact S.carrier → ∀ (U : ↑(Scheme.affineOpens X)), P S → P (S ⊔ ↑U)
s✝ : Set ↑(Scheme.affineOpens X)
hs✝ : Set.Finite s✝
hS : IsCompact (⨆ (i : ↑s✝), ↑↑i).carrier
x : ↑(Scheme.affineOpens X)
s : Set ↑(Scheme.affineOpens X)
a✝ : ¬x ∈ s
hs : Set.Finite s
h₄ : P (⨆ (i : ↑s), ↑↑i)
⊢ IsCompact (⨆ (i : ↑s), ↑↑i).carrier
[PROOFSTEP]
refine' ((isCompact_open_iff_eq_finset_affine_union _).mpr _).1
[GOAL]
X Y : Scheme
f : X ⟶ Y
Z : Scheme
P : Opens ↑↑X.toPresheafedSpace → Prop
h₁ : P ⊥
h₂ : ∀ (S : Opens ↑↑X.toPresheafedSpace), IsCompact S.carrier → ∀ (U : ↑(Scheme.affineOpens X)), P S → P (S ⊔ ↑U)
s✝ : Set ↑(Scheme.affineOpens X)
hs✝ : Set.Finite s✝
hS : IsCompact (⨆ (i : ↑s✝), ↑↑i).carrier
x : ↑(Scheme.affineOpens X)
s : Set ↑(Scheme.affineOpens X)
a✝ : ¬x ∈ s
hs : Set.Finite s
h₄ : P (⨆ (i : ↑s), ↑↑i)
⊢ ∃ s_1, Set.Finite s_1 ∧ (⨆ (i : ↑s), ↑↑i).carrier = ⋃ (i : ↑(Scheme.affineOpens X)) (_ : i ∈ s_1), ↑↑i
[PROOFSTEP]
exact ⟨s, hs, by simp⟩
[GOAL]
X Y : Scheme
f : X ⟶ Y
Z : Scheme
P : Opens ↑↑X.toPresheafedSpace → Prop
h₁ : P ⊥
h₂ : ∀ (S : Opens ↑↑X.toPresheafedSpace), IsCompact S.carrier → ∀ (U : ↑(Scheme.affineOpens X)), P S → P (S ⊔ ↑U)
s✝ : Set ↑(Scheme.affineOpens X)
hs✝ : Set.Finite s✝
hS : IsCompact (⨆ (i : ↑s✝), ↑↑i).carrier
x : ↑(Scheme.affineOpens X)
s : Set ↑(Scheme.affineOpens X)
a✝ : ¬x ∈ s
hs : Set.Finite s
h₄ : P (⨆ (i : ↑s), ↑↑i)
⊢ (⨆ (i : ↑s), ↑↑i).carrier = ⋃ (i : ↑(Scheme.affineOpens X)) (_ : i ∈ s), ↑↑i
[PROOFSTEP]
simp
[GOAL]
case intro.intro.H1
X Y : Scheme
f : X ⟶ Y
Z : Scheme
P : Opens ↑↑X.toPresheafedSpace → Prop
h₁ : P ⊥
h₂ : ∀ (S : Opens ↑↑X.toPresheafedSpace), IsCompact S.carrier → ∀ (U : ↑(Scheme.affineOpens X)), P S → P (S ⊔ ↑U)
s✝ : Set ↑(Scheme.affineOpens X)
hs✝ : Set.Finite s✝
hS : IsCompact (⨆ (i : ↑s✝), ↑↑i).carrier
x : ↑(Scheme.affineOpens X)
s : Set ↑(Scheme.affineOpens X)
a✝ : ¬x ∈ s
hs : Set.Finite s
h₄ : P (⨆ (i : ↑s), ↑↑i)
this : IsCompact (⨆ (i : ↑s), ↑↑i).carrier
⊢ P (⨆ (i : ↑(insert x s)), ↑↑i)
[PROOFSTEP]
convert h₂ _ this x h₄
[GOAL]
case h.e'_1
X Y : Scheme
f : X ⟶ Y
Z : Scheme
P : Opens ↑↑X.toPresheafedSpace → Prop
h₁ : P ⊥
h₂ : ∀ (S : Opens ↑↑X.toPresheafedSpace), IsCompact S.carrier → ∀ (U : ↑(Scheme.affineOpens X)), P S → P (S ⊔ ↑U)
s✝ : Set ↑(Scheme.affineOpens X)
hs✝ : Set.Finite s✝
hS : IsCompact (⨆ (i : ↑s✝), ↑↑i).carrier
x : ↑(Scheme.affineOpens X)
s : Set ↑(Scheme.affineOpens X)
a✝ : ¬x ∈ s
hs : Set.Finite s
h₄ : P (⨆ (i : ↑s), ↑↑i)
this : IsCompact (⨆ (i : ↑s), ↑↑i).carrier
⊢ ⨆ (i : ↑(insert x s)), ↑↑i = (⨆ (i : ↑s), ↑↑i) ⊔ ↑x
[PROOFSTEP]
rw [iSup_subtype, sup_comm]
[GOAL]
case h.e'_1
X Y : Scheme
f : X ⟶ Y
Z : Scheme
P : Opens ↑↑X.toPresheafedSpace → Prop
h₁ : P ⊥
h₂ : ∀ (S : Opens ↑↑X.toPresheafedSpace), IsCompact S.carrier → ∀ (U : ↑(Scheme.affineOpens X)), P S → P (S ⊔ ↑U)
s✝ : Set ↑(Scheme.affineOpens X)
hs✝ : Set.Finite s✝
hS : IsCompact (⨆ (i : ↑s✝), ↑↑i).carrier
x : ↑(Scheme.affineOpens X)
s : Set ↑(Scheme.affineOpens X)
a✝ : ¬x ∈ s
hs : Set.Finite s
h₄ : P (⨆ (i : ↑s), ↑↑i)
this : IsCompact (⨆ (i : ↑s), ↑↑i).carrier
⊢ ⨆ (i : ↑(Scheme.affineOpens X)) (h : i ∈ insert x s), ↑↑{ val := i, property := h } = ↑x ⊔ ⨆ (i : ↑s), ↑↑i
[PROOFSTEP]
conv_rhs => rw [iSup_subtype]
[GOAL]
X Y : Scheme
f : X ⟶ Y
Z : Scheme
P : Opens ↑↑X.toPresheafedSpace → Prop
h₁ : P ⊥
h₂ : ∀ (S : Opens ↑↑X.toPresheafedSpace), IsCompact S.carrier → ∀ (U : ↑(Scheme.affineOpens X)), P S → P (S ⊔ ↑U)
s✝ : Set ↑(Scheme.affineOpens X)
hs✝ : Set.Finite s✝
hS : IsCompact (⨆ (i : ↑s✝), ↑↑i).carrier
x : ↑(Scheme.affineOpens X)
s : Set ↑(Scheme.affineOpens X)
a✝ : ¬x ∈ s
hs : Set.Finite s
h₄ : P (⨆ (i : ↑s), ↑↑i)
this : IsCompact (⨆ (i : ↑s), ↑↑i).carrier
| ↑x ⊔ ⨆ (i : ↑s), ↑↑i
[PROOFSTEP]
rw [iSup_subtype]
[GOAL]
X Y : Scheme
f : X ⟶ Y
Z : Scheme
P : Opens ↑↑X.toPresheafedSpace → Prop
h₁ : P ⊥
h₂ : ∀ (S : Opens ↑↑X.toPresheafedSpace), IsCompact S.carrier → ∀ (U : ↑(Scheme.affineOpens X)), P S → P (S ⊔ ↑U)
s✝ : Set ↑(Scheme.affineOpens X)
hs✝ : Set.Finite s✝
hS : IsCompact (⨆ (i : ↑s✝), ↑↑i).carrier
x : ↑(Scheme.affineOpens X)
s : Set ↑(Scheme.affineOpens X)
a✝ : ¬x ∈ s
hs : Set.Finite s
h₄ : P (⨆ (i : ↑s), ↑↑i)
this : IsCompact (⨆ (i : ↑s), ↑↑i).carrier
| ↑x ⊔ ⨆ (i : ↑s), ↑↑i
[PROOFSTEP]
rw [iSup_subtype]
[GOAL]
X Y : Scheme
f : X ⟶ Y
Z : Scheme
P : Opens ↑↑X.toPresheafedSpace → Prop
h₁ : P ⊥
h₂ : ∀ (S : Opens ↑↑X.toPresheafedSpace), IsCompact S.carrier → ∀ (U : ↑(Scheme.affineOpens X)), P S → P (S ⊔ ↑U)
s✝ : Set ↑(Scheme.affineOpens X)
hs✝ : Set.Finite s✝
hS : IsCompact (⨆ (i : ↑s✝), ↑↑i).carrier
x : ↑(Scheme.affineOpens X)
s : Set ↑(Scheme.affineOpens X)
a✝ : ¬x ∈ s
hs : Set.Finite s
h₄ : P (⨆ (i : ↑s), ↑↑i)
this : IsCompact (⨆ (i : ↑s), ↑↑i).carrier
| ↑x ⊔ ⨆ (i : ↑s), ↑↑i
[PROOFSTEP]
rw [iSup_subtype]
[GOAL]
case h.e'_1
X Y : Scheme
f : X ⟶ Y
Z : Scheme
P : Opens ↑↑X.toPresheafedSpace → Prop
h₁ : P ⊥
h₂ : ∀ (S : Opens ↑↑X.toPresheafedSpace), IsCompact S.carrier → ∀ (U : ↑(Scheme.affineOpens X)), P S → P (S ⊔ ↑U)
s✝ : Set ↑(Scheme.affineOpens X)
hs✝ : Set.Finite s✝
hS : IsCompact (⨆ (i : ↑s✝), ↑↑i).carrier
x : ↑(Scheme.affineOpens X)
s : Set ↑(Scheme.affineOpens X)
a✝ : ¬x ∈ s
hs : Set.Finite s
h₄ : P (⨆ (i : ↑s), ↑↑i)
this : IsCompact (⨆ (i : ↑s), ↑↑i).carrier
⊢ ⨆ (i : ↑(Scheme.affineOpens X)) (h : i ∈ insert x s), ↑↑{ val := i, property := h } =
    ↑x ⊔ ⨆ (i : ↑(Scheme.affineOpens X)) (h : i ∈ s), ↑↑{ val := i, property := h }
[PROOFSTEP]
exact iSup_insert
[GOAL]
X✝ Y : Scheme
f✝ : X✝ ⟶ Y
Z : Scheme
X : Scheme
U : Opens ↑↑X.toPresheafedSpace
hU : IsAffineOpen U
x f : ↑(X.presheaf.obj (op U))
H : x |_ Scheme.basicOpen X f = 0
⊢ ∃ n, f ^ n * x = 0
[PROOFSTEP]
rw [← map_zero (X.presheaf.map (homOfLE <| X.basicOpen_le f : X.basicOpen f ⟶ U).op)] at H
[GOAL]
X✝ Y : Scheme
f✝ : X✝ ⟶ Y
Z : Scheme
X : Scheme
U : Opens ↑↑X.toPresheafedSpace
hU : IsAffineOpen U
x f : ↑(X.presheaf.obj (op U))
H : x |_ Scheme.basicOpen X f = ↑(X.presheaf.map (homOfLE (_ : Scheme.basicOpen X f ≤ U)).op) 0
⊢ ∃ n, f ^ n * x = 0
[PROOFSTEP]
obtain ⟨⟨_, n, rfl⟩, e⟩ := (isLocalization_basicOpen hU f).eq_iff_exists'.mp H
[GOAL]
case intro.mk.intro
X✝ Y : Scheme
f✝ : X✝ ⟶ Y
Z : Scheme
X : Scheme
U : Opens ↑↑X.toPresheafedSpace
hU : IsAffineOpen U
x f : ↑(X.presheaf.obj (op U))
H : x |_ Scheme.basicOpen X f = ↑(X.presheaf.map (homOfLE (_ : Scheme.basicOpen X f ≤ U)).op) 0
n : ℕ
e :
  ↑{ val := (fun x x_1 => x ^ x_1) f n,
          property := (_ : ∃ y, (fun x x_1 => x ^ x_1) f y = (fun x x_1 => x ^ x_1) f n) } *
      x =
    ↑{ val := (fun x x_1 => x ^ x_1) f n,
          property := (_ : ∃ y, (fun x x_1 => x ^ x_1) f y = (fun x x_1 => x ^ x_1) f n) } *
      0
⊢ ∃ n, f ^ n * x = 0
[PROOFSTEP]
exact ⟨n, by simpa [mul_comm x] using e⟩
[GOAL]
X✝ Y : Scheme
f✝ : X✝ ⟶ Y
Z : Scheme
X : Scheme
U : Opens ↑↑X.toPresheafedSpace
hU : IsAffineOpen U
x f : ↑(X.presheaf.obj (op U))
H : x |_ Scheme.basicOpen X f = ↑(X.presheaf.map (homOfLE (_ : Scheme.basicOpen X f ≤ U)).op) 0
n : ℕ
e :
  ↑{ val := (fun x x_1 => x ^ x_1) f n,
          property := (_ : ∃ y, (fun x x_1 => x ^ x_1) f y = (fun x x_1 => x ^ x_1) f n) } *
      x =
    ↑{ val := (fun x x_1 => x ^ x_1) f n,
          property := (_ : ∃ y, (fun x x_1 => x ^ x_1) f y = (fun x x_1 => x ^ x_1) f n) } *
      0
⊢ f ^ n * x = 0
[PROOFSTEP]
simpa [mul_comm x] using e
[GOAL]
X✝ Y : Scheme
f✝ : X✝ ⟶ Y
Z X : Scheme
U : Opens ↑↑X.toPresheafedSpace
hU : IsCompact U.carrier
x f : ↑(X.presheaf.obj (op U))
H : x |_ Scheme.basicOpen X f = 0
⊢ ∃ n, f ^ n * x = 0
[PROOFSTEP]
obtain ⟨s, hs, e⟩ := (isCompact_open_iff_eq_finset_affine_union U.1).mp ⟨hU, U.2⟩
[GOAL]
case intro.intro
X✝ Y : Scheme
f✝ : X✝ ⟶ Y
Z X : Scheme
U : Opens ↑↑X.toPresheafedSpace
hU : IsCompact U.carrier
x f : ↑(X.presheaf.obj (op U))
H : x |_ Scheme.basicOpen X f = 0
s : Set ↑(Scheme.affineOpens X)
hs : Set.Finite s
e : U.carrier = ⋃ (i : ↑(Scheme.affineOpens X)) (_ : i ∈ s), ↑↑i
⊢ ∃ n, f ^ n * x = 0
[PROOFSTEP]
replace e : U = iSup fun i : s => (i : Opens X.carrier)
[GOAL]
case e
X✝ Y : Scheme
f✝ : X✝ ⟶ Y
Z X : Scheme
U : Opens ↑↑X.toPresheafedSpace
hU : IsCompact U.carrier
x f : ↑(X.presheaf.obj (op U))
H : x |_ Scheme.basicOpen X f = 0
s : Set ↑(Scheme.affineOpens X)
hs : Set.Finite s
e : U.carrier = ⋃ (i : ↑(Scheme.affineOpens X)) (_ : i ∈ s), ↑↑i
⊢ U = ⨆ (i : ↑s), ↑↑i
[PROOFSTEP]
ext1
[GOAL]
case e.h
X✝ Y : Scheme
f✝ : X✝ ⟶ Y
Z X : Scheme
U : Opens ↑↑X.toPresheafedSpace
hU : IsCompact U.carrier
x f : ↑(X.presheaf.obj (op U))
H : x |_ Scheme.basicOpen X f = 0
s : Set ↑(Scheme.affineOpens X)
hs : Set.Finite s
e : U.carrier = ⋃ (i : ↑(Scheme.affineOpens X)) (_ : i ∈ s), ↑↑i
⊢ ↑U = ↑(⨆ (i : ↑s), ↑↑i)
[PROOFSTEP]
simpa using e
[GOAL]
case intro.intro
X✝ Y : Scheme
f✝ : X✝ ⟶ Y
Z X : Scheme
U : Opens ↑↑X.toPresheafedSpace
hU : IsCompact U.carrier
x f : ↑(X.presheaf.obj (op U))
H : x |_ Scheme.basicOpen X f = 0
s : Set ↑(Scheme.affineOpens X)
hs : Set.Finite s
e : U = ⨆ (i : ↑s), ↑↑i
⊢ ∃ n, f ^ n * x = 0
[PROOFSTEP]
have h₁ : ∀ i : s, i.1.1 ≤ U := by
  intro i
  change (i : Opens X.carrier) ≤ U
  rw [e]
    -- porting note: `exact le_iSup _ _` no longer works
  exact le_iSup (fun (i : s) => (i : Opens (X.toPresheafedSpace))) _
[GOAL]
X✝ Y : Scheme
f✝ : X✝ ⟶ Y
Z X : Scheme
U : Opens ↑↑X.toPresheafedSpace
hU : IsCompact U.carrier
x f : ↑(X.presheaf.obj (op U))
H : x |_ Scheme.basicOpen X f = 0
s : Set ↑(Scheme.affineOpens X)
hs : Set.Finite s
e : U = ⨆ (i : ↑s), ↑↑i
⊢ ∀ (i : ↑s), ↑↑i ≤ U
[PROOFSTEP]
intro i
[GOAL]
X✝ Y : Scheme
f✝ : X✝ ⟶ Y
Z X : Scheme
U : Opens ↑↑X.toPresheafedSpace
hU : IsCompact U.carrier
x f : ↑(X.presheaf.obj (op U))
H : x |_ Scheme.basicOpen X f = 0
s : Set ↑(Scheme.affineOpens X)
hs : Set.Finite s
e : U = ⨆ (i : ↑s), ↑↑i
i : ↑s
⊢ ↑↑i ≤ U
[PROOFSTEP]
change (i : Opens X.carrier) ≤ U
[GOAL]
X✝ Y : Scheme
f✝ : X✝ ⟶ Y
Z X : Scheme
U : Opens ↑↑X.toPresheafedSpace
hU : IsCompact U.carrier
x f : ↑(X.presheaf.obj (op U))
H : x |_ Scheme.basicOpen X f = 0
s : Set ↑(Scheme.affineOpens X)
hs : Set.Finite s
e : U = ⨆ (i : ↑s), ↑↑i
i : ↑s
⊢ ↑↑i ≤ U
[PROOFSTEP]
rw [e]
  -- porting note: `exact le_iSup _ _` no longer works
[GOAL]
X✝ Y : Scheme
f✝ : X✝ ⟶ Y
Z X : Scheme
U : Opens ↑↑X.toPresheafedSpace
hU : IsCompact U.carrier
x f : ↑(X.presheaf.obj (op U))
H : x |_ Scheme.basicOpen X f = 0
s : Set ↑(Scheme.affineOpens X)
hs : Set.Finite s
e : U = ⨆ (i : ↑s), ↑↑i
i : ↑s
⊢ ↑↑i ≤ ⨆ (i : ↑s), ↑↑i
[PROOFSTEP]
exact le_iSup (fun (i : s) => (i : Opens (X.toPresheafedSpace))) _
[GOAL]
case intro.intro
X✝ Y : Scheme
f✝ : X✝ ⟶ Y
Z X : Scheme
U : Opens ↑↑X.toPresheafedSpace
hU : IsCompact U.carrier
x f : ↑(X.presheaf.obj (op U))
H : x |_ Scheme.basicOpen X f = 0
s : Set ↑(Scheme.affineOpens X)
hs : Set.Finite s
e : U = ⨆ (i : ↑s), ↑↑i
h₁ : ∀ (i : ↑s), ↑↑i ≤ U
⊢ ∃ n, f ^ n * x = 0
[PROOFSTEP]
have H' := fun i : s =>
  exists_pow_mul_eq_zero_of_res_basicOpen_eq_zero_of_isAffineOpen X i.1.2 (X.presheaf.map (homOfLE (h₁ i)).op x)
    (X.presheaf.map (homOfLE (h₁ i)).op f) ?_
[GOAL]
case intro.intro.refine_2
X✝ Y : Scheme
f✝ : X✝ ⟶ Y
Z X : Scheme
U : Opens ↑↑X.toPresheafedSpace
hU : IsCompact U.carrier
x f : ↑(X.presheaf.obj (op U))
H : x |_ Scheme.basicOpen X f = 0
s : Set ↑(Scheme.affineOpens X)
hs : Set.Finite s
e : U = ⨆ (i : ↑s), ↑↑i
h₁ : ∀ (i : ↑s), ↑↑i ≤ U
H' :
  ∀ (i : ↑s),
    ∃ n, ↑(X.presheaf.map (homOfLE (_ : ↑↑i ≤ U)).op) f ^ n * ↑(X.presheaf.map (homOfLE (_ : ↑↑i ≤ U)).op) x = 0
⊢ ∃ n, f ^ n * x = 0
case intro.intro.refine_1
X✝ Y : Scheme
f✝ : X✝ ⟶ Y
Z X : Scheme
U : Opens ↑↑X.toPresheafedSpace
hU : IsCompact U.carrier
x f : ↑(X.presheaf.obj (op U))
H : x |_ Scheme.basicOpen X f = 0
s : Set ↑(Scheme.affineOpens X)
hs : Set.Finite s
e : U = ⨆ (i : ↑s), ↑↑i
h₁ : ∀ (i : ↑s), ↑↑i ≤ U
i : ↑s
⊢ ↑(X.presheaf.map (homOfLE (_ : ↑↑i ≤ U)).op) x |_
      Scheme.basicOpen X (↑(X.presheaf.map (homOfLE (_ : ↑↑i ≤ U)).op) f) =
    0
[PROOFSTEP]
swap
[GOAL]
case intro.intro.refine_1
X✝ Y : Scheme
f✝ : X✝ ⟶ Y
Z X : Scheme
U : Opens ↑↑X.toPresheafedSpace
hU : IsCompact U.carrier
x f : ↑(X.presheaf.obj (op U))
H : x |_ Scheme.basicOpen X f = 0
s : Set ↑(Scheme.affineOpens X)
hs : Set.Finite s
e : U = ⨆ (i : ↑s), ↑↑i
h₁ : ∀ (i : ↑s), ↑↑i ≤ U
i : ↑s
⊢ ↑(X.presheaf.map (homOfLE (_ : ↑↑i ≤ U)).op) x |_
      Scheme.basicOpen X (↑(X.presheaf.map (homOfLE (_ : ↑↑i ≤ U)).op) f) =
    0
[PROOFSTEP]
delta TopCat.Presheaf.restrictOpen TopCat.Presheaf.restrict at H ⊢
[GOAL]
case intro.intro.refine_1
X✝ Y : Scheme
f✝ : X✝ ⟶ Y
Z X : Scheme
U : Opens ↑↑X.toPresheafedSpace
hU : IsCompact U.carrier
x f : ↑(X.presheaf.obj (op U))
H : ↑(X.presheaf.map (homOfLE (_ : ∀ ⦃a : ↑↑X.toPresheafedSpace⦄, a ∈ ↑(Scheme.basicOpen X f) → a ∈ ↑U)).op) x = 0
s : Set ↑(Scheme.affineOpens X)
hs : Set.Finite s
e : U = ⨆ (i : ↑s), ↑↑i
h₁ : ∀ (i : ↑s), ↑↑i ≤ U
i : ↑s
⊢ ↑(X.presheaf.map
          (homOfLE
              (_ :
                ∀ ⦃a : ↑↑X.toPresheafedSpace⦄,
                  a ∈ ↑(Scheme.basicOpen X (↑(X.presheaf.map (homOfLE (_ : ↑↑i ≤ U)).op) f)) → a ∈ ↑↑↑i)).op)
      (↑(X.presheaf.map (homOfLE (_ : ↑↑i ≤ U)).op) x) =
    0
[PROOFSTEP]
convert congr_arg (X.presheaf.map (homOfLE _).op) H
[GOAL]
case h.e'_2
X✝ Y : Scheme
f✝ : X✝ ⟶ Y
Z X : Scheme
U : Opens ↑↑X.toPresheafedSpace
hU : IsCompact U.carrier
x f : ↑(X.presheaf.obj (op U))
H : ↑(X.presheaf.map (homOfLE (_ : ∀ ⦃a : ↑↑X.toPresheafedSpace⦄, a ∈ ↑(Scheme.basicOpen X f) → a ∈ ↑U)).op) x = 0
s : Set ↑(Scheme.affineOpens X)
hs : Set.Finite s
e : U = ⨆ (i : ↑s), ↑↑i
h₁ : ∀ (i : ↑s), ↑↑i ≤ U
i : ↑s
⊢ ↑(X.presheaf.map
          (homOfLE
              (_ :
                ∀ ⦃a : ↑↑X.toPresheafedSpace⦄,
                  a ∈ ↑(Scheme.basicOpen X (↑(X.presheaf.map (homOfLE (_ : ↑↑i ≤ U)).op) f)) → a ∈ ↑↑↑i)).op)
      (↑(X.presheaf.map (homOfLE (_ : ↑↑i ≤ U)).op) x) =
    ↑(X.presheaf.map (homOfLE ?intro.intro.refine_1.convert_1).op)
      (↑(X.presheaf.map (homOfLE (_ : ∀ ⦃a : ↑↑X.toPresheafedSpace⦄, a ∈ ↑(Scheme.basicOpen X f) → a ∈ ↑U)).op) x)
[PROOFSTEP]
simp only [← comp_apply, ← Functor.map_comp]
[GOAL]
case h.e'_2
X✝ Y : Scheme
f✝ : X✝ ⟶ Y
Z X : Scheme
U : Opens ↑↑X.toPresheafedSpace
hU : IsCompact U.carrier
x f : ↑(X.presheaf.obj (op U))
H : ↑(X.presheaf.map (homOfLE (_ : ∀ ⦃a : ↑↑X.toPresheafedSpace⦄, a ∈ ↑(Scheme.basicOpen X f) → a ∈ ↑U)).op) x = 0
s : Set ↑(Scheme.affineOpens X)
hs : Set.Finite s
e : U = ⨆ (i : ↑s), ↑↑i
h₁ : ∀ (i : ↑s), ↑↑i ≤ U
i : ↑s
⊢ ↑(X.presheaf.map
          ((homOfLE (_ : ↑↑i ≤ U)).op ≫
            (homOfLE
                (_ :
                  ∀ ⦃a : ↑↑X.toPresheafedSpace⦄,
                    a ∈ ↑(Scheme.basicOpen X (↑(X.presheaf.map (homOfLE (_ : ↑↑i ≤ U)).op) f)) → a ∈ ↑↑↑i)).op))
      x =
    ↑(X.presheaf.map
          ((homOfLE (_ : ∀ ⦃a : ↑↑X.toPresheafedSpace⦄, a ∈ ↑(Scheme.basicOpen X f) → a ∈ ↑U)).op ≫
            (homOfLE ?intro.intro.refine_1.convert_1).op))
      x
[PROOFSTEP]
rfl
[GOAL]
case h.e'_3
X✝ Y : Scheme
f✝ : X✝ ⟶ Y
Z X : Scheme
U : Opens ↑↑X.toPresheafedSpace
hU : IsCompact U.carrier
x f : ↑(X.presheaf.obj (op U))
H : ↑(X.presheaf.map (homOfLE (_ : ∀ ⦃a : ↑↑X.toPresheafedSpace⦄, a ∈ ↑(Scheme.basicOpen X f) → a ∈ ↑U)).op) x = 0
s : Set ↑(Scheme.affineOpens X)
hs : Set.Finite s
e : U = ⨆ (i : ↑s), ↑↑i
h₁ : ∀ (i : ↑s), ↑↑i ≤ U
i : ↑s
⊢ 0 = ↑(X.presheaf.map (homOfLE ?intro.intro.refine_1.convert_1).op) 0
[PROOFSTEP]
rw [map_zero]
[GOAL]
case intro.intro.refine_1.convert_1
X✝ Y : Scheme
f✝ : X✝ ⟶ Y
Z X : Scheme
U : Opens ↑↑X.toPresheafedSpace
hU : IsCompact U.carrier
x f : ↑(X.presheaf.obj (op U))
H : ↑(X.presheaf.map (homOfLE (_ : ∀ ⦃a : ↑↑X.toPresheafedSpace⦄, a ∈ ↑(Scheme.basicOpen X f) → a ∈ ↑U)).op) x = 0
s : Set ↑(Scheme.affineOpens X)
hs : Set.Finite s
e : U = ⨆ (i : ↑s), ↑↑i
h₁ : ∀ (i : ↑s), ↑↑i ≤ U
i : ↑s
⊢ Scheme.basicOpen X (↑(X.presheaf.map (homOfLE (_ : ↑↑i ≤ U)).op) f) ≤ Scheme.basicOpen X f
[PROOFSTEP]
simp only [Scheme.basicOpen_res, ge_iff_le, inf_le_right]
[GOAL]
case intro.intro.refine_2
X✝ Y : Scheme
f✝ : X✝ ⟶ Y
Z X : Scheme
U : Opens ↑↑X.toPresheafedSpace
hU : IsCompact U.carrier
x f : ↑(X.presheaf.obj (op U))
H : x |_ Scheme.basicOpen X f = 0
s : Set ↑(Scheme.affineOpens X)
hs : Set.Finite s
e : U = ⨆ (i : ↑s), ↑↑i
h₁ : ∀ (i : ↑s), ↑↑i ≤ U
H' :
  ∀ (i : ↑s),
    ∃ n, ↑(X.presheaf.map (homOfLE (_ : ↑↑i ≤ U)).op) f ^ n * ↑(X.presheaf.map (homOfLE (_ : ↑↑i ≤ U)).op) x = 0
⊢ ∃ n, f ^ n * x = 0
[PROOFSTEP]
choose n hn using H'
[GOAL]
case intro.intro.refine_2
X✝ Y : Scheme
f✝ : X✝ ⟶ Y
Z X : Scheme
U : Opens ↑↑X.toPresheafedSpace
hU : IsCompact U.carrier
x f : ↑(X.presheaf.obj (op U))
H : x |_ Scheme.basicOpen X f = 0
s : Set ↑(Scheme.affineOpens X)
hs : Set.Finite s
e : U = ⨆ (i : ↑s), ↑↑i
h₁ : ∀ (i : ↑s), ↑↑i ≤ U
n : ↑s → ℕ
hn :
  ∀ (i : ↑s), ↑(X.presheaf.map (homOfLE (_ : ↑↑i ≤ U)).op) f ^ n i * ↑(X.presheaf.map (homOfLE (_ : ↑↑i ≤ U)).op) x = 0
⊢ ∃ n, f ^ n * x = 0
[PROOFSTEP]
haveI := hs.to_subtype
[GOAL]
case intro.intro.refine_2
X✝ Y : Scheme
f✝ : X✝ ⟶ Y
Z X : Scheme
U : Opens ↑↑X.toPresheafedSpace
hU : IsCompact U.carrier
x f : ↑(X.presheaf.obj (op U))
H : x |_ Scheme.basicOpen X f = 0
s : Set ↑(Scheme.affineOpens X)
hs : Set.Finite s
e : U = ⨆ (i : ↑s), ↑↑i
h₁ : ∀ (i : ↑s), ↑↑i ≤ U
n : ↑s → ℕ
hn :
  ∀ (i : ↑s), ↑(X.presheaf.map (homOfLE (_ : ↑↑i ≤ U)).op) f ^ n i * ↑(X.presheaf.map (homOfLE (_ : ↑↑i ≤ U)).op) x = 0
this : Finite ↑s
⊢ ∃ n, f ^ n * x = 0
[PROOFSTEP]
cases nonempty_fintype s
[GOAL]
case intro.intro.refine_2.intro
X✝ Y : Scheme
f✝ : X✝ ⟶ Y
Z X : Scheme
U : Opens ↑↑X.toPresheafedSpace
hU : IsCompact U.carrier
x f : ↑(X.presheaf.obj (op U))
H : x |_ Scheme.basicOpen X f = 0
s : Set ↑(Scheme.affineOpens X)
hs : Set.Finite s
e : U = ⨆ (i : ↑s), ↑↑i
h₁ : ∀ (i : ↑s), ↑↑i ≤ U
n : ↑s → ℕ
hn :
  ∀ (i : ↑s), ↑(X.presheaf.map (homOfLE (_ : ↑↑i ≤ U)).op) f ^ n i * ↑(X.presheaf.map (homOfLE (_ : ↑↑i ≤ U)).op) x = 0
this : Finite ↑s
val✝ : Fintype ↑s
⊢ ∃ n, f ^ n * x = 0
[PROOFSTEP]
use Finset.univ.sup n
[GOAL]
case h
X✝ Y : Scheme
f✝ : X✝ ⟶ Y
Z X : Scheme
U : Opens ↑↑X.toPresheafedSpace
hU : IsCompact U.carrier
x f : ↑(X.presheaf.obj (op U))
H : x |_ Scheme.basicOpen X f = 0
s : Set ↑(Scheme.affineOpens X)
hs : Set.Finite s
e : U = ⨆ (i : ↑s), ↑↑i
h₁ : ∀ (i : ↑s), ↑↑i ≤ U
n : ↑s → ℕ
hn :
  ∀ (i : ↑s), ↑(X.presheaf.map (homOfLE (_ : ↑↑i ≤ U)).op) f ^ n i * ↑(X.presheaf.map (homOfLE (_ : ↑↑i ≤ U)).op) x = 0
this : Finite ↑s
val✝ : Fintype ↑s
⊢ f ^ Finset.sup Finset.univ n * x = 0
[PROOFSTEP]
suffices ∀ i : s, X.presheaf.map (homOfLE (h₁ i)).op (f ^ Finset.univ.sup n * x) = 0
  by
  subst e
  apply TopCat.Sheaf.eq_of_locally_eq X.sheaf fun i : s => (i : Opens X.carrier)
  intro i
  rw [map_zero]
  apply this
[GOAL]
X✝ Y : Scheme
f✝ : X✝ ⟶ Y
Z X : Scheme
U : Opens ↑↑X.toPresheafedSpace
hU : IsCompact U.carrier
x f : ↑(X.presheaf.obj (op U))
H : x |_ Scheme.basicOpen X f = 0
s : Set ↑(Scheme.affineOpens X)
hs : Set.Finite s
e : U = ⨆ (i : ↑s), ↑↑i
h₁ : ∀ (i : ↑s), ↑↑i ≤ U
n : ↑s → ℕ
hn :
  ∀ (i : ↑s), ↑(X.presheaf.map (homOfLE (_ : ↑↑i ≤ U)).op) f ^ n i * ↑(X.presheaf.map (homOfLE (_ : ↑↑i ≤ U)).op) x = 0
this✝ : Finite ↑s
val✝ : Fintype ↑s
this : ∀ (i : ↑s), ↑(X.presheaf.map (homOfLE (_ : ↑↑i ≤ U)).op) (f ^ Finset.sup Finset.univ n * x) = 0
⊢ f ^ Finset.sup Finset.univ n * x = 0
[PROOFSTEP]
subst e
[GOAL]
X✝ Y : Scheme
f✝ : X✝ ⟶ Y
Z X : Scheme
s : Set ↑(Scheme.affineOpens X)
hs : Set.Finite s
n : ↑s → ℕ
this✝ : Finite ↑s
val✝ : Fintype ↑s
hU : IsCompact (⨆ (i : ↑s), ↑↑i).carrier
x f : ↑(X.presheaf.obj (op (⨆ (i : ↑s), ↑↑i)))
H : x |_ Scheme.basicOpen X f = 0
h₁ : ∀ (i : ↑s), ↑↑i ≤ ⨆ (i : ↑s), ↑↑i
hn :
  ∀ (i : ↑s),
    ↑(X.presheaf.map (homOfLE (_ : ↑↑i ≤ ⨆ (i : ↑s), ↑↑i)).op) f ^ n i *
        ↑(X.presheaf.map (homOfLE (_ : ↑↑i ≤ ⨆ (i : ↑s), ↑↑i)).op) x =
      0
this : ∀ (i : ↑s), ↑(X.presheaf.map (homOfLE (_ : ↑↑i ≤ ⨆ (i : ↑s), ↑↑i)).op) (f ^ Finset.sup Finset.univ n * x) = 0
⊢ f ^ Finset.sup Finset.univ n * x = 0
[PROOFSTEP]
apply TopCat.Sheaf.eq_of_locally_eq X.sheaf fun i : s => (i : Opens X.carrier)
[GOAL]
case h
X✝ Y : Scheme
f✝ : X✝ ⟶ Y
Z X : Scheme
s : Set ↑(Scheme.affineOpens X)
hs : Set.Finite s
n : ↑s → ℕ
this✝ : Finite ↑s
val✝ : Fintype ↑s
hU : IsCompact (⨆ (i : ↑s), ↑↑i).carrier
x f : ↑(X.presheaf.obj (op (⨆ (i : ↑s), ↑↑i)))
H : x |_ Scheme.basicOpen X f = 0
h₁ : ∀ (i : ↑s), ↑↑i ≤ ⨆ (i : ↑s), ↑↑i
hn :
  ∀ (i : ↑s),
    ↑(X.presheaf.map (homOfLE (_ : ↑↑i ≤ ⨆ (i : ↑s), ↑↑i)).op) f ^ n i *
        ↑(X.presheaf.map (homOfLE (_ : ↑↑i ≤ ⨆ (i : ↑s), ↑↑i)).op) x =
      0
this : ∀ (i : ↑s), ↑(X.presheaf.map (homOfLE (_ : ↑↑i ≤ ⨆ (i : ↑s), ↑↑i)).op) (f ^ Finset.sup Finset.univ n * x) = 0
⊢ ∀ (i : ↑s),
    ↑((Scheme.sheaf X).val.map (Opens.leSupr (fun i => ↑↑i) i).op) (f ^ Finset.sup Finset.univ n * x) =
      ↑((Scheme.sheaf X).val.map (Opens.leSupr (fun i => ↑↑i) i).op) 0
[PROOFSTEP]
intro i
[GOAL]
case h
X✝ Y : Scheme
f✝ : X✝ ⟶ Y
Z X : Scheme
s : Set ↑(Scheme.affineOpens X)
hs : Set.Finite s
n : ↑s → ℕ
this✝ : Finite ↑s
val✝ : Fintype ↑s
hU : IsCompact (⨆ (i : ↑s), ↑↑i).carrier
x f : ↑(X.presheaf.obj (op (⨆ (i : ↑s), ↑↑i)))
H : x |_ Scheme.basicOpen X f = 0
h₁ : ∀ (i : ↑s), ↑↑i ≤ ⨆ (i : ↑s), ↑↑i
hn :
  ∀ (i : ↑s),
    ↑(X.presheaf.map (homOfLE (_ : ↑↑i ≤ ⨆ (i : ↑s), ↑↑i)).op) f ^ n i *
        ↑(X.presheaf.map (homOfLE (_ : ↑↑i ≤ ⨆ (i : ↑s), ↑↑i)).op) x =
      0
this : ∀ (i : ↑s), ↑(X.presheaf.map (homOfLE (_ : ↑↑i ≤ ⨆ (i : ↑s), ↑↑i)).op) (f ^ Finset.sup Finset.univ n * x) = 0
i : ↑s
⊢ ↑((Scheme.sheaf X).val.map (Opens.leSupr (fun i => ↑↑i) i).op) (f ^ Finset.sup Finset.univ n * x) =
    ↑((Scheme.sheaf X).val.map (Opens.leSupr (fun i => ↑↑i) i).op) 0
[PROOFSTEP]
rw [map_zero]
[GOAL]
case h
X✝ Y : Scheme
f✝ : X✝ ⟶ Y
Z X : Scheme
s : Set ↑(Scheme.affineOpens X)
hs : Set.Finite s
n : ↑s → ℕ
this✝ : Finite ↑s
val✝ : Fintype ↑s
hU : IsCompact (⨆ (i : ↑s), ↑↑i).carrier
x f : ↑(X.presheaf.obj (op (⨆ (i : ↑s), ↑↑i)))
H : x |_ Scheme.basicOpen X f = 0
h₁ : ∀ (i : ↑s), ↑↑i ≤ ⨆ (i : ↑s), ↑↑i
hn :
  ∀ (i : ↑s),
    ↑(X.presheaf.map (homOfLE (_ : ↑↑i ≤ ⨆ (i : ↑s), ↑↑i)).op) f ^ n i *
        ↑(X.presheaf.map (homOfLE (_ : ↑↑i ≤ ⨆ (i : ↑s), ↑↑i)).op) x =
      0
this : ∀ (i : ↑s), ↑(X.presheaf.map (homOfLE (_ : ↑↑i ≤ ⨆ (i : ↑s), ↑↑i)).op) (f ^ Finset.sup Finset.univ n * x) = 0
i : ↑s
⊢ ↑((Scheme.sheaf X).val.map (Opens.leSupr (fun i => ↑↑i) i).op) (f ^ Finset.sup Finset.univ n * x) = 0
[PROOFSTEP]
apply this
[GOAL]
case h
X✝ Y : Scheme
f✝ : X✝ ⟶ Y
Z X : Scheme
U : Opens ↑↑X.toPresheafedSpace
hU : IsCompact U.carrier
x f : ↑(X.presheaf.obj (op U))
H : x |_ Scheme.basicOpen X f = 0
s : Set ↑(Scheme.affineOpens X)
hs : Set.Finite s
e : U = ⨆ (i : ↑s), ↑↑i
h₁ : ∀ (i : ↑s), ↑↑i ≤ U
n : ↑s → ℕ
hn :
  ∀ (i : ↑s), ↑(X.presheaf.map (homOfLE (_ : ↑↑i ≤ U)).op) f ^ n i * ↑(X.presheaf.map (homOfLE (_ : ↑↑i ≤ U)).op) x = 0
this : Finite ↑s
val✝ : Fintype ↑s
⊢ ∀ (i : ↑s), ↑(X.presheaf.map (homOfLE (_ : ↑↑i ≤ U)).op) (f ^ Finset.sup Finset.univ n * x) = 0
[PROOFSTEP]
intro i
[GOAL]
case h
X✝ Y : Scheme
f✝ : X✝ ⟶ Y
Z X : Scheme
U : Opens ↑↑X.toPresheafedSpace
hU : IsCompact U.carrier
x f : ↑(X.presheaf.obj (op U))
H : x |_ Scheme.basicOpen X f = 0
s : Set ↑(Scheme.affineOpens X)
hs : Set.Finite s
e : U = ⨆ (i : ↑s), ↑↑i
h₁ : ∀ (i : ↑s), ↑↑i ≤ U
n : ↑s → ℕ
hn :
  ∀ (i : ↑s), ↑(X.presheaf.map (homOfLE (_ : ↑↑i ≤ U)).op) f ^ n i * ↑(X.presheaf.map (homOfLE (_ : ↑↑i ≤ U)).op) x = 0
this : Finite ↑s
val✝ : Fintype ↑s
i : ↑s
⊢ ↑(X.presheaf.map (homOfLE (_ : ↑↑i ≤ U)).op) (f ^ Finset.sup Finset.univ n * x) = 0
[PROOFSTEP]
replace hn := congr_arg (fun x => X.presheaf.map (homOfLE (h₁ i)).op (f ^ (Finset.univ.sup n - n i)) * x) (hn i)
[GOAL]
case h
X✝ Y : Scheme
f✝ : X✝ ⟶ Y
Z X : Scheme
U : Opens ↑↑X.toPresheafedSpace
hU : IsCompact U.carrier
x f : ↑(X.presheaf.obj (op U))
H : x |_ Scheme.basicOpen X f = 0
s : Set ↑(Scheme.affineOpens X)
hs : Set.Finite s
e : U = ⨆ (i : ↑s), ↑↑i
h₁ : ∀ (i : ↑s), ↑↑i ≤ U
n : ↑s → ℕ
this : Finite ↑s
val✝ : Fintype ↑s
i : ↑s
hn :
  (fun x => ↑(X.presheaf.map (homOfLE (_ : ↑↑i ≤ U)).op) (f ^ (Finset.sup Finset.univ n - n i)) * x)
      (↑(X.presheaf.map (homOfLE (_ : ↑↑i ≤ U)).op) f ^ n i * ↑(X.presheaf.map (homOfLE (_ : ↑↑i ≤ U)).op) x) =
    (fun x => ↑(X.presheaf.map (homOfLE (_ : ↑↑i ≤ U)).op) (f ^ (Finset.sup Finset.univ n - n i)) * x) 0
⊢ ↑(X.presheaf.map (homOfLE (_ : ↑↑i ≤ U)).op) (f ^ Finset.sup Finset.univ n * x) = 0
[PROOFSTEP]
dsimp at hn
[GOAL]
case h
X✝ Y : Scheme
f✝ : X✝ ⟶ Y
Z X : Scheme
U : Opens ↑↑X.toPresheafedSpace
hU : IsCompact U.carrier
x f : ↑(X.presheaf.obj (op U))
H : x |_ Scheme.basicOpen X f = 0
s : Set ↑(Scheme.affineOpens X)
hs : Set.Finite s
e : U = ⨆ (i : ↑s), ↑↑i
h₁ : ∀ (i : ↑s), ↑↑i ≤ U
n : ↑s → ℕ
this : Finite ↑s
val✝ : Fintype ↑s
i : ↑s
hn :
  ↑(X.presheaf.map (homOfLE (_ : ↑↑i ≤ U)).op) (f ^ (Finset.sup Finset.univ n - n i)) *
      (↑(X.presheaf.map (homOfLE (_ : ↑↑i ≤ U)).op) f ^ n i * ↑(X.presheaf.map (homOfLE (_ : ↑↑i ≤ U)).op) x) =
    ↑(X.presheaf.map (homOfLE (_ : ↑↑i ≤ U)).op) (f ^ (Finset.sup Finset.univ n - n i)) * 0
⊢ ↑(X.presheaf.map (homOfLE (_ : ↑↑i ≤ U)).op) (f ^ Finset.sup Finset.univ n * x) = 0
[PROOFSTEP]
simp only [← map_mul, ← map_pow] at hn
[GOAL]
case h
X✝ Y : Scheme
f✝ : X✝ ⟶ Y
Z X : Scheme
U : Opens ↑↑X.toPresheafedSpace
hU : IsCompact U.carrier
x f : ↑(X.presheaf.obj (op U))
H : x |_ Scheme.basicOpen X f = 0
s : Set ↑(Scheme.affineOpens X)
hs : Set.Finite s
e : U = ⨆ (i : ↑s), ↑↑i
h₁ : ∀ (i : ↑s), ↑↑i ≤ U
n : ↑s → ℕ
this : Finite ↑s
val✝ : Fintype ↑s
i : ↑s
hn :
  ↑(X.presheaf.map (homOfLE (_ : ↑↑i ≤ U)).op) (f ^ (Finset.sup Finset.univ n - n i) * (f ^ n i * x)) =
    ↑(X.presheaf.map (homOfLE (_ : ↑↑i ≤ U)).op) (f ^ (Finset.sup Finset.univ n - n i)) * 0
⊢ ↑(X.presheaf.map (homOfLE (_ : ↑↑i ≤ U)).op) (f ^ Finset.sup Finset.univ n * x) = 0
[PROOFSTEP]
rwa [mul_zero, ← mul_assoc, ← pow_add, tsub_add_cancel_of_le] at hn
[GOAL]
case h
X✝ Y : Scheme
f✝ : X✝ ⟶ Y
Z X : Scheme
U : Opens ↑↑X.toPresheafedSpace
hU : IsCompact U.carrier
x f : ↑(X.presheaf.obj (op U))
H : x |_ Scheme.basicOpen X f = 0
s : Set ↑(Scheme.affineOpens X)
hs : Set.Finite s
e : U = ⨆ (i : ↑s), ↑↑i
h₁ : ∀ (i : ↑s), ↑↑i ≤ U
n : ↑s → ℕ
this : Finite ↑s
val✝ : Fintype ↑s
i : ↑s
hn : ↑(X.presheaf.map (homOfLE (_ : ↑↑i ≤ U)).op) (f ^ (Finset.sup Finset.univ n - n i + n i) * x) = 0
⊢ n i ≤ Finset.sup Finset.univ n
[PROOFSTEP]
apply Finset.le_sup (Finset.mem_univ i)


[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


[GOAL]
L : Language
M : Type u_1
s : Setoid M
ps : Prestructure L s
n : ℕ
f : Functions L n
x : Fin n → M
⊢ (funMap f fun i => Quotient.mk s (x i)) = Quotient.mk s (funMap f x)
[PROOFSTEP]
change Quotient.map (@funMap L M ps.toStructure n f) Prestructure.fun_equiv (Quotient.finChoice _) = _
[GOAL]
L : Language
M : Type u_1
s : Setoid M
ps : Prestructure L s
n : ℕ
f : Functions L n
x : Fin n → M
⊢ Quotient.map (funMap f) (_ : ∀ (x y : Fin n → M), x ≈ y → funMap f x ≈ funMap f y)
      (Quotient.finChoice fun i => Quotient.mk s (x i)) =
    Quotient.mk s (funMap f x)
[PROOFSTEP]
rw [Quotient.finChoice_eq, Quotient.map_mk]
[GOAL]
L : Language
M : Type u_1
s : Setoid M
ps : Prestructure L s
n : ℕ
r : Relations L n
x : Fin n → M
⊢ (RelMap r fun i => Quotient.mk s (x i)) ↔ RelMap r x
[PROOFSTEP]
change Quotient.lift (@RelMap L M ps.toStructure n r) Prestructure.rel_equiv (Quotient.finChoice _) ↔ _
[GOAL]
L : Language
M : Type u_1
s : Setoid M
ps : Prestructure L s
n : ℕ
r : Relations L n
x : Fin n → M
⊢ Quotient.lift (RelMap r) (_ : ∀ (x y : Fin n → M), x ≈ y → RelMap r x = RelMap r y)
      (Quotient.finChoice fun i => Quotient.mk s (x i)) ↔
    RelMap r x
[PROOFSTEP]
rw [Quotient.finChoice_eq, Quotient.lift_mk]
[GOAL]
L : Language
M : Type u_1
s : Setoid M
ps : Prestructure L s
β : Type u_2
t : Term L β
x : β → M
⊢ realize (fun i => Quotient.mk s (x i)) t = Quotient.mk s (realize x t)
[PROOFSTEP]
induction' t with _ _ _ _ ih
[GOAL]
case var
L : Language
M : Type u_1
s : Setoid M
ps : Prestructure L s
β : Type u_2
x : β → M
_a✝ : β
⊢ realize (fun i => Quotient.mk s (x i)) (var _a✝) = Quotient.mk s (realize x (var _a✝))
[PROOFSTEP]
rfl
[GOAL]
case func
L : Language
M : Type u_1
s : Setoid M
ps : Prestructure L s
β : Type u_2
x : β → M
l✝ : ℕ
_f✝ : Functions L l✝
_ts✝ : Fin l✝ → Term L β
ih : ∀ (a : Fin l✝), realize (fun i => Quotient.mk s (x i)) (_ts✝ a) = Quotient.mk s (realize x (_ts✝ a))
⊢ realize (fun i => Quotient.mk s (x i)) (func _f✝ _ts✝) = Quotient.mk s (realize x (func _f✝ _ts✝))
[PROOFSTEP]
simp only [ih, funMap_quotient_mk', Term.realize]