Homogeneous subsemirings of a graded semiring

This file defines homogeneous subsemirings of a graded semiring, as well as operations on them.

Main definitions

• HomogeneousSubsemiring 𝒜: The type of subsemirings which satisfy SetLike.IsHomogeneous.

theorem DirectSum.SetLike.IsHomogeneous.mem_iff {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [AddMonoid ι] [Semiring A] [SetLike σ A] [AddSubmonoidClass σ A] (𝒜 : ι → σ) [DecidableEq ι] [GradedRing 𝒜] {R : Subsemiring A} (hR : IsHomogeneous 𝒜 R) {a : A} : a ∈ R ↔ ∀ (i : ι), ↑(((decompose 𝒜) a) i) ∈ R

structure HomogeneousSubsemiring {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [AddMonoid ι] [Semiring A] [SetLike σ A] [AddSubmonoidClass σ A] (𝒜 : ι → σ) [DecidableEq ι] [GradedRing 𝒜] extends Subsemiring A : Type u_3

A HomogeneousSubsemiring is a Subsemiring that satisfies IsHomogeneous.

• carrier : Set A
• mul_mem' {a b : A} : a ∈ self.carrier → b ∈ self.carrier → a * b ∈ self.carrier
• one_mem' : 1 ∈ self.carrier
• add_mem' {a b : A} : a ∈ self.carrier → b ∈ self.carrier → a + b ∈ self.carrier
• zero_mem' : 0 ∈ self.carrier
• is_homogeneous' : DirectSum.SetLike.IsHomogeneous 𝒜 self.toSubsemiring

theorem HomogeneousSubsemiring.toSubsemiring_injective {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [AddMonoid ι] [Semiring A] [SetLike σ A] [AddSubmonoidClass σ A] {𝒜 : ι → σ} [DecidableEq ι] [GradedRing 𝒜] : Function.Injective toSubsemiring

instance HomogeneousSubsemiring.setLike {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [AddMonoid ι] [Semiring A] [SetLike σ A] [AddSubmonoidClass σ A] {𝒜 : ι → σ} [DecidableEq ι] [GradedRing 𝒜] : SetLike (HomogeneousSubsemiring 𝒜) A

Equations

• HomogeneousSubsemiring.setLike = { coe := fun (x : HomogeneousSubsemiring 𝒜) => x.carrier, coe_injective' := ⋯ }

theorem HomogeneousSubsemiring.isHomogeneous {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [AddMonoid ι] [Semiring A] [SetLike σ A] [AddSubmonoidClass σ A] {𝒜 : ι → σ} [DecidableEq ι] [GradedRing 𝒜] (R : HomogeneousSubsemiring 𝒜) : DirectSum.SetLike.IsHomogeneous 𝒜 R

instance HomogeneousSubsemiring.subsemiringClass {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [AddMonoid ι] [Semiring A] [SetLike σ A] [AddSubmonoidClass σ A] {𝒜 : ι → σ} [DecidableEq ι] [GradedRing 𝒜] : SubsemiringClass (HomogeneousSubsemiring 𝒜) A

theorem HomogeneousSubsemiring.ext {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [AddMonoid ι] [Semiring A] [SetLike σ A] [AddSubmonoidClass σ A] {𝒜 : ι → σ} [DecidableEq ι] [GradedRing 𝒜] {R S : HomogeneousSubsemiring 𝒜} (h : R.toSubsemiring = S.toSubsemiring) : R = S

theorem HomogeneousSubsemiring.ext_iff {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [AddMonoid ι] [Semiring A] [SetLike σ A] [AddSubmonoidClass σ A] {𝒜 : ι → σ} [DecidableEq ι] [GradedRing 𝒜] {R S : HomogeneousSubsemiring 𝒜} : R = S ↔ R.toSubsemiring = S.toSubsemiring

theorem HomogeneousSubsemiring.ext' {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [AddMonoid ι] [Semiring A] [SetLike σ A] [AddSubmonoidClass σ A] {𝒜 : ι → σ} [DecidableEq ι] [GradedRing 𝒜] {R S : HomogeneousSubsemiring 𝒜} (h : ∀ (i : ι), ∀ a ∈ 𝒜 i, a ∈ R ↔ a ∈ S) : R = S

@[simp]

theorem HomogeneousSubsemiring.mem_iff {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [AddMonoid ι] [Semiring A] [SetLike σ A] [AddSubmonoidClass σ A] {𝒜 : ι → σ} [DecidableEq ι] [GradedRing 𝒜] {R : HomogeneousSubsemiring 𝒜} {a : A} : a ∈ R.toSubsemiring ↔ a ∈ R

theorem IsHomogeneous.subsemiringClosure {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [AddMonoid ι] [Semiring A] [SetLike σ A] [AddSubmonoidClass σ A] {𝒜 : ι → σ} [DecidableEq ι] [GradedRing 𝒜] {s : Set A} (h : ∀ (i : ι) ⦃x : A⦄, x ∈ s → ↑(((DirectSum.decompose 𝒜) x) i) ∈ s) : DirectSum.SetLike.IsHomogeneous 𝒜 (Subsemiring.closure s)

theorem IsHomogeneous.subsemiringClosure_of_isHomogeneousElem {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [AddMonoid ι] [Semiring A] [SetLike σ A] [AddSubmonoidClass σ A] {𝒜 : ι → σ} [DecidableEq ι] [GradedRing 𝒜] {s : Set A} (h : ∀ x ∈ s, SetLike.IsHomogeneousElem 𝒜 x) : DirectSum.SetLike.IsHomogeneous 𝒜 (Subsemiring.closure s)

def Subsemiring.homogeneousCore {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [AddMonoid ι] [Semiring A] [SetLike σ A] [AddSubmonoidClass σ A] (𝒜 : ι → σ) [DecidableEq ι] [GradedRing 𝒜] (R : Subsemiring A) : HomogeneousSubsemiring 𝒜

For any subsemiring R, not necessarily homogeneous, R.homogeneousCore 𝒜 is the largest homogeneous subsemiring contained in R.

Equations

• Subsemiring.homogeneousCore 𝒜 R = { toSubsemiring := Subsemiring.closure (Subtype.val '' (Subtype.val ⁻¹' ↑R)), is_homogeneous' := ⋯ }

theorem Subsemiring.homogeneousCore_mono {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [AddMonoid ι] [Semiring A] [SetLike σ A] [AddSubmonoidClass σ A] (𝒜 : ι → σ) [DecidableEq ι] [GradedRing 𝒜] : Monotone (homogeneousCore 𝒜)

theorem Subsemiring.toSubsemiring_homogeneousCore_le {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [AddMonoid ι] [Semiring A] [SetLike σ A] [AddSubmonoidClass σ A] (𝒜 : ι → σ) [DecidableEq ι] [GradedRing 𝒜] (R : Subsemiring A) : (homogeneousCore 𝒜 R).toSubsemiring ≤ R

theorem Subsemiring.isHomogeneous_iff_forall_subset {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [AddMonoid ι] [Semiring A] [SetLike σ A] [AddSubmonoidClass σ A] (𝒜 : ι → σ) [DecidableEq ι] [GradedRing 𝒜] (R : Subsemiring A) : DirectSum.SetLike.IsHomogeneous 𝒜 R ↔ ∀ (i : ι), ↑R ⊆ ⇑(GradedRing.proj 𝒜 i) ⁻¹' ↑R

theorem Subsemiring.isHomogeneous_iff_subset_iInter {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [AddMonoid ι] [Semiring A] [SetLike σ A] [AddSubmonoidClass σ A] (𝒜 : ι → σ) [DecidableEq ι] [GradedRing 𝒜] (R : Subsemiring A) : DirectSum.SetLike.IsHomogeneous 𝒜 R ↔ ↑R ⊆ ⋂ (i : ι), ⇑(GradedRing.proj 𝒜 i) ⁻¹' ↑R