Homogeneous ideals of a graded algebra #
This file defines homogeneous ideals of GradedRing 𝒜 where 𝒜 : ι → Submodule R A and
operations on them.
Main definitions #
For any I : Ideal A:
Ideal.IsHomogeneous 𝒜 I: The property that an ideal is closed underGradedRing.proj.HomogeneousIdeal 𝒜: The structure extending ideals which satisfyIdeal.IsHomogeneous.Ideal.homogeneousCore I 𝒜: The largest homogeneous ideal smaller thanI.Ideal.homogeneousHull I 𝒜: The smallest homogeneous ideal larger thanI.
Main statements #
HomogeneousIdeal.completeLattice:Ideal.IsHomogeneousis preserved by⊥,⊤,⊔,⊓,⨆,⨅, and so the subtype of homogeneous ideals inherits a complete lattice structure.Ideal.homogeneousCore.gi:Ideal.homogeneousCoreforms a Galois insertion with coercion.Ideal.homogeneousHull.gi:Ideal.homogeneousHullforms a Galois insertion with coercion.
Implementation notes #
We introduce Ideal.homogeneousCore' earlier than might be expected so that we can get access
to Ideal.IsHomogeneous.iff_exists as quickly as possible.
Tags #
graded algebra, homogeneous
@[reducible, inline]
abbrev
Ideal.IsHomogeneous
{ι : Type u_1}
{σ : Type u_2}
{A : Type u_3}
[Semiring A]
[SetLike σ A]
[AddSubmonoidClass σ A]
(𝒜 : ι → σ)
[DecidableEq ι]
[AddMonoid ι]
[GradedRing 𝒜]
(I : Ideal A)
:
An I : Ideal A is homogeneous if for every r ∈ I, all homogeneous components
of r are in I.
Instances For
theorem
Ideal.IsHomogeneous.mem_iff
{ι : Type u_1}
{σ : Type u_2}
{A : Type u_3}
[Semiring A]
[SetLike σ A]
[AddSubmonoidClass σ A]
(𝒜 : ι → σ)
[DecidableEq ι]
[AddMonoid ι]
[GradedRing 𝒜]
{I : Ideal A}
(hI : IsHomogeneous 𝒜 I)
{x : A}
:
x ∈ I ↔ ∀ (i : ι), ↑(((DirectSum.decompose 𝒜) x) i) ∈ I
@[reducible, inline]
abbrev
HomogeneousIdeal
{ι : Type u_1}
{σ : Type u_2}
{A : Type u_3}
[Semiring A]
[SetLike σ A]
[AddSubmonoidClass σ A]
(𝒜 : ι → σ)
[DecidableEq ι]
[AddMonoid ι]
[GradedRing 𝒜]
:
Type u_3
For any Semiring A, we collect the homogeneous ideals of A into a type.
Instances For
@[reducible, inline]
abbrev
HomogeneousIdeal.toIdeal
{ι : Type u_1}
{σ : Type u_2}
{A : Type u_3}
[Semiring A]
[SetLike σ A]
[AddSubmonoidClass σ A]
{𝒜 : ι → σ}
[DecidableEq ι]
[AddMonoid ι]
[GradedRing 𝒜]
(I : HomogeneousIdeal 𝒜)
:
Ideal A
Converting a homogeneous ideal to an ideal.
Instances For
@[simp]
theorem
coe_toIdeal
{ι : Type u_1}
{σ : Type u_2}
{A : Type u_3}
[Semiring A]
[SetLike σ A]
[AddSubmonoidClass σ A]
{𝒜 : ι → σ}
[DecidableEq ι]
[AddMonoid ι]
[GradedRing 𝒜]
(I : HomogeneousIdeal 𝒜)
:
↑I.toIdeal = ↑I
theorem
HomogeneousIdeal.isHomogeneous
{ι : Type u_1}
{σ : Type u_2}
{A : Type u_3}
[Semiring A]
[SetLike σ A]
[AddSubmonoidClass σ A]
{𝒜 : ι → σ}
[DecidableEq ι]
[AddMonoid ι]
[GradedRing 𝒜]
(I : HomogeneousIdeal 𝒜)
:
theorem
HomogeneousIdeal.toIdeal_injective
{ι : Type u_1}
{σ : Type u_2}
{A : Type u_3}
[Semiring A]
[SetLike σ A]
[AddSubmonoidClass σ A]
{𝒜 : ι → σ}
[DecidableEq ι]
[AddMonoid ι]
[GradedRing 𝒜]
:
Function.Injective toIdeal
@[simp]
theorem
toIdeal_le_toIdeal_iff
{ι : Type u_1}
{σ : Type u_2}
{A : Type u_3}
[Semiring A]
[SetLike σ A]
[AddSubmonoidClass σ A]
{𝒜 : ι → σ}
[DecidableEq ι]
[AddMonoid ι]
[GradedRing 𝒜]
{I J : HomogeneousIdeal 𝒜}
:
@[implicit_reducible]
instance
HomogeneousIdeal.setLike
{ι : Type u_1}
{σ : Type u_2}
{A : Type u_3}
[Semiring A]
[SetLike σ A]
[AddSubmonoidClass σ A]
{𝒜 : ι → σ}
[DecidableEq ι]
[AddMonoid ι]
[GradedRing 𝒜]
:
SetLike (HomogeneousIdeal 𝒜) A
@[implicit_reducible]
instance
instPartialOrderHomogeneousIdeal
{ι : Type u_1}
{σ : Type u_2}
{A : Type u_3}
[Semiring A]
[SetLike σ A]
[AddSubmonoidClass σ A]
{𝒜 : ι → σ}
[DecidableEq ι]
[AddMonoid ι]
[GradedRing 𝒜]
:
theorem
HomogeneousIdeal.ext
{ι : Type u_1}
{σ : Type u_2}
{A : Type u_3}
[Semiring A]
[SetLike σ A]
[AddSubmonoidClass σ A]
{𝒜 : ι → σ}
[DecidableEq ι]
[AddMonoid ι]
[GradedRing 𝒜]
{I J : HomogeneousIdeal 𝒜}
(h : I.toIdeal = J.toIdeal)
:
I = J
theorem
HomogeneousIdeal.ext_iff
{ι : Type u_1}
{σ : Type u_2}
{A : Type u_3}
[Semiring A]
[SetLike σ A]
[AddSubmonoidClass σ A]
{𝒜 : ι → σ}
[DecidableEq ι]
[AddMonoid ι]
[GradedRing 𝒜]
{I J : HomogeneousIdeal 𝒜}
:
theorem
HomogeneousIdeal.ext'
{ι : Type u_1}
{σ : Type u_2}
{A : Type u_3}
[Semiring A]
[SetLike σ A]
[AddSubmonoidClass σ A]
{𝒜 : ι → σ}
[DecidableEq ι]
[AddMonoid ι]
[GradedRing 𝒜]
{I J : HomogeneousIdeal 𝒜}
(h : ∀ (i : ι), ∀ x ∈ 𝒜 i, x ∈ I ↔ x ∈ J)
:
I = J
@[simp]
theorem
HomogeneousIdeal.mem_iff
{ι : Type u_1}
{σ : Type u_2}
{A : Type u_3}
[Semiring A]
[SetLike σ A]
[AddSubmonoidClass σ A]
{𝒜 : ι → σ}
[DecidableEq ι]
[AddMonoid ι]
[GradedRing 𝒜]
{I : HomogeneousIdeal 𝒜}
{x : A}
:
x ∈ I.toIdeal ↔ x ∈ I
def
Ideal.homogeneousCore'
{ι : Type u_1}
{σ : Type u_2}
{A : Type u_3}
[Semiring A]
[SetLike σ A]
(𝒜 : ι → σ)
(I : Ideal A)
:
Ideal A
For any I : Ideal A, not necessarily homogeneous, I.homogeneousCore' 𝒜
is the largest homogeneous ideal of A contained in I, as an ideal.
Instances For
theorem
Ideal.isHomogeneous_iff_forall_subset
{ι : Type u_1}
{σ : Type u_2}
{A : Type u_3}
[Semiring A]
[SetLike σ A]
[AddSubmonoidClass σ A]
(𝒜 : ι → σ)
[DecidableEq ι]
[AddMonoid ι]
[GradedRing 𝒜]
(I : Ideal A)
:
IsHomogeneous 𝒜 I ↔ ∀ (i : ι), ↑I ⊆ ⇑(GradedRing.proj 𝒜 i) ⁻¹' ↑I
theorem
Ideal.isHomogeneous_iff_subset_iInter
{ι : Type u_1}
{σ : Type u_2}
{A : Type u_3}
[Semiring A]
[SetLike σ A]
[AddSubmonoidClass σ A]
(𝒜 : ι → σ)
[DecidableEq ι]
[AddMonoid ι]
[GradedRing 𝒜]
(I : Ideal A)
:
IsHomogeneous 𝒜 I ↔ ↑I ⊆ ⋂ (i : ι), ⇑(GradedRing.proj 𝒜 i) ⁻¹' ↑I
theorem
Ideal.mul_homogeneous_element_mem_of_mem
{ι : Type u_1}
{σ : Type u_2}
{A : Type u_3}
[Semiring A]
[SetLike σ A]
[AddSubmonoidClass σ A]
(𝒜 : ι → σ)
[DecidableEq ι]
[AddMonoid ι]
[GradedRing 𝒜]
{I : Ideal A}
(r x : A)
(hx₁ : SetLike.IsHomogeneousElem 𝒜 x)
(hx₂ : x ∈ I)
(j : ι)
:
(GradedRing.proj 𝒜 j) (r * x) ∈ I
theorem
Ideal.homogeneous_span
{ι : Type u_1}
{σ : Type u_2}
{A : Type u_3}
[Semiring A]
[SetLike σ A]
[AddSubmonoidClass σ A]
(𝒜 : ι → σ)
[DecidableEq ι]
[AddMonoid ι]
[GradedRing 𝒜]
(s : Set A)
(h : ∀ x ∈ s, SetLike.IsHomogeneousElem 𝒜 x)
:
IsHomogeneous 𝒜 (span s)
def
Ideal.homogeneousCore
{ι : Type u_1}
{σ : Type u_2}
{A : Type u_3}
[Semiring A]
[SetLike σ A]
[AddSubmonoidClass σ A]
(𝒜 : ι → σ)
[DecidableEq ι]
[AddMonoid ι]
[GradedRing 𝒜]
(I : Ideal A)
:
For any I : Ideal A, not necessarily homogeneous, I.homogeneousCore' 𝒜
is the largest homogeneous ideal of A contained in I.
Instances For
theorem
Ideal.homogeneousCore_mono
{ι : Type u_1}
{σ : Type u_2}
{A : Type u_3}
[Semiring A]
[SetLike σ A]
[AddSubmonoidClass σ A]
(𝒜 : ι → σ)
[DecidableEq ι]
[AddMonoid ι]
[GradedRing 𝒜]
:
theorem
Ideal.toIdeal_homogeneousCore_le
{ι : Type u_1}
{σ : Type u_2}
{A : Type u_3}
[Semiring A]
[SetLike σ A]
[AddSubmonoidClass σ A]
(𝒜 : ι → σ)
[DecidableEq ι]
[AddMonoid ι]
[GradedRing 𝒜]
(I : Ideal A)
:
theorem
Ideal.mem_homogeneousCore_of_homogeneous_of_mem
{ι : Type u_1}
{σ : Type u_2}
{A : Type u_3}
[Semiring A]
[SetLike σ A]
[AddSubmonoidClass σ A]
{𝒜 : ι → σ}
[DecidableEq ι]
[AddMonoid ι]
[GradedRing 𝒜]
{I : Ideal A}
{x : A}
(h : SetLike.IsHomogeneousElem 𝒜 x)
(hmem : x ∈ I)
:
x ∈ homogeneousCore 𝒜 I
theorem
Ideal.IsHomogeneous.toIdeal_homogeneousCore_eq_self
{ι : Type u_1}
{σ : Type u_2}
{A : Type u_3}
[Semiring A]
[SetLike σ A]
[AddSubmonoidClass σ A]
{𝒜 : ι → σ}
[DecidableEq ι]
[AddMonoid ι]
[GradedRing 𝒜]
{I : Ideal A}
(h : IsHomogeneous 𝒜 I)
:
(homogeneousCore 𝒜 I).toIdeal = I
@[simp]
theorem
HomogeneousIdeal.toIdeal_homogeneousCore_eq_self
{ι : Type u_1}
{σ : Type u_2}
{A : Type u_3}
[Semiring A]
[SetLike σ A]
[AddSubmonoidClass σ A]
{𝒜 : ι → σ}
[DecidableEq ι]
[AddMonoid ι]
[GradedRing 𝒜]
(I : HomogeneousIdeal 𝒜)
:
Ideal.homogeneousCore 𝒜 I.toIdeal = I
theorem
Ideal.IsHomogeneous.iff_eq
{ι : Type u_1}
{σ : Type u_2}
{A : Type u_3}
[Semiring A]
[SetLike σ A]
[AddSubmonoidClass σ A]
(𝒜 : ι → σ)
[DecidableEq ι]
[AddMonoid ι]
[GradedRing 𝒜]
(I : Ideal A)
:
IsHomogeneous 𝒜 I ↔ (homogeneousCore 𝒜 I).toIdeal = I
theorem
Ideal.IsHomogeneous.iff_exists
{ι : Type u_1}
{σ : Type u_2}
{A : Type u_3}
[Semiring A]
[SetLike σ A]
[AddSubmonoidClass σ A]
(𝒜 : ι → σ)
[DecidableEq ι]
[AddMonoid ι]
[GradedRing 𝒜]
(I : Ideal A)
:
IsHomogeneous 𝒜 I ↔ ∃ (S : Set ↥(SetLike.homogeneousSubmonoid 𝒜)), I = span (Subtype.val '' S)
Operations #
In this section, we show that Ideal.IsHomogeneous is preserved by various notations, then use
these results to provide these notation typeclasses for HomogeneousIdeal.
theorem
Ideal.IsHomogeneous.bot
{ι : Type u_1}
{σ : Type u_2}
{A : Type u_3}
[Semiring A]
[DecidableEq ι]
[AddMonoid ι]
[SetLike σ A]
[AddSubmonoidClass σ A]
(𝒜 : ι → σ)
[GradedRing 𝒜]
:
theorem
Ideal.IsHomogeneous.top
{ι : Type u_1}
{σ : Type u_2}
{A : Type u_3}
[Semiring A]
[DecidableEq ι]
[AddMonoid ι]
[SetLike σ A]
[AddSubmonoidClass σ A]
(𝒜 : ι → σ)
[GradedRing 𝒜]
:
theorem
Ideal.IsHomogeneous.inf
{ι : Type u_1}
{σ : Type u_2}
{A : Type u_3}
[Semiring A]
[DecidableEq ι]
[AddMonoid ι]
[SetLike σ A]
[AddSubmonoidClass σ A]
{𝒜 : ι → σ}
[GradedRing 𝒜]
{I J : Ideal A}
(HI : IsHomogeneous 𝒜 I)
(HJ : IsHomogeneous 𝒜 J)
:
IsHomogeneous 𝒜 (I ⊓ J)
theorem
Ideal.IsHomogeneous.sup
{ι : Type u_1}
{σ : Type u_2}
{A : Type u_3}
[Semiring A]
[DecidableEq ι]
[AddMonoid ι]
[SetLike σ A]
[AddSubmonoidClass σ A]
{𝒜 : ι → σ}
[GradedRing 𝒜]
{I J : Ideal A}
(HI : IsHomogeneous 𝒜 I)
(HJ : IsHomogeneous 𝒜 J)
:
IsHomogeneous 𝒜 (I ⊔ J)
theorem
Ideal.IsHomogeneous.iSup
{ι : Type u_1}
{σ : Type u_2}
{A : Type u_3}
[Semiring A]
[DecidableEq ι]
[AddMonoid ι]
[SetLike σ A]
[AddSubmonoidClass σ A]
{𝒜 : ι → σ}
[GradedRing 𝒜]
{κ : Sort u_4}
{f : κ → Ideal A}
(h : ∀ (i : κ), IsHomogeneous 𝒜 (f i))
:
IsHomogeneous 𝒜 (⨆ (i : κ), f i)
theorem
Ideal.IsHomogeneous.iInf
{ι : Type u_1}
{σ : Type u_2}
{A : Type u_3}
[Semiring A]
[DecidableEq ι]
[AddMonoid ι]
[SetLike σ A]
[AddSubmonoidClass σ A]
{𝒜 : ι → σ}
[GradedRing 𝒜]
{κ : Sort u_4}
{f : κ → Ideal A}
(h : ∀ (i : κ), IsHomogeneous 𝒜 (f i))
:
IsHomogeneous 𝒜 (⨅ (i : κ), f i)
theorem
Ideal.IsHomogeneous.iSup₂
{ι : Type u_1}
{σ : Type u_2}
{A : Type u_3}
[Semiring A]
[DecidableEq ι]
[AddMonoid ι]
[SetLike σ A]
[AddSubmonoidClass σ A]
{𝒜 : ι → σ}
[GradedRing 𝒜]
{κ : Sort u_4}
{κ' : κ → Sort u_5}
{f : (i : κ) → κ' i → Ideal A}
(h : ∀ (i : κ) (j : κ' i), IsHomogeneous 𝒜 (f i j))
:
IsHomogeneous 𝒜 (⨆ (i : κ), ⨆ (j : κ' i), f i j)
theorem
Ideal.IsHomogeneous.iInf₂
{ι : Type u_1}
{σ : Type u_2}
{A : Type u_3}
[Semiring A]
[DecidableEq ι]
[AddMonoid ι]
[SetLike σ A]
[AddSubmonoidClass σ A]
{𝒜 : ι → σ}
[GradedRing 𝒜]
{κ : Sort u_4}
{κ' : κ → Sort u_5}
{f : (i : κ) → κ' i → Ideal A}
(h : ∀ (i : κ) (j : κ' i), IsHomogeneous 𝒜 (f i j))
:
IsHomogeneous 𝒜 (⨅ (i : κ), ⨅ (j : κ' i), f i j)
theorem
Ideal.IsHomogeneous.sSup
{ι : Type u_1}
{σ : Type u_2}
{A : Type u_3}
[Semiring A]
[DecidableEq ι]
[AddMonoid ι]
[SetLike σ A]
[AddSubmonoidClass σ A]
{𝒜 : ι → σ}
[GradedRing 𝒜]
{ℐ : Set (Ideal A)}
(h : ∀ I ∈ ℐ, IsHomogeneous 𝒜 I)
:
IsHomogeneous 𝒜 (SupSet.sSup ℐ)
theorem
Ideal.IsHomogeneous.sInf
{ι : Type u_1}
{σ : Type u_2}
{A : Type u_3}
[Semiring A]
[DecidableEq ι]
[AddMonoid ι]
[SetLike σ A]
[AddSubmonoidClass σ A]
{𝒜 : ι → σ}
[GradedRing 𝒜]
{ℐ : Set (Ideal A)}
(h : ∀ I ∈ ℐ, IsHomogeneous 𝒜 I)
:
IsHomogeneous 𝒜 (InfSet.sInf ℐ)
@[implicit_reducible]
instance
HomogeneousIdeal.instTop
{ι : Type u_1}
{σ : Type u_2}
{A : Type u_3}
[Semiring A]
[DecidableEq ι]
[AddMonoid ι]
[SetLike σ A]
[AddSubmonoidClass σ A]
{𝒜 : ι → σ}
[GradedRing 𝒜]
:
Top (HomogeneousIdeal 𝒜)
@[implicit_reducible]
instance
HomogeneousIdeal.instBot
{ι : Type u_1}
{σ : Type u_2}
{A : Type u_3}
[Semiring A]
[DecidableEq ι]
[AddMonoid ι]
[SetLike σ A]
[AddSubmonoidClass σ A]
{𝒜 : ι → σ}
[GradedRing 𝒜]
:
Bot (HomogeneousIdeal 𝒜)
@[implicit_reducible]
instance
HomogeneousIdeal.instMax
{ι : Type u_1}
{σ : Type u_2}
{A : Type u_3}
[Semiring A]
[DecidableEq ι]
[AddMonoid ι]
[SetLike σ A]
[AddSubmonoidClass σ A]
{𝒜 : ι → σ}
[GradedRing 𝒜]
:
Max (HomogeneousIdeal 𝒜)
@[implicit_reducible]
instance
HomogeneousIdeal.instMin
{ι : Type u_1}
{σ : Type u_2}
{A : Type u_3}
[Semiring A]
[DecidableEq ι]
[AddMonoid ι]
[SetLike σ A]
[AddSubmonoidClass σ A]
{𝒜 : ι → σ}
[GradedRing 𝒜]
:
Min (HomogeneousIdeal 𝒜)
@[implicit_reducible]
instance
HomogeneousIdeal.instSupSet
{ι : Type u_1}
{σ : Type u_2}
{A : Type u_3}
[Semiring A]
[DecidableEq ι]
[AddMonoid ι]
[SetLike σ A]
[AddSubmonoidClass σ A]
{𝒜 : ι → σ}
[GradedRing 𝒜]
:
@[implicit_reducible]
instance
HomogeneousIdeal.instInfSet
{ι : Type u_1}
{σ : Type u_2}
{A : Type u_3}
[Semiring A]
[DecidableEq ι]
[AddMonoid ι]
[SetLike σ A]
[AddSubmonoidClass σ A]
{𝒜 : ι → σ}
[GradedRing 𝒜]
:
@[simp]
theorem
HomogeneousIdeal.coe_top
{ι : Type u_1}
{σ : Type u_2}
{A : Type u_3}
[Semiring A]
[DecidableEq ι]
[AddMonoid ι]
[SetLike σ A]
[AddSubmonoidClass σ A]
{𝒜 : ι → σ}
[GradedRing 𝒜]
:
@[simp]
theorem
HomogeneousIdeal.coe_bot
{ι : Type u_1}
{σ : Type u_2}
{A : Type u_3}
[Semiring A]
[DecidableEq ι]
[AddMonoid ι]
[SetLike σ A]
[AddSubmonoidClass σ A]
{𝒜 : ι → σ}
[GradedRing 𝒜]
:
↑⊥ = 0
@[simp]
theorem
HomogeneousIdeal.coe_sup
{ι : Type u_1}
{σ : Type u_2}
{A : Type u_3}
[Semiring A]
[DecidableEq ι]
[AddMonoid ι]
[SetLike σ A]
[AddSubmonoidClass σ A]
{𝒜 : ι → σ}
[GradedRing 𝒜]
(I J : HomogeneousIdeal 𝒜)
:
↑(I ⊔ J) = ↑I + ↑J
@[simp]
theorem
HomogeneousIdeal.coe_inf
{ι : Type u_1}
{σ : Type u_2}
{A : Type u_3}
[Semiring A]
[DecidableEq ι]
[AddMonoid ι]
[SetLike σ A]
[AddSubmonoidClass σ A]
{𝒜 : ι → σ}
[GradedRing 𝒜]
(I J : HomogeneousIdeal 𝒜)
:
↑(I ⊓ J) = ↑I ∩ ↑J
@[simp]
theorem
HomogeneousIdeal.toIdeal_top
{ι : Type u_1}
{σ : Type u_2}
{A : Type u_3}
[Semiring A]
[DecidableEq ι]
[AddMonoid ι]
[SetLike σ A]
[AddSubmonoidClass σ A]
{𝒜 : ι → σ}
[GradedRing 𝒜]
:
@[simp]
theorem
HomogeneousIdeal.toIdeal_bot
{ι : Type u_1}
{σ : Type u_2}
{A : Type u_3}
[Semiring A]
[DecidableEq ι]
[AddMonoid ι]
[SetLike σ A]
[AddSubmonoidClass σ A]
{𝒜 : ι → σ}
[GradedRing 𝒜]
:
@[simp]
theorem
HomogeneousIdeal.toIdeal_sup
{ι : Type u_1}
{σ : Type u_2}
{A : Type u_3}
[Semiring A]
[DecidableEq ι]
[AddMonoid ι]
[SetLike σ A]
[AddSubmonoidClass σ A]
{𝒜 : ι → σ}
[GradedRing 𝒜]
(I J : HomogeneousIdeal 𝒜)
:
@[simp]
theorem
HomogeneousIdeal.toIdeal_inf
{ι : Type u_1}
{σ : Type u_2}
{A : Type u_3}
[Semiring A]
[DecidableEq ι]
[AddMonoid ι]
[SetLike σ A]
[AddSubmonoidClass σ A]
{𝒜 : ι → σ}
[GradedRing 𝒜]
(I J : HomogeneousIdeal 𝒜)
:
@[simp]
theorem
HomogeneousIdeal.toIdeal_sSup
{ι : Type u_1}
{σ : Type u_2}
{A : Type u_3}
[Semiring A]
[DecidableEq ι]
[AddMonoid ι]
[SetLike σ A]
[AddSubmonoidClass σ A]
{𝒜 : ι → σ}
[GradedRing 𝒜]
(ℐ : Set (HomogeneousIdeal 𝒜))
:
@[simp]
theorem
HomogeneousIdeal.toIdeal_sInf
{ι : Type u_1}
{σ : Type u_2}
{A : Type u_3}
[Semiring A]
[DecidableEq ι]
[AddMonoid ι]
[SetLike σ A]
[AddSubmonoidClass σ A]
{𝒜 : ι → σ}
[GradedRing 𝒜]
(ℐ : Set (HomogeneousIdeal 𝒜))
:
@[simp]
theorem
HomogeneousIdeal.toIdeal_iSup
{ι : Type u_1}
{σ : Type u_2}
{A : Type u_3}
[Semiring A]
[DecidableEq ι]
[AddMonoid ι]
[SetLike σ A]
[AddSubmonoidClass σ A]
{𝒜 : ι → σ}
[GradedRing 𝒜]
{κ : Sort u_4}
(s : κ → HomogeneousIdeal 𝒜)
:
@[simp]
theorem
HomogeneousIdeal.toIdeal_iInf
{ι : Type u_1}
{σ : Type u_2}
{A : Type u_3}
[Semiring A]
[DecidableEq ι]
[AddMonoid ι]
[SetLike σ A]
[AddSubmonoidClass σ A]
{𝒜 : ι → σ}
[GradedRing 𝒜]
{κ : Sort u_4}
(s : κ → HomogeneousIdeal 𝒜)
:
theorem
HomogeneousIdeal.toIdeal_iSup₂
{ι : Type u_1}
{σ : Type u_2}
{A : Type u_3}
[Semiring A]
[DecidableEq ι]
[AddMonoid ι]
[SetLike σ A]
[AddSubmonoidClass σ A]
{𝒜 : ι → σ}
[GradedRing 𝒜]
{κ : Sort u_4}
{κ' : κ → Sort u_5}
(s : (i : κ) → κ' i → HomogeneousIdeal 𝒜)
:
theorem
HomogeneousIdeal.toIdeal_iInf₂
{ι : Type u_1}
{σ : Type u_2}
{A : Type u_3}
[Semiring A]
[DecidableEq ι]
[AddMonoid ι]
[SetLike σ A]
[AddSubmonoidClass σ A]
{𝒜 : ι → σ}
[GradedRing 𝒜]
{κ : Sort u_4}
{κ' : κ → Sort u_5}
(s : (i : κ) → κ' i → HomogeneousIdeal 𝒜)
:
@[simp]
theorem
HomogeneousIdeal.eq_top_iff
{ι : Type u_1}
{σ : Type u_2}
{A : Type u_3}
[Semiring A]
[DecidableEq ι]
[AddMonoid ι]
[SetLike σ A]
[AddSubmonoidClass σ A]
{𝒜 : ι → σ}
[GradedRing 𝒜]
(I : HomogeneousIdeal 𝒜)
:
@[simp]
theorem
HomogeneousIdeal.eq_bot_iff
{ι : Type u_1}
{σ : Type u_2}
{A : Type u_3}
[Semiring A]
[DecidableEq ι]
[AddMonoid ι]
[SetLike σ A]
[AddSubmonoidClass σ A]
{𝒜 : ι → σ}
[GradedRing 𝒜]
(I : HomogeneousIdeal 𝒜)
:
@[implicit_reducible]
instance
HomogeneousIdeal.completeLattice
{ι : Type u_1}
{σ : Type u_2}
{A : Type u_3}
[Semiring A]
[DecidableEq ι]
[AddMonoid ι]
[SetLike σ A]
[AddSubmonoidClass σ A]
{𝒜 : ι → σ}
[GradedRing 𝒜]
:
@[implicit_reducible]
instance
HomogeneousIdeal.instAdd
{ι : Type u_1}
{σ : Type u_2}
{A : Type u_3}
[Semiring A]
[DecidableEq ι]
[AddMonoid ι]
[SetLike σ A]
[AddSubmonoidClass σ A]
{𝒜 : ι → σ}
[GradedRing 𝒜]
:
Add (HomogeneousIdeal 𝒜)
@[simp]
theorem
HomogeneousIdeal.toIdeal_add
{ι : Type u_1}
{σ : Type u_2}
{A : Type u_3}
[Semiring A]
[DecidableEq ι]
[AddMonoid ι]
[SetLike σ A]
[AddSubmonoidClass σ A]
{𝒜 : ι → σ}
[GradedRing 𝒜]
(I J : HomogeneousIdeal 𝒜)
:
@[implicit_reducible]
instance
HomogeneousIdeal.instInhabited
{ι : Type u_1}
{σ : Type u_2}
{A : Type u_3}
[Semiring A]
[DecidableEq ι]
[AddMonoid ι]
[SetLike σ A]
[AddSubmonoidClass σ A]
{𝒜 : ι → σ}
[GradedRing 𝒜]
:
Inhabited (HomogeneousIdeal 𝒜)
theorem
Ideal.IsHomogeneous.mul
{ι : Type u_1}
{σ : Type u_2}
{A : Type u_3}
[CommSemiring A]
[DecidableEq ι]
[AddMonoid ι]
[SetLike σ A]
[AddSubmonoidClass σ A]
{𝒜 : ι → σ}
[GradedRing 𝒜]
{I J : Ideal A}
(HI : IsHomogeneous 𝒜 I)
(HJ : IsHomogeneous 𝒜 J)
:
IsHomogeneous 𝒜 (I * J)
@[implicit_reducible]
instance
instMulHomogeneousIdeal
{ι : Type u_1}
{σ : Type u_2}
{A : Type u_3}
[CommSemiring A]
[DecidableEq ι]
[AddMonoid ι]
[SetLike σ A]
[AddSubmonoidClass σ A]
{𝒜 : ι → σ}
[GradedRing 𝒜]
:
Mul (HomogeneousIdeal 𝒜)
@[simp]
theorem
HomogeneousIdeal.toIdeal_mul
{ι : Type u_1}
{σ : Type u_2}
{A : Type u_3}
[CommSemiring A]
[DecidableEq ι]
[AddMonoid ι]
[SetLike σ A]
[AddSubmonoidClass σ A]
{𝒜 : ι → σ}
[GradedRing 𝒜]
(I J : HomogeneousIdeal 𝒜)
:
Homogeneous core #
Note that many results about the homogeneous core came earlier in this file, as they are helpful for building the lattice structure.
theorem
Ideal.homogeneousCore.gc
{ι : Type u_1}
{σ : Type u_2}
{A : Type u_3}
[Semiring A]
[DecidableEq ι]
[AddMonoid ι]
[SetLike σ A]
[AddSubmonoidClass σ A]
(𝒜 : ι → σ)
[GradedRing 𝒜]
:
def
Ideal.homogeneousCore.gi
{ι : Type u_1}
{σ : Type u_2}
{A : Type u_3}
[Semiring A]
[DecidableEq ι]
[AddMonoid ι]
[SetLike σ A]
[AddSubmonoidClass σ A]
(𝒜 : ι → σ)
[GradedRing 𝒜]
:
toIdeal : HomogeneousIdeal 𝒜 → Ideal A and Ideal.homogeneousCore 𝒜 forms a Galois
coinsertion.
Instances For
theorem
Ideal.homogeneousCore_eq_sSup
{ι : Type u_1}
{σ : Type u_2}
{A : Type u_3}
[Semiring A]
[DecidableEq ι]
[AddMonoid ι]
[SetLike σ A]
[AddSubmonoidClass σ A]
(𝒜 : ι → σ)
[GradedRing 𝒜]
(I : Ideal A)
:
homogeneousCore 𝒜 I = sSup {J : HomogeneousIdeal 𝒜 | J.toIdeal ≤ I}
theorem
Ideal.homogeneousCore'_eq_sSup
{ι : Type u_1}
{σ : Type u_2}
{A : Type u_3}
[Semiring A]
[DecidableEq ι]
[AddMonoid ι]
[SetLike σ A]
[AddSubmonoidClass σ A]
(𝒜 : ι → σ)
[GradedRing 𝒜]
(I : Ideal A)
:
homogeneousCore' 𝒜 I = sSup {J : Ideal A | IsHomogeneous 𝒜 J ∧ J ≤ I}
Homogeneous hulls #
def
Ideal.homogeneousHull
{ι : Type u_1}
{σ : Type u_2}
{A : Type u_3}
[Semiring A]
[DecidableEq ι]
[AddMonoid ι]
[SetLike σ A]
[AddSubmonoidClass σ A]
(𝒜 : ι → σ)
[GradedRing 𝒜]
(I : Ideal A)
:
For any I : Ideal A, not necessarily homogeneous, I.homogeneousHull 𝒜 is
the smallest homogeneous ideal containing I.
Instances For
theorem
Ideal.le_toIdeal_homogeneousHull
{ι : Type u_1}
{σ : Type u_2}
{A : Type u_3}
[Semiring A]
[DecidableEq ι]
[AddMonoid ι]
[SetLike σ A]
[AddSubmonoidClass σ A]
(𝒜 : ι → σ)
[GradedRing 𝒜]
(I : Ideal A)
:
theorem
Ideal.homogeneousHull_mono
{ι : Type u_1}
{σ : Type u_2}
{A : Type u_3}
[Semiring A]
[DecidableEq ι]
[AddMonoid ι]
[SetLike σ A]
[AddSubmonoidClass σ A]
(𝒜 : ι → σ)
[GradedRing 𝒜]
:
theorem
Ideal.IsHomogeneous.toIdeal_homogeneousHull_eq_self
{ι : Type u_1}
{σ : Type u_2}
{A : Type u_3}
[Semiring A]
[DecidableEq ι]
[AddMonoid ι]
[SetLike σ A]
[AddSubmonoidClass σ A]
{𝒜 : ι → σ}
[GradedRing 𝒜]
{I : Ideal A}
(h : IsHomogeneous 𝒜 I)
:
(homogeneousHull 𝒜 I).toIdeal = I
@[simp]
theorem
HomogeneousIdeal.homogeneousHull_toIdeal_eq_self
{ι : Type u_1}
{σ : Type u_2}
{A : Type u_3}
[Semiring A]
[DecidableEq ι]
[AddMonoid ι]
[SetLike σ A]
[AddSubmonoidClass σ A]
{𝒜 : ι → σ}
[GradedRing 𝒜]
(I : HomogeneousIdeal 𝒜)
:
Ideal.homogeneousHull 𝒜 I.toIdeal = I
theorem
Ideal.toIdeal_homogeneousHull_eq_iSup
{ι : Type u_1}
{σ : Type u_2}
{A : Type u_3}
[Semiring A]
[DecidableEq ι]
[AddMonoid ι]
[SetLike σ A]
[AddSubmonoidClass σ A]
(𝒜 : ι → σ)
[GradedRing 𝒜]
(I : Ideal A)
:
(homogeneousHull 𝒜 I).toIdeal = ⨆ (i : ι), span (⇑(GradedRing.proj 𝒜 i) '' ↑I)
theorem
Ideal.homogeneousHull_eq_iSup
{ι : Type u_1}
{σ : Type u_2}
{A : Type u_3}
[Semiring A]
[DecidableEq ι]
[AddMonoid ι]
[SetLike σ A]
[AddSubmonoidClass σ A]
(𝒜 : ι → σ)
[GradedRing 𝒜]
(I : Ideal A)
:
homogeneousHull 𝒜 I = ⨆ (i : ι), { toSubmodule := span (⇑(GradedRing.proj 𝒜 i) '' ↑I), is_homogeneous' := ⋯ }
theorem
Ideal.homogeneousHull.gc
{ι : Type u_1}
{σ : Type u_2}
{A : Type u_3}
[Semiring A]
[DecidableEq ι]
[AddMonoid ι]
[SetLike σ A]
[AddSubmonoidClass σ A]
(𝒜 : ι → σ)
[GradedRing 𝒜]
:
def
Ideal.homogeneousHull.gi
{ι : Type u_1}
{σ : Type u_2}
{A : Type u_3}
[Semiring A]
[DecidableEq ι]
[AddMonoid ι]
[SetLike σ A]
[AddSubmonoidClass σ A]
(𝒜 : ι → σ)
[GradedRing 𝒜]
:
Ideal.homogeneousHull 𝒜 and toIdeal : HomogeneousIdeal 𝒜 → Ideal A form a Galois
insertion.
Instances For
theorem
Ideal.homogeneousHull_eq_sInf
{ι : Type u_1}
{σ : Type u_2}
{A : Type u_3}
[Semiring A]
[DecidableEq ι]
[AddMonoid ι]
[SetLike σ A]
[AddSubmonoidClass σ A]
(𝒜 : ι → σ)
[GradedRing 𝒜]
(I : Ideal A)
:
homogeneousHull 𝒜 I = sInf {J : HomogeneousIdeal 𝒜 | I ≤ J.toIdeal}
def
HomogeneousIdeal.irrelevant
{ι : Type u_1}
{σ : Type u_2}
{A : Type u_3}
[Semiring A]
[DecidableEq ι]
[AddCommMonoid ι]
[PartialOrder ι]
[CanonicallyOrderedAdd ι]
[SetLike σ A]
[AddSubmonoidClass σ A]
(𝒜 : ι → σ)
[GradedRing 𝒜]
:
For a graded ring ⨁ᵢ 𝒜ᵢ graded by
[AddCommMonoid ι] [PartialOrder ι] [CanonicallyOrderedAdd ι], the irrelevant ideal refers to
⨁_{i>0} 𝒜ᵢ, or equivalently {a | a₀ = 0}. This definition is used in Proj construction where
ι is always ℕ so the irrelevant ideal is simply elements with 0 as 0-th coordinate.
Instances For
For a graded ring ⨁ᵢ 𝒜ᵢ graded by
[AddCommMonoid ι] [PartialOrder ι] [CanonicallyOrderedAdd ι], the irrelevant ideal refers to
⨁_{i>0} 𝒜ᵢ, or equivalently {a | a₀ = 0}. This definition is used in Proj construction where
ι is always ℕ so the irrelevant ideal is simply elements with 0 as 0-th coordinate.
Instances For
@[simp]
theorem
HomogeneousIdeal.mem_irrelevant_iff
{ι : Type u_1}
{σ : Type u_2}
{A : Type u_3}
[Semiring A]
[DecidableEq ι]
[AddCommMonoid ι]
[PartialOrder ι]
[CanonicallyOrderedAdd ι]
[SetLike σ A]
[AddSubmonoidClass σ A]
(𝒜 : ι → σ)
[GradedRing 𝒜]
(a : A)
:
a ∈ irrelevant 𝒜 ↔ (GradedRing.proj 𝒜 0) a = 0
@[simp]
theorem
HomogeneousIdeal.toIdeal_irrelevant
{ι : Type u_1}
{σ : Type u_2}
{A : Type u_3}
[Semiring A]
[DecidableEq ι]
[AddCommMonoid ι]
[PartialOrder ι]
[CanonicallyOrderedAdd ι]
[SetLike σ A]
[AddSubmonoidClass σ A]
(𝒜 : ι → σ)
[GradedRing 𝒜]
:
theorem
HomogeneousIdeal.mem_irrelevant_of_mem
{ι : Type u_1}
{σ : Type u_2}
{A : Type u_3}
[Semiring A]
[DecidableEq ι]
[AddCommMonoid ι]
[PartialOrder ι]
[CanonicallyOrderedAdd ι]
[SetLike σ A]
[AddSubmonoidClass σ A]
(𝒜 : ι → σ)
[GradedRing 𝒜]
{x : A}
{i : ι}
(hi : 0 < i)
(hx : x ∈ 𝒜 i)
:
x ∈ irrelevant 𝒜
theorem
HomogeneousIdeal.irrelevant_eq_iSup
{ι : Type u_1}
{σ : Type u_2}
{A : Type u_3}
[Semiring A]
[DecidableEq ι]
[AddCommMonoid ι]
[PartialOrder ι]
[CanonicallyOrderedAdd ι]
[SetLike σ A]
[AddSubmonoidClass σ A]
(𝒜 : ι → σ)
[GradedRing 𝒜]
:
(irrelevant 𝒜).toAddSubmonoid = ⨆ (i : ι), ⨆ (_ : i > 0), AddSubmonoid.ofClass (𝒜 i)
irrelevant 𝒜 = ⨁_{i>0} 𝒜ᵢ
theorem
HomogeneousIdeal.irrelevant_eq_closure
{ι : Type u_1}
{σ : Type u_2}
{A : Type u_3}
[Semiring A]
[DecidableEq ι]
[AddCommMonoid ι]
[PartialOrder ι]
[CanonicallyOrderedAdd ι]
[SetLike σ A]
[AddSubmonoidClass σ A]
(𝒜 : ι → σ)
[GradedRing 𝒜]
:
(irrelevant 𝒜).toAddSubmonoid = AddSubmonoid.closure (⋃ (i : ι), ⋃ (_ : i > 0), ↑(𝒜 i))
theorem
HomogeneousIdeal.irrelevant_eq_span
{ι : Type u_1}
{σ : Type u_2}
{A : Type u_3}
[Semiring A]
[DecidableEq ι]
[AddCommMonoid ι]
[PartialOrder ι]
[CanonicallyOrderedAdd ι]
[SetLike σ A]
[AddSubmonoidClass σ A]
(𝒜 : ι → σ)
[GradedRing 𝒜]
:
(irrelevant 𝒜).toIdeal = Ideal.span (⋃ (i : ι), ⋃ (_ : i > 0), ↑(𝒜 i))
theorem
HomogeneousIdeal.toAddSubmonoid_irrelevant_le
{ι : Type u_1}
{σ : Type u_2}
{A : Type u_3}
[Semiring A]
[DecidableEq ι]
[AddCommMonoid ι]
[PartialOrder ι]
[CanonicallyOrderedAdd ι]
[SetLike σ A]
[AddSubmonoidClass σ A]
(𝒜 : ι → σ)
[GradedRing 𝒜]
{P : AddSubmonoid A}
:
(irrelevant 𝒜).toAddSubmonoid ≤ P ↔ ∀ i > 0, AddSubmonoid.ofClass (𝒜 i) ≤ P
theorem
HomogeneousIdeal.toIdeal_irrelevant_le
{ι : Type u_1}
{σ : Type u_2}
{A : Type u_3}
[Semiring A]
[DecidableEq ι]
[AddCommMonoid ι]
[PartialOrder ι]
[CanonicallyOrderedAdd ι]
[SetLike σ A]
[AddSubmonoidClass σ A]
(𝒜 : ι → σ)
[GradedRing 𝒜]
{I : Ideal A}
:
(irrelevant 𝒜).toIdeal ≤ I ↔ ∀ i > 0, AddSubmonoid.ofClass (𝒜 i) ≤ I.toAddSubmonoid
theorem
HomogeneousIdeal.irrelevant_le
{ι : Type u_1}
{σ : Type u_2}
{A : Type u_3}
[Semiring A]
[DecidableEq ι]
[AddCommMonoid ι]
[PartialOrder ι]
[CanonicallyOrderedAdd ι]
[SetLike σ A]
[AddSubmonoidClass σ A]
(𝒜 : ι → σ)
[GradedRing 𝒜]
{P : HomogeneousIdeal 𝒜}
:
irrelevant 𝒜 ≤ P ↔ ∀ i > 0, AddSubmonoid.ofClass (𝒜 i) ≤ P.toAddSubmonoid