Homogeneous submodules of a graded module

This file defines homogeneous submodule of a graded module ⨁ᵢ ℳᵢ over graded ring ⨁ᵢ 𝒜ᵢ and operations on them.

Main definitions

For any p : Submodule A M:

• Submodule.IsHomogeneous ℳ p: The property that a submodule is closed under GradedModule.proj.
• HomogeneousSubmodule 𝒜 ℳ: The structure extending submodules which satisfy Submodule.IsHomogeneous.

Implementation notes

The notion of homogeneous submodule does not rely on a graded ring, only a decomposition of the the module. However, most interesting properties of homogeneous submodules do rely on the base ring being a graded ring. For technical reasons, we make HomogeneousSubmodule depend on a graded ring. For example, if the definition of a homogeneous submodule does not depend on a graded ring, the instance that HomogeneousSubmodule is a complete lattice cannot be synthesized due to synthesation order.

Tags

graded algebra, homogeneous

def Submodule.IsHomogeneous {ιM : Type u_2} {σM : Type u_4} {A : Type u_5} {M : Type u_6} [Semiring A] [AddCommMonoid M] [Module A M] (p : Submodule A M) (ℳ : ιM → σM) [DecidableEq ιM] [SetLike σM M] [AddSubmonoidClass σM M] [DirectSum.Decomposition ℳ] : Prop

An A-submodule p ⊆ M is homogeneous if for every m ∈ p, all homogeneous components of m are in p.

Equations

• p.IsHomogeneous ℳ = DirectSum.SetLike.IsHomogeneous ℳ p

theorem Submodule.IsHomogeneous.mem_iff {ιM : Type u_2} {σM : Type u_4} {A : Type u_5} {M : Type u_6} [Semiring A] [AddCommMonoid M] [Module A M] {p : Submodule A M} (ℳ : ιM → σM) [DecidableEq ιM] [SetLike σM M] [AddSubmonoidClass σM M] [DirectSum.Decomposition ℳ] (hp : p.IsHomogeneous ℳ) {x : M} : x ∈ p ↔ ∀ (i : ιM), ↑(((DirectSum.decompose ℳ) x) i) ∈ p

structure HomogeneousSubmodule {ιA : Type u_1} {ιM : Type u_2} {σA : Type u_3} {σM : Type u_4} {A : Type u_5} {M : Type u_6} [Semiring A] [AddCommMonoid M] [Module A M] (𝒜 : ιA → σA) (ℳ : ιM → σM) [DecidableEq ιA] [AddMonoid ιA] [SetLike σA A] [AddSubmonoidClass σA A] [GradedRing 𝒜] [DecidableEq ιM] [SetLike σM M] [AddSubmonoidClass σM M] [DirectSum.Decomposition ℳ] [VAdd ιA ιM] [SetLike.GradedSMul 𝒜 ℳ] extends Submodule A M : Type u_6

For any Semiring A, we collect the homogeneous submodule of A-modules into a type.

• carrier : Set M
• add_mem' {a b : M} : a ∈ self.carrier → b ∈ self.carrier → a + b ∈ self.carrier
• zero_mem' : 0 ∈ self.carrier
• smul_mem' (c : A) {x : M} : x ∈ self.carrier → c • x ∈ self.carrier
• is_homogeneous' : self.IsHomogeneous ℳ

instance instSetLikeHomogeneousSubmodule {ιA : Type u_1} {ιM : Type u_2} {σA : Type u_3} {σM : Type u_4} {A : Type u_5} {M : Type u_6} [Semiring A] [AddCommMonoid M] [Module A M] (𝒜 : ιA → σA) (ℳ : ιM → σM) [DecidableEq ιA] [AddMonoid ιA] [SetLike σA A] [AddSubmonoidClass σA A] [GradedRing 𝒜] [DecidableEq ιM] [SetLike σM M] [AddSubmonoidClass σM M] [DirectSum.Decomposition ℳ] [VAdd ιA ιM] [SetLike.GradedSMul 𝒜 ℳ] : SetLike (HomogeneousSubmodule 𝒜 ℳ) M

