ι : Type u_2
σ : Type u_3
R : Type ?u.208850
A : Type u_1
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)
ι : Type u_2
σ : Type u_3
R : Type ?u.208850
A : Type u_1
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
⊢ I ≤ toIdeal (homogeneousHull 𝒜 I)
intro r hr
no goals
ι : Type u_2
σ : Type u_3
R : Type ?u.208850
A : Type u_1
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)
classical
rw [← DirectSum.sum_support_decompose 𝒜 r]
refine' Ideal.sum_mem _ _
intro j _
apply Ideal.subset_span
use j
use ⟨r, hr⟩
ι : Type u_2
σ : Type u_3
R : Type ?u.208850
A : Type u_1
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)
ι : Type u_2
σ : Type u_3
R : Type ?u.208850
A : Type u_1
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)
rw [← DirectSum.sum_support_decompose 𝒜 r]
ι : Type u_2
σ : Type u_3
R : Type ?u.208850
A : Type u_1
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)
ι : Type u_2
σ : Type u_3
R : Type ?u.208850
A : Type u_1
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)
refine' Ideal.sum_mem _ _
ι : Type u_2
σ : Type u_3
R : Type ?u.208850
A : Type u_1
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)
ι : Type u_2
σ : Type u_3
R : Type ?u.208850
A : Type u_1
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)
intro j _
case a
ι : Type u_2
σ : Type u_3
R : Type ?u.208850
A : Type u_1
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}
ι : Type u_2
σ : Type u_3
R : Type ?u.208850
A : Type u_1
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)
apply Ideal.subset_span
case a
ι : Type u_2
σ : Type u_3
R : Type ?u.208850
A : Type u_1
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)
case a
ι : Type u_2
σ : Type u_3
R : Type ?u.208850
A : Type u_1
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}
use j
no goals
case a
ι : Type u_2
σ : Type u_3
R : Type ?u.208850
A : Type u_1
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)
use ⟨r, hr⟩