mathlib documentation

ring_theory.graded_algebra.homogeneous_ideal

Homogeneous ideals of a graded algebra #

This file defines homogeneous ideals of graded_ring ๐’œ where ๐’œ : ฮน โ†’ submodule R A and operations on them.

Main definitions #

For any I : ideal A:

Main statements #

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
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

For any semiring A, we collect the homogeneous ideals of A into a type.

Instances for homogeneous_ideal
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 ๐’œ) :

Converting a homogeneous ideal to an ideal

Equations
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 ๐’œ] :
Equations
@[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) :

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
theorem ideal.homogeneous_core'_mono {ฮน : Type u_1} {ฯƒ : Type u_2} {A : Type u_4} [semiring A] [set_like ฯƒ A] (๐’œ : ฮน โ†’ ฯƒ) :
theorem ideal.homogeneous_core'_le {ฮน : Type u_1} {ฯƒ : Type u_2} {A : Type u_4} [semiring A] [set_like ฯƒ A] (๐’œ : ฮน โ†’ ฯƒ) (I : ideal A) :
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) :
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) :
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
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) :
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) :
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) :
@[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 ๐’œ) :
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) :
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) :

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) :
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) :
@[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) :
ideal.is_homogeneous ๐’œ (has_Sup.Sup โ„)
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) :
ideal.is_homogeneous ๐’œ (has_Inf.Inf โ„)
@[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 ๐’œ] :
Equations
@[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
@[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
@[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
@[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
@[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
@[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
@[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 ๐’œ) :
(โจ† (i : ฮบ), s i).to_ideal = โจ† (i : ฮบ), (s i).to_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 ๐’œ) :
(โจ… (i : ฮบ), s i).to_ideal = โจ… (i : ฮบ), (s i).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} {ฮบ' : ฮบ โ†’ Sort u_5} (s : ฮ  (i : ฮบ), ฮบ' i โ†’ homogeneous_ideal ๐’œ) :
(โจ† (i : ฮบ) (j : ฮบ' i), s i j).to_ideal = โจ† (i : ฮบ) (j : ฮบ' i), (s i j).to_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 ๐’œ) :
(โจ… (i : ฮบ) (j : ฮบ' i), s i j).to_ideal = โจ… (i : ฮบ) (j : ฮบ' i), (s i j).to_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
@[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
@[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
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) :
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) :

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
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) :
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) :
@[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 ๐’œ) :
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
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) :
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) :
@[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 ๐’œ] :