mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicGeometry.PullbackCarrier

Goal state before:
pp: case h₁
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
t : ↥(pullback f g)
⊢ (Spec.map (ofPointTensor t) ≫ (Triplet.ofPoint t).SpecTensorTo) ≫ pullback.snd f g =
    (pullback f g).fromSpecResidueField t ≫ pullback.snd f g

Tactic:
·

Goal state after:
case h₁
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
t : ↥(pullback f g)
⊢ (Spec.map (ofPointTensor t) ≫ (Triplet.ofPoint t).SpecTensorTo) ≫ pullback.snd f g =
    (pullback f g).fromSpecResidueField t ≫ pullback.snd f g
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: case a.inr.refine_2
X Y : Scheme
f : X ⟶ Y
inst✝ : QuasiCompact f
this✝ : ∀ {X Y : Scheme} (f : X ⟶ Y) [QuasiCompact f], (∃ S, Y = Spec S) → ↑(ker f).support ⊆ closure (Set.range ⇑f)
hY : ¬∃ S, Y = Spec S
𝒰 : Y.OpenCover := Y.affineCover
i : 𝒰.I₀
x : ↥(𝒰.X i)
hx : (𝒰.f i) x ∈ ↑(ker f).support
inst : QuasiCompact (Cover.pullbackHom 𝒰 f i)
this : x ∈ closure (Set.range ⇑(Cover.pullbackHom 𝒰 f i))
⊢ (𝒰.f i) x ∈ closure (Set.range ⇑f)

pp: case a.inr.refine_1
X Y : Scheme
f : X ⟶ Y
inst✝ : QuasiCompact f
this : ∀ {X Y : Scheme} (f : X ⟶ Y) [QuasiCompact f], (∃ S, Y = Spec S) → ↑(ker f).support ⊆ closure (Set.range ⇑f)
hY : ¬∃ S, Y = Spec S
𝒰 : Y.OpenCover := Y.affineCover
i : 𝒰.I₀
x : ↥(𝒰.X i)
hx : (𝒰.f i) x ∈ ↑(ker f).support
inst : QuasiCompact (Cover.pullbackHom 𝒰 f i)
⊢ x ∈ (𝒰.X i).zeroLocus ↑((ker (Cover.pullbackHom 𝒰 f i)).ideal ⟨⊤, ⋯⟩)

Tactic:
·

Goal state after:
case a.inr.refine_2
X Y : Scheme
f : X ⟶ Y
inst✝ : QuasiCompact f
this✝ : ∀ {X Y : Scheme} (f : X ⟶ Y) [QuasiCompact f], (∃ S, Y = Spec S) → ↑(ker f).support ⊆ closure (Set.range ⇑f)
hY : ¬∃ S, Y = Spec S
𝒰 : Y.OpenCover := Y.affineCover
i : 𝒰.I₀
x : ↥(𝒰.X i)
hx : (𝒰.f i) x ∈ ↑(ker f).support
inst : QuasiCompact (Cover.pullbackHom 𝒰 f i)
this : x ∈ closure (Set.range ⇑(Cover.pullbackHom 𝒰 f i))
⊢ (𝒰.f i) x ∈ closure (Set.range ⇑f)
Module: Mathlib.AlgebraicGeometry.PullbackCarrier

Goal state before:
pp: case h₀
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
T : Triplet f g
p : ↥(Spec T.tensor)
⊢ (Spec.map (Hom.residueFieldMap T.SpecTensorTo p) ≫
        Spec.map (ofPointTensor (T.SpecTensorTo p)) ≫ Spec.map (tensorCongr ⋯).hom) ≫
      Spec.map T.tensorInl =
    (Spec T.tensor).fromSpecResidueField p ≫ Spec.map T.tensorInl

pp: case h₁
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
T : Triplet f g
p : ↥(Spec T.tensor)
⊢ (Spec.map (Hom.residueFieldMap T.SpecTensorTo p) ≫
        Spec.map (ofPointTensor (T.SpecTensorTo p)) ≫ Spec.map (tensorCongr ⋯).hom) ≫
      Spec.map T.tensorInr =
    (Spec T.tensor).fromSpecResidueField p ≫ Spec.map T.tensorInr

Tactic:
·

Goal state after:
case h₀
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
T : Triplet f g
p : ↥(Spec T.tensor)
⊢ (Spec.map (Hom.residueFieldMap T.SpecTensorTo p) ≫
        Spec.map (ofPointTensor (T.SpecTensorTo p)) ≫ Spec.map (tensorCongr ⋯).hom) ≫
      Spec.map T.tensorInl =
    (Spec T.tensor).fromSpecResidueField p ≫ Spec.map T.tensorInl
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: case h₀
X : Scheme
I : X.IdealSheafData
i : ↑X.affineOpens
⊢ I.glueDataT i i ≫ pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯) =
    𝟙 (I.glueDataObjPullback (i, i).1 (i, i).2) ≫ pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)

