[GOAL]
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
k : ℕ
h : ∀ (i : ℕ), i < k + 1 → coeff x i = 0
⊢ ↑verschiebung (shift x (Nat.succ k)) = shift x k
[PROOFSTEP]
ext ⟨j⟩
[GOAL]
case h.zero
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
k : ℕ
h : ∀ (i : ℕ), i < k + 1 → coeff x i = 0
⊢ coeff (↑verschiebung (shift x (Nat.succ k))) Nat.zero = coeff (shift x k) Nat.zero
[PROOFSTEP]
rw [verschiebung_coeff_zero, shift_coeff, h]
[GOAL]
case h.zero.a
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
k : ℕ
h : ∀ (i : ℕ), i < k + 1 → coeff x i = 0
⊢ k + Nat.zero < k + 1
[PROOFSTEP]
apply Nat.lt_succ_self
[GOAL]
case h.succ
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
k : ℕ
h : ∀ (i : ℕ), i < k + 1 → coeff x i = 0
n✝ : ℕ
⊢ coeff (↑verschiebung (shift x (Nat.succ k))) (Nat.succ n✝) = coeff (shift x k) (Nat.succ n✝)
[PROOFSTEP]
simp only [verschiebung_coeff_succ, shift]
[GOAL]
case h.succ
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
k : ℕ
h : ∀ (i : ℕ), i < k + 1 → coeff x i = 0
n✝ : ℕ
⊢ coeff x (Nat.succ k + n✝) = coeff x (k + Nat.succ n✝)
[PROOFSTEP]
congr 1
[GOAL]
case h.succ.e_a
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
k : ℕ
h : ∀ (i : ℕ), i < k + 1 → coeff x i = 0
n✝ : ℕ
⊢ Nat.succ k + n✝ = k + Nat.succ n✝
[PROOFSTEP]
rw [Nat.add_succ, add_comm, Nat.add_succ, add_comm]
[GOAL]
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
n : ℕ
h : ∀ (i : ℕ), i < n → coeff x i = 0
⊢ x = (↑verschiebung)^[n] (shift x n)
[PROOFSTEP]
induction' n with k ih
[GOAL]
case zero
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
n : ℕ
h✝ : ∀ (i : ℕ), i < n → coeff x i = 0
h : ∀ (i : ℕ), i < Nat.zero → coeff x i = 0
⊢ x = (↑verschiebung)^[Nat.zero] (shift x Nat.zero)
[PROOFSTEP]
cases x
[GOAL]
case zero.mk'
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
n : ℕ
coeff✝ : ℕ → R
h✝ : ∀ (i : ℕ), i < n → coeff { coeff := coeff✝ } i = 0
h : ∀ (i : ℕ), i < Nat.zero → coeff { coeff := coeff✝ } i = 0
⊢ { coeff := coeff✝ } = (↑verschiebung)^[Nat.zero] (shift { coeff := coeff✝ } Nat.zero)
[PROOFSTEP]
simp [shift]
[GOAL]
case succ
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
n : ℕ
h✝ : ∀ (i : ℕ), i < n → coeff x i = 0
k : ℕ
ih : (∀ (i : ℕ), i < k → coeff x i = 0) → x = (↑verschiebung)^[k] (shift x k)
h : ∀ (i : ℕ), i < Nat.succ k → coeff x i = 0
⊢ x = (↑verschiebung)^[Nat.succ k] (shift x (Nat.succ k))
[PROOFSTEP]
dsimp
[GOAL]
case succ
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
n : ℕ
h✝ : ∀ (i : ℕ), i < n → coeff x i = 0
k : ℕ
ih : (∀ (i : ℕ), i < k → coeff x i = 0) → x = (↑verschiebung)^[k] (shift x k)
h : ∀ (i : ℕ), i < Nat.succ k → coeff x i = 0
⊢ x = (↑verschiebung)^[k] (↑verschiebung (shift x (Nat.succ k)))
[PROOFSTEP]
rw [verschiebung_shift]
[GOAL]
case succ
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
n : ℕ
h✝ : ∀ (i : ℕ), i < n → coeff x i = 0
k : ℕ
ih : (∀ (i : ℕ), i < k → coeff x i = 0) → x = (↑verschiebung)^[k] (shift x k)
h : ∀ (i : ℕ), i < Nat.succ k → coeff x i = 0
⊢ x = (↑verschiebung)^[k] (shift x k)
[PROOFSTEP]
exact ih fun i hi => h _ (hi.trans (Nat.lt_succ_self _))
[GOAL]
case succ.h
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
n : ℕ
h✝ : ∀ (i : ℕ), i < n → coeff x i = 0
k : ℕ
ih : (∀ (i : ℕ), i < k → coeff x i = 0) → x = (↑verschiebung)^[k] (shift x k)
h : ∀ (i : ℕ), i < Nat.succ k → coeff x i = 0
⊢ ∀ (i : ℕ), i < k + 1 → coeff x i = 0
[PROOFSTEP]
exact h
[GOAL]
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
hx : x ≠ 0
⊢ ∃ n x', coeff x' 0 ≠ 0 ∧ x = (↑verschiebung)^[n] x'
[PROOFSTEP]
have hex : ∃ k : ℕ, x.coeff k ≠ 0 := by
  by_contra' hall
  apply hx
  ext i
  simp only [hall, zero_coeff]
