Gradings of homogeneous submodules and of their quotients

Let G be an internal integer grading of an R-module M, and let U be a submodule which is homogeneous in Mathlib's sense SetLike.IsHomogeneous: it contains every homogeneous component of each of its elements. Then U and M ⧸ U inherit internal gradings.

• On U, the degree-p piece is the part of U lying in G.piece p.
• On M ⧸ U, the degree-p piece is the image of G.piece p under the quotient map. The images span because the quotient map is surjective, and they are independent because an element of U is the sum of its homogeneous components, all of which lie in U.

In both cases the homogeneous projections are those of M, transported along the inclusion and the quotient map respectively. Combining the two gives the grading of a subquotient, such as the cohomology ker d ⧸ im d of a differential of degree one.

The kernel of a homogeneous linear map is homogeneous (TauCeti.LinearMap.IsHomogeneous.isHomogeneous_ker), so it inherits a grading in the same way. The map may be linear over a larger ring S than the ring R of the grading, as for a differential over a polynomial ring whose variables move the degree; the kernel is then an S-module graded by R-submodules.

Main definitions

• TauCeti.InternalGrading.submodule: the grading of a homogeneous submodule.
• TauCeti.InternalGrading.ker: the grading of the kernel of a homogeneous linear map.
• TauCeti.InternalGrading.quotient: the grading of the quotient by a homogeneous submodule.

Main results

• TauCeti.InternalGrading.coe_decompose_submodule: homogeneous projection in a homogeneous submodule is homogeneous projection in the ambient module.
• TauCeti.InternalGrading.mem_ker_piece: an element of the kernel of a homogeneous map is homogeneous exactly when it is homogeneous in the source.
• TauCeti.InternalGrading.decompose_quotient_mk: homogeneous projection commutes with the quotient map.
• TauCeti.InternalGrading.isHomogeneous_mkQ: the quotient map has degree zero.

noncomputable def TauCeti.InternalGrading.submodule {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] (G : InternalGrading R M) (U : Submodule R M) (hU : DirectSum.SetLike.IsHomogeneous G.piece U) : InternalGrading R ↥U

The internal grading of a homogeneous submodule: its degree-p piece consists of the elements lying in the degree-p piece of the ambient grading.

Equations

• G.submodule U hU = { piece := fun (p : ℤ) => Submodule.comap U.subtype (G.piece p), isInternal := ⋯ }

@[simp]

theorem TauCeti.InternalGrading.submodule_piece {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] (G : InternalGrading R M) (U : Submodule R M) (hU : DirectSum.SetLike.IsHomogeneous G.piece U) (p : ℤ) : (G.submodule U hU).piece p = Submodule.comap U.subtype (G.piece p)

theorem TauCeti.InternalGrading.mem_submodule_piece {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] (G : InternalGrading R M) (U : Submodule R M) (hU : DirectSum.SetLike.IsHomogeneous G.piece U) {p : ℤ} {x : ↥U} : x ∈ (G.submodule U hU).piece p ↔ ↑x ∈ G.piece p

@[simp]

theorem TauCeti.InternalGrading.coe_decompose_submodule {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] (G : InternalGrading R M) (U : Submodule R M) (hU : DirectSum.SetLike.IsHomogeneous G.piece U) (p : ℤ) (x : ↥U) : ↑↑(((DirectSum.decompose (G.submodule U hU).piece) x) p) = ↑(((DirectSum.decompose G.piece) ↑x) p)

Homogeneous projection in a homogeneous submodule is homogeneous projection in the ambient module.

theorem TauCeti.InternalGrading.isHomogeneous_subtype {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] (G : InternalGrading R M) (U : Submodule R M) (hU : DirectSum.SetLike.IsHomogeneous G.piece U) : LinearMap.IsHomogeneous U.subtype (G.submodule U hU).piece G.piece 0

The inclusion of a homogeneous submodule has degree zero.

noncomputable def TauCeti.InternalGrading.ker {R : Type u_1} {M : Type u_2} {S : Type u_3} {N : Type u_4} [Semiring R] [Semiring S] [SMul R S] [AddCommMonoid M] [Module R M] [Module S M] [IsScalarTower R S M] [AddCommMonoid N] [Module R N] [Module S N] [IsScalarTower R S N] (G : InternalGrading R M) {H : InternalGrading R N} {f : M →ₗ[S] N} {r : ℤ} (hf : LinearMap.IsHomogeneous f G.piece H.piece r) : InternalGrading R ↥f.ker