pp: case h₁
X : Scheme
I : X.IdealSheafData
i : ↑X.affineOpens
⊢ I.glueDataT i i ≫ pullback.snd (I.glueDataObjι i) (X.homOfLE ⋯) =
    𝟙 (I.glueDataObjPullback (i, i).1 (i, i).2) ≫ pullback.snd (I.glueDataObjι i) (X.homOfLE ⋯)

Tactic:
·

Goal state after:
case h₀
X : Scheme
I : X.IdealSheafData
i : ↑X.affineOpens
⊢ I.glueDataT i i ≫ pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯) =
    𝟙 (I.glueDataObjPullback (i, i).1 (i, i).2) ≫ pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)
Module: Mathlib.AlgebraicGeometry.Morphisms.Affine

Goal state before:
pp: case refine_1
X : Scheme
s : Set ↑Γ(X, ⊤)
hs : Ideal.span s = ⊤
hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)
U V : ↑X.affineOpens
s' : Finset ↑Γ(X, ⊤)
hs' : ↑s' ⊆ s
e : Ideal.span ↑s' = ⊤
i : ↑↑s'
⊢ IsCompact (↑↑U ∩ ↑(X.basicOpen ↑i))

pp: case refine_2
X : Scheme
s : Set ↑Γ(X, ⊤)
hs : Ideal.span s = ⊤
hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)
U V : ↑X.affineOpens
s' : Finset ↑Γ(X, ⊤)
hs' : ↑s' ⊆ s
e : Ideal.span ↑s' = ⊤
i : ↑↑s'
⊢ IsCompact (↑↑V ∩ ↑(X.basicOpen ↑i))

Tactic:
·

Goal state after:
case refine_1
X : Scheme
s : Set ↑Γ(X, ⊤)
hs : Ideal.span s = ⊤
hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)
U V : ↑X.affineOpens
s' : Finset ↑Γ(X, ⊤)
hs' : ↑s' ⊆ s
e : Ideal.span ↑s' = ⊤
i : ↑↑s'
⊢ IsCompact (↑↑U ∩ ↑(X.basicOpen ↑i))
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: case h₁
X : Scheme
I : X.IdealSheafData
i : ↑X.affineOpens
⊢ I.glueDataT i i ≫ pullback.snd (I.glueDataObjι i) (X.homOfLE ⋯) =
    𝟙 (I.glueDataObjPullback (i, i).1 (i, i).2) ≫ pullback.snd (I.glueDataObjι i) (X.homOfLE ⋯)

Tactic:
·

Goal state after:
case h₁
X : Scheme
I : X.IdealSheafData
i : ↑X.affineOpens
⊢ I.glueDataT i i ≫ pullback.snd (I.glueDataObjι i) (X.homOfLE ⋯) =
    𝟙 (I.glueDataObjPullback (i, i).1 (i, i).2) ≫ pullback.snd (I.glueDataObjι i) (X.homOfLE ⋯)
Module: Mathlib.AlgebraicGeometry.PullbackCarrier

Goal state before:
pp: case h₁
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
T : Triplet f g
p : ↥(Spec T.tensor)
⊢ (Spec.map (Hom.residueFieldMap T.SpecTensorTo p) ≫
        Spec.map (ofPointTensor (T.SpecTensorTo p)) ≫ Spec.map (tensorCongr ⋯).hom) ≫
      Spec.map T.tensorInr =
    (Spec T.tensor).fromSpecResidueField p ≫ Spec.map T.tensorInr

Tactic:
·

