theorem
GradedRingHom.map_relevant
{ι : Type u_1}
{A : Type u_2}
{B : Type u_3}
{σ : Type u_4}
{τ : Type u_5}
[AddCommGroup ι]
[AddGroup.FG ι]
[DecidableEq ι]
[CommRing A]
[SetLike σ A]
[AddSubgroupClass σ A]
{𝒜 : ι → σ}
[GradedRing 𝒜]
[CommRing B]
[SetLike τ B]
[AddSubgroupClass τ B]
{ℬ : ι → τ}
[GradedRing ℬ]
(Ψ : GradedRingHom 𝒜 ℬ)
{a : A}
{hom_a : SetLike.Homogeneous 𝒜 a}
(rel_a : HomogeneousSubmonoid.ElemIsRelevant a hom_a)
:
theorem
GradedRingHom.map_dagger_le
{ι : Type u_1}
{A : Type u_2}
{B : Type u_3}
{σ : Type u_4}
{τ : Type u_5}
[AddCommGroup ι]
[AddGroup.FG ι]
[DecidableEq ι]
[CommRing A]
[SetLike σ A]
[AddSubgroupClass σ A]
{𝒜 : ι → σ}
[GradedRing 𝒜]
[CommRing B]
[SetLike τ B]
[AddSubgroupClass τ B]
{ℬ : ι → τ}
[GradedRing ℬ]
(Ψ : GradedRingHom 𝒜 ℬ)
:
Ideal.map Ψ (HomogeneousSubmonoid.dagger 𝒜).toIdeal ≤ (HomogeneousSubmonoid.dagger ℬ).toIdeal
theorem
GradedRingHom.radical_dagger_eq_of_surjective
{ι : Type u_1}
{A : Type u_2}
{B : Type u_3}
{σ : Type u_4}
{τ : Type u_5}
[AddCommGroup ι]
[AddGroup.FG ι]
[DecidableEq ι]
[CommRing A]
[SetLike σ A]
[AddSubgroupClass σ A]
{𝒜 : ι → σ}
[GradedRing 𝒜]
[CommRing B]
[SetLike τ B]
[AddSubgroupClass τ B]
{ℬ : ι → τ}
[GradedRing ℬ]
(Ψ : GradedRingHom 𝒜 ℬ)
(surj : Function.Surjective ⇑Ψ)
:
(Ideal.map Ψ (HomogeneousSubmonoid.dagger 𝒜).toIdeal).radical = (HomogeneousSubmonoid.dagger ℬ).toIdeal.radical