[GOAL]
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
hx : x ≠ 0
⊢ ∃ k, coeff x k ≠ 0
[PROOFSTEP]
by_contra' hall
[GOAL]
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
hx : x ≠ 0
hall : ∀ (k : ℕ), coeff x k = 0
⊢ False
[PROOFSTEP]
apply hx
[GOAL]
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
hx : x ≠ 0
hall : ∀ (k : ℕ), coeff x k = 0
⊢ x = 0
[PROOFSTEP]
ext i
[GOAL]
case h
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
hx : x ≠ 0
hall : ∀ (k : ℕ), coeff x k = 0
i : ℕ
⊢ coeff x i = coeff 0 i
[PROOFSTEP]
simp only [hall, zero_coeff]
[GOAL]
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
hx : x ≠ 0
hex : ∃ k, coeff x k ≠ 0
⊢ ∃ n x', coeff x' 0 ≠ 0 ∧ x = (↑verschiebung)^[n] x'
[PROOFSTEP]
let n := Nat.find hex
[GOAL]
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
hx : x ≠ 0
hex : ∃ k, coeff x k ≠ 0
n : ℕ := Nat.find hex
⊢ ∃ n x', coeff x' 0 ≠ 0 ∧ x = (↑verschiebung)^[n] x'
[PROOFSTEP]
use n, x.shift n
[GOAL]
case h
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
hx : x ≠ 0
hex : ∃ k, coeff x k ≠ 0
n : ℕ := Nat.find hex
⊢ coeff (shift x n) 0 ≠ 0 ∧ x = (↑verschiebung)^[n] (shift x n)
[PROOFSTEP]
refine' ⟨Nat.find_spec hex, eq_iterate_verschiebung fun i hi => not_not.mp _⟩
[GOAL]
case h
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
hx : x ≠ 0
hex : ∃ k, coeff x k ≠ 0
n : ℕ := Nat.find hex
i : ℕ
hi : i < n
⊢ ¬¬coeff x i = 0
[PROOFSTEP]
exact Nat.find_min hex hi
[GOAL]
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝² : CommRing R
inst✝¹ : CharP R p
inst✝ : NoZeroDivisors R
x y : 𝕎 R
⊢ x * y = 0 → x = 0 ∨ y = 0
[PROOFSTEP]
contrapose!
[GOAL]
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝² : CommRing R
inst✝¹ : CharP R p
inst✝ : NoZeroDivisors R
x y : 𝕎 R
⊢ x ≠ 0 ∧ y ≠ 0 → x * y ≠ 0
[PROOFSTEP]
rintro ⟨ha, hb⟩
[GOAL]
case intro
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝² : CommRing R
inst✝¹ : CharP R p
inst✝ : NoZeroDivisors R
x y : 𝕎 R
ha : x ≠ 0
hb : y ≠ 0
⊢ x * y ≠ 0
[PROOFSTEP]
rcases verschiebung_nonzero ha with ⟨na, wa, hwa0, rfl⟩
[GOAL]
case intro.intro.intro.intro
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝² : CommRing R
inst✝¹ : CharP R p
inst✝ : NoZeroDivisors R
y : 𝕎 R
hb : y ≠ 0
na : ℕ
wa : 𝕎 R
hwa0 : coeff wa 0 ≠ 0
ha : (↑verschiebung)^[na] wa ≠ 0
⊢ (↑verschiebung)^[na] wa * y ≠ 0
[PROOFSTEP]
rcases verschiebung_nonzero hb with ⟨nb, wb, hwb0, rfl⟩
[GOAL]
case intro.intro.intro.intro.intro.intro.intro
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝² : CommRing R
inst✝¹ : CharP R p
inst✝ : NoZeroDivisors R
na : ℕ
wa : 𝕎 R
hwa0 : coeff wa 0 ≠ 0
ha : (↑verschiebung)^[na] wa ≠ 0
nb : ℕ
wb : 𝕎 R
hwb0 : coeff wb 0 ≠ 0
hb : (↑verschiebung)^[nb] wb ≠ 0
⊢ (↑verschiebung)^[na] wa * (↑verschiebung)^[nb] wb ≠ 0
[PROOFSTEP]
refine' ne_of_apply_ne (fun x => x.coeff (na + nb)) _
[GOAL]
case intro.intro.intro.intro.intro.intro.intro
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝² : CommRing R
inst✝¹ : CharP R p
inst✝ : NoZeroDivisors R
na : ℕ
wa : 𝕎 R
hwa0 : coeff wa 0 ≠ 0
ha : (↑verschiebung)^[na] wa ≠ 0
nb : ℕ
wb : 𝕎 R
hwb0 : coeff wb 0 ≠ 0
hb : (↑verschiebung)^[nb] wb ≠ 0
⊢ (fun x => coeff x (na + nb)) ((↑verschiebung)^[na] wa * (↑verschiebung)^[nb] wb) ≠ (fun x => coeff x (na + nb)) 0
[PROOFSTEP]
dsimp only
[GOAL]
case intro.intro.intro.intro.intro.intro.intro
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝² : CommRing R
inst✝¹ : CharP R p
inst✝ : NoZeroDivisors R
na : ℕ
wa : 𝕎 R
hwa0 : coeff wa 0 ≠ 0
ha : (↑verschiebung)^[na] wa ≠ 0
nb : ℕ
wb : 𝕎 R
hwb0 : coeff wb 0 ≠ 0
hb : (↑verschiebung)^[nb] wb ≠ 0
⊢ coeff ((↑verschiebung)^[na] wa * (↑verschiebung)^[nb] wb) (na + nb) ≠ coeff 0 (na + nb)
[PROOFSTEP]
rw [iterate_verschiebung_mul_coeff, zero_coeff]
[GOAL]
case intro.intro.intro.intro.intro.intro.intro
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝² : CommRing R
inst✝¹ : CharP R p
inst✝ : NoZeroDivisors R
na : ℕ
wa : 𝕎 R
hwa0 : coeff wa 0 ≠ 0
ha : (↑verschiebung)^[na] wa ≠ 0
nb : ℕ
wb : 𝕎 R
hwb0 : coeff wb 0 ≠ 0
hb : (↑verschiebung)^[nb] wb ≠ 0
⊢ coeff wa 0 ^ p ^ nb * coeff wb 0 ^ p ^ na ≠ 0
[PROOFSTEP]
exact mul_ne_zero (pow_ne_zero _ hwa0) (pow_ne_zero _ hwb0)