Goal state after:
case h₁
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
T : Triplet f g
p : ↥(Spec T.tensor)
⊢ (Spec.map (Hom.residueFieldMap T.SpecTensorTo p) ≫
        Spec.map (ofPointTensor (T.SpecTensorTo p)) ≫ Spec.map (tensorCongr ⋯).hom) ≫
      Spec.map T.tensorInr =
    (Spec T.tensor).fromSpecResidueField p ≫ Spec.map T.tensorInr
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: case h₀
X : Scheme
I : X.IdealSheafData
i j k : ↑X.affineOpens
⊢ (pullback.lift (I.glueDataT'Aux (i, j).1 (i, j).2 (i, k).2 (j, k).2 ⋯)
          (I.glueDataT'Aux (i, j).1 (i, j).2 (i, k).2 (j, i).2 ⋯) ⋯ ≫
        pullback.snd (pullback.fst (I.glueDataObjι (j, k).1) (X.homOfLE ⋯))
          (pullback.fst (I.glueDataObjι (j, i).1) (X.homOfLE ⋯))) ≫
      pullback.fst (I.glueDataObjι (j, i).1) (X.homOfLE ⋯) =
    (pullback.fst (pullback.fst (I.glueDataObjι (i, j).1) (X.homOfLE ⋯))
          (pullback.fst (I.glueDataObjι (i, k).1) (X.homOfLE ⋯)) ≫
        I.glueDataT i j) ≫
      pullback.fst (I.glueDataObjι (j, i).1) (X.homOfLE ⋯)

pp: case h₁
X : Scheme
I : X.IdealSheafData
i j k : ↑X.affineOpens
⊢ (pullback.lift (I.glueDataT'Aux (i, j).1 (i, j).2 (i, k).2 (j, k).2 ⋯)
          (I.glueDataT'Aux (i, j).1 (i, j).2 (i, k).2 (j, i).2 ⋯) ⋯ ≫
        pullback.snd (pullback.fst (I.glueDataObjι (j, k).1) (X.homOfLE ⋯))
          (pullback.fst (I.glueDataObjι (j, i).1) (X.homOfLE ⋯))) ≫
      pullback.snd (I.glueDataObjι (j, i).1) (X.homOfLE ⋯) =
    (pullback.fst (pullback.fst (I.glueDataObjι (i, j).1) (X.homOfLE ⋯))
          (pullback.fst (I.glueDataObjι (i, k).1) (X.homOfLE ⋯)) ≫
        I.glueDataT i j) ≫
      pullback.snd (I.glueDataObjι (j, i).1) (X.homOfLE ⋯)

Tactic:
·

Goal state after:
case h₀
X : Scheme
I : X.IdealSheafData
i j k : ↑X.affineOpens
⊢ (pullback.lift (I.glueDataT'Aux (i, j).1 (i, j).2 (i, k).2 (j, k).2 ⋯)
          (I.glueDataT'Aux (i, j).1 (i, j).2 (i, k).2 (j, i).2 ⋯) ⋯ ≫
        pullback.snd (pullback.fst (I.glueDataObjι (j, k).1) (X.homOfLE ⋯))
          (pullback.fst (I.glueDataObjι (j, i).1) (X.homOfLE ⋯))) ≫
      pullback.fst (I.glueDataObjι (j, i).1) (X.homOfLE ⋯) =
    (pullback.fst (pullback.fst (I.glueDataObjι (i, j).1) (X.homOfLE ⋯))
          (pullback.fst (I.glueDataObjι (i, k).1) (X.homOfLE ⋯)) ≫
        I.glueDataT i j) ≫
      pullback.fst (I.glueDataObjι (j, i).1) (X.homOfLE ⋯)
Module: Mathlib.AlgebraicGeometry.Morphisms.Affine

Goal state before:
pp: case refine_2
X : Scheme
s : Set ↑Γ(X, ⊤)
hs : Ideal.span s = ⊤
hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)
U V : ↑X.affineOpens
s' : Finset ↑Γ(X, ⊤)
hs' : ↑s' ⊆ s
e : Ideal.span ↑s' = ⊤
i : ↑↑s'
⊢ IsCompact (↑↑V ∩ ↑(X.basicOpen ↑i))

Tactic:
·

Goal state after:
case refine_2
X : Scheme
s : Set ↑Γ(X, ⊤)
hs : Ideal.span s = ⊤
hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)
U V : ↑X.affineOpens
s' : Finset ↑Γ(X, ⊤)
hs' : ↑s' ⊆ s
e : Ideal.span ↑s' = ⊤
i : ↑↑s'
⊢ IsCompact (↑↑V ∩ ↑(X.basicOpen ↑i))
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: case a.inr.refine_1
X Y : Scheme
f : X ⟶ Y
inst✝ : QuasiCompact f
this : ∀ {X Y : Scheme} (f : X ⟶ Y) [QuasiCompact f], (∃ S, Y = Spec S) → ↑(ker f).support ⊆ closure (Set.range ⇑f)
hY : ¬∃ S, Y = Spec S
𝒰 : Y.OpenCover := Y.affineCover
i : 𝒰.I₀
x : ↥(𝒰.X i)
hx : (𝒰.f i) x ∈ ↑(ker f).support
inst : QuasiCompact (Cover.pullbackHom 𝒰 f i)
⊢ x ∈ (𝒰.X i).zeroLocus ↑((ker (Cover.pullbackHom 𝒰 f i)).ideal ⟨⊤, ⋯⟩)

Tactic:
·

Goal state after:
case a.inr.refine_1
X Y : Scheme
f : X ⟶ Y
inst✝ : QuasiCompact f
this : ∀ {X Y : Scheme} (f : X ⟶ Y) [QuasiCompact f], (∃ S, Y = Spec S) → ↑(ker f).support ⊆ closure (Set.range ⇑f)
hY : ¬∃ S, Y = Spec S
𝒰 : Y.OpenCover := Y.affineCover
i : 𝒰.I₀
x : ↥(𝒰.X i)
hx : (𝒰.f i) x ∈ ↑(ker f).support
inst : QuasiCompact (Cover.pullbackHom 𝒰 f i)
⊢ x ∈ (𝒰.X i).zeroLocus ↑((ker (Cover.pullbackHom 𝒰 f i)).ideal ⟨⊤, ⋯⟩)
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: case h₁
X : Scheme
I : X.IdealSheafData
i j k : ↑X.affineOpens
⊢ (pullback.lift (I.glueDataT'Aux (i, j).1 (i, j).2 (i, k).2 (j, k).2 ⋯)
          (I.glueDataT'Aux (i, j).1 (i, j).2 (i, k).2 (j, i).2 ⋯) ⋯ ≫
        pullback.snd (pullback.fst (I.glueDataObjι (j, k).1) (X.homOfLE ⋯))
          (pullback.fst (I.glueDataObjι (j, i).1) (X.homOfLE ⋯))) ≫
      pullback.snd (I.glueDataObjι (j, i).1) (X.homOfLE ⋯) =
    (pullback.fst (pullback.fst (I.glueDataObjι (i, j).1) (X.homOfLE ⋯))
          (pullback.fst (I.glueDataObjι (i, k).1) (X.homOfLE ⋯)) ≫
        I.glueDataT i j) ≫
      pullback.snd (I.glueDataObjι (j, i).1) (X.homOfLE ⋯)

Tactic:
·

Goal state after:
case h₁
X : Scheme
I : X.IdealSheafData
i j k : ↑X.affineOpens
⊢ (pullback.lift (I.glueDataT'Aux (i, j).1 (i, j).2 (i, k).2 (j, k).2 ⋯)
          (I.glueDataT'Aux (i, j).1 (i, j).2 (i, k).2 (j, i).2 ⋯) ⋯ ≫
        pullback.snd (pullback.fst (I.glueDataObjι (j, k).1) (X.homOfLE ⋯))
          (pullback.fst (I.glueDataObjι (j, i).1) (X.homOfLE ⋯))) ≫
      pullback.snd (I.glueDataObjι (j, i).1) (X.homOfLE ⋯) =
    (pullback.fst (pullback.fst (I.glueDataObjι (i, j).1) (X.homOfLE ⋯))
          (pullback.fst (I.glueDataObjι (i, k).1) (X.homOfLE ⋯)) ≫
        I.glueDataT i j) ≫
      pullback.snd (I.glueDataObjι (j, i).1) (X.homOfLE ⋯)
Module: Mathlib.AlgebraicGeometry.PullbackCarrier

Goal state before:
pp: case mp
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
T₁ T₂ : (T : Triplet f g) × ↥(Spec T.tensor)
⊢ T₁ = T₂ → ∃ (e : T₁.fst = T₂.fst), (Spec.map (Triplet.tensorCongr e).inv) T₁.snd = T₂.snd

pp: case mpr
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
T₁ T₂ : (T : Triplet f g) × ↥(Spec T.tensor)
⊢ (∃ (e : T₁.fst = T₂.fst), (Spec.map (Triplet.tensorCongr e).inv) T₁.snd = T₂.snd) → T₁ = T₂

Tactic:
·

Goal state after:
case mp
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
T₁ T₂ : (T : Triplet f g) × ↥(Spec T.tensor)
⊢ T₁ = T₂ → ∃ (e : T₁.fst = T₂.fst), (Spec.map (Triplet.tensorCongr e).inv) T₁.snd = T₂.snd
Module: Mathlib.AlgebraicGeometry.PullbackCarrier

Goal state before:
pp: case mp
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
T₁ T₂ : (T : Triplet f g) × ↥(Spec T.tensor)
⊢ T₁ = T₂ → ∃ (e : T₁.fst = T₂.fst), (Spec.map (Triplet.tensorCongr e).inv) T₁.snd = T₂.snd

pp: case mpr
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
T₁ T₂ : (T : Triplet f g) × ↥(Spec T.tensor)
⊢ (∃ (e : T₁.fst = T₂.fst), (Spec.map (Triplet.tensorCongr e).inv) T₁.snd = T₂.snd) → T₁ = T₂

Tactic:
· rintro rfl
    simp

Goal state after:
case mpr
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
T₁ T₂ : (T : Triplet f g) × ↥(Spec T.tensor)
⊢ (∃ (e : T₁.fst = T₂.fst), (Spec.map (Triplet.tensorCongr e).inv) T₁.snd = T₂.snd) → T₁ = T₂
Module: Mathlib.AlgebraicGeometry.PullbackCarrier

Goal state before:
pp: case mpr
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
T₁ T₂ : (T : Triplet f g) × ↥(Spec T.tensor)
⊢ (∃ (e : T₁.fst = T₂.fst), (Spec.map (Triplet.tensorCongr e).inv) T₁.snd = T₂.snd) → T₁ = T₂

Tactic:
·

Goal state after:
case mpr
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
T₁ T₂ : (T : Triplet f g) × ↥(Spec T.tensor)
⊢ (∃ (e : T₁.fst = T₂.fst), (Spec.map (Triplet.tensorCongr e).inv) T₁.snd = T₂.snd) → T₁ = T₂
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: case a.inr.refine_1
X Y : Scheme
f : X ⟶ Y
inst✝ : QuasiCompact f
this : ∀ {X Y : Scheme} (f : X ⟶ Y) [QuasiCompact f], (∃ S, Y = Spec S) → ↑(ker f).support ⊆ closure (Set.range ⇑f)
hY : ¬∃ S, Y = Spec S
𝒰 : Y.OpenCover := Y.affineCover
i : 𝒰.I₀
x : ↥(𝒰.X i)
hx : (𝒰.f i) x ∈ ↑(ker f).support
inst : QuasiCompact (Cover.pullbackHom 𝒰 f i)
⊢ (𝒰.f i) x ∈ Y.zeroLocus ↑((ker f).ideal ⟨𝒰.f i ''ᵁ ↑⟨⊤, ⋯⟩, ⋯⟩) ∩ Set.range ⇑(𝒰.f i)

pp: case a.inr.refine_1.h
X Y : Scheme
f : X ⟶ Y
inst✝ : QuasiCompact f
this : ∀ {X Y : Scheme} (f : X ⟶ Y) [QuasiCompact f], (∃ S, Y = Spec S) → ↑(ker f).support ⊆ closure (Set.range ⇑f)
hY : ¬∃ S, Y = Spec S
𝒰 : Y.OpenCover := Y.affineCover
i : 𝒰.I₀
x : ↥(𝒰.X i)
hx : (𝒰.f i) x ∈ ↑(ker f).support
inst : QuasiCompact (Cover.pullbackHom 𝒰 f i)
⊢ Function.Surjective ⇑(CommRingCat.Hom.hom (appIso (𝒰.f i) ↑⟨⊤, ⋯⟩).inv)

pp: case a.inr.refine_1.H
X Y : Scheme
f : X ⟶ Y
inst✝ : QuasiCompact f
this : ∀ {X Y : Scheme} (f : X ⟶ Y) [QuasiCompact f], (∃ S, Y = Spec S) → ↑(ker f).support ⊆ closure (Set.range ⇑f)
hY : ¬∃ S, Y = Spec S
𝒰 : Y.OpenCover := Y.affineCover
i : 𝒰.I₀
x : ↥(𝒰.X i)
hx : (𝒰.f i) x ∈ ↑(ker f).support
inst : QuasiCompact (Cover.pullbackHom 𝒰 f i)
⊢ IsPullback (Cover.pullbackHom 𝒰 f i) ((Precoverage.ZeroHypercover.pullback₁ f 𝒰).f i) (𝒰.f i) f

Tactic:
·

Goal state after:
case a.inr.refine_1
X Y : Scheme
f : X ⟶ Y
inst✝ : QuasiCompact f
this : ∀ {X Y : Scheme} (f : X ⟶ Y) [QuasiCompact f], (∃ S, Y = Spec S) → ↑(ker f).support ⊆ closure (Set.range ⇑f)
hY : ¬∃ S, Y = Spec S
𝒰 : Y.OpenCover := Y.affineCover
i : 𝒰.I₀
x : ↥(𝒰.X i)
hx : (𝒰.f i) x ∈ ↑(ker f).support
inst : QuasiCompact (Cover.pullbackHom 𝒰 f i)
⊢ (𝒰.f i) x ∈ Y.zeroLocus ↑((ker f).ideal ⟨𝒰.f i ''ᵁ ↑⟨⊤, ⋯⟩, ⋯⟩) ∩ Set.range ⇑(𝒰.f i)
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: case h₀
X : Scheme
I : X.IdealSheafData
i j k : ↑X.affineOpens
⊢ (pullback.lift (I.glueDataT'Aux i j k k ⋯) (I.glueDataT'Aux i j k i ⋯) ⋯ ≫
        pullback.lift (I.glueDataT'Aux j k i i ⋯) (I.glueDataT'Aux j k i j ⋯) ⋯ ≫
          pullback.lift (I.glueDataT'Aux k i j j ⋯) (I.glueDataT'Aux k i j k ⋯) ⋯) ≫
      pullback.fst (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) =
    𝟙 (pullback (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯))) ≫
      pullback.fst (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯))

pp: case h₁
X : Scheme
I : X.IdealSheafData
i j k : ↑X.affineOpens
⊢ (pullback.lift (I.glueDataT'Aux i j k k ⋯) (I.glueDataT'Aux i j k i ⋯) ⋯ ≫
        pullback.lift (I.glueDataT'Aux j k i i ⋯) (I.glueDataT'Aux j k i j ⋯) ⋯ ≫
          pullback.lift (I.glueDataT'Aux k i j j ⋯) (I.glueDataT'Aux k i j k ⋯) ⋯) ≫
      pullback.snd (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) =
    𝟙 (pullback (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯))) ≫
      pullback.snd (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯))

Tactic:
·

Goal state after:
case h₀
X : Scheme
I : X.IdealSheafData
i j k : ↑X.affineOpens
⊢ (pullback.lift (I.glueDataT'Aux i j k k ⋯) (I.glueDataT'Aux i j k i ⋯) ⋯ ≫
        pullback.lift (I.glueDataT'Aux j k i i ⋯) (I.glueDataT'Aux j k i j ⋯) ⋯ ≫
          pullback.lift (I.glueDataT'Aux k i j j ⋯) (I.glueDataT'Aux k i j k ⋯) ⋯) ≫
      pullback.fst (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) =
    𝟙 (pullback (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯))) ≫
      pullback.fst (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯))
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: case h₀.h₀
X : Scheme
I : X.IdealSheafData
i j k : ↑X.affineOpens
⊢ ((pullback.lift (I.glueDataT'Aux i j k k ⋯) (I.glueDataT'Aux i j k i ⋯) ⋯ ≫
          pullback.lift (I.glueDataT'Aux j k i i ⋯) (I.glueDataT'Aux j k i j ⋯) ⋯ ≫
            pullback.lift (I.glueDataT'Aux k i j j ⋯) (I.glueDataT'Aux k i j k ⋯) ⋯) ≫
        pullback.fst (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯))) ≫
      pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯) =
    (𝟙 (pullback (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯))) ≫
        pullback.fst (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯))) ≫
      pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)

