Homogeneous parts of polynomial-linear maps

For internally integer-graded coefficient modules on which X has the same degree δ, each degree component of a polynomial-linear map is again polynomial-linear. The component of degree r sends a homogeneous input of degree p to the degree-(p + r) projection of its image. Neither injectivity of X nor a sign condition on δ is required.

The construction uses Mathlib's DirectSum.decomposeLinearEquiv, DirectSum.component, and DirectSum.toModule to sum the selected projections over the finite input decomposition. Its degree-zero part can turn an ungraded retraction onto a homogeneous submodule into a homogeneous retraction.

Main definitions and results

• InternalGrading.homogeneousPart: the polynomial-linear component of degree r.
• InternalGrading.homogeneousPart_apply_of_mem: its value on homogeneous inputs.
• InternalGrading.homogeneousPart_zero and InternalGrading.homogeneousPart_add: components preserve zero and addition of maps.
• InternalGrading.homogeneousPart_eq_self: taking the component of a homogeneous map at its degree recovers the map.
• InternalGrading.isHomogeneous_homogeneousPart: the component has degree r.

noncomputable def TauCeti.InternalGrading.homogeneousPart {k : Type u_1} {M : Type u_2} {N : Type u_3} [CommSemiring k] [AddCommMonoid M] [AddCommMonoid N] [Module k M] [Module k N] [Module (Polynomial k) M] [Module (Polynomial k) N] [IsScalarTower k (Polynomial k) M] [IsScalarTower k (Polynomial k) N] (G : InternalGrading k M) (H : InternalGrading k N) {δ : ℤ} (hX : ∀ ⦃p : ℤ⦄ ⦃x : M⦄, x ∈ G.piece p → Polynomial.X • x ∈ G.piece (p + δ)) (hY : ∀ ⦃p : ℤ⦄ ⦃y : N⦄, y ∈ H.piece p → Polynomial.X • y ∈ H.piece (p + δ)) (f : M →ₗ[Polynomial k] N) (r : ℤ) : M →ₗ[Polynomial k] N

The degree-r part of a polynomial-linear map between internally graded modules on which X shifts degree by the same integer δ. It selects the degree-(p + r) component of the image of each degree-p input component and sums these finitely many values.

Equations

• G.homogeneousPart H hX hY f r = { toFun := ⇑(TauCeti.InternalGrading.componentMap✝ G H f r), map_add' := ⋯, map_smul' := ⋯ }

theorem TauCeti.InternalGrading.homogeneousPart_apply_of_mem {k : Type u_1} {M : Type u_2} {N : Type u_3} [CommSemiring k] [AddCommMonoid M] [AddCommMonoid N] [Module k M] [Module k N] [Module (Polynomial k) M] [Module (Polynomial k) N] [IsScalarTower k (Polynomial k) M] [IsScalarTower k (Polynomial k) N] (G : InternalGrading k M) (H : InternalGrading k N) {δ : ℤ} (hX : ∀ ⦃p : ℤ⦄ ⦃x : M⦄, x ∈ G.piece p → Polynomial.X • x ∈ G.piece (p + δ)) (hY : ∀ ⦃p : ℤ⦄ ⦃y : N⦄, y ∈ H.piece p → Polynomial.X • y ∈ H.piece (p + δ)) (f : M →ₗ[Polynomial k] N) (r : ℤ) {p : ℤ} {x : M} (hx : x ∈ G.piece p) : (G.homogeneousPart H hX hY f r) x = ↑(((DirectSum.decompose H.piece) (f x)) (p + r))

On a degree-p input, the degree-r part of a map is the degree-(p + r) projection of its image.

