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.IsHomogeneous
is preserved by⊥
,⊤
,⊔
,⊓
,⨆
,⨅
, and so the subtype of homogeneous ideals inherits a complete lattice structure.Ideal.homogeneousCore.gi
:Ideal.homogeneousCore
forms a galois insertion with coercion.Ideal.homogeneousHull.gi
:Ideal.homogeneousHull
forms 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
An I : Ideal A
is homogeneous if for every r ∈ I
, all homogeneous components
of r
are in I
.
Equations
- Ideal.IsHomogeneous 𝒜 I = ∀ (i : ι) ⦃r : A⦄, r ∈ I → ↑(((DirectSum.decompose 𝒜) r) i) ∈ I
Instances For
For any Semiring A
, we collect the homogeneous ideals of A
into a type.
Instances For
Converting a homogeneous ideal to an ideal.
Equations
- I.toIdeal = I.toSubmodule
Instances For
Equations
- HomogeneousIdeal.setLike = { coe := fun (I : HomogeneousIdeal 𝒜) => ↑I.toIdeal, coe_injective' := ⋯ }
For any I : Ideal A
, not necessarily homogeneous, I.homogeneousCore' 𝒜
is the largest homogeneous ideal of A
contained in I
, as an ideal.
Equations
- Ideal.homogeneousCore' 𝒜 I = Ideal.span (Subtype.val '' (Subtype.val ⁻¹' ↑I))
Instances For
For any I : Ideal A
, not necessarily homogeneous, I.homogeneousCore' 𝒜
is the largest homogeneous ideal of A
contained in I
.
Equations
- Ideal.homogeneousCore 𝒜 I = { toSubmodule := Ideal.homogeneousCore' 𝒜 I, is_homogeneous' := ⋯ }
Instances For
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
.
Equations
- HomogeneousIdeal.instPartialOrder = SetLike.instPartialOrder
Equations
- HomogeneousIdeal.instMax = { max := fun (I J : HomogeneousIdeal 𝒜) => { toSubmodule := I.toIdeal ⊔ J.toIdeal, is_homogeneous' := ⋯ } }
Equations
- HomogeneousIdeal.instMin = { min := fun (I J : HomogeneousIdeal 𝒜) => { toSubmodule := I.toIdeal ⊓ J.toIdeal, is_homogeneous' := ⋯ } }
Equations
- HomogeneousIdeal.instSupSet = { sSup := fun (S : Set (HomogeneousIdeal 𝒜)) => { toSubmodule := ⨆ s ∈ S, s.toIdeal, is_homogeneous' := ⋯ } }
Equations
- HomogeneousIdeal.instInfSet = { sInf := fun (S : Set (HomogeneousIdeal 𝒜)) => { toSubmodule := ⨅ s ∈ S, s.toIdeal, is_homogeneous' := ⋯ } }
Equations
- HomogeneousIdeal.completeLattice = Function.Injective.completeLattice HomogeneousIdeal.toIdeal ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
Equations
- HomogeneousIdeal.instAdd = { add := fun (x1 x2 : HomogeneousIdeal 𝒜) => x1 ⊔ x2 }
Equations
- instMulHomogeneousIdeal = { mul := fun (I J : HomogeneousIdeal 𝒜) => { toSubmodule := I.toIdeal * J.toIdeal, is_homogeneous' := ⋯ } }
Homogeneous core #
Note that many results about the homogeneous core came earlier in this file, as they are helpful for building the lattice structure.
toIdeal : HomogeneousIdeal 𝒜 → Ideal A
and Ideal.homogeneousCore 𝒜
forms a galois
coinsertion.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Homogeneous hulls #
For any I : Ideal A
, not necessarily homogeneous, I.homogeneousHull 𝒜
is
the smallest homogeneous ideal containing I
.
Equations
- Ideal.homogeneousHull 𝒜 I = { toSubmodule := Ideal.span {r : A | ∃ (i : ι) (x : ↥I), ↑(((DirectSum.decompose 𝒜) ↑x) i) = r}, is_homogeneous' := ⋯ }
Instances For
Ideal.homogeneousHull 𝒜
and toIdeal : HomogeneousIdeal 𝒜 → Ideal A
form a galois
insertion.
Equations
- One or more equations did not get rendered due to their size.
Instances For
For a graded ring ⨁ᵢ 𝒜ᵢ
graded by a CanonicallyOrderedAddCommMonoid ι
, 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.
Future work #
Here in the definition, ι
is assumed to be CanonicallyOrderedAddCommMonoid
. However, the notion
of irrelevant ideal makes sense in a more general setting by defining it as the ideal of elements
with 0
as i-th coordinate for all i ≤ 0
, i.e. {a | ∀ (i : ι), i ≤ 0 → aᵢ = 0}
.
Equations
- HomogeneousIdeal.irrelevant 𝒜 = { toSubmodule := RingHom.ker (GradedRing.projZeroRingHom 𝒜), is_homogeneous' := ⋯ }