pp: case h₁
X : Scheme
I : X.IdealSheafData
i j k : ↑X.affineOpens
⊢ ((pullback.lift (I.glueDataT'Aux i j k k ⋯) (I.glueDataT'Aux i j k i ⋯) ⋯ ≫
          pullback.lift (I.glueDataT'Aux j k i i ⋯) (I.glueDataT'Aux j k i j ⋯) ⋯ ≫
            pullback.lift (I.glueDataT'Aux k i j j ⋯) (I.glueDataT'Aux k i j k ⋯) ⋯) ≫
        pullback.fst (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯))) ≫
      pullback.snd (I.glueDataObjι i) (X.homOfLE ⋯) =
    (𝟙 (pullback (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯))) ≫
        pullback.fst (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯))) ≫
      pullback.snd (I.glueDataObjι i) (X.homOfLE ⋯)

Tactic:
·

Goal state after:
case h₀.h₀
X : Scheme
I : X.IdealSheafData
i j k : ↑X.affineOpens
⊢ ((pullback.lift (I.glueDataT'Aux i j k k ⋯) (I.glueDataT'Aux i j k i ⋯) ⋯ ≫
          pullback.lift (I.glueDataT'Aux j k i i ⋯) (I.glueDataT'Aux j k i j ⋯) ⋯ ≫
            pullback.lift (I.glueDataT'Aux k i j j ⋯) (I.glueDataT'Aux k i j k ⋯) ⋯) ≫
        pullback.fst (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯))) ≫
      pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯) =
    (𝟙 (pullback (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯))) ≫
        pullback.fst (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯))) ≫
      pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: case a.inr.refine_1.h
X Y : Scheme
f : X ⟶ Y
inst✝ : QuasiCompact f
this : ∀ {X Y : Scheme} (f : X ⟶ Y) [QuasiCompact f], (∃ S, Y = Spec S) → ↑(ker f).support ⊆ closure (Set.range ⇑f)
hY : ¬∃ S, Y = Spec S
𝒰 : Y.OpenCover := Y.affineCover
i : 𝒰.I₀
x : ↥(𝒰.X i)
hx : (𝒰.f i) x ∈ ↑(ker f).support
inst : QuasiCompact (Cover.pullbackHom 𝒰 f i)
⊢ Function.Surjective ⇑(CommRingCat.Hom.hom (appIso (𝒰.f i) ↑⟨⊤, ⋯⟩).inv)

pp: case a.inr.refine_1.H
X Y : Scheme
f : X ⟶ Y
inst✝ : QuasiCompact f
this : ∀ {X Y : Scheme} (f : X ⟶ Y) [QuasiCompact f], (∃ S, Y = Spec S) → ↑(ker f).support ⊆ closure (Set.range ⇑f)
hY : ¬∃ S, Y = Spec S
𝒰 : Y.OpenCover := Y.affineCover
i : 𝒰.I₀
x : ↥(𝒰.X i)
hx : (𝒰.f i) x ∈ ↑(ker f).support
inst : QuasiCompact (Cover.pullbackHom 𝒰 f i)
⊢ IsPullback (Cover.pullbackHom 𝒰 f i) ((Precoverage.ZeroHypercover.pullback₁ f 𝒰).f i) (𝒰.f i) f

