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 𝒜)
:
Map a homogeneous ideal along a graded ring homomorphism. The underlying ideal is
(definitionally) equal to Ideal.map.
Instances For
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 ℬ)
:
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' := ⋯ }
Instances For
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 ℬ}
:
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 ℬ}
:
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 ℬ}
:
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 : 𝒜 →+*ᵍ ℬ)
:
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 : 𝒜 →+*ᵍ ℬ)
:
@[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 ℬ}
:
@[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 ℬ}
:
@[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 𝒜}
:
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]
:
@[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 𝒜}
:
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 𝒜}
:
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 𝒜}
:
@[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 𝒜}
:
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 𝒞}
:
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 ℬ))
: