ι : Type u_1
σ : Type u_2
R : Type ?u.110347
A : Type u_3
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)
ι : Type u_1
σ : Type u_2
R : Type ?u.110347
A : Type u_3
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)
rw [Ideal.IsHomogeneous.iff_eq, eq_comm]
no goals
ι : Type u_1
σ : Type u_2
R : Type ?u.110347
A : Type u_3
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)
exact ((Set.image_preimage.compose (Submodule.gi _ _).gc).exists_eq_l _).symm