Tactic:
·

Goal state after:
case a.inr.refine_1.h
X Y : Scheme
f : X ⟶ Y
inst✝ : QuasiCompact f
this : ∀ {X Y : Scheme} (f : X ⟶ Y) [QuasiCompact f], (∃ S, Y = Spec S) → ↑(ker f).support ⊆ closure (Set.range ⇑f)
hY : ¬∃ S, Y = Spec S
𝒰 : Y.OpenCover := Y.affineCover
i : 𝒰.I₀
x : ↥(𝒰.X i)
hx : (𝒰.f i) x ∈ ↑(ker f).support
inst : QuasiCompact (Cover.pullbackHom 𝒰 f i)
⊢ Function.Surjective ⇑(CommRingCat.Hom.hom (appIso (𝒰.f i) ↑⟨⊤, ⋯⟩).inv)
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: case a.inr.refine_1.H
X Y : Scheme
f : X ⟶ Y
inst✝ : QuasiCompact f
this : ∀ {X Y : Scheme} (f : X ⟶ Y) [QuasiCompact f], (∃ S, Y = Spec S) → ↑(ker f).support ⊆ closure (Set.range ⇑f)
hY : ¬∃ S, Y = Spec S
𝒰 : Y.OpenCover := Y.affineCover
i : 𝒰.I₀
x : ↥(𝒰.X i)
hx : (𝒰.f i) x ∈ ↑(ker f).support
inst : QuasiCompact (Cover.pullbackHom 𝒰 f i)
⊢ IsPullback (Cover.pullbackHom 𝒰 f i) ((Precoverage.ZeroHypercover.pullback₁ f 𝒰).f i) (𝒰.f i) f

