Ideal.homogeneousCore'_le
theorem Ideal.homogeneousCore'_le :
∀ {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [inst : Semiring A] [inst_1 : SetLike σ A] (𝒜 : ι → σ) (I : Ideal A),
Ideal.homogeneousCore' 𝒜 I ≤ I
This theorem states that for any type `ι`, any set-like type `σ`, any semiring `A`, any map `𝒜` from `ι` to `σ`, and any ideal `I` in `A`, the 'homogeneous core' of the ideal `I` (as calculated by the function `Ideal.homogeneousCore'`) is a sub-ideal of `I`. In other words, all elements of the 'homogeneous core' of `I` also belong to `I`.
More concisely: For any semiring `A`, ideal `I`, map `𝒜` from type `ι` to set-like `σ`, the homogeneous core of `I` (as calculated by `Ideal.homogeneousCore'`) is a sub-ideal of `I`.
|
Ideal.IsHomogeneous.toIdeal_homogeneousCore_eq_self
theorem Ideal.IsHomogeneous.toIdeal_homogeneousCore_eq_self :
∀ {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [inst : Semiring A] [inst_1 : SetLike σ A]
[inst_2 : AddSubmonoidClass σ A] {𝒜 : ι → σ} [inst_3 : DecidableEq ι] [inst_4 : AddMonoid ι]
[inst_5 : GradedRing 𝒜] {I : Ideal A}, Ideal.IsHomogeneous 𝒜 I → (Ideal.homogeneousCore 𝒜 I).toIdeal = I
This theorem asserts that for any ideal `I` of a semiring `A`, if `I` is a homogeneous ideal under grading by `𝒜`, then the ideal obtained by converting the homogeneous core of `I` to an ideal is equal to `I` itself. Here, the homogeneous core of an ideal is the set of all elements whose all homogeneous components belong to the ideal. A homogeneous ideal is an ideal in which for every element, all its homogeneous components are in the ideal.
More concisely: For any homogeneous ideal `I` in a graded semiring `A`, the ideal generated by the homogeneous components of elements in `I` is equal to `I` itself.
|
HomogeneousIdeal.isHomogeneous
theorem HomogeneousIdeal.isHomogeneous :
∀ {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [inst : Semiring A] [inst_1 : SetLike σ A]
[inst_2 : AddSubmonoidClass σ A] {𝒜 : ι → σ} [inst_3 : DecidableEq ι] [inst_4 : AddMonoid ι]
[inst_5 : GradedRing 𝒜] (I : HomogeneousIdeal 𝒜), Ideal.IsHomogeneous 𝒜 I.toIdeal
The theorem `HomogeneousIdeal.isHomogeneous` states that for any given types `ι`, `σ`, `A`, and any given semiring `A`, any given set-like `σ` of `A`, any addSubmonoid class of `σ` over `A`, any function `𝒜` from `ι` to `σ`, a decidable equality on `ι`, an addition operation on `ι`, and a Graded Ring `𝒜`, if we have a homogeneous ideal `I` of `𝒜`, then the ideal we get by converting this homogeneous ideal to an ideal using the `HomogeneousIdeal.toIdeal` function is also a homogeneous ideal according to the `Ideal.IsHomogeneous` property. In short, this theorem ensures that the conversion of a homogeneous ideal to an ideal preserves the homogeneous property.
More concisely: Given a homogeneous ideal in a graded ring, the ideal obtained by converting it using `HomogeneousIdeal.toIdeal` function is also a homogeneous ideal.
|
HomogeneousIdeal.ext
theorem HomogeneousIdeal.ext :
∀ {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [inst : Semiring A] [inst_1 : SetLike σ A]
[inst_2 : AddSubmonoidClass σ A] {𝒜 : ι → σ} [inst_3 : DecidableEq ι] [inst_4 : AddMonoid ι]
[inst_5 : GradedRing 𝒜] {I J : HomogeneousIdeal 𝒜}, I.toIdeal = J.toIdeal → I = J
This theorem states that for any given types `ι`, `σ`, and `A` where `A` is a semiring, `σ` is a set-like structure in `A` and supports addition with a submonoid structure, `ι` has a decidable equality and addition structure, `𝒜` is a map from `ι` to `σ`, and a graded ring is defined over `𝒜`, then for any two homogeneous ideals `I` and `J` over `𝒜`, if their conversions to ideals in `A` (using the `HomogeneousIdeal.toIdeal` function) are equal, then the homogeneous ideals `I` and `J` are themselves equal. This theorem asserts the injectivity of the conversion operation from a homogeneous ideal to an ideal.
More concisely: Given types `ι`, `σ`, and `A`, where `A` is a semiring, `σ` is a set-like semigroup over `A`, `ι` has decidable equality and addition, `𝒜 : ι → σ`, and a graded ring is defined over `𝒜`, the conversion function `HomogeneousIdeal.toIdeal` from homogeneous ideals over `𝒜` to ideals in `A` is injective.
|
HomogeneousIdeal.toIdeal_injective
theorem HomogeneousIdeal.toIdeal_injective :
∀ {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [inst : Semiring A] [inst_1 : SetLike σ A]
[inst_2 : AddSubmonoidClass σ A] {𝒜 : ι → σ} [inst_3 : DecidableEq ι] [inst_4 : AddMonoid ι]
[inst_5 : GradedRing 𝒜], Function.Injective HomogeneousIdeal.toIdeal
The theorem `HomogeneousIdeal.toIdeal_injective` asserts that for any types `ι`, `σ`, and `A`, given that `A` forms a semiring, `σ` is a set-like of `A`, `σ` also forms an additive submonoid of `A`, `𝒜` is a function from `ι` to `σ`, the equality of `ι` is decidable, `ι` forms an additive monoid, and `𝒜` forms a graded ring, the function `HomogeneousIdeal.toIdeal` that converts a homogeneous ideal to an ideal is injective. In other words, if two homogeneous ideals are mapped to the same ideal by the function `HomogeneousIdeal.toIdeal`, then those two homogeneous ideals are the same. This injectivity holds universally across all such `ι`, `σ`, and `A`.
More concisely: Given a semiring `A`, a set-like `σ` that forms an additive submonoid and is graded over a decidably-equivalent additive monoid `ι`, the function `HomogeneousIdeal.toIdeal` mapping homogeneous ideals to ideals is injective.
|
Ideal.toIdeal_homogeneousCore_le
theorem Ideal.toIdeal_homogeneousCore_le :
∀ {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [inst : Semiring A] [inst_1 : SetLike σ A]
[inst_2 : AddSubmonoidClass σ A] (𝒜 : ι → σ) [inst_3 : DecidableEq ι] [inst_4 : AddMonoid ι]
[inst_5 : GradedRing 𝒜] (I : Ideal A), (Ideal.homogeneousCore 𝒜 I).toIdeal ≤ I
This theorem asserts that for any semiring `A`, any type `σ` such that `σ` behaves like a subset of `A`, any type `ι` with decidable equality and addition operation, any function `𝒜` from `ι` to `σ`, and any ideal `I` in `A`, the ideal obtained by converting the homogeneous core of `I` via function `𝒜` into an ideal is a subset of `I`. The homogeneous core of an ideal is the sub-ideal consisting of all homogeneous elements of the ideal.
In simpler terms, the theorem states that the ideal formed by the homogeneous elements of an ideal (when considered in the context of a graded ring structure given by `𝒜`) is always contained within the original ideal. This is a statement about the relationship between an ideal and its homogeneous core in a graded ring structure.
More concisely: Given a semiring `A`, a type `σ` behaving like a subset of `A`, a decidable type `ι`, a function `𝒜` from `ι` to `σ`, and an ideal `I` in `A`, the ideal generated by the homogeneous elements of `I` under `𝒜` is contained in `I`.
|
Ideal.le_toIdeal_homogeneousHull
theorem Ideal.le_toIdeal_homogeneousHull :
∀ {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [inst : Semiring A] [inst_1 : DecidableEq ι] [inst_2 : AddMonoid ι]
[inst_3 : SetLike σ A] [inst_4 : AddSubmonoidClass σ A] (𝒜 : ι → σ) [inst_5 : GradedRing 𝒜] (I : Ideal A),
I ≤ (Ideal.homogeneousHull 𝒜 I).toIdeal
This theorem, `Ideal.le_toIdeal_homogeneousHull`, asserts that for any semiring `A`, any ideal `I` in `A`, any function `𝒜` mapping from a type `ι` to a type `σ`, and given suitable conditions that `A` is `SetLike` (can be treated as a set) and `σ` is an `AddSubmonoidClass` of `A`, if `ι` has decidable equality and `ι` is an add monoid, and the function `𝒜` forms a graded ring, then the ideal `I` is less than or equal to the ideal obtained from converting the homogeneous hull of `I` with respect to `𝒜` into an ideal. In other words, the ideal `I` is contained within or equal to the ideal that results from taking the homogeneous hull of `I` and then converting that into an ideal. The homogeneous hull of an ideal is a type of "closure" of the ideal that includes all elements that can be formed by taking homogeneous elements (those that can be expressed as a single grade in a graded ring) from the ideal.
More concisely: For any semiring `A`, ideal `I` in `A`, function `𝒜` mapping from a decidable add monoid `ι` to an add-submonoid `σ` of `A`, if `I` is contained in the ideal obtained from the homogeneous hull of `I` with respect to `𝒜`, then `I` is contained in or equal to the ideal generated by the homogeneous hull.
|