[GOAL]
ι : Type u_1
σ : Type u_2
R : Type u_3
A : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : SetLike σ A
inst✝³ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : GradedRing 𝒜
I : Ideal A
x✝¹ x✝ : HomogeneousIdeal 𝒜
x : Submodule A A
hx : Ideal.IsHomogeneous 𝒜 x
y : Submodule A A
hy : Ideal.IsHomogeneous 𝒜 y
h : x = y
⊢ { toSubmodule := x, is_homogeneous' := hx } = { toSubmodule := y, is_homogeneous' := hy }
[PROOFSTEP]
simp [h]
[GOAL]
ι : Type u_1
σ : Type u_2
R : Type u_3
A : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : SetLike σ A
inst✝³ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : GradedRing 𝒜
I✝ I : Ideal A
r x : A
hx₁ : Homogeneous 𝒜 x
hx₂ : x ∈ I
j : ι
⊢ ↑(GradedRing.proj 𝒜 j) (r * x) ∈ I
[PROOFSTEP]
classical
rw [← DirectSum.sum_support_decompose 𝒜 r, Finset.sum_mul, map_sum]
apply Ideal.sum_mem
intro k _
obtain ⟨i, hi⟩ := hx₁
have mem₁ : (DirectSum.decompose 𝒜 r k : A) * x ∈ 𝒜 (k + i) := GradedMul.mul_mem (SetLike.coe_mem _) hi
erw [GradedRing.proj_apply, DirectSum.decompose_of_mem 𝒜 mem₁, coe_of_apply]
split_ifs
· exact I.mul_mem_left _ hx₂
· exact I.zero_mem
[GOAL]
ι : Type u_1
σ : Type u_2
R : Type u_3
A : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : SetLike σ A
inst✝³ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : GradedRing 𝒜
I✝ I : Ideal A
r x : A
hx₁ : Homogeneous 𝒜 x
hx₂ : x ∈ I
j : ι
⊢ ↑(GradedRing.proj 𝒜 j) (r * x) ∈ I
[PROOFSTEP]
rw [← DirectSum.sum_support_decompose 𝒜 r, Finset.sum_mul, map_sum]
[GOAL]
ι : Type u_1
σ : Type u_2
R : Type u_3
A : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : SetLike σ A
inst✝³ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : GradedRing 𝒜
I✝ I : Ideal A
r x : A
hx₁ : Homogeneous 𝒜 x
hx₂ : x ∈ I
j : ι
⊢ ∑ x_1 in DFinsupp.support (↑(decompose 𝒜) r), ↑(GradedRing.proj 𝒜 j) (↑(↑(↑(decompose 𝒜) r) x_1) * x) ∈ I
[PROOFSTEP]
apply Ideal.sum_mem
[GOAL]
case a
ι : Type u_1
σ : Type u_2
R : Type u_3
A : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : SetLike σ A
inst✝³ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : GradedRing 𝒜
I✝ I : Ideal A
r x : A
hx₁ : Homogeneous 𝒜 x
hx₂ : x ∈ I
j : ι
⊢ ∀ (c : ι), c ∈ DFinsupp.support (↑(decompose 𝒜) r) → ↑(GradedRing.proj 𝒜 j) (↑(↑(↑(decompose 𝒜) r) c) * x) ∈ I
[PROOFSTEP]
intro k _
[GOAL]
case a
ι : Type u_1
σ : Type u_2
R : Type u_3
A : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : SetLike σ A
inst✝³ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : GradedRing 𝒜
I✝ I : Ideal A
r x : A
hx₁ : Homogeneous 𝒜 x
hx₂ : x ∈ I
j k : ι
a✝ : k ∈ DFinsupp.support (↑(decompose 𝒜) r)
⊢ ↑(GradedRing.proj 𝒜 j) (↑(↑(↑(decompose 𝒜) r) k) * x) ∈ I
[PROOFSTEP]
obtain ⟨i, hi⟩ := hx₁
[GOAL]
case a.intro
ι : Type u_1
σ : Type u_2
R : Type u_3
A : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : SetLike σ A
inst✝³ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : GradedRing 𝒜
I✝ I : Ideal A
r x : A
hx₂ : x ∈ I
j k : ι
a✝ : k ∈ DFinsupp.support (↑(decompose 𝒜) r)
i : ι
hi : x ∈ 𝒜 i
⊢ ↑(GradedRing.proj 𝒜 j) (↑(↑(↑(decompose 𝒜) r) k) * x) ∈ I
[PROOFSTEP]
have mem₁ : (DirectSum.decompose 𝒜 r k : A) * x ∈ 𝒜 (k + i) := GradedMul.mul_mem (SetLike.coe_mem _) hi
[GOAL]
case a.intro
ι : Type u_1
σ : Type u_2
R : Type u_3
A : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : SetLike σ A
inst✝³ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : GradedRing 𝒜
I✝ I : Ideal A
r x : A
hx₂ : x ∈ I
j k : ι
a✝ : k ∈ DFinsupp.support (↑(decompose 𝒜) r)
i : ι
hi : x ∈ 𝒜 i
mem₁ : ↑(↑(↑(decompose 𝒜) r) k) * x ∈ 𝒜 (k + i)
⊢ ↑(GradedRing.proj 𝒜 j) (↑(↑(↑(decompose 𝒜) r) k) * x) ∈ I
[PROOFSTEP]
erw [GradedRing.proj_apply, DirectSum.decompose_of_mem 𝒜 mem₁, coe_of_apply]
[GOAL]
case a.intro
ι : Type u_1
σ : Type u_2
R : Type u_3
A : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : SetLike σ A
inst✝³ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : GradedRing 𝒜
I✝ I : Ideal A
r x : A
hx₂ : x ∈ I
j k : ι
a✝ : k ∈ DFinsupp.support (↑(decompose 𝒜) r)
i : ι
hi : x ∈ 𝒜 i
mem₁ : ↑(↑(↑(decompose 𝒜) r) k) * x ∈ 𝒜 (k + i)
⊢ ↑(if k + i = j then { val := ↑(↑(↑(decompose 𝒜) r) k) * x, property := mem₁ } else 0) ∈ I
[PROOFSTEP]
split_ifs
[GOAL]
case pos
ι : Type u_1
σ : Type u_2
R : Type u_3
A : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : SetLike σ A
inst✝³ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : GradedRing 𝒜
I✝ I : Ideal A
r x : A
hx₂ : x ∈ I
j k : ι
a✝ : k ∈ DFinsupp.support (↑(decompose 𝒜) r)
i : ι
hi : x ∈ 𝒜 i
mem₁ : ↑(↑(↑(decompose 𝒜) r) k) * x ∈ 𝒜 (k + i)
h✝ : k + i = j
⊢ ↑{ val := ↑(↑(↑(decompose 𝒜) r) k) * x, property := mem₁ } ∈ I
[PROOFSTEP]
exact I.mul_mem_left _ hx₂
[GOAL]
case neg
ι : Type u_1
σ : Type u_2
R : Type u_3
A : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : SetLike σ A
inst✝³ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : GradedRing 𝒜
I✝ I : Ideal A
r x : A
hx₂ : x ∈ I
j k : ι
a✝ : k ∈ DFinsupp.support (↑(decompose 𝒜) r)
i : ι
hi : x ∈ 𝒜 i
mem₁ : ↑(↑(↑(decompose 𝒜) r) k) * x ∈ 𝒜 (k + i)
h✝ : ¬k + i = j
⊢ ↑0 ∈ I
[PROOFSTEP]
exact I.zero_mem
[GOAL]
ι : Type u_1
σ : Type u_2
R : Type u_3
A : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : SetLike σ A
inst✝³ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : GradedRing 𝒜
I : Ideal A
s : Set A
h : ∀ (x : A), x ∈ s → Homogeneous 𝒜 x
⊢ IsHomogeneous 𝒜 (span s)
[PROOFSTEP]
rintro i r hr
[GOAL]
ι : Type u_1
σ : Type u_2
R : Type u_3
A : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : SetLike σ A
inst✝³ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : GradedRing 𝒜
I : Ideal A
s : Set A
h : ∀ (x : A), x ∈ s → Homogeneous 𝒜 x
i : ι
r : A
hr : r ∈ span s
⊢ ↑(↑(↑(decompose 𝒜) r) i) ∈ span s
[PROOFSTEP]
rw [Ideal.span, Finsupp.span_eq_range_total] at hr
[GOAL]
ι : Type u_1
σ : Type u_2
R : Type u_3
A : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : SetLike σ A
inst✝³ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : GradedRing 𝒜
I : Ideal A
s : Set A
h : ∀ (x : A), x ∈ s → Homogeneous 𝒜 x
i : ι
r : A
hr : r ∈ LinearMap.range (Finsupp.total (↑s) A A Subtype.val)
⊢ ↑(↑(↑(decompose 𝒜) r) i) ∈ span s
[PROOFSTEP]
rw [LinearMap.mem_range] at hr
[GOAL]
ι : Type u_1
σ : Type u_2
R : Type u_3
A : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : SetLike σ A
inst✝³ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : GradedRing 𝒜
I : Ideal A
s : Set A
h : ∀ (x : A), x ∈ s → Homogeneous 𝒜 x
i : ι
r : A
hr : ∃ y, ↑(Finsupp.total (↑s) A A Subtype.val) y = r
⊢ ↑(↑(↑(decompose 𝒜) r) i) ∈ span s
[PROOFSTEP]
obtain ⟨s, rfl⟩ := hr
[GOAL]
case intro
ι : Type u_1
σ : Type u_2
R : Type u_3
A : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : SetLike σ A
inst✝³ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : GradedRing 𝒜
I : Ideal A
s✝ : Set A
h : ∀ (x : A), x ∈ s✝ → Homogeneous 𝒜 x
i : ι
s : ↑s✝ →₀ A
⊢ ↑(↑(↑(decompose 𝒜) (↑(Finsupp.total (↑s✝) A A Subtype.val) s)) i) ∈ span s✝
[PROOFSTEP]
rw [Finsupp.total_apply, Finsupp.sum, decompose_sum, DFinsupp.finset_sum_apply, AddSubmonoidClass.coe_finset_sum]
[GOAL]
case intro
ι : Type u_1
σ : Type u_2
R : Type u_3
A : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : SetLike σ A
inst✝³ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : GradedRing 𝒜
I : Ideal A
s✝ : Set A
h : ∀ (x : A), x ∈ s✝ → Homogeneous 𝒜 x
i : ι
s : ↑s✝ →₀ A
⊢ ∑ i_1 in s.support, ↑(↑(↑(decompose 𝒜) (↑s i_1 • ↑i_1)) i) ∈ span s✝
[PROOFSTEP]
refine' Ideal.sum_mem _ _
[GOAL]
case intro
ι : Type u_1
σ : Type u_2
R : Type u_3
A : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : SetLike σ A
inst✝³ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : GradedRing 𝒜
I : Ideal A
s✝ : Set A
h : ∀ (x : A), x ∈ s✝ → Homogeneous 𝒜 x
i : ι
s : ↑s✝ →₀ A
⊢ ∀ (c : ↑s✝), c ∈ s.support → ↑(↑(↑(decompose 𝒜) (↑s c • ↑c)) i) ∈ span s✝
[PROOFSTEP]
rintro z hz1
[GOAL]
case intro
ι : Type u_1
σ : Type u_2
R : Type u_3
A : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : SetLike σ A
inst✝³ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : GradedRing 𝒜
I : Ideal A
s✝ : Set A
h : ∀ (x : A), x ∈ s✝ → Homogeneous 𝒜 x
i : ι
s : ↑s✝ →₀ A
z : ↑s✝
hz1 : z ∈ s.support
⊢ ↑(↑(↑(decompose 𝒜) (↑s z • ↑z)) i) ∈ span s✝
[PROOFSTEP]
rw [smul_eq_mul]
[GOAL]
case intro
ι : Type u_1
σ : Type u_2
R : Type u_3
A : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : SetLike σ A
inst✝³ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : GradedRing 𝒜
I : Ideal A
s✝ : Set A
h : ∀ (x : A), x ∈ s✝ → Homogeneous 𝒜 x
i : ι
s : ↑s✝ →₀ A
z : ↑s✝
hz1 : z ∈ s.support
⊢ ↑(↑(↑(decompose 𝒜) (↑s z * ↑z)) i) ∈ span s✝
[PROOFSTEP]
refine' Ideal.mul_homogeneous_element_mem_of_mem 𝒜 (s z) z _ _ i
[GOAL]
case intro.refine'_1
ι : Type u_1
σ : Type u_2
R : Type u_3
A : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : SetLike σ A
inst✝³ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : GradedRing 𝒜
I : Ideal A
s✝ : Set A
h : ∀ (x : A), x ∈ s✝ → Homogeneous 𝒜 x
i : ι
s : ↑s✝ →₀ A
z : ↑s✝
hz1 : z ∈ s.support
⊢ Homogeneous 𝒜 ↑z
[PROOFSTEP]
rcases z with ⟨z, hz2⟩
[GOAL]
case intro.refine'_1.mk
ι : Type u_1
σ : Type u_2
R : Type u_3
A : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : SetLike σ A
inst✝³ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : GradedRing 𝒜
I : Ideal A
s✝ : Set A
h : ∀ (x : A), x ∈ s✝ → Homogeneous 𝒜 x
i : ι
s : ↑s✝ →₀ A
z : A
hz2 : z ∈ s✝
hz1 : { val := z, property := hz2 } ∈ s.support
⊢ Homogeneous 𝒜 ↑{ val := z, property := hz2 }
[PROOFSTEP]
apply h _ hz2
[GOAL]
case intro.refine'_2
ι : Type u_1
σ : Type u_2
R : Type u_3
A : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : SetLike σ A
inst✝³ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : GradedRing 𝒜
I : Ideal A
s✝ : Set A
h : ∀ (x : A), x ∈ s✝ → Homogeneous 𝒜 x
i : ι
s : ↑s✝ →₀ A
z : ↑s✝
hz1 : z ∈ s.support
⊢ ↑z ∈ span s✝
[PROOFSTEP]
exact Ideal.subset_span z.2
[GOAL]
ι : Type u_1
σ : Type u_2
R : Type u_3
A : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : SetLike σ A
inst✝³ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : GradedRing 𝒜
I : Ideal A
h : IsHomogeneous 𝒜 I
⊢ HomogeneousIdeal.toIdeal (homogeneousCore 𝒜 I) = I
[PROOFSTEP]
apply le_antisymm (I.homogeneousCore'_le 𝒜) _
[GOAL]
ι : Type u_1
σ : Type u_2
R : Type u_3
A : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : SetLike σ A
inst✝³ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : GradedRing 𝒜
I : Ideal A
h : IsHomogeneous 𝒜 I
⊢ I ≤ homogeneousCore' 𝒜 I
[PROOFSTEP]
intro x hx
[GOAL]
ι : Type u_1
σ : Type u_2
R : Type u_3
A : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : SetLike σ A
inst✝³ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : GradedRing 𝒜
I : Ideal A
h : IsHomogeneous 𝒜 I
x : A
hx : x ∈ I
⊢ x ∈ homogeneousCore' 𝒜 I
[PROOFSTEP]
classical
rw [← DirectSum.sum_support_decompose 𝒜 x]
exact Ideal.sum_mem _ fun j _ => Ideal.subset_span ⟨⟨_, homogeneous_coe _⟩, h _ hx, rfl⟩
[GOAL]
ι : Type u_1
σ : Type u_2
R : Type u_3
A : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : SetLike σ A
inst✝³ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : GradedRing 𝒜
I : Ideal A
h : IsHomogeneous 𝒜 I
x : A
hx : x ∈ I
⊢ x ∈ homogeneousCore' 𝒜 I
[PROOFSTEP]
rw [← DirectSum.sum_support_decompose 𝒜 x]
[GOAL]
ι : Type u_1
σ : Type u_2
R : Type u_3
A : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : SetLike σ A
inst✝³ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : GradedRing 𝒜
I : Ideal A
h : IsHomogeneous 𝒜 I
x : A
hx : x ∈ I
⊢ ∑ i in DFinsupp.support (↑(decompose 𝒜) x), ↑(↑(↑(decompose 𝒜) x) i) ∈ homogeneousCore' 𝒜 I
[PROOFSTEP]
exact Ideal.sum_mem _ fun j _ => Ideal.subset_span ⟨⟨_, homogeneous_coe _⟩, h _ hx, rfl⟩
[GOAL]
ι : Type u_1
σ : Type u_2
R : Type u_3
A : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : SetLike σ A
inst✝³ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : GradedRing 𝒜
I✝ : Ideal A
I : HomogeneousIdeal 𝒜
⊢ Ideal.homogeneousCore 𝒜 (toIdeal I) = I
[PROOFSTEP]
ext1
[GOAL]
case h
ι : Type u_1
σ : Type u_2
R : Type u_3
A : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : SetLike σ A
inst✝³ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : GradedRing 𝒜
I✝ : Ideal A
I : HomogeneousIdeal 𝒜
⊢ toIdeal (Ideal.homogeneousCore 𝒜 (toIdeal I)) = toIdeal I
[PROOFSTEP]
convert Ideal.IsHomogeneous.toIdeal_homogeneousCore_eq_self I.isHomogeneous
[GOAL]
ι : Type u_1
σ : Type u_2
R : Type u_3
A : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : SetLike σ A
inst✝³ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : GradedRing 𝒜
I : Ideal A
⊢ IsHomogeneous 𝒜 I ↔ ∃ S, I = span (Subtype.val '' S)
[PROOFSTEP]
rw [Ideal.IsHomogeneous.iff_eq, eq_comm]
[GOAL]
ι : Type u_1
σ : Type u_2
R : Type u_3
A : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : SetLike σ A
inst✝³ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : GradedRing 𝒜
I : Ideal A
⊢ I = HomogeneousIdeal.toIdeal (homogeneousCore 𝒜 I) ↔ ∃ S, I = span (Subtype.val '' S)
[PROOFSTEP]
exact ((Set.image_preimage.compose (Submodule.gi _ _).gc).exists_eq_l _).symm
[GOAL]
ι : Type u_1
σ : Type u_2
R : Type u_3
A : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
i : ι
r : A
hr : r ∈ ⊥
⊢ ↑(↑(↑(decompose 𝒜) r) i) ∈ ⊥
[PROOFSTEP]
simp only [Ideal.mem_bot] at hr
[GOAL]
ι : Type u_1
σ : Type u_2
R : Type u_3
A : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
i : ι
r : A
hr : r = 0
⊢ ↑(↑(↑(decompose 𝒜) r) i) ∈ ⊥
[PROOFSTEP]
rw [hr, decompose_zero, zero_apply]
[GOAL]
ι : Type u_1
σ : Type u_2
R : Type u_3
A : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
i : ι
r : A
hr : r = 0
⊢ ↑0 ∈ ⊥
[PROOFSTEP]
apply Ideal.zero_mem
[GOAL]
ι : Type u_1
σ : Type u_2
R : Type u_3
A : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
i : ι
r : A
x✝ : r ∈ ⊤
⊢ ↑(↑(↑(decompose 𝒜) r) i) ∈ ⊤
[PROOFSTEP]
simp only [Submodule.mem_top]
[GOAL]
ι : Type u_1
σ : Type u_2
R : Type u_3
A : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I J : Ideal A
HI : IsHomogeneous 𝒜 I
HJ : IsHomogeneous 𝒜 J
⊢ IsHomogeneous 𝒜 (I ⊔ J)
[PROOFSTEP]
rw [iff_exists] at HI HJ ⊢
[GOAL]
ι : Type u_1
σ : Type u_2
R : Type u_3
A : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I J : Ideal A
HI : ∃ S, I = span (Subtype.val '' S)
HJ : ∃ S, J = span (Subtype.val '' S)
⊢ ∃ S, I ⊔ J = span (Subtype.val '' S)
[PROOFSTEP]
obtain ⟨⟨s₁, rfl⟩, ⟨s₂, rfl⟩⟩ := HI, HJ
[GOAL]
case intro.intro
ι : Type u_1
σ : Type u_2
R : Type u_3
A : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
s₁ s₂ : Set { x // x ∈ homogeneousSubmonoid 𝒜 }
⊢ ∃ S, span (Subtype.val '' s₁) ⊔ span (Subtype.val '' s₂) = span (Subtype.val '' S)
[PROOFSTEP]
refine' ⟨s₁ ∪ s₂, _⟩
[GOAL]
case intro.intro
ι : Type u_1
σ : Type u_2
R : Type u_3
A : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
s₁ s₂ : Set { x // x ∈ homogeneousSubmonoid 𝒜 }
⊢ span (Subtype.val '' s₁) ⊔ span (Subtype.val '' s₂) = span (Subtype.val '' (s₁ ∪ s₂))
[PROOFSTEP]
rw [Set.image_union]
[GOAL]
case intro.intro
ι : Type u_1
σ : Type u_2
R : Type u_3
A : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
s₁ s₂ : Set { x // x ∈ homogeneousSubmonoid 𝒜 }
⊢ span (Subtype.val '' s₁) ⊔ span (Subtype.val '' s₂) = span (Subtype.val '' s₁ ∪ Subtype.val '' s₂)
[PROOFSTEP]
exact (Submodule.span_union _ _).symm
[GOAL]
ι : Type u_1
σ : Type u_2
R : Type u_3
A : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
κ : Sort u_5
f : κ → Ideal A
h : ∀ (i : κ), IsHomogeneous 𝒜 (f i)
⊢ IsHomogeneous 𝒜 (⨆ (i : κ), f i)
[PROOFSTEP]
simp_rw [iff_exists] at h ⊢
[GOAL]
ι : Type u_1
σ : Type u_2
R : Type u_3
A : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
κ : Sort u_5
f : κ → Ideal A
h : ∀ (i : κ), ∃ S, f i = span (Subtype.val '' S)
⊢ ∃ S, ⨆ (i : κ), f i = span (Subtype.val '' S)
[PROOFSTEP]
choose s hs using h
[GOAL]
ι : Type u_1
σ : Type u_2
R : Type u_3
A : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
κ : Sort u_5
f : κ → Ideal A
s : κ → Set { x // x ∈ homogeneousSubmonoid 𝒜 }
hs : ∀ (i : κ), f i = span (Subtype.val '' s i)
⊢ ∃ S, ⨆ (i : κ), f i = span (Subtype.val '' S)
[PROOFSTEP]
refine' ⟨⋃ i, s i, _⟩
[GOAL]
ι : Type u_1
σ : Type u_2
R : Type u_3
A : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
κ : Sort u_5
f : κ → Ideal A
s : κ → Set { x // x ∈ homogeneousSubmonoid 𝒜 }
hs : ∀ (i : κ), f i = span (Subtype.val '' s i)
⊢ ⨆ (i : κ), f i = span (Subtype.val '' ⋃ (i : κ), s i)
[PROOFSTEP]
simp_rw [Set.image_iUnion, Ideal.span_iUnion]
[GOAL]
ι : Type u_1
σ : Type u_2
R : Type u_3
A : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
κ : Sort u_5
f : κ → Ideal A
s : κ → Set { x // x ∈ homogeneousSubmonoid 𝒜 }
hs : ∀ (i : κ), f i = span (Subtype.val '' s i)
⊢ ⨆ (i : κ), f i = ⨆ (i : κ), span (Subtype.val '' s i)
[PROOFSTEP]
congr
[GOAL]
case e_s
ι : Type u_1
σ : Type u_2
R : Type u_3
A : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
κ : Sort u_5
f : κ → Ideal A
s : κ → Set { x // x ∈ homogeneousSubmonoid 𝒜 }
hs : ∀ (i : κ), f i = span (Subtype.val '' s i)
⊢ (fun i => f i) = fun i => span (Subtype.val '' s i)
[PROOFSTEP]
exact funext hs
[GOAL]
ι : Type u_1
σ : Type u_2
R : Type u_3
A : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
κ : Sort u_5
f : κ → Ideal A
h : ∀ (i : κ), IsHomogeneous 𝒜 (f i)
⊢ IsHomogeneous 𝒜 (⨅ (i : κ), f i)
[PROOFSTEP]
intro i x hx
[GOAL]
ι : Type u_1
σ : Type u_2
R : Type u_3
A : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
κ : Sort u_5
f : κ → Ideal A
h : ∀ (i : κ), IsHomogeneous 𝒜 (f i)
i : ι
x : A
hx : x ∈ ⨅ (i : κ), f i
⊢ ↑(↑(↑(decompose 𝒜) x) i) ∈ ⨅ (i : κ), f i
[PROOFSTEP]
simp only [Ideal.mem_iInf] at hx ⊢
[GOAL]
ι : Type u_1
σ : Type u_2
R : Type u_3
A : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
κ : Sort u_5
f : κ → Ideal A
h : ∀ (i : κ), IsHomogeneous 𝒜 (f i)
i : ι
x : A
hx : ∀ (i : κ), x ∈ f i
⊢ ∀ (i_1 : κ), ↑(↑(↑(decompose 𝒜) x) i) ∈ f i_1
[PROOFSTEP]
exact fun j => h _ _ (hx j)
[GOAL]
ι : Type u_1
σ : Type u_2
R : Type u_3
A : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
ℐ : Set (Ideal A)
h : ∀ (I : Ideal A), I ∈ ℐ → IsHomogeneous 𝒜 I
⊢ IsHomogeneous 𝒜 (SupSet.sSup ℐ)
[PROOFSTEP]
rw [sSup_eq_iSup]
[GOAL]
ι : Type u_1
σ : Type u_2
R : Type u_3
A : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
ℐ : Set (Ideal A)
h : ∀ (I : Ideal A), I ∈ ℐ → IsHomogeneous 𝒜 I
⊢ IsHomogeneous 𝒜 (⨆ (a : Ideal A) (_ : a ∈ ℐ), a)
[PROOFSTEP]
exact iSup₂ h
[GOAL]
ι : Type u_1
σ : Type u_2
R : Type u_3
A : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
ℐ : Set (Ideal A)
h : ∀ (I : Ideal A), I ∈ ℐ → IsHomogeneous 𝒜 I
⊢ IsHomogeneous 𝒜 (InfSet.sInf ℐ)
[PROOFSTEP]
rw [sInf_eq_iInf]
[GOAL]
ι : Type u_1
σ : Type u_2
R : Type u_3
A : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
ℐ : Set (Ideal A)
h : ∀ (I : Ideal A), I ∈ ℐ → IsHomogeneous 𝒜 I
⊢ IsHomogeneous 𝒜 (⨅ (a : Ideal A) (_ : a ∈ ℐ), a)
[PROOFSTEP]
exact iInf₂ h
[GOAL]
ι : Type u_1
σ : Type u_2
R : Type u_3
A : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
κ : Sort u_5
s : κ → HomogeneousIdeal 𝒜
⊢ toIdeal (⨆ (i : κ), s i) = ⨆ (i : κ), toIdeal (s i)
[PROOFSTEP]
rw [iSup, toIdeal_sSup, iSup_range]
[GOAL]
ι : Type u_1
σ : Type u_2
R : Type u_3
A : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
κ : Sort u_5
s : κ → HomogeneousIdeal 𝒜
⊢ toIdeal (⨅ (i : κ), s i) = ⨅ (i : κ), toIdeal (s i)
[PROOFSTEP]
rw [iInf, toIdeal_sInf, iInf_range]
[GOAL]
ι : Type u_1
σ : Type u_2
R : Type u_3
A : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
κ : Sort u_5
κ' : κ → Sort u_6
s : (i : κ) → κ' i → HomogeneousIdeal 𝒜
⊢ toIdeal (⨆ (i : κ) (j : κ' i), s i j) = ⨆ (i : κ) (j : κ' i), toIdeal (s i j)
[PROOFSTEP]
simp_rw [toIdeal_iSup]
[GOAL]
ι : Type u_1
σ : Type u_2
R : Type u_3
A : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
κ : Sort u_5
κ' : κ → Sort u_6
s : (i : κ) → κ' i → HomogeneousIdeal 𝒜
⊢ toIdeal (⨅ (i : κ) (j : κ' i), s i j) = ⨅ (i : κ) (j : κ' i), toIdeal (s i j)
[PROOFSTEP]
simp_rw [toIdeal_iInf]
[GOAL]
ι : Type u_1
σ : Type u_2
R : Type u_3
A : Type u_4
inst✝⁵ : CommSemiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I✝ I J : Ideal A
HI : IsHomogeneous 𝒜 I
HJ : IsHomogeneous 𝒜 J
⊢ IsHomogeneous 𝒜 (I * J)
[PROOFSTEP]
rw [Ideal.IsHomogeneous.iff_exists] at HI HJ ⊢
[GOAL]
ι : Type u_1
σ : Type u_2
R : Type u_3
A : Type u_4
inst✝⁵ : CommSemiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I✝ I J : Ideal A
HI : ∃ S, I = span (Subtype.val '' S)
HJ : ∃ S, J = span (Subtype.val '' S)
⊢ ∃ S, I * J = span (Subtype.val '' S)
[PROOFSTEP]
obtain ⟨⟨s₁, rfl⟩, ⟨s₂, rfl⟩⟩ := HI, HJ
[GOAL]
case intro.intro
ι : Type u_1
σ : Type u_2
R : Type u_3
A : Type u_4
inst✝⁵ : CommSemiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
s₁ s₂ : Set { x // x ∈ homogeneousSubmonoid 𝒜 }
⊢ ∃ S, span (Subtype.val '' s₁) * span (Subtype.val '' s₂) = span (Subtype.val '' S)
[PROOFSTEP]
rw [Ideal.span_mul_span']
[GOAL]
case intro.intro
ι : Type u_1
σ : Type u_2
R : Type u_3
A : Type u_4
inst✝⁵ : CommSemiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
s₁ s₂ : Set { x // x ∈ homogeneousSubmonoid 𝒜 }
⊢ ∃ S, span (Subtype.val '' s₁ * Subtype.val '' s₂) = span (Subtype.val '' S)
[PROOFSTEP]
exact ⟨s₁ * s₂, congr_arg _ <| (Set.image_mul (homogeneousSubmonoid 𝒜).subtype).symm⟩
[GOAL]
ι : Type u_1
σ : Type u_2
R : Type u_3
A : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
⊢ homogeneousCore' 𝒜 I = sSup {J | IsHomogeneous 𝒜 J ∧ J ≤ I}
[PROOFSTEP]
refine' (IsLUB.sSup_eq _).symm
[GOAL]
ι : Type u_1
σ : Type u_2
R : Type u_3
A : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
⊢ IsLUB {J | IsHomogeneous 𝒜 J ∧ J ≤ I} (homogeneousCore' 𝒜 I)
[PROOFSTEP]
apply IsGreatest.isLUB
[GOAL]
case h
ι : Type u_1
σ : Type u_2
R : Type u_3
A : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
⊢ IsGreatest {J | IsHomogeneous 𝒜 J ∧ J ≤ I} (homogeneousCore' 𝒜 I)
[PROOFSTEP]
have coe_mono : Monotone (toIdeal : HomogeneousIdeal 𝒜 → Ideal A) := fun x y => id
[GOAL]
case h
ι : Type u_1
σ : Type u_2
R : Type u_3
A : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
coe_mono : Monotone toIdeal
⊢ IsGreatest {J | IsHomogeneous 𝒜 J ∧ J ≤ I} (homogeneousCore' 𝒜 I)
[PROOFSTEP]
convert coe_mono.map_isGreatest (Ideal.homogeneousCore.gc 𝒜).isGreatest_u using 1
[GOAL]
case h.e'_3
ι : Type u_1
σ : Type u_2
R : Type u_3
A : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
coe_mono : Monotone toIdeal
⊢ {J | IsHomogeneous 𝒜 J ∧ J ≤ I} = toIdeal '' {a | toIdeal a ≤ I}
[PROOFSTEP]
ext x
[GOAL]
case h.e'_3.h
ι : Type u_1
σ : Type u_2
R : Type u_3
A : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
coe_mono : Monotone toIdeal
x : Ideal A
⊢ x ∈ {J | IsHomogeneous 𝒜 J ∧ J ≤ I} ↔ x ∈ toIdeal '' {a | toIdeal a ≤ I}
[PROOFSTEP]
rw [mem_image, mem_setOf_eq]
[GOAL]
case h.e'_3.h
ι : Type u_1
σ : Type u_2
R : Type u_3
A : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
coe_mono : Monotone toIdeal
x : Ideal A
⊢ IsHomogeneous 𝒜 x ∧ x ≤ I ↔ ∃ x_1, x_1 ∈ {a | toIdeal a ≤ I} ∧ toIdeal x_1 = x
[PROOFSTEP]
refine' ⟨fun hI => ⟨⟨x, hI.1⟩, ⟨hI.2, rfl⟩⟩, _⟩
[GOAL]
case h.e'_3.h
ι : Type u_1
σ : Type u_2
R : Type u_3
A : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
coe_mono : Monotone toIdeal
x : Ideal A
⊢ (∃ x_1, x_1 ∈ {a | toIdeal a ≤ I} ∧ toIdeal x_1 = x) → IsHomogeneous 𝒜 x ∧ x ≤ I
[PROOFSTEP]
rintro ⟨x, ⟨hx, rfl⟩⟩
[GOAL]
case h.e'_3.h.intro.intro
ι : Type u_1
σ : Type u_2
R : Type u_3
A : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
coe_mono : Monotone toIdeal
x : HomogeneousIdeal 𝒜
hx : x ∈ {a | toIdeal a ≤ I}
⊢ IsHomogeneous 𝒜 (toIdeal x) ∧ toIdeal x ≤ I
[PROOFSTEP]
exact ⟨x.isHomogeneous, hx⟩
[GOAL]
ι : Type u_1
σ : Type u_2
R : Type u_3
A : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
⊢ IsHomogeneous 𝒜 (span {r | ∃ i x, ↑(↑(↑(decompose 𝒜) ↑x) i) = r})
[PROOFSTEP]
refine' Ideal.homogeneous_span _ _ fun x hx => _
[GOAL]
ι : Type u_1
σ : Type u_2
R : Type u_3
A : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
x : A
hx : x ∈ {r | ∃ i x, ↑(↑(↑(decompose 𝒜) ↑x) i) = r}
⊢ Homogeneous 𝒜 x
[PROOFSTEP]
obtain ⟨i, x, rfl⟩ := hx
[GOAL]
case intro.intro
ι : Type u_1
σ : Type u_2
R : Type u_3
A : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
i : ι
x : { x // x ∈ I }
⊢ Homogeneous 𝒜 ↑(↑(↑(decompose 𝒜) ↑x) i)
[PROOFSTEP]
apply SetLike.homogeneous_coe
[GOAL]
ι : Type u_1
σ : Type u_2
R : Type u_3
A : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
⊢ I ≤ toIdeal (homogeneousHull 𝒜 I)
[PROOFSTEP]
intro r hr
[GOAL]
ι : Type u_1
σ : Type u_2
R : Type u_3
A : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
r : A
hr : r ∈ I
⊢ r ∈ toIdeal (homogeneousHull 𝒜 I)
[PROOFSTEP]
classical
rw [← DirectSum.sum_support_decompose 𝒜 r]
refine' Ideal.sum_mem _ _
intro j _
apply Ideal.subset_span
use j
use⟨r, hr⟩
[GOAL]
ι : Type u_1
σ : Type u_2
R : Type u_3
A : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
r : A
hr : r ∈ I
⊢ r ∈ toIdeal (homogeneousHull 𝒜 I)
[PROOFSTEP]
rw [← DirectSum.sum_support_decompose 𝒜 r]
[GOAL]
ι : Type u_1
σ : Type u_2
R : Type u_3
A : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
r : A
hr : r ∈ I
⊢ ∑ i in DFinsupp.support (↑(decompose 𝒜) r), ↑(↑(↑(decompose 𝒜) r) i) ∈ toIdeal (homogeneousHull 𝒜 I)
[PROOFSTEP]
refine' Ideal.sum_mem _ _
[GOAL]
ι : Type u_1
σ : Type u_2
R : Type u_3
A : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
r : A
hr : r ∈ I
⊢ ∀ (c : ι), c ∈ DFinsupp.support (↑(decompose 𝒜) r) → ↑(↑(↑(decompose 𝒜) r) c) ∈ toIdeal (homogeneousHull 𝒜 I)
[PROOFSTEP]
intro j _
[GOAL]
ι : Type u_1
σ : Type u_2
R : Type u_3
A : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
r : A
hr : r ∈ I
j : ι
a✝ : j ∈ DFinsupp.support (↑(decompose 𝒜) r)
⊢ ↑(↑(↑(decompose 𝒜) r) j) ∈ toIdeal (homogeneousHull 𝒜 I)
[PROOFSTEP]
apply Ideal.subset_span
[GOAL]
case a
ι : Type u_1
σ : Type u_2
R : Type u_3
A : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
r : A
hr : r ∈ I
j : ι
a✝ : j ∈ DFinsupp.support (↑(decompose 𝒜) r)
⊢ ↑(↑(↑(decompose 𝒜) r) j) ∈ {r | ∃ i x, ↑(↑(↑(decompose 𝒜) ↑x) i) = r}
[PROOFSTEP]
use j
[GOAL]
case h
ι : Type u_1
σ : Type u_2
R : Type u_3
A : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
r : A
hr : r ∈ I
j : ι
a✝ : j ∈ DFinsupp.support (↑(decompose 𝒜) r)
⊢ ∃ x, ↑(↑(↑(decompose 𝒜) ↑x) j) = ↑(↑(↑(decompose 𝒜) r) j)
[PROOFSTEP]
use⟨r, hr⟩
[GOAL]
ι : Type u_1
σ : Type u_2
R : Type u_3
A : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I✝ I J : Ideal A
I_le_J : I ≤ J
⊢ homogeneousHull 𝒜 I ≤ homogeneousHull 𝒜 J
[PROOFSTEP]
apply Ideal.span_mono
[GOAL]
case a
ι : Type u_1
σ : Type u_2
R : Type u_3
A : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I✝ I J : Ideal A
I_le_J : I ≤ J
⊢ {r | ∃ i x, ↑(↑(↑(decompose 𝒜) ↑x) i) = r} ⊆ {r | ∃ i x, ↑(↑(↑(decompose 𝒜) ↑x) i) = r}
[PROOFSTEP]
rintro r ⟨hr1, ⟨x, hx⟩, rfl⟩
[GOAL]
case a.intro.intro.mk
ι : Type u_1
σ : Type u_2
R : Type u_3
A : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I✝ I J : Ideal A
I_le_J : I ≤ J
hr1 : ι
x : A
hx : x ∈ I
⊢ ↑(↑(↑(decompose 𝒜) ↑{ val := x, property := hx }) hr1) ∈ {r | ∃ i x, ↑(↑(↑(decompose 𝒜) ↑x) i) = r}
[PROOFSTEP]
refine' ⟨hr1, ⟨⟨x, I_le_J hx⟩, rfl⟩⟩
[GOAL]
ι : Type u_1
σ : Type u_2
R : Type u_3
A : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
h : IsHomogeneous 𝒜 I
⊢ toIdeal (homogeneousHull 𝒜 I) = I
[PROOFSTEP]
apply le_antisymm _ (Ideal.le_toIdeal_homogeneousHull _ _)
[GOAL]
ι : Type u_1
σ : Type u_2
R : Type u_3
A : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
h : IsHomogeneous 𝒜 I
⊢ toIdeal (homogeneousHull 𝒜 I) ≤ I
[PROOFSTEP]
apply Ideal.span_le.2
[GOAL]
ι : Type u_1
σ : Type u_2
R : Type u_3
A : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
h : IsHomogeneous 𝒜 I
⊢ {r | ∃ i x, ↑(↑(↑(decompose 𝒜) ↑x) i) = r} ⊆ ↑I
[PROOFSTEP]
rintro _ ⟨i, x, rfl⟩
[GOAL]
case intro.intro
ι : Type u_1
σ : Type u_2
R : Type u_3
A : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
h : IsHomogeneous 𝒜 I
i : ι
x : { x // x ∈ I }
⊢ ↑(↑(↑(decompose 𝒜) ↑x) i) ∈ ↑I
[PROOFSTEP]
exact h _ x.prop
[GOAL]
ι : Type u_1
σ : Type u_2
R : Type u_3
A : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
⊢ toIdeal (homogeneousHull 𝒜 I) = ⨆ (i : ι), span (↑(GradedRing.proj 𝒜 i) '' ↑I)
[PROOFSTEP]
rw [← Ideal.span_iUnion]
[GOAL]
ι : Type u_1
σ : Type u_2
R : Type u_3
A : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
⊢ toIdeal (homogeneousHull 𝒜 I) = span (⋃ (i : ι), ↑(GradedRing.proj 𝒜 i) '' ↑I)
[PROOFSTEP]
apply congr_arg Ideal.span _
[GOAL]
ι : Type u_1
σ : Type u_2
R : Type u_3
A : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
⊢ {r | ∃ i x, ↑(↑(↑(decompose 𝒜) ↑x) i) = r} = ⋃ (i : ι), ↑(GradedRing.proj 𝒜 i) '' ↑I
[PROOFSTEP]
ext1
[GOAL]
case h
ι : Type u_1
σ : Type u_2
R : Type u_3
A : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
x✝ : A
⊢ x✝ ∈ {r | ∃ i x, ↑(↑(↑(decompose 𝒜) ↑x) i) = r} ↔ x✝ ∈ ⋃ (i : ι), ↑(GradedRing.proj 𝒜 i) '' ↑I
[PROOFSTEP]
simp only [Set.mem_iUnion, Set.mem_image, mem_setOf_eq, GradedRing.proj_apply, SetLike.exists, exists_prop,
  Subtype.coe_mk, SetLike.mem_coe]
[GOAL]
ι : Type u_1
σ : Type u_2
R : Type u_3
A : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
i : ι
⊢ ∀ (x : A), x ∈ ↑(GradedRing.proj 𝒜 i) '' ↑I → Homogeneous 𝒜 x
[PROOFSTEP]
rintro _ ⟨x, -, rfl⟩
[GOAL]
case intro.intro
ι : Type u_1
σ : Type u_2
R : Type u_3
A : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
i : ι
x : A
⊢ Homogeneous 𝒜 (↑(GradedRing.proj 𝒜 i) x)
[PROOFSTEP]
apply SetLike.homogeneous_coe
[GOAL]
ι : Type u_1
σ : Type u_2
R : Type u_3
A : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
⊢ homogeneousHull 𝒜 I =
    ⨆ (i : ι),
      { toSubmodule := span (↑(GradedRing.proj 𝒜 i) '' ↑I),
        is_homogeneous' := (_ : IsHomogeneous 𝒜 (span (↑(GradedRing.proj 𝒜 i) '' ↑I))) }
[PROOFSTEP]
ext1
[GOAL]
case h
ι : Type u_1
σ : Type u_2
R : Type u_3
A : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
⊢ toIdeal (homogeneousHull 𝒜 I) =
    toIdeal
      (⨆ (i : ι),
        { toSubmodule := span (↑(GradedRing.proj 𝒜 i) '' ↑I),
          is_homogeneous' := (_ : IsHomogeneous 𝒜 (span (↑(GradedRing.proj 𝒜 i) '' ↑I))) })
[PROOFSTEP]
rw [Ideal.toIdeal_homogeneousHull_eq_iSup, toIdeal_iSup]
[GOAL]
case h
ι : Type u_1
σ : Type u_2
R : Type u_3
A : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
⊢ ⨆ (i : ι), span (↑(GradedRing.proj 𝒜 i) '' ↑I) =
    ⨆ (i : ι),
      toIdeal
        { toSubmodule := span (↑(GradedRing.proj 𝒜 i) '' ↑I),
          is_homogeneous' := (_ : IsHomogeneous 𝒜 (span (↑(GradedRing.proj 𝒜 i) '' ↑I))) }
[PROOFSTEP]
rfl
[GOAL]
ι : Type u_1
σ : Type u_2
R : Type u_3
A : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : CanonicallyOrderedAddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
i : ι
r : A
hr : ↑(↑(↑(decompose 𝒜) r) 0) = 0
⊢ ↑(↑(↑(decompose 𝒜) r) i) ∈ RingHom.ker (projZeroRingHom 𝒜)
[PROOFSTEP]
change (decompose 𝒜 (decompose 𝒜 r _ : A) 0 : A) = 0
[GOAL]
ι : Type u_1
σ : Type u_2
R : Type u_3
A : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : CanonicallyOrderedAddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
i : ι
r : A
hr : ↑(↑(↑(decompose 𝒜) r) 0) = 0
⊢ ↑(↑(↑(decompose 𝒜) ↑(↑(↑(decompose 𝒜) r) i)) 0) = 0
[PROOFSTEP]
by_cases h : i = 0
[GOAL]
case pos
ι : Type u_1
σ : Type u_2
R : Type u_3
A : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : CanonicallyOrderedAddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
i : ι
r : A
hr : ↑(↑(↑(decompose 𝒜) r) 0) = 0
h : i = 0
⊢ ↑(↑(↑(decompose 𝒜) ↑(↑(↑(decompose 𝒜) r) i)) 0) = 0
[PROOFSTEP]
rw [h, hr, decompose_zero, zero_apply, ZeroMemClass.coe_zero]
[GOAL]
case neg
ι : Type u_1
σ : Type u_2
R : Type u_3
A : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : CanonicallyOrderedAddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
i : ι
r : A
hr : ↑(↑(↑(decompose 𝒜) r) 0) = 0
h : ¬i = 0
⊢ ↑(↑(↑(decompose 𝒜) ↑(↑(↑(decompose 𝒜) r) i)) 0) = 0
[PROOFSTEP]
rw [decompose_of_mem_ne 𝒜 (SetLike.coe_mem _) h]