Tactic:
·

Goal state after:
case a.inr.refine_1.H
X Y : Scheme
f : X ⟶ Y
inst✝ : QuasiCompact f
this : ∀ {X Y : Scheme} (f : X ⟶ Y) [QuasiCompact f], (∃ S, Y = Spec S) → ↑(ker f).support ⊆ closure (Set.range ⇑f)
hY : ¬∃ S, Y = Spec S
𝒰 : Y.OpenCover := Y.affineCover
i : 𝒰.I₀
x : ↥(𝒰.X i)
hx : (𝒰.f i) x ∈ ↑(ker f).support
inst : QuasiCompact (Cover.pullbackHom 𝒰 f i)
⊢ IsPullback (Cover.pullbackHom 𝒰 f i) ((Precoverage.ZeroHypercover.pullback₁ f 𝒰).f i) (𝒰.f i) f
Module: Mathlib.AlgebraicGeometry.Morphisms.Affine

Goal state before:
pp: case refine_1
X : Scheme
s : Set ↑Γ(X, ⊤)
hs : Ideal.span s = ⊤
hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)
this✝ : QuasiSeparatedSpace ↥X
this : CompactSpace ↥X
i : ↑s
⊢ PrimeSpectrum.basicOpen ↑i ∈ (Spec Γ(X, ⊤)).affineOpens

