Documentation

Mathlib.RingTheory.GradedAlgebra.HomogeneousIdeal

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:

Main statements #

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

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

Equations
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 : Ideal.IsHomogeneous 𝒜 I) {x : A} :
    x I ∀ (i : ι), (((DirectSum.decompose 𝒜) x) i) I
    structure HomogeneousIdeal {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [Semiring A] [SetLike σ A] [AddSubmonoidClass σ A] (𝒜 : ισ) [DecidableEq ι] [AddMonoid ι] [GradedRing 𝒜] extends Submodule , AddSubmonoid , SubMulAction , AddSubsemigroup :
    Type u_3

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

      Instances For
        theorem HomogeneousIdeal.is_homogeneous' {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [Semiring A] [SetLike σ A] [AddSubmonoidClass σ A] {𝒜 : ισ} [DecidableEq ι] [AddMonoid ι] [GradedRing 𝒜] (self : HomogeneousIdeal 𝒜) :
        Ideal.IsHomogeneous 𝒜 self.toSubmodule
        def HomogeneousIdeal.toIdeal {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [Semiring A] [SetLike σ A] [AddSubmonoidClass σ A] {𝒜 : ισ} [DecidableEq ι] [AddMonoid ι] [GradedRing 𝒜] (I : HomogeneousIdeal 𝒜) :

        Converting a homogeneous ideal to an ideal.

        Equations
        • I.toIdeal = I.toSubmodule
        Instances For
          theorem HomogeneousIdeal.isHomogeneous {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [Semiring A] [SetLike σ A] [AddSubmonoidClass σ A] {𝒜 : ισ} [DecidableEq ι] [AddMonoid ι] [GradedRing 𝒜] (I : HomogeneousIdeal 𝒜) :
          Ideal.IsHomogeneous 𝒜 I.toIdeal
          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 HomogeneousIdeal.toIdeal
          instance HomogeneousIdeal.setLike {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [Semiring A] [SetLike σ A] [AddSubmonoidClass σ A] {𝒜 : ισ} [DecidableEq ι] [AddMonoid ι] [GradedRing 𝒜] :
          Equations
          • HomogeneousIdeal.setLike = { coe := fun (I : HomogeneousIdeal 𝒜) => I.toIdeal, coe_injective' := }
          theorem HomogeneousIdeal.ext {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [Semiring A] [SetLike σ A] [AddSubmonoidClass σ A] {𝒜 : ισ} [DecidableEq ι] [AddMonoid ι] [GradedRing 𝒜] {I : HomogeneousIdeal 𝒜} {J : HomogeneousIdeal 𝒜} (h : I.toIdeal = J.toIdeal) :
          I = J
          theorem HomogeneousIdeal.ext' {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [Semiring A] [SetLike σ A] [AddSubmonoidClass σ A] {𝒜 : ισ} [DecidableEq ι] [AddMonoid ι] [GradedRing 𝒜] {I : HomogeneousIdeal 𝒜} {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) :

          For any I : Ideal A, not necessarily homogeneous, I.homogeneousCore' 𝒜 is the largest homogeneous ideal of A contained in I, as an ideal.

          Equations
          Instances For
            theorem Ideal.homogeneousCore'_mono {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [Semiring A] [SetLike σ A] (𝒜 : ισ) :
            theorem Ideal.homogeneousCore'_le {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [Semiring A] [SetLike σ A] (𝒜 : ισ) (I : Ideal A) :
            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) :
            Ideal.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) :
            Ideal.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 : A) (x : A) (hx₁ : SetLike.Homogeneous 𝒜 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 : xs, SetLike.Homogeneous 𝒜 x) :
            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.

            Equations
            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) :
              (Ideal.homogeneousCore 𝒜 I).toIdeal I
              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.Homogeneous 𝒜 x) (hmem : x 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 : Ideal.IsHomogeneous 𝒜 I) :
              (Ideal.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) :
              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) :
              Ideal.IsHomogeneous 𝒜 I ∃ (S : Set (SetLike.homogeneousSubmonoid 𝒜)), I = Ideal.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 : Ideal A} {J : Ideal A} (HI : Ideal.IsHomogeneous 𝒜 I) (HJ : Ideal.IsHomogeneous 𝒜 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 : Ideal A} {J : Ideal A} (HI : Ideal.IsHomogeneous 𝒜 I) (HJ : Ideal.IsHomogeneous 𝒜 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 : κ), Ideal.IsHomogeneous 𝒜 (f i)) :
              Ideal.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 : κ), Ideal.IsHomogeneous 𝒜 (f i)) :
              Ideal.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 : κ) → κ' iIdeal A} (h : ∀ (i : κ) (j : κ' i), Ideal.IsHomogeneous 𝒜 (f i j)) :
              Ideal.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 : κ) → κ' iIdeal A} (h : ∀ (i : κ) (j : κ' i), Ideal.IsHomogeneous 𝒜 (f i j)) :
              Ideal.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, Ideal.IsHomogeneous 𝒜 I) :
              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, Ideal.IsHomogeneous 𝒜 I) :
              instance HomogeneousIdeal.instPartialOrder {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [Semiring A] [DecidableEq ι] [AddMonoid ι] [SetLike σ A] [AddSubmonoidClass σ A] {𝒜 : ισ} [GradedRing 𝒜] :
              Equations
              • HomogeneousIdeal.instPartialOrder = SetLike.instPartialOrder
              instance HomogeneousIdeal.instTop {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [Semiring A] [DecidableEq ι] [AddMonoid ι] [SetLike σ A] [AddSubmonoidClass σ A] {𝒜 : ισ} [GradedRing 𝒜] :
              Equations
              • HomogeneousIdeal.instTop = { top := { toSubmodule := , is_homogeneous' := } }
              instance HomogeneousIdeal.instBot {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [Semiring A] [DecidableEq ι] [AddMonoid ι] [SetLike σ A] [AddSubmonoidClass σ A] {𝒜 : ισ} [GradedRing 𝒜] :
              Equations
              • HomogeneousIdeal.instBot = { bot := { toSubmodule := , is_homogeneous' := } }
              instance HomogeneousIdeal.instMax {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [Semiring A] [DecidableEq ι] [AddMonoid ι] [SetLike σ A] [AddSubmonoidClass σ A] {𝒜 : ισ} [GradedRing 𝒜] :
              Equations
              • HomogeneousIdeal.instMax = { max := fun (I J : HomogeneousIdeal 𝒜) => { toSubmodule := I.toIdeal J.toIdeal, is_homogeneous' := } }
              instance HomogeneousIdeal.instMin {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [Semiring A] [DecidableEq ι] [AddMonoid ι] [SetLike σ A] [AddSubmonoidClass σ A] {𝒜 : ισ} [GradedRing 𝒜] :
              Equations
              • HomogeneousIdeal.instMin = { min := fun (I J : HomogeneousIdeal 𝒜) => { toSubmodule := I.toIdeal J.toIdeal, is_homogeneous' := } }
              instance HomogeneousIdeal.instSupSet {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [Semiring A] [DecidableEq ι] [AddMonoid ι] [SetLike σ A] [AddSubmonoidClass σ A] {𝒜 : ισ} [GradedRing 𝒜] :
              Equations
              • HomogeneousIdeal.instSupSet = { sSup := fun (S : Set (HomogeneousIdeal 𝒜)) => { toSubmodule := sS, s.toIdeal, is_homogeneous' := } }
              instance HomogeneousIdeal.instInfSet {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [Semiring A] [DecidableEq ι] [AddMonoid ι] [SetLike σ A] [AddSubmonoidClass σ A] {𝒜 : ισ} [GradedRing 𝒜] :
              Equations
              • HomogeneousIdeal.instInfSet = { sInf := fun (S : Set (HomogeneousIdeal 𝒜)) => { toSubmodule := sS, s.toIdeal, is_homogeneous' := } }
              @[simp]
              theorem HomogeneousIdeal.coe_top {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [Semiring A] [DecidableEq ι] [AddMonoid ι] [SetLike σ A] [AddSubmonoidClass σ A] {𝒜 : ισ} [GradedRing 𝒜] :
              = Set.univ
              @[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 : HomogeneousIdeal 𝒜) (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 : HomogeneousIdeal 𝒜) (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 𝒜] :
              .toIdeal =
              @[simp]
              theorem HomogeneousIdeal.toIdeal_bot {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [Semiring A] [DecidableEq ι] [AddMonoid ι] [SetLike σ A] [AddSubmonoidClass σ A] {𝒜 : ισ} [GradedRing 𝒜] :
              .toIdeal =
              @[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 : HomogeneousIdeal 𝒜) (J : HomogeneousIdeal 𝒜) :
              (I J).toIdeal = I.toIdeal J.toIdeal
              @[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 : HomogeneousIdeal 𝒜) (J : HomogeneousIdeal 𝒜) :
              (I J).toIdeal = I.toIdeal J.toIdeal
              @[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 𝒜)) :
              (sSup ).toIdeal = s, s.toIdeal
              @[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 𝒜)) :
              (sInf ).toIdeal = s, s.toIdeal
              @[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 𝒜) :
              (⨆ (i : κ), s i).toIdeal = ⨆ (i : κ), (s i).toIdeal
              @[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 𝒜) :
              (⨅ (i : κ), s i).toIdeal = ⨅ (i : κ), (s i).toIdeal
              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 : κ) → κ' iHomogeneousIdeal 𝒜) :
              (⨆ (i : κ), ⨆ (j : κ' i), s i j).toIdeal = ⨆ (i : κ), ⨆ (j : κ' i), (s i j).toIdeal
              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 : κ) → κ' iHomogeneousIdeal 𝒜) :
              (⨅ (i : κ), ⨅ (j : κ' i), s i j).toIdeal = ⨅ (i : κ), ⨅ (j : κ' i), (s i j).toIdeal
              @[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 𝒜) :
              I = I.toIdeal =
              @[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 𝒜) :
              I = I.toIdeal =
              instance HomogeneousIdeal.completeLattice {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [Semiring A] [DecidableEq ι] [AddMonoid ι] [SetLike σ A] [AddSubmonoidClass σ A] {𝒜 : ισ} [GradedRing 𝒜] :
              Equations
              instance HomogeneousIdeal.instAdd {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [Semiring A] [DecidableEq ι] [AddMonoid ι] [SetLike σ A] [AddSubmonoidClass σ A] {𝒜 : ισ} [GradedRing 𝒜] :
              Equations
              @[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 : HomogeneousIdeal 𝒜) (J : HomogeneousIdeal 𝒜) :
              (I + J).toIdeal = I.toIdeal + J.toIdeal
              instance HomogeneousIdeal.instInhabited {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [Semiring A] [DecidableEq ι] [AddMonoid ι] [SetLike σ A] [AddSubmonoidClass σ A] {𝒜 : ισ} [GradedRing 𝒜] :
              Equations
              • HomogeneousIdeal.instInhabited = { default := }
              theorem Ideal.IsHomogeneous.mul {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [CommSemiring A] [DecidableEq ι] [AddMonoid ι] [SetLike σ A] [AddSubmonoidClass σ A] {𝒜 : ισ} [GradedRing 𝒜] {I : Ideal A} {J : Ideal A} (HI : Ideal.IsHomogeneous 𝒜 I) (HJ : Ideal.IsHomogeneous 𝒜 J) :
              instance instMulHomogeneousIdeal {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [CommSemiring A] [DecidableEq ι] [AddMonoid ι] [SetLike σ A] [AddSubmonoidClass σ A] {𝒜 : ισ} [GradedRing 𝒜] :
              Equations
              • instMulHomogeneousIdeal = { mul := fun (I J : HomogeneousIdeal 𝒜) => { toSubmodule := I.toIdeal * J.toIdeal, is_homogeneous' := } }
              @[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 : HomogeneousIdeal 𝒜) (J : HomogeneousIdeal 𝒜) :
              (I * J).toIdeal = I.toIdeal * J.toIdeal

              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 𝒜] :
              GaloisConnection HomogeneousIdeal.toIdeal (Ideal.homogeneousCore 𝒜)
              def Ideal.homogeneousCore.gi {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [Semiring A] [DecidableEq ι] [AddMonoid ι] [SetLike σ A] [AddSubmonoidClass σ A] (𝒜 : ισ) [GradedRing 𝒜] :
              GaloisCoinsertion HomogeneousIdeal.toIdeal (Ideal.homogeneousCore 𝒜)

              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
                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) :
                Ideal.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) :

                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.

                Equations
                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) :
                  I (Ideal.homogeneousHull 𝒜 I).toIdeal
                  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 : Ideal.IsHomogeneous 𝒜 I) :
                  (Ideal.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) :
                  (Ideal.homogeneousHull 𝒜 I).toIdeal = ⨆ (i : ι), Ideal.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) :
                  Ideal.homogeneousHull 𝒜 I = ⨆ (i : ι), { toSubmodule := Ideal.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 𝒜] :
                  GaloisConnection (Ideal.homogeneousHull 𝒜) HomogeneousIdeal.toIdeal
                  def Ideal.homogeneousHull.gi {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [Semiring A] [DecidableEq ι] [AddMonoid ι] [SetLike σ A] [AddSubmonoidClass σ A] (𝒜 : ισ) [GradedRing 𝒜] :
                  GaloisInsertion (Ideal.homogeneousHull 𝒜) HomogeneousIdeal.toIdeal

                  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
                    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) :
                    Ideal.homogeneousHull 𝒜 I = sInf {J : HomogeneousIdeal 𝒜 | I J.toIdeal}
                    def HomogeneousIdeal.irrelevant {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [Semiring A] [DecidableEq ι] [CanonicallyOrderedAddCommMonoid ι] [SetLike σ A] [AddSubmonoidClass σ A] (𝒜 : ισ) [GradedRing 𝒜] :

                    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
                    Instances For
                      @[simp]
                      theorem HomogeneousIdeal.mem_irrelevant_iff {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [Semiring A] [DecidableEq ι] [CanonicallyOrderedAddCommMonoid ι] [SetLike σ A] [AddSubmonoidClass σ A] (𝒜 : ισ) [GradedRing 𝒜] (a : A) :
                      @[simp]