ι : Type u_2
σ : Type u_3
A : Type u_1
inst✝⁴ : CommRing A
inst✝³ : LinearOrderedCancelAddCommMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
hI : IsHomogeneous 𝒜 I
⊢ InfSet.sInf {J | I ≤ J ∧ IsPrime J} = InfSet.sInf {J | IsHomogeneous 𝒜 J ∧ I ≤ J ∧ IsPrime J}
ι : Type u_2
σ : Type u_3
A : Type u_1
inst✝⁴ : CommRing A
inst✝³ : LinearOrderedCancelAddCommMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
hI : IsHomogeneous 𝒜 I
⊢ radical I = InfSet.sInf {J | IsHomogeneous 𝒜 J ∧ I ≤ J ∧ IsPrime J}
rw [Ideal.radical_eq_sInf]
case a
ι : Type u_2
σ : Type u_3
A : Type u_1
inst✝⁴ : CommRing A
inst✝³ : LinearOrderedCancelAddCommMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
hI : IsHomogeneous 𝒜 I
⊢ InfSet.sInf {J | I ≤ J ∧ IsPrime J} ≤ InfSet.sInf {J | IsHomogeneous 𝒜 J ∧ I ≤ J ∧ IsPrime J}

case a
ι : Type u_2
σ : Type u_3
A : Type u_1
inst✝⁴ : CommRing A
inst✝³ : LinearOrderedCancelAddCommMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
hI : IsHomogeneous 𝒜 I
⊢ InfSet.sInf {J | IsHomogeneous 𝒜 J ∧ I ≤ J ∧ IsPrime J} ≤ InfSet.sInf {J | I ≤ J ∧ IsPrime J}
ι : Type u_2
σ : Type u_3
A : Type u_1
inst✝⁴ : CommRing A
inst✝³ : LinearOrderedCancelAddCommMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
hI : IsHomogeneous 𝒜 I
⊢ InfSet.sInf {J | I ≤ J ∧ IsPrime J} = InfSet.sInf {J | IsHomogeneous 𝒜 J ∧ I ≤ J ∧ IsPrime J}
apply le_antisymm
no goals
case a
ι : Type u_2
σ : Type u_3
A : Type u_1
inst✝⁴ : CommRing A
inst✝³ : LinearOrderedCancelAddCommMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
hI : IsHomogeneous 𝒜 I
⊢ InfSet.sInf {J | I ≤ J ∧ IsPrime J} ≤ InfSet.sInf {J | IsHomogeneous 𝒜 J ∧ I ≤ J ∧ IsPrime J}
exact sInf_le_sInf fun J => And.right
case a
ι : Type u_2
σ : Type u_3
A : Type u_1
inst✝⁴ : CommRing A
inst✝³ : LinearOrderedCancelAddCommMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
hI : IsHomogeneous 𝒜 I
⊢ ∀ (x : Ideal A), x ∈ {J | I ≤ J ∧ IsPrime J} → ∃ y, y ∈ {J | IsHomogeneous 𝒜 J ∧ I ≤ J ∧ IsPrime J} ∧ y ≤ x
case a
ι : Type u_2
σ : Type u_3
A : Type u_1
inst✝⁴ : CommRing A
inst✝³ : LinearOrderedCancelAddCommMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
hI : IsHomogeneous 𝒜 I
⊢ InfSet.sInf {J | IsHomogeneous 𝒜 J ∧ I ≤ J ∧ IsPrime J} ≤ InfSet.sInf {J | I ≤ J ∧ IsPrime J}
refine sInf_le_sInf_of_forall_exists_le ?_
case a.intro
ι : Type u_2
σ : Type u_3
A : Type u_1
inst✝⁴ : CommRing A
inst✝³ : LinearOrderedCancelAddCommMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
hI : IsHomogeneous 𝒜 I
J : Ideal A
HJ₁ : I ≤ J
HJ₂ : IsPrime J
⊢ ∃ y, y ∈ {J | IsHomogeneous 𝒜 J ∧ I ≤ J ∧ IsPrime J} ∧ y ≤ J
case a
ι : Type u_2
σ : Type u_3
A : Type u_1
inst✝⁴ : CommRing A
inst✝³ : LinearOrderedCancelAddCommMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
hI : IsHomogeneous 𝒜 I
⊢ ∀ (x : Ideal A), x ∈ {J | I ≤ J ∧ IsPrime J} → ∃ y, y ∈ {J | IsHomogeneous 𝒜 J ∧ I ≤ J ∧ IsPrime J} ∧ y ≤ x
rintro J ⟨HJ₁, HJ₂⟩
case a.intro
ι : Type u_2
σ : Type u_3
A : Type u_1
inst✝⁴ : CommRing A
inst✝³ : LinearOrderedCancelAddCommMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
hI : IsHomogeneous 𝒜 I
J : Ideal A
HJ₁ : I ≤ J
HJ₂ : IsPrime J
⊢ HomogeneousIdeal.toIdeal (homogeneousCore 𝒜 J) ∈ {J | IsHomogeneous 𝒜 J ∧ I ≤ J ∧ IsPrime J}
case a.intro
ι : Type u_2
σ : Type u_3
A : Type u_1
inst✝⁴ : CommRing A
inst✝³ : LinearOrderedCancelAddCommMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
hI : IsHomogeneous 𝒜 I
J : Ideal A
HJ₁ : I ≤ J
HJ₂ : IsPrime J
⊢ ∃ y, y ∈ {J | IsHomogeneous 𝒜 J ∧ I ≤ J ∧ IsPrime J} ∧ y ≤ J
refine ⟨(J.homogeneousCore 𝒜).toIdeal, ?_, J.toIdeal_homogeneousCore_le _⟩
case a.intro
ι : Type u_2
σ : Type u_3
A : Type u_1
inst✝⁴ : CommRing A
inst✝³ : LinearOrderedCancelAddCommMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
hI : IsHomogeneous 𝒜 I
J : Ideal A
HJ₁ : I ≤ J
HJ₂ : IsPrime J
⊢ I ≤ HomogeneousIdeal.toIdeal (homogeneousCore 𝒜 J)
case a.intro
ι : Type u_2
σ : Type u_3
A : Type u_1
inst✝⁴ : CommRing A
inst✝³ : LinearOrderedCancelAddCommMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
hI : IsHomogeneous 𝒜 I
J : Ideal A
HJ₁ : I ≤ J
HJ₂ : IsPrime J
⊢ HomogeneousIdeal.toIdeal (homogeneousCore 𝒜 J) ∈ {J | IsHomogeneous 𝒜 J ∧ I ≤ J ∧ IsPrime J}
refine ⟨HomogeneousIdeal.isHomogeneous _, ?_, HJ₂.homogeneousCore⟩
no goals
case a.intro
ι : Type u_2
σ : Type u_3
A : Type u_1
inst✝⁴ : CommRing A
inst✝³ : LinearOrderedCancelAddCommMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
hI : IsHomogeneous 𝒜 I
J : Ideal A
HJ₁ : I ≤ J
HJ₂ : IsPrime J
⊢ I ≤ HomogeneousIdeal.toIdeal (homogeneousCore 𝒜 J)
exact hI.toIdeal_homogeneousCore_eq_self.symm.trans_le (Ideal.homogeneousCore_mono _ HJ₁)