ι : Type u_1
σ : Type u_2
R : Type ?u.212520
A : Type u_3
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
ι : Type u_1
σ : Type u_2
R : Type ?u.212520
A : Type u_3
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
apply le_antisymm _ (Ideal.le_toIdeal_homogeneousHull _ _)
ι : Type u_1
σ : Type u_2
R : Type ?u.212520
A : Type u_3
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
ι : Type u_1
σ : Type u_2
R : Type ?u.212520
A : Type u_3
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
apply Ideal.span_le.2
case intro.intro
ι : Type u_1
σ : Type u_2
R : Type ?u.212520
A : Type u_3
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
ι : Type u_1
σ : Type u_2
R : Type ?u.212520
A : Type u_3
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
rintro _ ⟨i, x, rfl⟩
no goals
case intro.intro
ι : Type u_1
σ : Type u_2
R : Type ?u.212520
A : Type u_3
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
exact h _ x.prop