Maps on homogeneous ideals

In this file we define HomogeneousIdeal.map and HomogeneousIdeal.comap.

def HomogeneousIdeal.map {A : Type u_1} {B : Type u_2} {σ : Type u_4} {τ : Type u_5} {ι : Type u_7} [Semiring A] [Semiring B] [SetLike σ A] [SetLike τ B] [AddSubmonoidClass σ A] [AddSubmonoidClass τ B] [DecidableEq ι] [AddMonoid ι] {𝒜 : ι → σ} {ℬ : ι → τ} [GradedRing 𝒜] [GradedRing ℬ] (f : 𝒜 →+*ᵍ ℬ) (I : HomogeneousIdeal 𝒜) : HomogeneousIdeal ℬ

Map a homogeneous ideal along a graded ring homomorphism. The underlying ideal is (definitionally) equal to Ideal.map.

Equations

• HomogeneousIdeal.map f I = { toSubmodule := Ideal.map f I.toIdeal, is_homogeneous' := ⋯ }

def HomogeneousIdeal.comap {A : Type u_1} {B : Type u_2} {σ : Type u_4} {τ : Type u_5} {ι : Type u_7} [Semiring A] [Semiring B] [SetLike σ A] [SetLike τ B] [AddSubmonoidClass σ A] [AddSubmonoidClass τ B] [DecidableEq ι] [AddMonoid ι] {𝒜 : ι → σ} {ℬ : ι → τ} [GradedRing 𝒜] [GradedRing ℬ] (f : 𝒜 →+*ᵍ ℬ) (I : HomogeneousIdeal ℬ) : HomogeneousIdeal 𝒜

Pull back a homogeneous ideal along a graded ring homomorphism. The underlying ideal is (definitionally) equal to Ideal.comap, whose underlying set is definitionally equal to the preimage.

Equations

• HomogeneousIdeal.comap f I = { toSubmodule := Ideal.comap f I.toIdeal, is_homogeneous' := ⋯ }

theorem HomogeneousIdeal.map_le_iff_le_comap {A : Type u_1} {B : Type u_2} {σ : Type u_4} {τ : Type u_5} {ι : Type u_7} [Semiring A] [Semiring B] [SetLike σ A] [SetLike τ B] [AddSubmonoidClass σ A] [AddSubmonoidClass τ B] [DecidableEq ι] [AddMonoid ι] {𝒜 : ι → σ} {ℬ : ι → τ} [GradedRing 𝒜] [GradedRing ℬ] (f : 𝒜 →+*ᵍ ℬ) {I : HomogeneousIdeal 𝒜} {J : HomogeneousIdeal ℬ} : map f I ≤ J ↔ I ≤ comap f J

theorem HomogeneousIdeal.le_comap_of_map_le {A : Type u_1} {B : Type u_2} {σ : Type u_4} {τ : Type u_5} {ι : Type u_7} [Semiring A] [Semiring B] [SetLike σ A] [SetLike τ B] [AddSubmonoidClass σ A] [AddSubmonoidClass τ B] [DecidableEq ι] [AddMonoid ι] {𝒜 : ι → σ} {ℬ : ι → τ} [GradedRing 𝒜] [GradedRing ℬ] (f : 𝒜 →+*ᵍ ℬ) {I : HomogeneousIdeal 𝒜} {J : HomogeneousIdeal ℬ} : map f I ≤ J → I ≤ comap f J

Alias of the forward direction of HomogeneousIdeal.map_le_iff_le_comap.

theorem HomogeneousIdeal.map_le_of_le_comap {A : Type u_1} {B : Type u_2} {σ : Type u_4} {τ : Type u_5} {ι : Type u_7} [Semiring A] [Semiring B] [SetLike σ A] [SetLike τ B] [AddSubmonoidClass σ A] [AddSubmonoidClass τ B] [DecidableEq ι] [AddMonoid ι] {𝒜 : ι → σ} {ℬ : ι → τ} [GradedRing 𝒜] [GradedRing ℬ] (f : 𝒜 →+*ᵍ ℬ) {I : HomogeneousIdeal 𝒜} {J : HomogeneousIdeal ℬ} : I ≤ comap f J → map f I ≤ J

Alias of the reverse direction of HomogeneousIdeal.map_le_iff_le_comap.

theorem HomogeneousIdeal.gc_map_comap {A : Type u_1} {B : Type u_2} {σ : Type u_4} {τ : Type u_5} {ι : Type u_7} [Semiring A] [Semiring B] [SetLike σ A] [SetLike τ B] [AddSubmonoidClass σ A] [AddSubmonoidClass τ B] [DecidableEq ι] [AddMonoid ι] {𝒜 : ι → σ} {ℬ : ι → τ} [GradedRing 𝒜] [GradedRing ℬ] (f : 𝒜 →+*ᵍ ℬ) : GaloisConnection (map f) (comap f)

theorem HomogeneousIdeal.map_mono {A : Type u_1} {B : Type u_2} {σ : Type u_4} {τ : Type u_5} {ι : Type u_7} [Semiring A] [Semiring B] [SetLike σ A] [SetLike τ B] [AddSubmonoidClass σ A] [AddSubmonoidClass τ B] [DecidableEq ι] [AddMonoid ι] {𝒜 : ι → σ} {ℬ : ι → τ} [GradedRing 𝒜] [GradedRing ℬ] (f : 𝒜 →+*ᵍ ℬ) : Monotone (map f)

theorem HomogeneousIdeal.comap_mono {A : Type u_1} {B : Type u_2} {σ : Type u_4} {τ : Type u_5} {ι : Type u_7} [Semiring A] [Semiring B] [SetLike σ A] [SetLike τ B] [AddSubmonoidClass σ A] [AddSubmonoidClass τ B] [DecidableEq ι] [AddMonoid ι] {𝒜 : ι → σ} {ℬ : ι → τ} [GradedRing 𝒜] [GradedRing ℬ] (f : 𝒜 →+*ᵍ ℬ) : Monotone (comap f)

@[simp]

theorem HomogeneousIdeal.toIdeal_comap {A : Type u_1} {B : Type u_2} {σ : Type u_4} {τ : Type u_5} {ι : Type u_7} [Semiring A] [Semiring B] [SetLike σ A] [SetLike τ B] [AddSubmonoidClass σ A] [AddSubmonoidClass τ B] [DecidableEq ι] [AddMonoid ι] {𝒜 : ι → σ} {ℬ : ι → τ} [GradedRing 𝒜] [GradedRing ℬ] (f : 𝒜 →+*ᵍ ℬ) {J : HomogeneousIdeal ℬ} : (comap f J).toIdeal = Ideal.comap f J.toIdeal

@[simp]

theorem HomogeneousIdeal.coe_comap {A : Type u_1} {B : Type u_2} {σ : Type u_4} {τ : Type u_5} {ι : Type u_7} [Semiring A] [Semiring B] [SetLike σ A] [SetLike τ B] [AddSubmonoidClass σ A] [AddSubmonoidClass τ B] [DecidableEq ι] [AddMonoid ι] {𝒜 : ι → σ} {ℬ : ι → τ} [GradedRing 𝒜] [GradedRing ℬ] (f : 𝒜 →+*ᵍ ℬ) {J : HomogeneousIdeal ℬ} : ↑(comap f J) = ⇑f ⁻¹' ↑J

@[simp]

theorem HomogeneousIdeal.toIdeal_map {A : Type u_1} {B : Type u_2} {σ : Type u_4} {τ : Type u_5} {ι : Type u_7} [Semiring A] [Semiring B] [SetLike σ A] [SetLike τ B] [AddSubmonoidClass σ A] [AddSubmonoidClass τ B] [DecidableEq ι] [AddMonoid ι] {𝒜 : ι → σ} {ℬ : ι → τ} [GradedRing 𝒜] [GradedRing ℬ] (f : 𝒜 →+*ᵍ ℬ) {I : HomogeneousIdeal 𝒜} : (map f I).toIdeal = Ideal.map f I.toIdeal

instance HomogeneousIdeal.isPrime_comap {A : Type u_1} {B : Type u_2} {σ : Type u_4} {τ : Type u_5} {ι : Type u_7} [Semiring A] [Semiring B] [SetLike σ A] [SetLike τ B] [AddSubmonoidClass σ A] [AddSubmonoidClass τ B] [DecidableEq ι] [AddMonoid ι] {𝒜 : ι → σ} {ℬ : ι → τ} [GradedRing 𝒜] [GradedRing ℬ] (f : 𝒜 →+*ᵍ ℬ) {J : HomogeneousIdeal ℬ} [J.toIdeal.IsPrime] : (comap f J).toIdeal.IsPrime

@[simp]

theorem HomogeneousIdeal.map_id {A : Type u_1} {σ : Type u_4} {ι : Type u_7} [Semiring A] [SetLike σ A] [AddSubmonoidClass σ A] [DecidableEq ι] [AddMonoid ι] {𝒜 : ι → σ} [GradedRing 𝒜] {I : HomogeneousIdeal 𝒜} : map (GradedRingHom.id 𝒜) I = I

theorem HomogeneousIdeal.map_map {A : Type u_1} {B : Type u_2} {C : Type u_3} {σ : Type u_4} {τ : Type u_5} {ω : Type u_6} {ι : Type u_7} [Semiring A] [Semiring B] [Semiring C] [SetLike σ A] [SetLike τ B] [SetLike ω C] [AddSubmonoidClass σ A] [AddSubmonoidClass τ B] [AddSubmonoidClass ω C] [DecidableEq ι] [AddMonoid ι] {𝒜 : ι → σ} {ℬ : ι → τ} {𝒞 : ι → ω} [GradedRing 𝒜] [GradedRing ℬ] [GradedRing 𝒞] (f : 𝒜 →+*ᵍ ℬ) (g : ℬ →+*ᵍ 𝒞) {I : HomogeneousIdeal 𝒜} : map g (map f I) = map (g.comp f) I

theorem HomogeneousIdeal.map_comp {A : Type u_1} {B : Type u_2} {C : Type u_3} {σ : Type u_4} {τ : Type u_5} {ω : Type u_6} {ι : Type u_7} [Semiring A] [Semiring B] [Semiring C] [SetLike σ A] [SetLike τ B] [SetLike ω C] [AddSubmonoidClass σ A] [AddSubmonoidClass τ B] [AddSubmonoidClass ω C] [DecidableEq ι] [AddMonoid ι] {𝒜 : ι → σ} {ℬ : ι → τ} {𝒞 : ι → ω} [GradedRing 𝒜] [GradedRing ℬ] [GradedRing 𝒞] (f : 𝒜 →+*ᵍ ℬ) (g : ℬ →+*ᵍ 𝒞) {I : HomogeneousIdeal 𝒜} : map (g.comp f) I = map g (map f I)

@[simp]

theorem HomogeneousIdeal.comap_id {A : Type u_1} {σ : Type u_4} {ι : Type u_7} [Semiring A] [SetLike σ A] [AddSubmonoidClass σ A] [DecidableEq ι] [AddMonoid ι] {𝒜 : ι → σ} [GradedRing 𝒜] {I : HomogeneousIdeal 𝒜} : comap (GradedRingHom.id 𝒜) I = I

theorem HomogeneousIdeal.comap_comap {A : Type u_1} {B : Type u_2} {C : Type u_3} {σ : Type u_4} {τ : Type u_5} {ω : Type u_6} {ι : Type u_7} [Semiring A] [Semiring B] [Semiring C] [SetLike σ A] [SetLike τ B] [SetLike ω C] [AddSubmonoidClass σ A] [AddSubmonoidClass τ B] [AddSubmonoidClass ω C] [DecidableEq ι] [AddMonoid ι] {𝒜 : ι → σ} {ℬ : ι → τ} {𝒞 : ι → ω} [GradedRing 𝒜] [GradedRing ℬ] [GradedRing 𝒞] (f : 𝒜 →+*ᵍ ℬ) (g : ℬ →+*ᵍ 𝒞) {K : HomogeneousIdeal 𝒞} : comap f (comap g K) = comap (g.comp f) K

theorem HomogeneousIdeal.irrelevant_le_map_comp {A : Type u_1} {B : Type u_2} {C : Type u_3} {σ : Type u_4} {τ : Type u_5} {ω : Type u_6} {ι : Type u_7} [Semiring A] [Semiring B] [Semiring C] [SetLike σ A] [SetLike τ B] [SetLike ω C] [AddSubmonoidClass σ A] [AddSubmonoidClass τ B] [AddSubmonoidClass ω C] [DecidableEq ι] [AddCommMonoid ι] [PartialOrder ι] [CanonicallyOrderedAdd ι] {𝒜 : ι → σ} {ℬ : ι → τ} {𝒞 : ι → ω} [GradedRing 𝒜] [GradedRing ℬ] [GradedRing 𝒞] {f : 𝒜 →+*ᵍ ℬ} {g : ℬ →+*ᵍ 𝒞} (hf : irrelevant ℬ ≤ map f (irrelevant 𝒜)) (hg : irrelevant 𝒞 ≤ map g (irrelevant ℬ)) : irrelevant 𝒞 ≤ map (g.comp f) (irrelevant 𝒜)