Homogeneous ideals of a graded algebra #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
This file defines homogeneous ideals of graded_ring 𝒜 where 𝒜 : ι → submodule R A and
operations on them.
Main definitions #
For any I : ideal A:
ideal.is_homogeneous 𝒜 I: The property that an ideal is closed undergraded_ring.proj.homogeneous_ideal 𝒜: The structure extending ideals which satisfyideal.is_homogeneousideal.homogeneous_core I 𝒜: The largest homogeneous ideal smaller thanI.ideal.homogeneous_hull I 𝒜: The smallest homogeneous ideal larger thanI.
Main statements #
homogeneous_ideal.complete_lattice:ideal.is_homogeneousis preserved by⊥,⊤,⊔,⊓,⨆,⨅, and so the subtype of homogeneous ideals inherits a complete lattice structure.ideal.homogeneous_core.gi:ideal.homogeneous_coreforms a galois insertion with coercion.ideal.homogeneous_hull.gi:ideal.homogeneous_hullforms a galois insertion with coercion.
Implementation notes #
We introduce ideal.homogeneous_core' earlier than might be expected so that we can get access
to ideal.is_homogeneous.iff_exists as quickly as possible.
Tags #
graded algebra, homogeneous
def
ideal.is_homogeneous
{ι : Type u_1}
{σ : Type u_2}
{A : Type u_4}
[semiring A]
[set_like σ A]
[add_submonoid_class σ A]
(𝒜 : ι → σ)
[decidable_eq ι]
[add_monoid ι]
[graded_ring 𝒜]
(I : ideal A) :
Prop
An I : ideal A is homogeneous if for every r ∈ I, all homogeneous components
of r are in I.
Equations
- ideal.is_homogeneous 𝒜 I = ∀ (i : ι) ⦃r : A⦄, r ∈ I → ↑(⇑(⇑(direct_sum.decompose 𝒜) r) i) ∈ I
structure
homogeneous_ideal
{ι : Type u_1}
{σ : Type u_2}
{A : Type u_4}
[semiring A]
[set_like σ A]
[add_submonoid_class σ A]
(𝒜 : ι → σ)
[decidable_eq ι]
[add_monoid ι]
[graded_ring 𝒜] :
Type u_4
- to_submodule : submodule A A
- is_homogeneous' : ideal.is_homogeneous 𝒜 self.to_submodule
For any semiring A, we collect the homogeneous ideals of A into a type.
Instances for homogeneous_ideal
- homogeneous_ideal.has_sizeof_inst
- homogeneous_ideal.set_like
- homogeneous_ideal.partial_order
- homogeneous_ideal.has_top
- homogeneous_ideal.has_bot
- homogeneous_ideal.has_sup
- homogeneous_ideal.has_inf
- homogeneous_ideal.has_Sup
- homogeneous_ideal.has_Inf
- homogeneous_ideal.complete_lattice
- homogeneous_ideal.has_add
- homogeneous_ideal.inhabited
- homogeneous_ideal.has_mul
def
homogeneous_ideal.to_ideal
{ι : Type u_1}
{σ : Type u_2}
{A : Type u_4}
[semiring A]
[set_like σ A]
[add_submonoid_class σ A]
{𝒜 : ι → σ}
[decidable_eq ι]
[add_monoid ι]
[graded_ring 𝒜]
(I : homogeneous_ideal 𝒜) :
ideal A
Converting a homogeneous ideal to an ideal
Equations
- I.to_ideal = I.to_submodule
Instances for homogeneous_ideal.to_ideal
theorem
homogeneous_ideal.is_homogeneous
{ι : Type u_1}
{σ : Type u_2}
{A : Type u_4}
[semiring A]
[set_like σ A]
[add_submonoid_class σ A]
{𝒜 : ι → σ}
[decidable_eq ι]
[add_monoid ι]
[graded_ring 𝒜]
(I : homogeneous_ideal 𝒜) :
theorem
homogeneous_ideal.to_ideal_injective
{ι : Type u_1}
{σ : Type u_2}
{A : Type u_4}
[semiring A]
[set_like σ A]
[add_submonoid_class σ A]
{𝒜 : ι → σ}
[decidable_eq ι]
[add_monoid ι]
[graded_ring 𝒜] :
@[protected, instance]
def
homogeneous_ideal.set_like
{ι : Type u_1}
{σ : Type u_2}
{A : Type u_4}
[semiring A]
[set_like σ A]
[add_submonoid_class σ A]
{𝒜 : ι → σ}
[decidable_eq ι]
[add_monoid ι]
[graded_ring 𝒜] :
set_like (homogeneous_ideal 𝒜) A
Equations
- homogeneous_ideal.set_like = {coe := λ (I : homogeneous_ideal 𝒜), ↑(I.to_ideal), coe_injective' := _}
@[ext]
theorem
homogeneous_ideal.ext
{ι : Type u_1}
{σ : Type u_2}
{A : Type u_4}
[semiring A]
[set_like σ A]
[add_submonoid_class σ A]
{𝒜 : ι → σ}
[decidable_eq ι]
[add_monoid ι]
[graded_ring 𝒜]
{I J : homogeneous_ideal 𝒜}
(h : I.to_ideal = J.to_ideal) :
I = J
@[simp]
theorem
homogeneous_ideal.mem_iff
{ι : Type u_1}
{σ : Type u_2}
{A : Type u_4}
[semiring A]
[set_like σ A]
[add_submonoid_class σ A]
{𝒜 : ι → σ}
[decidable_eq ι]
[add_monoid ι]
[graded_ring 𝒜]
{I : homogeneous_ideal 𝒜}
{x : A} :
def
ideal.homogeneous_core'
{ι : Type u_1}
{σ : Type u_2}
{A : Type u_4}
[semiring A]
[set_like σ A]
(𝒜 : ι → σ)
(I : ideal A) :
ideal A
For any I : ideal A, not necessarily homogeneous, I.homogeneous_core' 𝒜
is the largest homogeneous ideal of A contained in I, as an ideal.
Equations
- ideal.homogeneous_core' 𝒜 I = ideal.span (coe '' (coe ⁻¹' ↑I))
theorem
ideal.is_homogeneous_iff_forall_subset
{ι : Type u_1}
{σ : Type u_2}
{A : Type u_4}
[semiring A]
[set_like σ A]
[add_submonoid_class σ A]
(𝒜 : ι → σ)
[decidable_eq ι]
[add_monoid ι]
[graded_ring 𝒜]
(I : ideal A) :
ideal.is_homogeneous 𝒜 I ↔ ∀ (i : ι), ↑I ⊆ ⇑(graded_ring.proj 𝒜 i) ⁻¹' ↑I
theorem
ideal.is_homogeneous_iff_subset_Inter
{ι : Type u_1}
{σ : Type u_2}
{A : Type u_4}
[semiring A]
[set_like σ A]
[add_submonoid_class σ A]
(𝒜 : ι → σ)
[decidable_eq ι]
[add_monoid ι]
[graded_ring 𝒜]
(I : ideal A) :
ideal.is_homogeneous 𝒜 I ↔ ↑I ⊆ ⋂ (i : ι), ⇑(graded_ring.proj 𝒜 i) ⁻¹' ↑I
theorem
ideal.mul_homogeneous_element_mem_of_mem
{ι : Type u_1}
{σ : Type u_2}
{A : Type u_4}
[semiring A]
[set_like σ A]
[add_submonoid_class σ A]
(𝒜 : ι → σ)
[decidable_eq ι]
[add_monoid ι]
[graded_ring 𝒜]
{I : ideal A}
(r x : A)
(hx₁ : set_like.is_homogeneous 𝒜 x)
(hx₂ : x ∈ I)
(j : ι) :
⇑(graded_ring.proj 𝒜 j) (r * x) ∈ I
theorem
ideal.is_homogeneous_span
{ι : Type u_1}
{σ : Type u_2}
{A : Type u_4}
[semiring A]
[set_like σ A]
[add_submonoid_class σ A]
(𝒜 : ι → σ)
[decidable_eq ι]
[add_monoid ι]
[graded_ring 𝒜]
(s : set A)
(h : ∀ (x : A), x ∈ s → set_like.is_homogeneous 𝒜 x) :
def
ideal.homogeneous_core
{ι : Type u_1}
{σ : Type u_2}
{A : Type u_4}
[semiring A]
[set_like σ A]
[add_submonoid_class σ A]
(𝒜 : ι → σ)
[decidable_eq ι]
[add_monoid ι]
[graded_ring 𝒜]
(I : ideal A) :
For any I : ideal A, not necessarily homogeneous, I.homogeneous_core' 𝒜
is the largest homogeneous ideal of A contained in I.
Equations
- ideal.homogeneous_core 𝒜 I = {to_submodule := ideal.homogeneous_core' 𝒜 I, is_homogeneous' := _}
theorem
ideal.homogeneous_core_mono
{ι : Type u_1}
{σ : Type u_2}
{A : Type u_4}
[semiring A]
[set_like σ A]
[add_submonoid_class σ A]
(𝒜 : ι → σ)
[decidable_eq ι]
[add_monoid ι]
[graded_ring 𝒜] :
theorem
ideal.to_ideal_homogeneous_core_le
{ι : Type u_1}
{σ : Type u_2}
{A : Type u_4}
[semiring A]
[set_like σ A]
[add_submonoid_class σ A]
(𝒜 : ι → σ)
[decidable_eq ι]
[add_monoid ι]
[graded_ring 𝒜]
(I : ideal A) :
(ideal.homogeneous_core 𝒜 I).to_ideal ≤ I
theorem
ideal.mem_homogeneous_core_of_is_homogeneous_of_mem
{ι : Type u_1}
{σ : Type u_2}
{A : Type u_4}
[semiring A]
[set_like σ A]
[add_submonoid_class σ A]
{𝒜 : ι → σ}
[decidable_eq ι]
[add_monoid ι]
[graded_ring 𝒜]
{I : ideal A}
{x : A}
(h : set_like.is_homogeneous 𝒜 x)
(hmem : x ∈ I) :
x ∈ ideal.homogeneous_core 𝒜 I
theorem
ideal.is_homogeneous.to_ideal_homogeneous_core_eq_self
{ι : Type u_1}
{σ : Type u_2}
{A : Type u_4}
[semiring A]
[set_like σ A]
[add_submonoid_class σ A]
{𝒜 : ι → σ}
[decidable_eq ι]
[add_monoid ι]
[graded_ring 𝒜]
{I : ideal A}
(h : ideal.is_homogeneous 𝒜 I) :
(ideal.homogeneous_core 𝒜 I).to_ideal = I
@[simp]
theorem
homogeneous_ideal.to_ideal_homogeneous_core_eq_self
{ι : Type u_1}
{σ : Type u_2}
{A : Type u_4}
[semiring A]
[set_like σ A]
[add_submonoid_class σ A]
{𝒜 : ι → σ}
[decidable_eq ι]
[add_monoid ι]
[graded_ring 𝒜]
(I : homogeneous_ideal 𝒜) :
ideal.homogeneous_core 𝒜 I.to_ideal = I
theorem
ideal.is_homogeneous.iff_eq
{ι : Type u_1}
{σ : Type u_2}
{A : Type u_4}
[semiring A]
[set_like σ A]
[add_submonoid_class σ A]
(𝒜 : ι → σ)
[decidable_eq ι]
[add_monoid ι]
[graded_ring 𝒜]
(I : ideal A) :
ideal.is_homogeneous 𝒜 I ↔ (ideal.homogeneous_core 𝒜 I).to_ideal = I
theorem
ideal.is_homogeneous.iff_exists
{ι : Type u_1}
{σ : Type u_2}
{A : Type u_4}
[semiring A]
[set_like σ A]
[add_submonoid_class σ A]
(𝒜 : ι → σ)
[decidable_eq ι]
[add_monoid ι]
[graded_ring 𝒜]
(I : ideal A) :
ideal.is_homogeneous 𝒜 I ↔ ∃ (S : set ↥(set_like.homogeneous_submonoid 𝒜)), I = ideal.span (coe '' S)
Operations #
In this section, we show that ideal.is_homogeneous is preserved by various notations, then use
these results to provide these notation typeclasses for homogeneous_ideal.
theorem
ideal.is_homogeneous.bot
{ι : Type u_1}
{σ : Type u_2}
{A : Type u_4}
[semiring A]
[decidable_eq ι]
[add_monoid ι]
[set_like σ A]
[add_submonoid_class σ A]
(𝒜 : ι → σ)
[graded_ring 𝒜] :
theorem
ideal.is_homogeneous.top
{ι : Type u_1}
{σ : Type u_2}
{A : Type u_4}
[semiring A]
[decidable_eq ι]
[add_monoid ι]
[set_like σ A]
[add_submonoid_class σ A]
(𝒜 : ι → σ)
[graded_ring 𝒜] :
theorem
ideal.is_homogeneous.inf
{ι : Type u_1}
{σ : Type u_2}
{A : Type u_4}
[semiring A]
[decidable_eq ι]
[add_monoid ι]
[set_like σ A]
[add_submonoid_class σ A]
{𝒜 : ι → σ}
[graded_ring 𝒜]
{I J : ideal A}
(HI : ideal.is_homogeneous 𝒜 I)
(HJ : ideal.is_homogeneous 𝒜 J) :
ideal.is_homogeneous 𝒜 (I ⊓ J)
theorem
ideal.is_homogeneous.sup
{ι : Type u_1}
{σ : Type u_2}
{A : Type u_4}
[semiring A]
[decidable_eq ι]
[add_monoid ι]
[set_like σ A]
[add_submonoid_class σ A]
{𝒜 : ι → σ}
[graded_ring 𝒜]
{I J : ideal A}
(HI : ideal.is_homogeneous 𝒜 I)
(HJ : ideal.is_homogeneous 𝒜 J) :
ideal.is_homogeneous 𝒜 (I ⊔ J)
@[protected]
theorem
ideal.is_homogeneous.supr
{ι : Type u_1}
{σ : Type u_2}
{A : Type u_4}
[semiring A]
[decidable_eq ι]
[add_monoid ι]
[set_like σ A]
[add_submonoid_class σ A]
{𝒜 : ι → σ}
[graded_ring 𝒜]
{κ : Sort u_3}
{f : κ → ideal A}
(h : ∀ (i : κ), ideal.is_homogeneous 𝒜 (f i)) :
ideal.is_homogeneous 𝒜 (⨆ (i : κ), f i)
@[protected]
theorem
ideal.is_homogeneous.infi
{ι : Type u_1}
{σ : Type u_2}
{A : Type u_4}
[semiring A]
[decidable_eq ι]
[add_monoid ι]
[set_like σ A]
[add_submonoid_class σ A]
{𝒜 : ι → σ}
[graded_ring 𝒜]
{κ : Sort u_3}
{f : κ → ideal A}
(h : ∀ (i : κ), ideal.is_homogeneous 𝒜 (f i)) :
ideal.is_homogeneous 𝒜 (⨅ (i : κ), f i)
theorem
ideal.is_homogeneous.supr₂
{ι : Type u_1}
{σ : Type u_2}
{A : Type u_4}
[semiring A]
[decidable_eq ι]
[add_monoid ι]
[set_like σ A]
[add_submonoid_class σ A]
{𝒜 : ι → σ}
[graded_ring 𝒜]
{κ : Sort u_3}
{κ' : κ → Sort u_5}
{f : Π (i : κ), κ' i → ideal A}
(h : ∀ (i : κ) (j : κ' i), ideal.is_homogeneous 𝒜 (f i j)) :
ideal.is_homogeneous 𝒜 (⨆ (i : κ) (j : κ' i), f i j)
theorem
ideal.is_homogeneous.infi₂
{ι : Type u_1}
{σ : Type u_2}
{A : Type u_4}
[semiring A]
[decidable_eq ι]
[add_monoid ι]
[set_like σ A]
[add_submonoid_class σ A]
{𝒜 : ι → σ}
[graded_ring 𝒜]
{κ : Sort u_3}
{κ' : κ → Sort u_5}
{f : Π (i : κ), κ' i → ideal A}
(h : ∀ (i : κ) (j : κ' i), ideal.is_homogeneous 𝒜 (f i j)) :
ideal.is_homogeneous 𝒜 (⨅ (i : κ) (j : κ' i), f i j)
theorem
ideal.is_homogeneous.Sup
{ι : Type u_1}
{σ : Type u_2}
{A : Type u_4}
[semiring A]
[decidable_eq ι]
[add_monoid ι]
[set_like σ A]
[add_submonoid_class σ A]
{𝒜 : ι → σ}
[graded_ring 𝒜]
{ℐ : set (ideal A)}
(h : ∀ (I : ideal A), I ∈ ℐ → ideal.is_homogeneous 𝒜 I) :
theorem
ideal.is_homogeneous.Inf
{ι : Type u_1}
{σ : Type u_2}
{A : Type u_4}
[semiring A]
[decidable_eq ι]
[add_monoid ι]
[set_like σ A]
[add_submonoid_class σ A]
{𝒜 : ι → σ}
[graded_ring 𝒜]
{ℐ : set (ideal A)}
(h : ∀ (I : ideal A), I ∈ ℐ → ideal.is_homogeneous 𝒜 I) :
@[protected, instance]
def
homogeneous_ideal.partial_order
{ι : Type u_1}
{σ : Type u_2}
{A : Type u_4}
[semiring A]
[decidable_eq ι]
[add_monoid ι]
[set_like σ A]
[add_submonoid_class σ A]
{𝒜 : ι → σ}
[graded_ring 𝒜] :
@[protected, instance]
def
homogeneous_ideal.has_top
{ι : Type u_1}
{σ : Type u_2}
{A : Type u_4}
[semiring A]
[decidable_eq ι]
[add_monoid ι]
[set_like σ A]
[add_submonoid_class σ A]
{𝒜 : ι → σ}
[graded_ring 𝒜] :
Equations
- homogeneous_ideal.has_top = {top := {to_submodule := ⊤, is_homogeneous' := _}}
@[protected, instance]
def
homogeneous_ideal.has_bot
{ι : Type u_1}
{σ : Type u_2}
{A : Type u_4}
[semiring A]
[decidable_eq ι]
[add_monoid ι]
[set_like σ A]
[add_submonoid_class σ A]
{𝒜 : ι → σ}
[graded_ring 𝒜] :
Equations
- homogeneous_ideal.has_bot = {bot := {to_submodule := ⊥, is_homogeneous' := _}}
@[protected, instance]
def
homogeneous_ideal.has_sup
{ι : Type u_1}
{σ : Type u_2}
{A : Type u_4}
[semiring A]
[decidable_eq ι]
[add_monoid ι]
[set_like σ A]
[add_submonoid_class σ A]
{𝒜 : ι → σ}
[graded_ring 𝒜] :
Equations
- homogeneous_ideal.has_sup = {sup := λ (I J : homogeneous_ideal 𝒜), {to_submodule := I.to_ideal ⊔ J.to_ideal, is_homogeneous' := _}}
@[protected, instance]
def
homogeneous_ideal.has_inf
{ι : Type u_1}
{σ : Type u_2}
{A : Type u_4}
[semiring A]
[decidable_eq ι]
[add_monoid ι]
[set_like σ A]
[add_submonoid_class σ A]
{𝒜 : ι → σ}
[graded_ring 𝒜] :
Equations
- homogeneous_ideal.has_inf = {inf := λ (I J : homogeneous_ideal 𝒜), {to_submodule := I.to_ideal ⊓ J.to_ideal, is_homogeneous' := _}}
@[protected, instance]
def
homogeneous_ideal.has_Sup
{ι : Type u_1}
{σ : Type u_2}
{A : Type u_4}
[semiring A]
[decidable_eq ι]
[add_monoid ι]
[set_like σ A]
[add_submonoid_class σ A]
{𝒜 : ι → σ}
[graded_ring 𝒜] :
Equations
- homogeneous_ideal.has_Sup = {Sup := λ (S : set (homogeneous_ideal 𝒜)), {to_submodule := ⨆ (s : homogeneous_ideal 𝒜) (H : s ∈ S), s.to_ideal, is_homogeneous' := _}}
@[protected, instance]
def
homogeneous_ideal.has_Inf
{ι : Type u_1}
{σ : Type u_2}
{A : Type u_4}
[semiring A]
[decidable_eq ι]
[add_monoid ι]
[set_like σ A]
[add_submonoid_class σ A]
{𝒜 : ι → σ}
[graded_ring 𝒜] :
Equations
- homogeneous_ideal.has_Inf = {Inf := λ (S : set (homogeneous_ideal 𝒜)), {to_submodule := ⨅ (s : homogeneous_ideal 𝒜) (H : s ∈ S), s.to_ideal, is_homogeneous' := _}}
@[simp]
theorem
homogeneous_ideal.coe_top
{ι : Type u_1}
{σ : Type u_2}
{A : Type u_4}
[semiring A]
[decidable_eq ι]
[add_monoid ι]
[set_like σ A]
[add_submonoid_class σ A]
{𝒜 : ι → σ}
[graded_ring 𝒜] :
@[simp]
theorem
homogeneous_ideal.coe_bot
{ι : Type u_1}
{σ : Type u_2}
{A : Type u_4}
[semiring A]
[decidable_eq ι]
[add_monoid ι]
[set_like σ A]
[add_submonoid_class σ A]
{𝒜 : ι → σ}
[graded_ring 𝒜] :
@[simp]
theorem
homogeneous_ideal.coe_sup
{ι : Type u_1}
{σ : Type u_2}
{A : Type u_4}
[semiring A]
[decidable_eq ι]
[add_monoid ι]
[set_like σ A]
[add_submonoid_class σ A]
{𝒜 : ι → σ}
[graded_ring 𝒜]
(I J : homogeneous_ideal 𝒜) :
@[simp]
theorem
homogeneous_ideal.coe_inf
{ι : Type u_1}
{σ : Type u_2}
{A : Type u_4}
[semiring A]
[decidable_eq ι]
[add_monoid ι]
[set_like σ A]
[add_submonoid_class σ A]
{𝒜 : ι → σ}
[graded_ring 𝒜]
(I J : homogeneous_ideal 𝒜) :
@[simp]
theorem
homogeneous_ideal.to_ideal_top
{ι : Type u_1}
{σ : Type u_2}
{A : Type u_4}
[semiring A]
[decidable_eq ι]
[add_monoid ι]
[set_like σ A]
[add_submonoid_class σ A]
{𝒜 : ι → σ}
[graded_ring 𝒜] :
@[simp]
theorem
homogeneous_ideal.to_ideal_bot
{ι : Type u_1}
{σ : Type u_2}
{A : Type u_4}
[semiring A]
[decidable_eq ι]
[add_monoid ι]
[set_like σ A]
[add_submonoid_class σ A]
{𝒜 : ι → σ}
[graded_ring 𝒜] :
@[simp]
theorem
homogeneous_ideal.to_ideal_sup
{ι : Type u_1}
{σ : Type u_2}
{A : Type u_4}
[semiring A]
[decidable_eq ι]
[add_monoid ι]
[set_like σ A]
[add_submonoid_class σ A]
{𝒜 : ι → σ}
[graded_ring 𝒜]
(I J : homogeneous_ideal 𝒜) :
@[simp]
theorem
homogeneous_ideal.to_ideal_inf
{ι : Type u_1}
{σ : Type u_2}
{A : Type u_4}
[semiring A]
[decidable_eq ι]
[add_monoid ι]
[set_like σ A]
[add_submonoid_class σ A]
{𝒜 : ι → σ}
[graded_ring 𝒜]
(I J : homogeneous_ideal 𝒜) :
@[simp]
theorem
homogeneous_ideal.to_ideal_Sup
{ι : Type u_1}
{σ : Type u_2}
{A : Type u_4}
[semiring A]
[decidable_eq ι]
[add_monoid ι]
[set_like σ A]
[add_submonoid_class σ A]
{𝒜 : ι → σ}
[graded_ring 𝒜]
(ℐ : set (homogeneous_ideal 𝒜)) :
(has_Sup.Sup ℐ).to_ideal = ⨆ (s : homogeneous_ideal 𝒜) (H : s ∈ ℐ), s.to_ideal
@[simp]
theorem
homogeneous_ideal.to_ideal_Inf
{ι : Type u_1}
{σ : Type u_2}
{A : Type u_4}
[semiring A]
[decidable_eq ι]
[add_monoid ι]
[set_like σ A]
[add_submonoid_class σ A]
{𝒜 : ι → σ}
[graded_ring 𝒜]
(ℐ : set (homogeneous_ideal 𝒜)) :
(has_Inf.Inf ℐ).to_ideal = ⨅ (s : homogeneous_ideal 𝒜) (H : s ∈ ℐ), s.to_ideal
@[simp]
theorem
homogeneous_ideal.to_ideal_supr
{ι : Type u_1}
{σ : Type u_2}
{A : Type u_4}
[semiring A]
[decidable_eq ι]
[add_monoid ι]
[set_like σ A]
[add_submonoid_class σ A]
{𝒜 : ι → σ}
[graded_ring 𝒜]
{κ : Sort u_3}
(s : κ → homogeneous_ideal 𝒜) :
@[simp]
theorem
homogeneous_ideal.to_ideal_infi
{ι : Type u_1}
{σ : Type u_2}
{A : Type u_4}
[semiring A]
[decidable_eq ι]
[add_monoid ι]
[set_like σ A]
[add_submonoid_class σ A]
{𝒜 : ι → σ}
[graded_ring 𝒜]
{κ : Sort u_3}
(s : κ → homogeneous_ideal 𝒜) :
@[simp]
theorem
homogeneous_ideal.to_ideal_supr₂
{ι : Type u_1}
{σ : Type u_2}
{A : Type u_4}
[semiring A]
[decidable_eq ι]
[add_monoid ι]
[set_like σ A]
[add_submonoid_class σ A]
{𝒜 : ι → σ}
[graded_ring 𝒜]
{κ : Sort u_3}
{κ' : κ → Sort u_5}
(s : Π (i : κ), κ' i → homogeneous_ideal 𝒜) :
@[simp]
theorem
homogeneous_ideal.to_ideal_infi₂
{ι : Type u_1}
{σ : Type u_2}
{A : Type u_4}
[semiring A]
[decidable_eq ι]
[add_monoid ι]
[set_like σ A]
[add_submonoid_class σ A]
{𝒜 : ι → σ}
[graded_ring 𝒜]
{κ : Sort u_3}
{κ' : κ → Sort u_5}
(s : Π (i : κ), κ' i → homogeneous_ideal 𝒜) :
@[simp]
theorem
homogeneous_ideal.eq_top_iff
{ι : Type u_1}
{σ : Type u_2}
{A : Type u_4}
[semiring A]
[decidable_eq ι]
[add_monoid ι]
[set_like σ A]
[add_submonoid_class σ A]
{𝒜 : ι → σ}
[graded_ring 𝒜]
(I : homogeneous_ideal 𝒜) :
@[simp]
theorem
homogeneous_ideal.eq_bot_iff
{ι : Type u_1}
{σ : Type u_2}
{A : Type u_4}
[semiring A]
[decidable_eq ι]
[add_monoid ι]
[set_like σ A]
[add_submonoid_class σ A]
{𝒜 : ι → σ}
[graded_ring 𝒜]
(I : homogeneous_ideal 𝒜) :
@[protected, instance]
def
homogeneous_ideal.complete_lattice
{ι : Type u_1}
{σ : Type u_2}
{A : Type u_4}
[semiring A]
[decidable_eq ι]
[add_monoid ι]
[set_like σ A]
[add_submonoid_class σ A]
{𝒜 : ι → σ}
[graded_ring 𝒜] :
Equations
- homogeneous_ideal.complete_lattice = function.injective.complete_lattice homogeneous_ideal.to_ideal homogeneous_ideal.complete_lattice._proof_1 homogeneous_ideal.complete_lattice._proof_2 homogeneous_ideal.complete_lattice._proof_3 homogeneous_ideal.complete_lattice._proof_4 homogeneous_ideal.complete_lattice._proof_5 homogeneous_ideal.complete_lattice._proof_6 homogeneous_ideal.complete_lattice._proof_7
@[protected, instance]
def
homogeneous_ideal.has_add
{ι : Type u_1}
{σ : Type u_2}
{A : Type u_4}
[semiring A]
[decidable_eq ι]
[add_monoid ι]
[set_like σ A]
[add_submonoid_class σ A]
{𝒜 : ι → σ}
[graded_ring 𝒜] :
Equations
@[simp]
theorem
homogeneous_ideal.to_ideal_add
{ι : Type u_1}
{σ : Type u_2}
{A : Type u_4}
[semiring A]
[decidable_eq ι]
[add_monoid ι]
[set_like σ A]
[add_submonoid_class σ A]
{𝒜 : ι → σ}
[graded_ring 𝒜]
(I J : homogeneous_ideal 𝒜) :
@[protected, instance]
def
homogeneous_ideal.inhabited
{ι : Type u_1}
{σ : Type u_2}
{A : Type u_4}
[semiring A]
[decidable_eq ι]
[add_monoid ι]
[set_like σ A]
[add_submonoid_class σ A]
{𝒜 : ι → σ}
[graded_ring 𝒜] :
Equations
theorem
ideal.is_homogeneous.mul
{ι : Type u_1}
{σ : Type u_2}
{A : Type u_4}
[comm_semiring A]
[decidable_eq ι]
[add_monoid ι]
[set_like σ A]
[add_submonoid_class σ A]
{𝒜 : ι → σ}
[graded_ring 𝒜]
{I J : ideal A}
(HI : ideal.is_homogeneous 𝒜 I)
(HJ : ideal.is_homogeneous 𝒜 J) :
ideal.is_homogeneous 𝒜 (I * J)
@[protected, instance]
def
homogeneous_ideal.has_mul
{ι : Type u_1}
{σ : Type u_2}
{A : Type u_4}
[comm_semiring A]
[decidable_eq ι]
[add_monoid ι]
[set_like σ A]
[add_submonoid_class σ A]
{𝒜 : ι → σ}
[graded_ring 𝒜] :
Equations
- homogeneous_ideal.has_mul = {mul := λ (I J : homogeneous_ideal 𝒜), {to_submodule := I.to_ideal * J.to_ideal, is_homogeneous' := _}}
@[simp]
theorem
homogeneous_ideal.to_ideal_mul
{ι : Type u_1}
{σ : Type u_2}
{A : Type u_4}
[comm_semiring A]
[decidable_eq ι]
[add_monoid ι]
[set_like σ A]
[add_submonoid_class σ A]
{𝒜 : ι → σ}
[graded_ring 𝒜]
(I J : homogeneous_ideal 𝒜) :
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.homogeneous_core.gc
{ι : Type u_1}
{σ : Type u_2}
{A : Type u_4}
[semiring A]
[decidable_eq ι]
[add_monoid ι]
[set_like σ A]
[add_submonoid_class σ A]
(𝒜 : ι → σ)
[graded_ring 𝒜] :
def
ideal.homogeneous_core.gi
{ι : Type u_1}
{σ : Type u_2}
{A : Type u_4}
[semiring A]
[decidable_eq ι]
[add_monoid ι]
[set_like σ A]
[add_submonoid_class σ A]
(𝒜 : ι → σ)
[graded_ring 𝒜] :
to_ideal : homogeneous_ideal 𝒜 → ideal A and ideal.homogeneous_core 𝒜 forms a galois
coinsertion
Equations
- ideal.homogeneous_core.gi 𝒜 = {choice := λ (I : ideal A) (HI : I ≤ (ideal.homogeneous_core 𝒜 I).to_ideal), {to_submodule := I, is_homogeneous' := _}, gc := _, u_l_le := _, choice_eq := _}
theorem
ideal.homogeneous_core_eq_Sup
{ι : Type u_1}
{σ : Type u_2}
{A : Type u_4}
[semiring A]
[decidable_eq ι]
[add_monoid ι]
[set_like σ A]
[add_submonoid_class σ A]
(𝒜 : ι → σ)
[graded_ring 𝒜]
(I : ideal A) :
ideal.homogeneous_core 𝒜 I = has_Sup.Sup {J : homogeneous_ideal 𝒜 | J.to_ideal ≤ I}
theorem
ideal.homogeneous_core'_eq_Sup
{ι : Type u_1}
{σ : Type u_2}
{A : Type u_4}
[semiring A]
[decidable_eq ι]
[add_monoid ι]
[set_like σ A]
[add_submonoid_class σ A]
(𝒜 : ι → σ)
[graded_ring 𝒜]
(I : ideal A) :
ideal.homogeneous_core' 𝒜 I = has_Sup.Sup {J : ideal A | ideal.is_homogeneous 𝒜 J ∧ J ≤ I}
Homogeneous hulls #
def
ideal.homogeneous_hull
{ι : Type u_1}
{σ : Type u_2}
{A : Type u_4}
[semiring A]
[decidable_eq ι]
[add_monoid ι]
[set_like σ A]
[add_submonoid_class σ A]
(𝒜 : ι → σ)
[graded_ring 𝒜]
(I : ideal A) :
For any I : ideal A, not necessarily homogeneous, I.homogeneous_hull 𝒜 is
the smallest homogeneous ideal containing I.
Equations
- ideal.homogeneous_hull 𝒜 I = {to_submodule := ideal.span {r : A | ∃ (i : ι) (x : ↥I), ↑(⇑(⇑(direct_sum.decompose 𝒜) ↑x) i) = r}, is_homogeneous' := _}
theorem
ideal.le_to_ideal_homogeneous_hull
{ι : Type u_1}
{σ : Type u_2}
{A : Type u_4}
[semiring A]
[decidable_eq ι]
[add_monoid ι]
[set_like σ A]
[add_submonoid_class σ A]
(𝒜 : ι → σ)
[graded_ring 𝒜]
(I : ideal A) :
I ≤ (ideal.homogeneous_hull 𝒜 I).to_ideal
theorem
ideal.homogeneous_hull_mono
{ι : Type u_1}
{σ : Type u_2}
{A : Type u_4}
[semiring A]
[decidable_eq ι]
[add_monoid ι]
[set_like σ A]
[add_submonoid_class σ A]
(𝒜 : ι → σ)
[graded_ring 𝒜] :
theorem
ideal.is_homogeneous.to_ideal_homogeneous_hull_eq_self
{ι : Type u_1}
{σ : Type u_2}
{A : Type u_4}
[semiring A]
[decidable_eq ι]
[add_monoid ι]
[set_like σ A]
[add_submonoid_class σ A]
{𝒜 : ι → σ}
[graded_ring 𝒜]
{I : ideal A}
(h : ideal.is_homogeneous 𝒜 I) :
(ideal.homogeneous_hull 𝒜 I).to_ideal = I
@[simp]
theorem
homogeneous_ideal.homogeneous_hull_to_ideal_eq_self
{ι : Type u_1}
{σ : Type u_2}
{A : Type u_4}
[semiring A]
[decidable_eq ι]
[add_monoid ι]
[set_like σ A]
[add_submonoid_class σ A]
{𝒜 : ι → σ}
[graded_ring 𝒜]
(I : homogeneous_ideal 𝒜) :
ideal.homogeneous_hull 𝒜 I.to_ideal = I
theorem
ideal.to_ideal_homogeneous_hull_eq_supr
{ι : Type u_1}
{σ : Type u_2}
{A : Type u_4}
[semiring A]
[decidable_eq ι]
[add_monoid ι]
[set_like σ A]
[add_submonoid_class σ A]
(𝒜 : ι → σ)
[graded_ring 𝒜]
(I : ideal A) :
(ideal.homogeneous_hull 𝒜 I).to_ideal = ⨆ (i : ι), ideal.span (⇑(graded_ring.proj 𝒜 i) '' ↑I)
theorem
ideal.homogeneous_hull_eq_supr
{ι : Type u_1}
{σ : Type u_2}
{A : Type u_4}
[semiring A]
[decidable_eq ι]
[add_monoid ι]
[set_like σ A]
[add_submonoid_class σ A]
(𝒜 : ι → σ)
[graded_ring 𝒜]
(I : ideal A) :
ideal.homogeneous_hull 𝒜 I = ⨆ (i : ι), {to_submodule := ideal.span (⇑(graded_ring.proj 𝒜 i) '' ↑I), is_homogeneous' := _}
theorem
ideal.homogeneous_hull.gc
{ι : Type u_1}
{σ : Type u_2}
{A : Type u_4}
[semiring A]
[decidable_eq ι]
[add_monoid ι]
[set_like σ A]
[add_submonoid_class σ A]
(𝒜 : ι → σ)
[graded_ring 𝒜] :
def
ideal.homogeneous_hull.gi
{ι : Type u_1}
{σ : Type u_2}
{A : Type u_4}
[semiring A]
[decidable_eq ι]
[add_monoid ι]
[set_like σ A]
[add_submonoid_class σ A]
(𝒜 : ι → σ)
[graded_ring 𝒜] :
ideal.homogeneous_hull 𝒜 and to_ideal : homogeneous_ideal 𝒜 → ideal A form a galois
insertion
Equations
- ideal.homogeneous_hull.gi 𝒜 = {choice := λ (I : ideal A) (H : (ideal.homogeneous_hull 𝒜 I).to_ideal ≤ I), {to_submodule := I, is_homogeneous' := _}, gc := _, le_l_u := _, choice_eq := _}
theorem
ideal.homogeneous_hull_eq_Inf
{ι : Type u_1}
{σ : Type u_2}
{A : Type u_4}
[semiring A]
[decidable_eq ι]
[add_monoid ι]
[set_like σ A]
[add_submonoid_class σ A]
(𝒜 : ι → σ)
[graded_ring 𝒜]
(I : ideal A) :
ideal.homogeneous_hull 𝒜 I = has_Inf.Inf {J : homogeneous_ideal 𝒜 | I ≤ J.to_ideal}
def
homogeneous_ideal.irrelevant
{ι : Type u_1}
{σ : Type u_2}
{A : Type u_4}
[semiring A]
[decidable_eq ι]
[canonically_ordered_add_monoid ι]
[set_like σ A]
[add_submonoid_class σ A]
(𝒜 : ι → σ)
[graded_ring 𝒜] :
For a graded ring ⨁ᵢ 𝒜ᵢ graded by a canonically_ordered_add_monoid ι, 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 canonically_ordered_add_monoid. 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
@[simp]
theorem
homogeneous_ideal.mem_irrelevant_iff
{ι : Type u_1}
{σ : Type u_2}
{A : Type u_4}
[semiring A]
[decidable_eq ι]
[canonically_ordered_add_monoid ι]
[set_like σ A]
[add_submonoid_class σ A]
(𝒜 : ι → σ)
[graded_ring 𝒜]
(a : A) :
a ∈ homogeneous_ideal.irrelevant 𝒜 ↔ ⇑(graded_ring.proj 𝒜 0) a = 0
@[simp]
theorem
homogeneous_ideal.to_ideal_irrelevant
{ι : Type u_1}
{σ : Type u_2}
{A : Type u_4}
[semiring A]
[decidable_eq ι]
[canonically_ordered_add_monoid ι]
[set_like σ A]
[add_submonoid_class σ A]
(𝒜 : ι → σ)
[graded_ring 𝒜] :