The internal grading of the kernel of a homogeneous linear map: its degree-p piece consists of the elements of the kernel lying in the degree-p piece of M.

Equations

• G.ker hf = { piece := fun (p : ℤ) => Submodule.comap (↑R f.ker.subtype) (G.piece p), isInternal := ⋯ }

@[simp]

theorem TauCeti.InternalGrading.mem_ker_piece {R : Type u_1} {M : Type u_2} {S : Type u_3} {N : Type u_4} [Semiring R] [Semiring S] [SMul R S] [AddCommMonoid M] [Module R M] [Module S M] [IsScalarTower R S M] [AddCommMonoid N] [Module R N] [Module S N] [IsScalarTower R S N] (G : InternalGrading R M) {H : InternalGrading R N} {f : M →ₗ[S] N} {r : ℤ} (hf : LinearMap.IsHomogeneous f G.piece H.piece r) {p : ℤ} {z : ↥f.ker} : z ∈ (G.ker hf).piece p ↔ ↑z ∈ G.piece p

An element of the kernel of f is homogeneous of degree p exactly when it is homogeneous of degree p in M.

@[simp]

theorem TauCeti.InternalGrading.coe_decompose_ker {R : Type u_1} {M : Type u_2} {S : Type u_3} {N : Type u_4} [Semiring R] [Semiring S] [SMul R S] [AddCommMonoid M] [Module R M] [Module S M] [IsScalarTower R S M] [AddCommMonoid N] [Module R N] [Module S N] [IsScalarTower R S N] (G : InternalGrading R M) {H : InternalGrading R N} {f : M →ₗ[S] N} {r : ℤ} (hf : LinearMap.IsHomogeneous f G.piece H.piece r) (p : ℤ) (z : ↥f.ker) : ↑↑(((DirectSum.decompose (G.ker hf).piece) z) p) = ↑(((DirectSum.decompose G.piece) ↑z) p)

Homogeneous projection in the kernel of f is homogeneous projection in M.

noncomputable def TauCeti.InternalGrading.quotient {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (G : InternalGrading R M) (U : Submodule R M) (hU : DirectSum.SetLike.IsHomogeneous G.piece U) : InternalGrading R (M ⧸ U)

The internal grading of the quotient by a homogeneous submodule: its degree-p piece is the image of the degree-p piece of M.

Equations

• G.quotient U hU = { piece := fun (p : ℤ) => Submodule.map U.mkQ (G.piece p), isInternal := ⋯ }

@[simp]

theorem TauCeti.InternalGrading.quotient_piece {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (G : InternalGrading R M) (U : Submodule R M) (hU : DirectSum.SetLike.IsHomogeneous G.piece U) (p : ℤ) : (G.quotient U hU).piece p = Submodule.map U.mkQ (G.piece p)

theorem TauCeti.InternalGrading.mem_quotient_piece_iff {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (G : InternalGrading R M) (U : Submodule R M) (hU : DirectSum.SetLike.IsHomogeneous G.piece U) {p : ℤ} {y : M ⧸ U} : y ∈ (G.quotient U hU).piece p ↔ ∃ x ∈ G.piece p, Submodule.Quotient.mk x = y

An element of the quotient has degree p exactly when it is the class of an element of degree p.

theorem TauCeti.InternalGrading.mk_mem_quotient_piece {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (G : InternalGrading R M) (U : Submodule R M) (hU : DirectSum.SetLike.IsHomogeneous G.piece U) {p : ℤ} {x : M} (hx : x ∈ G.piece p) : Submodule.Quotient.mk x ∈ (G.quotient U hU).piece p

The class of an element of degree p has degree p.

theorem TauCeti.InternalGrading.isHomogeneous_mkQ {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (G : InternalGrading R M) (U : Submodule R M) (hU : DirectSum.SetLike.IsHomogeneous G.piece U) : LinearMap.IsHomogeneous U.mkQ G.piece (G.quotient U hU).piece 0

The quotient map by a homogeneous submodule has degree zero.

@[simp]

theorem TauCeti.InternalGrading.decompose_quotient_mk {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (G : InternalGrading R M) (U : Submodule R M) (hU : DirectSum.SetLike.IsHomogeneous G.piece U) (p : ℤ) (x : M) : ↑(((DirectSum.decompose (G.quotient U hU).piece) (Submodule.Quotient.mk x)) p) = Submodule.Quotient.mk ↑(((DirectSum.decompose G.piece) x) p)

Homogeneous projection commutes with the quotient map.