ι : Type u_1
σ : Type u_2
R : Type ?u.105177
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : SetLike σ A
inst✝³ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : GradedRing 𝒜
I : Ideal A
h : IsHomogeneous 𝒜 I
⊢ I ≤ homogeneousCore' 𝒜 I
ι : Type u_1
σ : Type u_2
R : Type ?u.105177
A : Type u_3
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
apply le_antisymm (I.homogeneousCore'_le 𝒜) _
ι : Type u_1
σ : Type u_2
R : Type ?u.105177
A : Type u_3
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
ι : Type u_1
σ : Type u_2
R : Type ?u.105177
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : SetLike σ A
inst✝³ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : GradedRing 𝒜
I : Ideal A
h : IsHomogeneous 𝒜 I
⊢ I ≤ homogeneousCore' 𝒜 I
intro x hx
no goals
ι : Type u_1
σ : Type u_2
R : Type ?u.105177
A : Type u_3
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
classical
rw [← DirectSum.sum_support_decompose 𝒜 x]
exact Ideal.sum_mem _ fun j _ => Ideal.subset_span ⟨⟨_, homogeneous_coe _⟩, h _ hx, rfl⟩
ι : Type u_1
σ : Type u_2
R : Type ?u.105177
A : Type u_3
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
ι : Type u_1
σ : Type u_2
R : Type ?u.105177
A : Type u_3
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
rw [← DirectSum.sum_support_decompose 𝒜 x]
no goals
ι : Type u_1
σ : Type u_2
R : Type ?u.105177
A : Type u_3
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
exact Ideal.sum_mem _ fun j _ => Ideal.subset_span ⟨⟨_, homogeneous_coe _⟩, h _ hx, rfl⟩