The degree-zero part of a module homomorphism

An arbitrary homomorphism between internally graded modules need not be homogeneous, nor a finite sum of homogeneous homomorphisms. Its degree-zero part nevertheless exists: on a homogeneous input of degree p, retain just the degree-p component of the output.

This operation preserves linearity over the graded algebra, not just over the coefficient ring. Composition with a degree-zero map on either side commutes with taking the degree-zero part. Consequently an ungraded lift of a graded map can be replaced by a graded lift. This is the bridge from projective underlying modules to projective objects in the graded category.

References

• C. Năstăsescu and F. Van Oystaeyen, Methods of Graded Rings, Section 2.3, for graded projective modules and the homogeneous-component argument.

noncomputable def TauCeti.InternalGrading.degreeZeroPart {k : Type uk} [CommSemiring k] {A : Type uA} [Semiring A] [Algebra k A] {M : Type uM} [AddCommMonoid M] [Module A M] [Module k M] [IsScalarTower k A M] {N : Type uN} [AddCommMonoid N] [Module A N] [Module k N] [IsScalarTower k A N] (G : InternalGrading k M) (H : InternalGrading k N) (𝒜 : ℤ → Submodule k A) [SetLike.GradedSMul 𝒜 G.piece] [SetLike.GradedSMul 𝒜 H.piece] [DirectSum.Decomposition 𝒜] (f : M →ₗ[A] N) : M →ₗ[A] N

The degree-zero part of an A-linear map between graded A-modules. On a homogeneous input of degree p, it retains the degree-p component of the output. No finite-generation hypothesis is needed.

Equations

• G.degreeZeroPart H 𝒜 f = { toFun := ⇑(TauCeti.InternalGrading.degreeZeroPartBase✝ G H f), map_add' := ⋯, map_smul' := ⋯ }

theorem TauCeti.InternalGrading.degreeZeroPart_apply_of_mem {k : Type uk} [CommSemiring k] {A : Type uA} [Semiring A] [Algebra k A] {M : Type uM} [AddCommMonoid M] [Module A M] [Module k M] [IsScalarTower k A M] {N : Type uN} [AddCommMonoid N] [Module A N] [Module k N] [IsScalarTower k A N] (G : InternalGrading k M) (H : InternalGrading k N) (𝒜 : ℤ → Submodule k A) [SetLike.GradedSMul 𝒜 G.piece] [SetLike.GradedSMul 𝒜 H.piece] [DirectSum.Decomposition 𝒜] (f : M →ₗ[A] N) {p : ℤ} {x : M} (hx : x ∈ G.piece p) : (G.degreeZeroPart H 𝒜 f) x = ↑(((DirectSum.decompose H.piece) (f x)) p)

On a homogeneous input, the degree-zero part is the corresponding output component.

theorem TauCeti.InternalGrading.isHomogeneous_degreeZeroPart {k : Type uk} [CommSemiring k] {A : Type uA} [Semiring A] [Algebra k A] {M : Type uM} [AddCommMonoid M] [Module A M] [Module k M] [IsScalarTower k A M] {N : Type uN} [AddCommMonoid N] [Module A N] [Module k N] [IsScalarTower k A N] (G : InternalGrading k M) (H : InternalGrading k N) (𝒜 : ℤ → Submodule k A) [SetLike.GradedSMul 𝒜 G.piece] [SetLike.GradedSMul 𝒜 H.piece] [DirectSum.Decomposition 𝒜] (f : M →ₗ[A] N) : LinearMap.IsHomogeneous (G.degreeZeroPart H 𝒜 f) G.piece H.piece 0

The degree-zero part is a homogeneous module map of degree zero.

@[simp]

theorem TauCeti.InternalGrading.degreeZeroPart_eq_self_iff {k : Type uk} [CommSemiring k] {A : Type uA} [Semiring A] [Algebra k A] {M : Type uM} [AddCommMonoid M] [Module A M] [Module k M] [IsScalarTower k A M] {N : Type uN} [AddCommMonoid N] [Module A N] [Module k N] [IsScalarTower k A N] (G : InternalGrading k M) (H : InternalGrading k N) (𝒜 : ℤ → Submodule k A) [SetLike.GradedSMul 𝒜 G.piece] [SetLike.GradedSMul 𝒜 H.piece] [DirectSum.Decomposition 𝒜] (f : M →ₗ[A] N) : G.degreeZeroPart H 𝒜 f = f ↔ LinearMap.IsHomogeneous f G.piece H.piece 0

Taking the degree-zero part fixes precisely the maps homogeneous of degree zero.

theorem TauCeti.InternalGrading.comp_degreeZeroPart {k : Type uk} [CommSemiring k] {A : Type uA} [Semiring A] [Algebra k A] {M : Type uM} [AddCommMonoid M] [Module A M] [Module k M] [IsScalarTower k A M] {N : Type uN} [AddCommMonoid N] [Module A N] [Module k N] [IsScalarTower k A N] (G : InternalGrading k M) (H : InternalGrading k N) (𝒜 : ℤ → Submodule k A) [SetLike.GradedSMul 𝒜 G.piece] [SetLike.GradedSMul 𝒜 H.piece] [DirectSum.Decomposition 𝒜] {P : Type uP} [AddCommMonoid P] [Module A P] [Module k P] [IsScalarTower k A P] (I : InternalGrading k P) [SetLike.GradedSMul 𝒜 I.piece] (f : M →ₗ[A] N) {g : N →ₗ[A] P} (hg : LinearMap.IsHomogeneous g H.piece I.piece 0) : g ∘ₗ G.degreeZeroPart H 𝒜 f = G.degreeZeroPart I 𝒜 (g ∘ₗ f)

Postcomposition by a homogeneous map of degree zero commutes with taking the degree-zero part. This allows an ungraded factorization of a graded map to be made graded.

theorem TauCeti.InternalGrading.degreeZeroPart_comp {k : Type uk} [CommSemiring k] {A : Type uA} [Semiring A] [Algebra k A] {M : Type uM} [AddCommMonoid M] [Module A M] [Module k M] [IsScalarTower k A M] {N : Type uN} [AddCommMonoid N] [Module A N] [Module k N] [IsScalarTower k A N] (G : InternalGrading k M) (H : InternalGrading k N) (𝒜 : ℤ → Submodule k A) [SetLike.GradedSMul 𝒜 G.piece] [SetLike.GradedSMul 𝒜 H.piece] [DirectSum.Decomposition 𝒜] {P : Type uP} [AddCommMonoid P] [Module A P] [Module k P] [IsScalarTower k A P] (I : InternalGrading k P) [SetLike.GradedSMul 𝒜 I.piece] (f : N →ₗ[A] P) {g : M →ₗ[A] N} (hg : LinearMap.IsHomogeneous g G.piece H.piece 0) : G.degreeZeroPart I 𝒜 (f ∘ₗ g) = H.degreeZeroPart I 𝒜 f ∘ₗ g

Precomposition by a homogeneous map of degree zero commutes with taking the degree-zero part.