Graded tensor duality

For internally graded modules, the tensor product of homogeneous functionals of degrees p and q is supported on total degree -(p+q). Mathlib's ordinary tensor-dual map therefore preserves degree. The graded comparison additionally uses the Koszul evaluation rule (φ ⊗ ψ)(x ⊗ y) = (-1)^(|ψ||x|) φ(x) ψ(y).

signedDualDistrib implements this rule over a commutative ring, with no finiteness assumption. For finite projective modules, signedDualDistribEquiv identifies the tensor product of the duals with the dual of the tensor product. The equivalence and its inverse preserve the internal total-degree gradings, so it also identifies each homogeneous piece. This comparison allows tensor powers and their graded duals to be interchanged in bar constructions.

The sign automorphism is InternalGrading.koszulTensorTwist; the underlying finite-projective comparison is Mathlib's TensorProduct.dualDistribEquiv. The graded evaluation convention follows E. Getzler and J. D. S. Jones, A-infinity algebras and the cyclic bar complex, Section 1.

theorem TauCeti.InternalGrading.dualDistrib_tmul_mem_dualPiece {R : Type u} {M : Type v} {N : Type w} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (G : InternalGrading R M) (H : InternalGrading R N) {p q : ℤ} {φ : Module.Dual R M} {ψ : Module.Dual R N} (hφ : φ ∈ G.dualPiece p) (hψ : ψ ∈ H.dualPiece q) : (TensorProduct.dualDistrib R M N) (φ ⊗ₜ[R] ψ) ∈ (G.tensorProduct H).dualPiece (p + q)

The ordinary tensor product of homogeneous functionals has the sum of their degrees. No finite-generation or projectivity hypothesis is needed for this support statement.

theorem TauCeti.InternalGrading.isHomogeneous_dualDistrib {R : Type u} {M : Type v} {N : Type w} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (G : InternalGrading R M) (H : InternalGrading R N) (hG : {p : ℤ | G.piece p ≠ ⊥}.Finite) (hH : {p : ℤ | H.piece p ≠ ⊥}.Finite) : LinearMap.IsHomogeneous (TensorProduct.dualDistrib R M N) ((G.dual hG).tensorProduct (H.dual hH)).piece (G.tensorProduct H).dualPiece 0

Mathlib's ordinary tensor-dual map preserves the internal total degree.

noncomputable def TauCeti.InternalGrading.signedDualDistrib {R : Type u} {M : Type v} {N : Type w} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (G : InternalGrading R M) (H : InternalGrading R N) : TensorProduct R (Module.Dual R M) (Module.Dual R N) →ₗ[R] Module.Dual R (TensorProduct R M N)

The graded tensor-dual map, with the Koszul sign in evaluation. It is the ordinary tensor-dual map precomposed on its argument with the sign automorphism.

Equations

• G.signedDualDistrib H = (↑(G.koszulTensorTwist H)).dualMap ∘ₗ TensorProduct.dualDistrib R M N

theorem TauCeti.InternalGrading.signedDualDistrib_apply {R : Type u} {M : Type v} {N : Type w} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (G : InternalGrading R M) (H : InternalGrading R N) (w : TensorProduct R (Module.Dual R M) (Module.Dual R N)) (z : TensorProduct R M N) : ((G.signedDualDistrib H) w) z = ((TensorProduct.dualDistrib R M N) w) ((G.koszulTensorTwist H) z)

Evaluation of the signed map uses the ordinary functional on the sign-twisted tensor.

theorem TauCeti.InternalGrading.signedDualDistrib_tmul_tmul {R : Type u} {M : Type v} {N : Type w} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (G : InternalGrading R M) (H : InternalGrading R N) (φ : Module.Dual R M) (ψ : Module.Dual R N) {p q : ℤ} {x : M} {y : N} (hx : x ∈ G.piece p) (hy : y ∈ H.piece q) : ((G.signedDualDistrib H) (φ ⊗ₜ[R] ψ)) (x ⊗ₜ[R] y) = (p * q).negOnePow • (φ x * ψ y)

On homogeneous arguments the signed comparison multiplies ordinary evaluation by the Koszul sign of their two degrees.

theorem TauCeti.InternalGrading.signedDualDistrib_tmul_tmul_of_mem_dualPiece {R : Type u} {M : Type v} {N : Type w} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (G : InternalGrading R M) (H : InternalGrading R N) (φ : Module.Dual R M) {ψ : Module.Dual R N} {p q s : ℤ} {x : M} {y : N} (hx : x ∈ G.piece p) (hy : y ∈ H.piece s) (hψ : ψ ∈ H.dualPiece q) : ((G.signedDualDistrib H) (φ ⊗ₜ[R] ψ)) (x ⊗ₜ[R] y) = (q * p).negOnePow • (φ x * ψ y)