Equations

• instSetLikeHomogeneousSubmodule 𝒜 ℳ = { coe := fun (X : HomogeneousSubmodule 𝒜 ℳ) => ↑X.toSubmodule, coe_injective' := ⋯ }

instance instAddSubmonoidClassHomogeneousSubmodule {ιA : Type u_1} {ιM : Type u_2} {σA : Type u_3} {σM : Type u_4} {A : Type u_5} {M : Type u_6} [Semiring A] [AddCommMonoid M] [Module A M] (𝒜 : ιA → σA) (ℳ : ιM → σM) [DecidableEq ιA] [AddMonoid ιA] [SetLike σA A] [AddSubmonoidClass σA A] [GradedRing 𝒜] [DecidableEq ιM] [SetLike σM M] [AddSubmonoidClass σM M] [DirectSum.Decomposition ℳ] [VAdd ιA ιM] [SetLike.GradedSMul 𝒜 ℳ] : AddSubmonoidClass (HomogeneousSubmodule 𝒜 ℳ) M

instance instSMulMemClassHomogeneousSubmodule {ιA : Type u_1} {ιM : Type u_2} {σA : Type u_3} {σM : Type u_4} {A : Type u_5} {M : Type u_6} [Semiring A] [AddCommMonoid M] [Module A M] (𝒜 : ιA → σA) (ℳ : ιM → σM) [DecidableEq ιA] [AddMonoid ιA] [SetLike σA A] [AddSubmonoidClass σA A] [GradedRing 𝒜] [DecidableEq ιM] [SetLike σM M] [AddSubmonoidClass σM M] [DirectSum.Decomposition ℳ] [VAdd ιA ιM] [SetLike.GradedSMul 𝒜 ℳ] : SMulMemClass (HomogeneousSubmodule 𝒜 ℳ) A M

theorem HomogeneousSubmodule.isHomogeneous {ιA : Type u_1} {ιM : Type u_2} {σA : Type u_3} {σM : Type u_4} {A : Type u_5} {M : Type u_6} [Semiring A] [AddCommMonoid M] [Module A M] {𝒜 : ιA → σA} {ℳ : ιM → σM} [DecidableEq ιA] [AddMonoid ιA] [SetLike σA A] [AddSubmonoidClass σA A] [GradedRing 𝒜] [DecidableEq ιM] [SetLike σM M] [AddSubmonoidClass σM M] [DirectSum.Decomposition ℳ] [VAdd ιA ιM] [SetLike.GradedSMul 𝒜 ℳ] (p : HomogeneousSubmodule 𝒜 ℳ) : p.IsHomogeneous ℳ

theorem HomogeneousSubmodule.toSubmodule_injective {ιA : Type u_1} {ιM : Type u_2} {σA : Type u_3} {σM : Type u_4} {A : Type u_5} {M : Type u_6} [Semiring A] [AddCommMonoid M] [Module A M] (𝒜 : ιA → σA) (ℳ : ιM → σM) [DecidableEq ιA] [AddMonoid ιA] [SetLike σA A] [AddSubmonoidClass σA A] [GradedRing 𝒜] [DecidableEq ιM] [SetLike σM M] [AddSubmonoidClass σM M] [DirectSum.Decomposition ℳ] [VAdd ιA ιM] [SetLike.GradedSMul 𝒜 ℳ] : Function.Injective toSubmodule

instance HomogeneousSubmodule.setLike {ιA : Type u_1} {ιM : Type u_2} {σA : Type u_3} {σM : Type u_4} {A : Type u_5} {M : Type u_6} [Semiring A] [AddCommMonoid M] [Module A M] (𝒜 : ιA → σA) (ℳ : ιM → σM) [DecidableEq ιA] [AddMonoid ιA] [SetLike σA A] [AddSubmonoidClass σA A] [GradedRing 𝒜] [DecidableEq ιM] [SetLike σM M] [AddSubmonoidClass σM M] [DirectSum.Decomposition ℳ] [VAdd ιA ιM] [SetLike.GradedSMul 𝒜 ℳ] : SetLike (HomogeneousSubmodule 𝒜 ℳ) M

Equations

• HomogeneousSubmodule.setLike 𝒜 ℳ = { coe := fun (p : HomogeneousSubmodule 𝒜 ℳ) => ↑p.toSubmodule, coe_injective' := ⋯ }

theorem HomogeneousSubmodule.ext {ιA : Type u_1} {ιM : Type u_2} {σA : Type u_3} {σM : Type u_4} {A : Type u_5} {M : Type u_6} [Semiring A] [AddCommMonoid M] [Module A M] (𝒜 : ιA → σA) (ℳ : ιM → σM) [DecidableEq ιA] [AddMonoid ιA] [SetLike σA A] [AddSubmonoidClass σA A] [GradedRing 𝒜] [DecidableEq ιM] [SetLike σM M] [AddSubmonoidClass σM M] [DirectSum.Decomposition ℳ] [VAdd ιA ιM] [SetLike.GradedSMul 𝒜 ℳ] {I J : HomogeneousSubmodule 𝒜 ℳ} (h : I.toSubmodule = J.toSubmodule) : I = J

theorem HomogeneousSubmodule.ext_iff {ιA : Type u_1} {ιM : Type u_2} {σA : Type u_3} {σM : Type u_4} {A : Type u_5} {M : Type u_6} [Semiring A] [AddCommMonoid M] [Module A M] {𝒜 : ιA → σA} {ℳ : ιM → σM} [DecidableEq ιA] [AddMonoid ιA] [SetLike σA A] [AddSubmonoidClass σA A] [GradedRing 𝒜] [DecidableEq ιM] [SetLike σM M] [AddSubmonoidClass σM M] [DirectSum.Decomposition ℳ] [VAdd ιA ιM] [SetLike.GradedSMul 𝒜 ℳ] {I J : HomogeneousSubmodule 𝒜 ℳ} : I = J ↔ I.toSubmodule = J.toSubmodule

theorem HomogeneousSubmodule.ext' {ιA : Type u_1} {ιM : Type u_2} {σA : Type u_3} {σM : Type u_4} {A : Type u_5} {M : Type u_6} [Semiring A] [AddCommMonoid M] [Module A M] (𝒜 : ιA → σA) (ℳ : ιM → σM) [DecidableEq ιA] [AddMonoid ιA] [SetLike σA A] [AddSubmonoidClass σA A] [GradedRing 𝒜] [DecidableEq ιM] [SetLike σM M] [AddSubmonoidClass σM M] [DirectSum.Decomposition ℳ] [VAdd ιA ιM] [SetLike.GradedSMul 𝒜 ℳ] {I J : HomogeneousSubmodule 𝒜 ℳ} (h : ∀ (i : ιM), ∀ x ∈ ℳ i, x ∈ I ↔ x ∈ J) : I = J

The set-theoretic extensionality of HomogeneousSubmodule.

@[simp]

theorem HomogeneousSubmodule.mem_toSubmodule_iff {ιA : Type u_1} {ιM : Type u_2} {σA : Type u_3} {σM : Type u_4} {A : Type u_5} {M : Type u_6} [Semiring A] [AddCommMonoid M] [Module A M] (𝒜 : ιA → σA) (ℳ : ιM → σM) [DecidableEq ιA] [AddMonoid ιA] [SetLike σA A] [AddSubmonoidClass σA A] [GradedRing 𝒜] [DecidableEq ιM] [SetLike σM M] [AddSubmonoidClass σM M] [DirectSum.Decomposition ℳ] [VAdd ιA ιM] [SetLike.GradedSMul 𝒜 ℳ] {I : HomogeneousSubmodule 𝒜 ℳ} {x : M} : x ∈ I.toSubmodule ↔ x ∈ I