pp: case refine_2
X : Scheme
s : Set ↑Γ(X, ⊤)
hs : Ideal.span s = ⊤
hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)
this✝ : QuasiSeparatedSpace ↥X
this : CompactSpace ↥X
⊢ ⨆ i, ↑⟨PrimeSpectrum.basicOpen ↑i, ⋯⟩ = ⊤

pp: case refine_3
X : Scheme
s : Set ↑Γ(X, ⊤)
hs : Ideal.span s = ⊤
hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)
this✝ : QuasiSeparatedSpace ↥X
this : CompactSpace ↥X
i : ↑s
⊢ IsAffine ↑(X.toSpecΓ ⁻¹ᵁ ↑⟨PrimeSpectrum.basicOpen ↑i, ⋯⟩)

pp: case refine_4
X : Scheme
s : Set ↑Γ(X, ⊤)
hs : Ideal.span s = ⊤
hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)
this✝ : QuasiSeparatedSpace ↥X
this : CompactSpace ↥X
i : ↑s
⊢ IsIso (Scheme.Hom.appTop (X.toSpecΓ ∣_ ↑⟨PrimeSpectrum.basicOpen ↑i, ⋯⟩))

Tactic:
·

Goal state after:
case refine_1
X : Scheme
s : Set ↑Γ(X, ⊤)
hs : Ideal.span s = ⊤
hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)
this✝ : QuasiSeparatedSpace ↥X
this : CompactSpace ↥X
i : ↑s
⊢ PrimeSpectrum.basicOpen ↑i ∈ (Spec Γ(X, ⊤)).affineOpens
Module: Mathlib.AlgebraicGeometry.PullbackCarrier

Goal state before:
pp: case refine_1
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
x : ↥X
⊢ x ∈ Set.range ⇑(pullback.fst f g) → x ∈ ⇑f ⁻¹' Set.range ⇑g

pp: case refine_2
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
x : ↥X
x✝ : x ∈ ⇑f ⁻¹' Set.range ⇑g
y : ↥Y
hy : g y = f x
⊢ x ∈ Set.range ⇑(pullback.fst f g)

Tactic:
·

Goal state after:
case refine_1
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
x : ↥X
⊢ x ∈ Set.range ⇑(pullback.fst f g) → x ∈ ⇑f ⁻¹' Set.range ⇑g
Module: Mathlib.AlgebraicGeometry.PullbackCarrier

Goal state before:
pp: case refine_2
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
x : ↥X
x✝ : x ∈ ⇑f ⁻¹' Set.range ⇑g
y : ↥Y
hy : g y = f x
⊢ x ∈ Set.range ⇑(pullback.fst f g)

Tactic:
·

Goal state after:
case refine_2
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
x : ↥X
x✝ : x ∈ ⇑f ⁻¹' Set.range ⇑g
y : ↥Y
hy : g y = f x
⊢ x ∈ Set.range ⇑(pullback.fst f g)
Module: Mathlib.AlgebraicGeometry.Morphisms.Affine

Goal state before:
pp: case refine_2
X : Scheme
s : Set ↑Γ(X, ⊤)
hs : Ideal.span s = ⊤
hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)
this✝ : QuasiSeparatedSpace ↥X
this : CompactSpace ↥X
⊢ ⨆ i, ↑⟨PrimeSpectrum.basicOpen ↑i, ⋯⟩ = ⊤

pp: case refine_3
X : Scheme
s : Set ↑Γ(X, ⊤)
hs : Ideal.span s = ⊤
hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)
this✝ : QuasiSeparatedSpace ↥X
this : CompactSpace ↥X
i : ↑s
⊢ IsAffine ↑(X.toSpecΓ ⁻¹ᵁ ↑⟨PrimeSpectrum.basicOpen ↑i, ⋯⟩)

pp: case refine_4
X : Scheme
s : Set ↑Γ(X, ⊤)
hs : Ideal.span s = ⊤
hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)
this✝ : QuasiSeparatedSpace ↥X
this : CompactSpace ↥X
i : ↑s
⊢ IsIso (Scheme.Hom.appTop (X.toSpecΓ ∣_ ↑⟨PrimeSpectrum.basicOpen ↑i, ⋯⟩))

Tactic:
·

Goal state after:
case refine_2
X : Scheme
s : Set ↑Γ(X, ⊤)
hs : Ideal.span s = ⊤
hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)
this✝ : QuasiSeparatedSpace ↥X
this : CompactSpace ↥X
⊢ ⨆ i, ↑⟨PrimeSpectrum.basicOpen ↑i, ⋯⟩ = ⊤