The evaluation sign is (-1)^(|ψ||x|), as prescribed for a tensor product of graded maps. If the degree of y does not match that of ψ, both sides vanish.

theorem TauCeti.InternalGrading.isHomogeneous_signedDualDistrib {R : Type u} {M : Type v} {N : Type w} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (G : InternalGrading R M) (H : InternalGrading R N) (hG : {p : ℤ | G.piece p ≠ ⊥}.Finite) (hH : {p : ℤ | H.piece p ≠ ⊥}.Finite) : LinearMap.IsHomogeneous (G.signedDualDistrib H) ((G.dual hG).tensorProduct (H.dual hH)).piece (G.tensorProduct H).dualPiece 0

The signed tensor-dual map preserves degree; this does not require projectivity.

noncomputable def TauCeti.InternalGrading.signedDualDistribEquiv {R : Type u} {M : Type v} {N : Type w} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [Module.Finite R M] [Module.Finite R N] [Module.Projective R M] [Module.Projective R N] (G : InternalGrading R M) (H : InternalGrading R N) : TensorProduct R (Module.Dual R M) (Module.Dual R N) ≃ₗ[R] Module.Dual R (TensorProduct R M N)

The signed tensor-dual equivalence for finite projective graded modules.

Equations

• G.signedDualDistribEquiv H = (TensorProduct.dualDistribEquiv R M N).trans (G.koszulTensorTwist H).dualMap

@[simp]

theorem TauCeti.InternalGrading.signedDualDistribEquiv_toLinearMap {R : Type u} {M : Type v} {N : Type w} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [Module.Finite R M] [Module.Finite R N] [Module.Projective R M] [Module.Projective R N] (G : InternalGrading R M) (H : InternalGrading R N) : ↑(G.signedDualDistribEquiv H) = G.signedDualDistrib H

The finite-projective equivalence has the signed tensor-dual map as its forward map.

@[simp]

theorem TauCeti.InternalGrading.signedDualDistribEquiv_apply {R : Type u} {M : Type v} {N : Type w} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [Module.Finite R M] [Module.Finite R N] [Module.Projective R M] [Module.Projective R N] (G : InternalGrading R M) (H : InternalGrading R N) (w : TensorProduct R (Module.Dual R M) (Module.Dual R N)) : (G.signedDualDistribEquiv H) w = (G.signedDualDistrib H) w

Applying the finite-projective equivalence is applying the signed tensor-dual map.

theorem TauCeti.InternalGrading.isHomogeneous_signedDualDistribEquiv {R : Type u} {M : Type v} {N : Type w} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [Module.Finite R M] [Module.Finite R N] [Module.Projective R M] [Module.Projective R N] (G : InternalGrading R M) (H : InternalGrading R N) : LinearMap.IsHomogeneous (↑(G.signedDualDistribEquiv H)) ((G.dual ⋯).tensorProduct (H.dual ⋯)).piece ((G.tensorProduct H).dual ⋯).piece 0

The signed tensor-dual equivalence preserves the internal grading.

theorem TauCeti.InternalGrading.isHomogeneous_signedDualDistribEquiv_symm {R : Type u} {M : Type v} {N : Type w} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [Module.Finite R M] [Module.Finite R N] [Module.Projective R M] [Module.Projective R N] (G : InternalGrading R M) (H : InternalGrading R N) : LinearMap.IsHomogeneous (↑(G.signedDualDistribEquiv H).symm) ((G.tensorProduct H).dual ⋯).piece ((G.dual ⋯).tensorProduct (H.dual ⋯)).piece 0

The inverse tensor-dual comparison preserves degree as well.

theorem TauCeti.InternalGrading.signedDualDistribEquiv_mem_piece_iff {R : Type u} {M : Type v} {N : Type w} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [Module.Finite R M] [Module.Finite R N] [Module.Projective R M] [Module.Projective R N] (G : InternalGrading R M) (H : InternalGrading R N) (p : ℤ) (w : TensorProduct R (Module.Dual R M) (Module.Dual R N)) : (G.signedDualDistribEquiv H) w ∈ (G.tensorProduct H).dualPiece p ↔ w ∈ ((G.dual ⋯).tensorProduct (H.dual ⋯)).piece p

A functional on the tensor product has degree p exactly when its inverse image under the signed comparison has total degree p.