theorem TauCeti.InternalGrading.homogeneousPart_zero {k : Type u_1} {M : Type u_2} {N : Type u_3} [CommSemiring k] [AddCommMonoid M] [AddCommMonoid N] [Module k M] [Module k N] [Module (Polynomial k) M] [Module (Polynomial k) N] [IsScalarTower k (Polynomial k) M] [IsScalarTower k (Polynomial k) N] (G : InternalGrading k M) (H : InternalGrading k N) {δ : ℤ} (hX : ∀ ⦃p : ℤ⦄ ⦃x : M⦄, x ∈ G.piece p → Polynomial.X • x ∈ G.piece (p + δ)) (hY : ∀ ⦃p : ℤ⦄ ⦃y : N⦄, y ∈ H.piece p → Polynomial.X • y ∈ H.piece (p + δ)) (r : ℤ) : G.homogeneousPart H hX hY 0 r = 0

Every homogeneous part of the zero map is zero. This case is also simplified by homogeneousPart_eq_self.

@[simp]

theorem TauCeti.InternalGrading.homogeneousPart_add {k : Type u_1} {M : Type u_2} {N : Type u_3} [CommSemiring k] [AddCommMonoid M] [AddCommMonoid N] [Module k M] [Module k N] [Module (Polynomial k) M] [Module (Polynomial k) N] [IsScalarTower k (Polynomial k) M] [IsScalarTower k (Polynomial k) N] (G : InternalGrading k M) (H : InternalGrading k N) {δ : ℤ} (hX : ∀ ⦃p : ℤ⦄ ⦃x : M⦄, x ∈ G.piece p → Polynomial.X • x ∈ G.piece (p + δ)) (hY : ∀ ⦃p : ℤ⦄ ⦃y : N⦄, y ∈ H.piece p → Polynomial.X • y ∈ H.piece (p + δ)) (f g : M →ₗ[Polynomial k] N) (r : ℤ) : G.homogeneousPart H hX hY (f + g) r = G.homogeneousPart H hX hY f r + G.homogeneousPart H hX hY g r

Taking a homogeneous part preserves addition of polynomial-linear maps.

@[simp]

theorem TauCeti.InternalGrading.homogeneousPart_eq_self {k : Type u_1} {M : Type u_2} {N : Type u_3} [CommSemiring k] [AddCommMonoid M] [AddCommMonoid N] [Module k M] [Module k N] [Module (Polynomial k) M] [Module (Polynomial k) N] [IsScalarTower k (Polynomial k) M] [IsScalarTower k (Polynomial k) N] (G : InternalGrading k M) (H : InternalGrading k N) {δ : ℤ} (hX : ∀ ⦃p : ℤ⦄ ⦃x : M⦄, x ∈ G.piece p → Polynomial.X • x ∈ G.piece (p + δ)) (hY : ∀ ⦃p : ℤ⦄ ⦃y : N⦄, y ∈ H.piece p → Polynomial.X • y ∈ H.piece (p + δ)) (f : M →ₗ[Polynomial k] N) (r : ℤ) (hf : LinearMap.IsHomogeneous f G.piece H.piece r) : G.homogeneousPart H hX hY f r = f

Taking the degree-r part of a map already homogeneous of degree r recovers the map.

theorem TauCeti.InternalGrading.isHomogeneous_homogeneousPart {k : Type u_1} {M : Type u_2} {N : Type u_3} [CommSemiring k] [AddCommMonoid M] [AddCommMonoid N] [Module k M] [Module k N] [Module (Polynomial k) M] [Module (Polynomial k) N] [IsScalarTower k (Polynomial k) M] [IsScalarTower k (Polynomial k) N] (G : InternalGrading k M) (H : InternalGrading k N) {δ : ℤ} (hX : ∀ ⦃p : ℤ⦄ ⦃x : M⦄, x ∈ G.piece p → Polynomial.X • x ∈ G.piece (p + δ)) (hY : ∀ ⦃p : ℤ⦄ ⦃y : N⦄, y ∈ H.piece p → Polynomial.X • y ∈ H.piece (p + δ)) (f : M →ₗ[Polynomial k] N) (r : ℤ) : LinearMap.IsHomogeneous (G.homogeneousPart H hX hY f r) G.piece H.piece r

The degree-r component of a polynomial-linear map is homogeneous of degree r.