[GOAL]
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
s : Set A
⊢ zeroLocus 𝒜 ↑(Ideal.span s) = zeroLocus 𝒜 s
[PROOFSTEP]
ext x
[GOAL]
case h
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
s : Set A
x : ProjectiveSpectrum 𝒜
⊢ x ∈ zeroLocus 𝒜 ↑(Ideal.span s) ↔ x ∈ zeroLocus 𝒜 s
[PROOFSTEP]
exact (Submodule.gi _ _).gc s x.asHomogeneousIdeal.toIdeal
[GOAL]
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
t : Set (ProjectiveSpectrum 𝒜)
⊢ ↑(vanishingIdeal t) = {f | ∀ (x : ProjectiveSpectrum 𝒜), x ∈ t → f ∈ x.asHomogeneousIdeal}
[PROOFSTEP]
ext f
[GOAL]
case h
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
t : Set (ProjectiveSpectrum 𝒜)
f : A
⊢ f ∈ ↑(vanishingIdeal t) ↔ f ∈ {f | ∀ (x : ProjectiveSpectrum 𝒜), x ∈ t → f ∈ x.asHomogeneousIdeal}
[PROOFSTEP]
rw [vanishingIdeal, SetLike.mem_coe, ← HomogeneousIdeal.mem_iff, HomogeneousIdeal.toIdeal_iInf, Submodule.mem_iInf]
[GOAL]
case h
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
t : Set (ProjectiveSpectrum 𝒜)
f : A
⊢ (∀ (i : ProjectiveSpectrum 𝒜), f ∈ HomogeneousIdeal.toIdeal (⨅ (_ : i ∈ t), i.asHomogeneousIdeal)) ↔
    f ∈ {f | ∀ (x : ProjectiveSpectrum 𝒜), x ∈ t → f ∈ x.asHomogeneousIdeal}
[PROOFSTEP]
refine' forall_congr' fun x => _
[GOAL]
case h
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
t : Set (ProjectiveSpectrum 𝒜)
f : A
x : ProjectiveSpectrum 𝒜
⊢ f ∈ HomogeneousIdeal.toIdeal (⨅ (_ : x ∈ t), x.asHomogeneousIdeal) ↔ x ∈ t → f ∈ x.asHomogeneousIdeal
[PROOFSTEP]
rw [HomogeneousIdeal.toIdeal_iInf, Submodule.mem_iInf, HomogeneousIdeal.mem_iff]
[GOAL]
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
t : Set (ProjectiveSpectrum 𝒜)
f : A
⊢ f ∈ vanishingIdeal t ↔ ∀ (x : ProjectiveSpectrum 𝒜), x ∈ t → f ∈ x.asHomogeneousIdeal
[PROOFSTEP]
rw [← SetLike.mem_coe, coe_vanishingIdeal, Set.mem_setOf_eq]
[GOAL]
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
x : ProjectiveSpectrum 𝒜
⊢ vanishingIdeal {x} = x.asHomogeneousIdeal
[PROOFSTEP]
simp [vanishingIdeal]
[GOAL]
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
⊢ GaloisConnection (fun s => zeroLocus 𝒜 s) fun t => ↑(vanishingIdeal t)
[PROOFSTEP]
have ideal_gc : GaloisConnection Ideal.span _ := (Submodule.gi A _).gc
[GOAL]
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
ideal_gc : GaloisConnection Ideal.span SetLike.coe
⊢ GaloisConnection (fun s => zeroLocus 𝒜 s) fun t => ↑(vanishingIdeal t)
[PROOFSTEP]
simpa [zeroLocus_span, Function.comp] using GaloisConnection.compose ideal_gc (gc_ideal 𝒜)
[GOAL]
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
I : HomogeneousIdeal 𝒜
t : (Set (ProjectiveSpectrum 𝒜))ᵒᵈ
⊢ (fun I => zeroLocus 𝒜 ↑I) I ≤ t ↔ I ≤ (fun t => vanishingIdeal t) t
[PROOFSTEP]
simpa [show I.toIdeal ≤ (vanishingIdeal t).toIdeal ↔ I ≤ vanishingIdeal t from Iff.rfl] using
  subset_zeroLocus_iff_le_vanishingIdeal t I.toIdeal
[GOAL]
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
⊢ vanishingIdeal ∅ = ⊤
[PROOFSTEP]
simpa using (gc_ideal _).u_top
[GOAL]
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
t t' : Set (ProjectiveSpectrum 𝒜)
⊢ vanishingIdeal (t ∪ t') = vanishingIdeal t ⊓ vanishingIdeal t'
[PROOFSTEP]
ext1
[GOAL]
case h
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
t t' : Set (ProjectiveSpectrum 𝒜)
⊢ HomogeneousIdeal.toIdeal (vanishingIdeal (t ∪ t')) = HomogeneousIdeal.toIdeal (vanishingIdeal t ⊓ vanishingIdeal t')
[PROOFSTEP]
exact (gc_ideal 𝒜).u_inf
[GOAL]
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
s : Set (Set A)
⊢ zeroLocus 𝒜 (⋃ (s' : Set A) (_ : s' ∈ s), s') = ⋂ (s' : Set A) (_ : s' ∈ s), zeroLocus 𝒜 s'
[PROOFSTEP]
simp only [zeroLocus_iUnion]
[GOAL]
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
γ : Sort u_3
t : γ → Set (ProjectiveSpectrum 𝒜)
⊢ HomogeneousIdeal.toIdeal (vanishingIdeal (⋃ (i : γ), t i)) =
    HomogeneousIdeal.toIdeal (⨅ (i : γ), vanishingIdeal (t i))
[PROOFSTEP]
convert (gc_ideal 𝒜).u_iInf
[GOAL]
case h.e'_3
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
γ : Sort u_3
t : γ → Set (ProjectiveSpectrum 𝒜)
⊢ HomogeneousIdeal.toIdeal (⨅ (i : γ), vanishingIdeal (t i)) =
    ⨅ (i : γ), HomogeneousIdeal.toIdeal (vanishingIdeal (t i))
[PROOFSTEP]
exact HomogeneousIdeal.toIdeal_iInf _
[GOAL]
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
s s' : Set A
⊢ zeroLocus 𝒜 s ∪ zeroLocus 𝒜 s' = zeroLocus 𝒜 ↑(Ideal.span s ⊓ Ideal.span s')
[PROOFSTEP]
rw [zeroLocus_inf]
[GOAL]
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
s s' : Set A
⊢ zeroLocus 𝒜 s ∪ zeroLocus 𝒜 s' = zeroLocus 𝒜 ↑(Ideal.span s) ∪ zeroLocus 𝒜 ↑(Ideal.span s')
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f g : A
x : ProjectiveSpectrum 𝒜
⊢ x ∈ zeroLocus 𝒜 {f * g} ↔ x ∈ zeroLocus 𝒜 {f} ∪ zeroLocus 𝒜 {g}
[PROOFSTEP]
simpa using x.isPrime.mul_mem_iff_mem_or_mem
[GOAL]
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : A
n : ℕ
hn : 0 < n
x : ProjectiveSpectrum 𝒜
⊢ x ∈ zeroLocus 𝒜 {f ^ n} ↔ x ∈ zeroLocus 𝒜 {f}
[PROOFSTEP]
simpa using x.isPrime.pow_mem_iff_mem n hn
[GOAL]
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
t t' : Set (ProjectiveSpectrum 𝒜)
⊢ vanishingIdeal t ⊔ vanishingIdeal t' ≤ vanishingIdeal (t ∩ t')
[PROOFSTEP]
intro r
[GOAL]
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
t t' : Set (ProjectiveSpectrum 𝒜)
r : A
⊢ r ∈ vanishingIdeal t ⊔ vanishingIdeal t' → r ∈ vanishingIdeal (t ∩ t')
[PROOFSTEP]
rw [← HomogeneousIdeal.mem_iff, HomogeneousIdeal.toIdeal_sup, mem_vanishingIdeal, Submodule.mem_sup]
[GOAL]
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
t t' : Set (ProjectiveSpectrum 𝒜)
r : A
⊢ (∃ y,
      y ∈ HomogeneousIdeal.toIdeal (vanishingIdeal t) ∧
        ∃ z, z ∈ HomogeneousIdeal.toIdeal (vanishingIdeal t') ∧ y + z = r) →
    ∀ (x : ProjectiveSpectrum 𝒜), x ∈ t ∩ t' → r ∈ x.asHomogeneousIdeal
[PROOFSTEP]
rintro ⟨f, hf, g, hg, rfl⟩ x ⟨hxt, hxt'⟩
[GOAL]
case intro.intro.intro.intro.intro
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
t t' : Set (ProjectiveSpectrum 𝒜)
f : A
hf : f ∈ HomogeneousIdeal.toIdeal (vanishingIdeal t)
g : A
hg : g ∈ HomogeneousIdeal.toIdeal (vanishingIdeal t')
x : ProjectiveSpectrum 𝒜
hxt : x ∈ t
hxt' : x ∈ t'
⊢ f + g ∈ x.asHomogeneousIdeal
[PROOFSTEP]
erw [mem_vanishingIdeal] at hf hg
[GOAL]
case intro.intro.intro.intro.intro
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
t t' : Set (ProjectiveSpectrum 𝒜)
f : A
hf : ∀ (x : ProjectiveSpectrum 𝒜), x ∈ t → f ∈ x.asHomogeneousIdeal
g : A
hg : ∀ (x : ProjectiveSpectrum 𝒜), x ∈ t' → g ∈ x.asHomogeneousIdeal
x : ProjectiveSpectrum 𝒜
hxt : x ∈ t
hxt' : x ∈ t'
⊢ f + g ∈ x.asHomogeneousIdeal
[PROOFSTEP]
apply Submodule.add_mem
[GOAL]
case intro.intro.intro.intro.intro.h₁
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
t t' : Set (ProjectiveSpectrum 𝒜)
f : A
hf : ∀ (x : ProjectiveSpectrum 𝒜), x ∈ t → f ∈ x.asHomogeneousIdeal
g : A
hg : ∀ (x : ProjectiveSpectrum 𝒜), x ∈ t' → g ∈ x.asHomogeneousIdeal
x : ProjectiveSpectrum 𝒜
hxt : x ∈ t
hxt' : x ∈ t'
⊢ f ∈ HomogeneousIdeal.toIdeal x.asHomogeneousIdeal
[PROOFSTEP]
solve_by_elim
[GOAL]
case intro.intro.intro.intro.intro.h₂
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
t t' : Set (ProjectiveSpectrum 𝒜)
f : A
hf : ∀ (x : ProjectiveSpectrum 𝒜), x ∈ t → f ∈ x.asHomogeneousIdeal
g : A
hg : ∀ (x : ProjectiveSpectrum 𝒜), x ∈ t' → g ∈ x.asHomogeneousIdeal
x : ProjectiveSpectrum 𝒜
hxt : x ∈ t
hxt' : x ∈ t'
⊢ g ∈ HomogeneousIdeal.toIdeal x.asHomogeneousIdeal
[PROOFSTEP]
solve_by_elim
[GOAL]
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : A
I : ProjectiveSpectrum 𝒜
⊢ I ∈ (zeroLocus 𝒜 {f})ᶜ ↔ ¬f ∈ I.asHomogeneousIdeal
[PROOFSTEP]
rw [Set.mem_compl_iff, mem_zeroLocus, Set.singleton_subset_iff]
[GOAL]
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : A
I : ProjectiveSpectrum 𝒜
⊢ ¬f ∈ ↑I.asHomogeneousIdeal ↔ ¬f ∈ I.asHomogeneousIdeal
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
⊢ zeroLocus 𝒜 Set.univ = ∅
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
⊢ ∀ (A_1 : Set (Set (ProjectiveSpectrum 𝒜))), A_1 ⊆ Set.range (zeroLocus 𝒜) → ⋂₀ A_1 ∈ Set.range (zeroLocus 𝒜)
[PROOFSTEP]
intro Zs h
[GOAL]
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
Zs : Set (Set (ProjectiveSpectrum 𝒜))
h : Zs ⊆ Set.range (zeroLocus 𝒜)
⊢ ⋂₀ Zs ∈ Set.range (zeroLocus 𝒜)
[PROOFSTEP]
rw [Set.sInter_eq_iInter]
[GOAL]
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
Zs : Set (Set (ProjectiveSpectrum 𝒜))
h : Zs ⊆ Set.range (zeroLocus 𝒜)
⊢ ⋂ (i : ↑Zs), ↑i ∈ Set.range (zeroLocus 𝒜)
[PROOFSTEP]
let f : Zs → Set _ := fun i => Classical.choose (h i.2)
[GOAL]
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
Zs : Set (Set (ProjectiveSpectrum 𝒜))
h : Zs ⊆ Set.range (zeroLocus 𝒜)
f : ↑Zs → Set A := fun i => Classical.choose (_ : ↑i ∈ Set.range (zeroLocus 𝒜))
⊢ ⋂ (i : ↑Zs), ↑i ∈ Set.range (zeroLocus 𝒜)
[PROOFSTEP]
have H : (Set.iInter fun i ↦ zeroLocus 𝒜 (f i)) ∈ Set.range (zeroLocus 𝒜) := ⟨_, zeroLocus_iUnion 𝒜 _⟩
[GOAL]
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
Zs : Set (Set (ProjectiveSpectrum 𝒜))
h : Zs ⊆ Set.range (zeroLocus 𝒜)
f : ↑Zs → Set A := fun i => Classical.choose (_ : ↑i ∈ Set.range (zeroLocus 𝒜))
H : ⋂ (i : ↑Zs), zeroLocus 𝒜 (f i) ∈ Set.range (zeroLocus 𝒜)
⊢ ⋂ (i : ↑Zs), ↑i ∈ Set.range (zeroLocus 𝒜)
[PROOFSTEP]
convert H using 2
[GOAL]
case h.e'_4.h.e'_3
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
Zs : Set (Set (ProjectiveSpectrum 𝒜))
h : Zs ⊆ Set.range (zeroLocus 𝒜)
f : ↑Zs → Set A := fun i => Classical.choose (_ : ↑i ∈ Set.range (zeroLocus 𝒜))
H : ⋂ (i : ↑Zs), zeroLocus 𝒜 (f i) ∈ Set.range (zeroLocus 𝒜)
⊢ (fun i => ↑i) = fun i => zeroLocus 𝒜 (f i)
[PROOFSTEP]
funext i
[GOAL]
case h.e'_4.h.e'_3.h
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
Zs : Set (Set (ProjectiveSpectrum 𝒜))
h : Zs ⊆ Set.range (zeroLocus 𝒜)
f : ↑Zs → Set A := fun i => Classical.choose (_ : ↑i ∈ Set.range (zeroLocus 𝒜))
H : ⋂ (i : ↑Zs), zeroLocus 𝒜 (f i) ∈ Set.range (zeroLocus 𝒜)
i : ↑Zs
⊢ ↑i = zeroLocus 𝒜 (f i)
[PROOFSTEP]
exact (Classical.choose_spec (h i.2)).symm
[GOAL]
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
⊢ ∀ (A_1 : Set (ProjectiveSpectrum 𝒜)),
    A_1 ∈ Set.range (zeroLocus 𝒜) →
      ∀ (B : Set (ProjectiveSpectrum 𝒜)), B ∈ Set.range (zeroLocus 𝒜) → A_1 ∪ B ∈ Set.range (zeroLocus 𝒜)
[PROOFSTEP]
rintro _ ⟨s, rfl⟩ _ ⟨t, rfl⟩
[GOAL]
case intro.intro
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
s t : Set A
⊢ zeroLocus 𝒜 s ∪ zeroLocus 𝒜 t ∈ Set.range (zeroLocus 𝒜)
[PROOFSTEP]
exact ⟨_, (union_zeroLocus 𝒜 s t).symm⟩
[GOAL]
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
U : Set (ProjectiveSpectrum 𝒜)
⊢ IsOpen U ↔ ∃ s, Uᶜ = zeroLocus 𝒜 s
[PROOFSTEP]
simp only [@eq_comm _ Uᶜ]
[GOAL]
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
U : Set (ProjectiveSpectrum 𝒜)
⊢ IsOpen U ↔ ∃ s, zeroLocus 𝒜 s = Uᶜ
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
Z : Set (ProjectiveSpectrum 𝒜)
⊢ IsClosed Z ↔ ∃ s, Z = zeroLocus 𝒜 s
[PROOFSTEP]
rw [← isOpen_compl_iff, isOpen_iff, compl_compl]
[GOAL]
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
s : Set A
⊢ IsClosed (zeroLocus 𝒜 s)
[PROOFSTEP]
rw [isClosed_iff_zeroLocus]
[GOAL]
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
s : Set A
⊢ ∃ s_1, zeroLocus 𝒜 s = zeroLocus 𝒜 s_1
[PROOFSTEP]
exact ⟨s, rfl⟩
[GOAL]
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
t : Set (ProjectiveSpectrum 𝒜)
⊢ zeroLocus 𝒜 ↑(vanishingIdeal t) = closure t
[PROOFSTEP]
apply Set.Subset.antisymm
[GOAL]
case h₁
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
t : Set (ProjectiveSpectrum 𝒜)
⊢ zeroLocus 𝒜 ↑(vanishingIdeal t) ⊆ closure t
[PROOFSTEP]
rintro x hx t' ⟨ht', ht⟩
[GOAL]
case h₁.intro
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
t : Set (ProjectiveSpectrum 𝒜)
x : ProjectiveSpectrum 𝒜
hx : x ∈ zeroLocus 𝒜 ↑(vanishingIdeal t)
t' : Set (ProjectiveSpectrum 𝒜)
ht' : IsClosed t'
ht : t ⊆ t'
⊢ x ∈ t'
[PROOFSTEP]
obtain ⟨fs, rfl⟩ : ∃ s, t' = zeroLocus 𝒜 s := by rwa [isClosed_iff_zeroLocus] at ht'
[GOAL]
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
t : Set (ProjectiveSpectrum 𝒜)
x : ProjectiveSpectrum 𝒜
hx : x ∈ zeroLocus 𝒜 ↑(vanishingIdeal t)
t' : Set (ProjectiveSpectrum 𝒜)
ht' : IsClosed t'
ht : t ⊆ t'
⊢ ∃ s, t' = zeroLocus 𝒜 s
[PROOFSTEP]
rwa [isClosed_iff_zeroLocus] at ht'
[GOAL]
case h₁.intro.intro
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
t : Set (ProjectiveSpectrum 𝒜)
x : ProjectiveSpectrum 𝒜
hx : x ∈ zeroLocus 𝒜 ↑(vanishingIdeal t)
fs : Set A
ht' : IsClosed (zeroLocus 𝒜 fs)
ht : t ⊆ zeroLocus 𝒜 fs
⊢ x ∈ zeroLocus 𝒜 fs
[PROOFSTEP]
rw [subset_zeroLocus_iff_subset_vanishingIdeal] at ht
[GOAL]
case h₁.intro.intro
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
t : Set (ProjectiveSpectrum 𝒜)
x : ProjectiveSpectrum 𝒜
hx : x ∈ zeroLocus 𝒜 ↑(vanishingIdeal t)
fs : Set A
ht' : IsClosed (zeroLocus 𝒜 fs)
ht : fs ⊆ ↑(vanishingIdeal t)
⊢ x ∈ zeroLocus 𝒜 fs
[PROOFSTEP]
exact Set.Subset.trans ht hx
[GOAL]
case h₂
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
t : Set (ProjectiveSpectrum 𝒜)
⊢ closure t ⊆ zeroLocus 𝒜 ↑(vanishingIdeal t)
[PROOFSTEP]
rw [(isClosed_zeroLocus _ _).closure_subset_iff]
[GOAL]
case h₂
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
t : Set (ProjectiveSpectrum 𝒜)
⊢ t ⊆ zeroLocus 𝒜 ↑(vanishingIdeal t)
[PROOFSTEP]
exact subset_zeroLocus_vanishingIdeal 𝒜 t
[GOAL]
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
t : Set (ProjectiveSpectrum 𝒜)
⊢ vanishingIdeal (closure t) = vanishingIdeal t
[PROOFSTEP]
have := (gc_ideal 𝒜).u_l_u_eq_u t
[GOAL]
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
t : Set (ProjectiveSpectrum 𝒜)
this :
  HomogeneousIdeal.toIdeal (vanishingIdeal (zeroLocus 𝒜 ↑(HomogeneousIdeal.toIdeal (vanishingIdeal t)))) =
    HomogeneousIdeal.toIdeal (vanishingIdeal t)
⊢ vanishingIdeal (closure t) = vanishingIdeal t
[PROOFSTEP]
ext1
[GOAL]
case h
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
t : Set (ProjectiveSpectrum 𝒜)
this :
  HomogeneousIdeal.toIdeal (vanishingIdeal (zeroLocus 𝒜 ↑(HomogeneousIdeal.toIdeal (vanishingIdeal t)))) =
    HomogeneousIdeal.toIdeal (vanishingIdeal t)
⊢ HomogeneousIdeal.toIdeal (vanishingIdeal (closure t)) = HomogeneousIdeal.toIdeal (vanishingIdeal t)
[PROOFSTEP]
erw [zeroLocus_vanishingIdeal_eq_closure 𝒜 t] at this
[GOAL]
case h
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
t : Set (ProjectiveSpectrum 𝒜)
this : HomogeneousIdeal.toIdeal (vanishingIdeal (closure t)) = HomogeneousIdeal.toIdeal (vanishingIdeal t)
⊢ HomogeneousIdeal.toIdeal (vanishingIdeal (closure t)) = HomogeneousIdeal.toIdeal (vanishingIdeal t)
[PROOFSTEP]
exact this
[GOAL]
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
r : A
x : ProjectiveSpectrum 𝒜
⊢ x ∈ ↑(basicOpen 𝒜 r) ↔ x ∈ (zeroLocus 𝒜 {r})ᶜ
[PROOFSTEP]
simp only [Set.mem_compl_iff, mem_zeroLocus, Set.singleton_subset_iff]
[GOAL]
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
r : A
x : ProjectiveSpectrum 𝒜
⊢ x ∈ ↑(basicOpen 𝒜 r) ↔ ¬r ∈ ↑x.asHomogeneousIdeal
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
⊢ ↑(basicOpen 𝒜 1) = ↑⊤
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
⊢ ↑(basicOpen 𝒜 0) = ↑⊥
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f g : A
⊢ ↑(basicOpen 𝒜 (f * g)) = ↑(basicOpen 𝒜 f ⊓ basicOpen 𝒜 g)
[PROOFSTEP]
simp [zeroLocus_singleton_mul]
[GOAL]
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f g : A
⊢ basicOpen 𝒜 (f * g) ≤ basicOpen 𝒜 f
[PROOFSTEP]
rw [basicOpen_mul 𝒜 f g]
[GOAL]
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f g : A
⊢ basicOpen 𝒜 f ⊓ basicOpen 𝒜 g ≤ basicOpen 𝒜 f
[PROOFSTEP]
exact inf_le_left
[GOAL]
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f g : A
⊢ basicOpen 𝒜 (f * g) ≤ basicOpen 𝒜 g
[PROOFSTEP]
rw [basicOpen_mul 𝒜 f g]
[GOAL]
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f g : A
⊢ basicOpen 𝒜 f ⊓ basicOpen 𝒜 g ≤ basicOpen 𝒜 g
[PROOFSTEP]
exact inf_le_right
[GOAL]
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : A
n : ℕ
hn : 0 < n
⊢ ↑(basicOpen 𝒜 (f ^ n)) = ↑(basicOpen 𝒜 f)
[PROOFSTEP]
simpa using zeroLocus_singleton_pow 𝒜 f n hn
[GOAL]
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : A
z : ProjectiveSpectrum 𝒜
⊢ z ∈ ↑(basicOpen 𝒜 f) ↔ z ∈ ↑(⨆ (i : ℕ), basicOpen 𝒜 (↑(GradedAlgebra.proj 𝒜 i) f))
[PROOFSTEP]
erw [mem_coe_basicOpen, TopologicalSpace.Opens.mem_sSup]
[GOAL]
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : A
z : ProjectiveSpectrum 𝒜
⊢ ¬f ∈ z.asHomogeneousIdeal ↔ ∃ u, (u ∈ Set.range fun i => basicOpen 𝒜 (↑(GradedAlgebra.proj 𝒜 i) f)) ∧ z ∈ u
[PROOFSTEP]
constructor
[GOAL]
case mp
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : A
z : ProjectiveSpectrum 𝒜
⊢ ¬f ∈ z.asHomogeneousIdeal → ∃ u, (u ∈ Set.range fun i => basicOpen 𝒜 (↑(GradedAlgebra.proj 𝒜 i) f)) ∧ z ∈ u
[PROOFSTEP]
intro hz
[GOAL]
case mpr
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : A
z : ProjectiveSpectrum 𝒜
⊢ (∃ u, (u ∈ Set.range fun i => basicOpen 𝒜 (↑(GradedAlgebra.proj 𝒜 i) f)) ∧ z ∈ u) → ¬f ∈ z.asHomogeneousIdeal
[PROOFSTEP]
intro hz
[GOAL]
case mp
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : A
z : ProjectiveSpectrum 𝒜
hz : ¬f ∈ z.asHomogeneousIdeal
⊢ ∃ u, (u ∈ Set.range fun i => basicOpen 𝒜 (↑(GradedAlgebra.proj 𝒜 i) f)) ∧ z ∈ u
[PROOFSTEP]
rcases show ∃ i, GradedAlgebra.proj 𝒜 i f ∉ z.asHomogeneousIdeal
    by
    contrapose! hz with H
    classical
    rw [← DirectSum.sum_support_decompose 𝒜 f]
    apply Ideal.sum_mem _ fun i _ => H i with
  ⟨i, hi⟩
[GOAL]
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : A
z : ProjectiveSpectrum 𝒜
hz : ¬f ∈ z.asHomogeneousIdeal
⊢ ∃ i, ¬↑(GradedAlgebra.proj 𝒜 i) f ∈ z.asHomogeneousIdeal
[PROOFSTEP]
contrapose! hz with H
[GOAL]
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : A
z : ProjectiveSpectrum 𝒜
H : ∀ (i : ℕ), ↑(GradedAlgebra.proj 𝒜 i) f ∈ z.asHomogeneousIdeal
⊢ f ∈ z.asHomogeneousIdeal
[PROOFSTEP]
classical
rw [← DirectSum.sum_support_decompose 𝒜 f]
apply Ideal.sum_mem _ fun i _ => H i
[GOAL]
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : A
z : ProjectiveSpectrum 𝒜
H : ∀ (i : ℕ), ↑(GradedAlgebra.proj 𝒜 i) f ∈ z.asHomogeneousIdeal
⊢ f ∈ z.asHomogeneousIdeal
[PROOFSTEP]
rw [← DirectSum.sum_support_decompose 𝒜 f]
[GOAL]
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : A
z : ProjectiveSpectrum 𝒜
H : ∀ (i : ℕ), ↑(GradedAlgebra.proj 𝒜 i) f ∈ z.asHomogeneousIdeal
⊢ ∑ i in DFinsupp.support (↑(decompose 𝒜) f), ↑(↑(↑(decompose 𝒜) f) i) ∈ z.asHomogeneousIdeal
[PROOFSTEP]
apply Ideal.sum_mem _ fun i _ => H i
[GOAL]
case mp.intro
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : A
z : ProjectiveSpectrum 𝒜
hz : ¬f ∈ z.asHomogeneousIdeal
i : ℕ
hi : ¬↑(GradedAlgebra.proj 𝒜 i) f ∈ z.asHomogeneousIdeal
⊢ ∃ u, (u ∈ Set.range fun i => basicOpen 𝒜 (↑(GradedAlgebra.proj 𝒜 i) f)) ∧ z ∈ u
[PROOFSTEP]
exact ⟨basicOpen 𝒜 (GradedAlgebra.proj 𝒜 i f), ⟨i, rfl⟩, by rwa [mem_basicOpen]⟩
[GOAL]
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : A
z : ProjectiveSpectrum 𝒜
hz : ¬f ∈ z.asHomogeneousIdeal
i : ℕ
hi : ¬↑(GradedAlgebra.proj 𝒜 i) f ∈ z.asHomogeneousIdeal
⊢ z ∈ basicOpen 𝒜 (↑(GradedAlgebra.proj 𝒜 i) f)
[PROOFSTEP]
rwa [mem_basicOpen]
[GOAL]
case mpr
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : A
z : ProjectiveSpectrum 𝒜
hz : ∃ u, (u ∈ Set.range fun i => basicOpen 𝒜 (↑(GradedAlgebra.proj 𝒜 i) f)) ∧ z ∈ u
⊢ ¬f ∈ z.asHomogeneousIdeal
[PROOFSTEP]
obtain ⟨_, ⟨i, rfl⟩, hz⟩ := hz
[GOAL]
case mpr.intro.intro.intro
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : A
z : ProjectiveSpectrum 𝒜
i : ℕ
hz : z ∈ (fun i => basicOpen 𝒜 (↑(GradedAlgebra.proj 𝒜 i) f)) i
⊢ ¬f ∈ z.asHomogeneousIdeal
[PROOFSTEP]
exact fun rid => hz (z.1.2 i rid)
[GOAL]
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
⊢ IsTopologicalBasis (Set.range fun r => ↑(basicOpen 𝒜 r))
[PROOFSTEP]
apply TopologicalSpace.isTopologicalBasis_of_open_of_nhds
[GOAL]
case h_open
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
⊢ ∀ (u : Set (ProjectiveSpectrum 𝒜)), (u ∈ Set.range fun r => ↑(basicOpen 𝒜 r)) → IsOpen u
[PROOFSTEP]
rintro _ ⟨r, rfl⟩
[GOAL]
case h_open.intro
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
r : A
⊢ IsOpen ((fun r => ↑(basicOpen 𝒜 r)) r)
[PROOFSTEP]
exact isOpen_basicOpen 𝒜
[GOAL]
case h_nhds
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
⊢ ∀ (a : ProjectiveSpectrum 𝒜) (u : Set (ProjectiveSpectrum 𝒜)),
    a ∈ u → IsOpen u → ∃ v, (v ∈ Set.range fun r => ↑(basicOpen 𝒜 r)) ∧ a ∈ v ∧ v ⊆ u
[PROOFSTEP]
rintro p U hp ⟨s, hs⟩
[GOAL]
case h_nhds.intro
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
p : ProjectiveSpectrum 𝒜
U : Set (ProjectiveSpectrum 𝒜)
hp : p ∈ U
s : Set A
hs : zeroLocus 𝒜 s = Uᶜ
⊢ ∃ v, (v ∈ Set.range fun r => ↑(basicOpen 𝒜 r)) ∧ p ∈ v ∧ v ⊆ U
[PROOFSTEP]
rw [← compl_compl U, Set.mem_compl_iff, ← hs, mem_zeroLocus, Set.not_subset] at hp
[GOAL]
case h_nhds.intro
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
p : ProjectiveSpectrum 𝒜
U : Set (ProjectiveSpectrum 𝒜)
s : Set A
hp : ∃ a, a ∈ s ∧ ¬a ∈ ↑p.asHomogeneousIdeal
hs : zeroLocus 𝒜 s = Uᶜ
⊢ ∃ v, (v ∈ Set.range fun r => ↑(basicOpen 𝒜 r)) ∧ p ∈ v ∧ v ⊆ U
[PROOFSTEP]
obtain ⟨f, hfs, hfp⟩ := hp
[GOAL]
case h_nhds.intro.intro.intro
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
p : ProjectiveSpectrum 𝒜
U : Set (ProjectiveSpectrum 𝒜)
s : Set A
hs : zeroLocus 𝒜 s = Uᶜ
f : A
hfs : f ∈ s
hfp : ¬f ∈ ↑p.asHomogeneousIdeal
⊢ ∃ v, (v ∈ Set.range fun r => ↑(basicOpen 𝒜 r)) ∧ p ∈ v ∧ v ⊆ U
[PROOFSTEP]
refine' ⟨basicOpen 𝒜 f, ⟨f, rfl⟩, hfp, _⟩
[GOAL]
case h_nhds.intro.intro.intro
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
p : ProjectiveSpectrum 𝒜
U : Set (ProjectiveSpectrum 𝒜)
s : Set A
hs : zeroLocus 𝒜 s = Uᶜ
f : A
hfs : f ∈ s
hfp : ¬f ∈ ↑p.asHomogeneousIdeal
⊢ ↑(basicOpen 𝒜 f) ⊆ U
[PROOFSTEP]
rw [← Set.compl_subset_compl, ← hs, basicOpen_eq_zeroLocus_compl, compl_compl]
[GOAL]
case h_nhds.intro.intro.intro
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
p : ProjectiveSpectrum 𝒜
U : Set (ProjectiveSpectrum 𝒜)
s : Set A
hs : zeroLocus 𝒜 s = Uᶜ
f : A
hfs : f ∈ s
hfp : ¬f ∈ ↑p.asHomogeneousIdeal
⊢ zeroLocus 𝒜 s ⊆ zeroLocus 𝒜 {f}
[PROOFSTEP]
exact zeroLocus_anti_mono 𝒜 (Set.singleton_subset_iff.mpr hfs)
[GOAL]
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
x✝¹ x✝ : ProjectiveSpectrum 𝒜
asHomogeneousIdeal✝¹ : HomogeneousIdeal 𝒜
isPrime✝¹ : Ideal.IsPrime (HomogeneousIdeal.toIdeal asHomogeneousIdeal✝¹)
not_irrelevant_le✝¹ : ¬HomogeneousIdeal.irrelevant 𝒜 ≤ asHomogeneousIdeal✝¹
asHomogeneousIdeal✝ : HomogeneousIdeal 𝒜
isPrime✝ : Ideal.IsPrime (HomogeneousIdeal.toIdeal asHomogeneousIdeal✝)
not_irrelevant_le✝ : ¬HomogeneousIdeal.irrelevant 𝒜 ≤ asHomogeneousIdeal✝
⊢ { asHomogeneousIdeal := asHomogeneousIdeal✝¹, isPrime := isPrime✝¹,
          not_irrelevant_le := not_irrelevant_le✝¹ }.asHomogeneousIdeal =
      { asHomogeneousIdeal := asHomogeneousIdeal✝, isPrime := isPrime✝,
          not_irrelevant_le := not_irrelevant_le✝ }.asHomogeneousIdeal →
    { asHomogeneousIdeal := asHomogeneousIdeal✝¹, isPrime := isPrime✝¹, not_irrelevant_le := not_irrelevant_le✝¹ } =
      { asHomogeneousIdeal := asHomogeneousIdeal✝, isPrime := isPrime✝, not_irrelevant_le := not_irrelevant_le✝ }
[PROOFSTEP]
simp only [mk.injEq, imp_self]
[GOAL]
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
x y : ProjectiveSpectrum 𝒜
⊢ x ≤ y ↔ y ∈ closure {x}
[PROOFSTEP]
rw [← as_ideal_le_as_ideal, ← zeroLocus_vanishingIdeal_eq_closure, mem_zeroLocus, vanishingIdeal_singleton]
[GOAL]
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
x y : ProjectiveSpectrum 𝒜
⊢ x.asHomogeneousIdeal ≤ y.asHomogeneousIdeal ↔ ↑x.asHomogeneousIdeal ⊆ ↑y.asHomogeneousIdeal
[PROOFSTEP]
simp only [as_ideal_le_as_ideal, coe_subset_coe]


[GOAL]
k : Type u
inst✝¹ : Field k
G : Type u
inst✝ : Monoid G
V : FdRep k G
g h : G
⊢ character V (h * g) = character V (g * h)
[PROOFSTEP]
simp only [trace_mul_comm, character, map_mul]
[GOAL]
k : Type u
inst✝¹ : Field k
G : Type u
inst✝ : Monoid G
V : FdRep k G
⊢ character V 1 = ↑(finrank k (CoeSort.coe V))
[PROOFSTEP]
simp only [character, map_one, trace_one]
[GOAL]
k : Type u
inst✝¹ : Field k
G : Type u
inst✝ : Monoid G
V W : FdRep k G
⊢ character (V ⊗ W) = character V * character W
[PROOFSTEP]
ext g
[GOAL]
case h
k : Type u
inst✝¹ : Field k
G : Type u
inst✝ : Monoid G
V W : FdRep k G
g : G
⊢ character (V ⊗ W) g = (character V * character W) g
[PROOFSTEP]
convert trace_tensorProduct' (V.ρ g) (W.ρ g)
[GOAL]
k : Type u
inst✝¹ : Field k
G : Type u
inst✝ : Monoid G
V W : FdRep k G
⊢ character
      (Action.FunctorCategoryEquivalence.inverse.obj
        (Action.FunctorCategoryEquivalence.functor.obj V ⊗ Action.FunctorCategoryEquivalence.functor.obj W)) =
    character V * character W
[PROOFSTEP]
simp [← char_tensor]
[GOAL]
k : Type u
inst✝¹ : Field k
G : Type u
inst✝ : Monoid G
V W : FdRep k G
i : V ≅ W
⊢ character V = character W
[PROOFSTEP]
ext g
[GOAL]
case h
k : Type u
inst✝¹ : Field k
G : Type u
inst✝ : Monoid G
V W : FdRep k G
i : V ≅ W
g : G
⊢ character V g = character W g
[PROOFSTEP]
simp only [character, FdRep.Iso.conj_ρ i]
[GOAL]
case h
k : Type u
inst✝¹ : Field k
G : Type u
inst✝ : Monoid G
V W : FdRep k G
i : V ≅ W
g : G
⊢ ↑(trace k (CoeSort.coe V)) (↑(ρ V) g) =
    ↑(trace k (CoeSort.coe W)) (↑(LinearEquiv.conj (isoToLinearEquiv i)) (↑(ρ V) g))
[PROOFSTEP]
exact (trace_conj' (V.ρ g) _).symm
[GOAL]
k : Type u
inst✝¹ : Field k
G : Type u
inst✝ : Group G
V : FdRep k G
g h : G
⊢ character V (h * g * h⁻¹) = character V g
[PROOFSTEP]
rw [char_mul_comm, inv_mul_cancel_left]
[GOAL]
k : Type u
inst✝¹ : Field k
G : Type u
inst✝ : Group G
V W : FdRep k G
g : G
⊢ character (of (linHom (ρ V) (ρ W))) g = character V g⁻¹ * character W g
[PROOFSTEP]
rw [← char_iso (dualTensorIsoLinHom _ _), char_tensor, Pi.mul_apply, char_dual]
[GOAL]
k : Type u
inst✝³ : Field k
G : Type u
inst✝² : Group G
inst✝¹ : Fintype G
inst✝ : Invertible ↑(Fintype.card G)
V : FdRep k G
⊢ ⅟↑(Fintype.card G) • ∑ g : G, character V g = ↑(finrank k { x // x ∈ invariants (ρ V) })
[PROOFSTEP]
erw [← (isProj_averageMap V.ρ).trace]
  -- Porting note: Changed `rw` to `erw`
[GOAL]
k : Type u
inst✝³ : Field k
G : Type u
inst✝² : Group G
inst✝¹ : Fintype G
inst✝ : Invertible ↑(Fintype.card G)
V : FdRep k G
⊢ ⅟↑(Fintype.card G) • ∑ g : G, character V g = ↑(trace k (CoeSort.coe V)) (averageMap (ρ V))
[PROOFSTEP]
simp [character, GroupAlgebra.average, _root_.map_sum]
[GOAL]
k : Type u
inst✝⁵ : Field k
G : GroupCat
inst✝⁴ : IsAlgClosed k
inst✝³ : Fintype ↑G
inst✝² : Invertible ↑(Fintype.card ↑G)
V W : FdRep k ↑G
inst✝¹ : Simple V
inst✝ : Simple W
⊢ ⅟↑(Fintype.card ↑G) • ∑ g : ↑G, character V g * character W g⁻¹ = if Nonempty (V ≅ W) then 1 else 0
[PROOFSTEP]
conv_lhs =>
  enter [2, 2, g]
  rw [mul_comm, ← char_dual, ← Pi.mul_apply, ← char_tensor]
  rw [char_iso (FdRep.dualTensorIsoLinHom W.ρ V)]
    -- The average over the group of the character of a representation equals the dimension of the
      -- space of invariants.
[GOAL]
k : Type u
inst✝⁵ : Field k
G : GroupCat
inst✝⁴ : IsAlgClosed k
inst✝³ : Fintype ↑G
inst✝² : Invertible ↑(Fintype.card ↑G)
V W : FdRep k ↑G
inst✝¹ : Simple V
inst✝ : Simple W
| ⅟↑(Fintype.card ↑G) • ∑ g : ↑G, character V g * character W g⁻¹
[PROOFSTEP]
  enter [2, 2, g]
  rw [mul_comm, ← char_dual, ← Pi.mul_apply, ← char_tensor]
  rw [char_iso (FdRep.dualTensorIsoLinHom W.ρ V)]
    -- The average over the group of the character of a representation equals the dimension of the
      -- space of invariants.
[GOAL]
k : Type u
inst✝⁵ : Field k
G : GroupCat
inst✝⁴ : IsAlgClosed k
inst✝³ : Fintype ↑G
inst✝² : Invertible ↑(Fintype.card ↑G)
V W : FdRep k ↑G
inst✝¹ : Simple V
inst✝ : Simple W
| ⅟↑(Fintype.card ↑G) • ∑ g : ↑G, character V g * character W g⁻¹
[PROOFSTEP]
  enter [2, 2, g]
  rw [mul_comm, ← char_dual, ← Pi.mul_apply, ← char_tensor]
  rw [char_iso (FdRep.dualTensorIsoLinHom W.ρ V)]
    -- The average over the group of the character of a representation equals the dimension of the
      -- space of invariants.
[GOAL]
k : Type u
inst✝⁵ : Field k
G : GroupCat
inst✝⁴ : IsAlgClosed k
inst✝³ : Fintype ↑G
inst✝² : Invertible ↑(Fintype.card ↑G)
V W : FdRep k ↑G
inst✝¹ : Simple V
inst✝ : Simple W
| ⅟↑(Fintype.card ↑G) • ∑ g : ↑G, character V g * character W g⁻¹
[PROOFSTEP]
enter [2, 2, g]
[GOAL]
case h
k : Type u
inst✝⁵ : Field k
G : GroupCat
inst✝⁴ : IsAlgClosed k
inst✝³ : Fintype ↑G
inst✝² : Invertible ↑(Fintype.card ↑G)
V W : FdRep k ↑G
inst✝¹ : Simple V
inst✝ : Simple W
g : ↑G
| character V g * character W g⁻¹
[PROOFSTEP]
rw [mul_comm, ← char_dual, ← Pi.mul_apply, ← char_tensor]
[GOAL]
case h
k : Type u
inst✝⁵ : Field k
G : GroupCat
inst✝⁴ : IsAlgClosed k
inst✝³ : Fintype ↑G
inst✝² : Invertible ↑(Fintype.card ↑G)
V W : FdRep k ↑G
inst✝¹ : Simple V
inst✝ : Simple W
g : ↑G
| character (of (dual (ρ W)) ⊗ V) g
[PROOFSTEP]
rw [char_iso (FdRep.dualTensorIsoLinHom W.ρ V)]
  -- The average over the group of the character of a representation equals the dimension of the
    -- space of invariants.
[GOAL]
k : Type u
inst✝⁵ : Field k
G : GroupCat
inst✝⁴ : IsAlgClosed k
inst✝³ : Fintype ↑G
inst✝² : Invertible ↑(Fintype.card ↑G)
V W : FdRep k ↑G
inst✝¹ : Simple V
inst✝ : Simple W
⊢ ⅟↑(Fintype.card ↑G) • ∑ g : ↑G, character (of (linHom (ρ W) (ρ V))) g = if Nonempty (V ≅ W) then 1 else 0
[PROOFSTEP]
rw [average_char_eq_finrank_invariants]
[GOAL]
k : Type u
inst✝⁵ : Field k
G : GroupCat
inst✝⁴ : IsAlgClosed k
inst✝³ : Fintype ↑G
inst✝² : Invertible ↑(Fintype.card ↑G)
V W : FdRep k ↑G
inst✝¹ : Simple V
inst✝ : Simple W
⊢ ↑(finrank k { x // x ∈ invariants (ρ (of (linHom (ρ W) (ρ V)))) }) = if Nonempty (V ≅ W) then 1 else 0
[PROOFSTEP]
rw [show (of (linHom W.ρ V.ρ)).ρ = linHom W.ρ V.ρ from FdRep.of_ρ (linHom W.ρ V.ρ)]
  -- The space of invariants of `Hom(W, V)` is the subspace of `G`-equivariant linear maps,
    -- `Hom_G(W, V)`.
[GOAL]
k : Type u
inst✝⁵ : Field k
G : GroupCat
inst✝⁴ : IsAlgClosed k
inst✝³ : Fintype ↑G
inst✝² : Invertible ↑(Fintype.card ↑G)
V W : FdRep k ↑G
inst✝¹ : Simple V
inst✝ : Simple W
⊢ ↑(finrank k { x // x ∈ invariants (linHom (ρ W) (ρ V)) }) = if Nonempty (V ≅ W) then 1 else 0
[PROOFSTEP]
erw [(linHom.invariantsEquivFdRepHom W V).finrank_eq]
  -- Porting note: Changed `rw` to `erw`
    -- By Schur's Lemma, the dimension of `Hom_G(W, V)` is `1` is `V ≅ W` and `0` otherwise.
[GOAL]
k : Type u
inst✝⁵ : Field k
G : GroupCat
inst✝⁴ : IsAlgClosed k
inst✝³ : Fintype ↑G
inst✝² : Invertible ↑(Fintype.card ↑G)
V W : FdRep k ↑G
inst✝¹ : Simple V
inst✝ : Simple W
⊢ ↑(finrank k (W ⟶ V)) = if Nonempty (V ≅ W) then 1 else 0
[PROOFSTEP]
rw_mod_cast [finrank_hom_simple_simple W V, Iso.nonempty_iso_symm]