Duals of internally graded modules

This file gives the linear dual of an internally graded module its canonical grading. A functional has degree p when it is supported on the original degree -p piece, and restriction identifies that degree with the linear dual of G.piece (-p). Consequently, evaluation can be nonzero only on degrees summing to zero.

The homogeneous pieces exhaust the dual as soon as the grading has only finitely many nonzero pieces, and no projectivity is needed for that. Finite generation of the module is one source of the hypothesis, through InternalGrading.finite_piece_ne_bot, and the dual grading inherits it through InternalGrading.finite_dualPiece_ne_bot. Later tensor-duality comparisons may add the finite-projectivity hypotheses needed to identify duals of tensor products.

The construction follows the graded-dual convention used for DG and A∞ objects in B. Keller, Introduction to A-infinity algebras and modules, Sections 3 and 7.

Main definitions

• InternalGrading.dualPiece: the degree-p submodule of the linear dual.
• InternalGrading.dualPieceEquiv: the identification of that submodule with the linear dual of the original degree--p piece, by restriction.
• InternalGrading.dual: the internal grading of the linear dual of a module whose grading has finitely many nonzero pieces.

Main results

• InternalGrading.mem_dualPiece_iff: a degree-p functional vanishes on every original degree other than -p.
• InternalGrading.dualPiece_apply_eq_zero_of_mem_piece_of_add_ne_zero: evaluation vanishes unless the degrees of the functional and vector sum to zero.
• InternalGrading.dualPiece_apply_eq_apply_decompose: a degree-p functional sees only the degree--p homogeneous component of its argument.
• InternalGrading.finite_dualPiece_ne_bot: the dual grading has finitely many nonzero pieces as soon as the original one does.
• InternalGrading.iSupIndep_dualPiece: the dual pieces are independent, without a finiteness hypothesis.
• InternalGrading.dual_decompose_apply: the degree-p component of a functional evaluates an arbitrary vector through its original degree--p component.
• InternalGrading.dual_decompose_apply_of_mem_piece: on the degree-q piece, a functional agrees with its own degree--q homogeneous component.

Implementation notes

The construction lives over a commutative semiring. Although independence and spanning do not in general assemble an internal direct sum without additive inverses, injectivity of the canonical map for these dual pieces follows directly by evaluating each summand on its matching primal piece.

This supplies the dual grading for Layer 0 of the DGAInfinity roadmap; the finite-projective identifications of duals of tensor products remain.

def TauCeti.InternalGrading.dualPiece {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] (G : InternalGrading R M) (p : ℤ) : Submodule R (Module.Dual R M)

The degree-p part of the graded dual consists of the functionals vanishing on every homogeneous piece except degree -p.

Equations

• G.dualPiece p = ⨅ (q : ℤ), ⨅ (_ : q ≠ -p), (G.piece q).dualAnnihilator

@[simp]

theorem TauCeti.InternalGrading.mem_dualPiece_iff {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] (G : InternalGrading R M) (p : ℤ) (φ : Module.Dual R M) : φ ∈ G.dualPiece p ↔ ∀ (q : ℤ), ∀ x ∈ G.piece q, q ≠ -p → φ x = 0

A functional belongs to degree p of the graded dual exactly when it vanishes on every original degree other than -p.

theorem TauCeti.InternalGrading.dualPiece_apply_eq_zero_of_mem_piece_of_add_ne_zero {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] (G : InternalGrading R M) {p q : ℤ} {φ : Module.Dual R M} {x : M} (hφ : φ ∈ G.dualPiece p) (hx : x ∈ G.piece q) (hpq : p + q ≠ 0) : φ x = 0

A functional in dual degree p vanishes on an original homogeneous vector of degree q unless p + q = 0.

theorem TauCeti.InternalGrading.dualPiece_apply_eq_apply_decompose {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] (G : InternalGrading R M) {p : ℤ} {φ : Module.Dual R M} (hφ : φ ∈ G.dualPiece p) (x : M) : φ x = φ ↑(((DirectSum.decompose G.piece) x) (-p))

A functional of dual degree p sees only the degree--p homogeneous component of its argument: it annihilates every other component of the decomposition.

noncomputable def TauCeti.InternalGrading.dualPieceEquiv {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] (G : InternalGrading R M) (p : ℤ) : ↥(G.dualPiece p) ≃ₗ[R] Module.Dual R ↥(G.piece (-p))

Restricting a functional of dual degree p to the degree--p piece identifies G.dualPiece p with the linear dual of that piece: the restriction determines the functional, and every functional on the piece extends along the homogeneous component of degree -p.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.InternalGrading.dualPieceEquiv_apply {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] (G : InternalGrading R M) (p : ℤ) (φ : ↥(G.dualPiece p)) (y : ↥(G.piece (-p))) : ((G.dualPieceEquiv p) φ) y = ↑φ ↑y

A functional of dual degree p restricts to the degree--p piece by evaluation.

theorem TauCeti.InternalGrading.dualPieceEquiv_symm_apply {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] (G : InternalGrading R M) (p : ℤ) (ψ : Module.Dual R ↥(G.piece (-p))) (x : M) : ↑((G.dualPieceEquiv p).symm ψ) x = ψ (((DirectSum.decompose G.piece) x) (-p))

The functional of dual degree p extending ψ evaluates an arbitrary vector on its degree--p homogeneous component.

@[simp]

theorem TauCeti.InternalGrading.dualPieceEquiv_symm_apply_coe {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] (G : InternalGrading R M) (p : ℤ) (ψ : Module.Dual R ↥(G.piece (-p))) (y : ↥(G.piece (-p))) : ↑((G.dualPieceEquiv p).symm ψ) ↑y = ψ y

The functional of dual degree p extending ψ restricts to ψ on the degree--p piece.

theorem TauCeti.InternalGrading.dualPiece_eq_bot_of_piece_eq_bot {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] (G : InternalGrading R M) {p : ℤ} (h : G.piece (-p) = ⊥) : G.dualPiece p = ⊥

Dual degree p is zero as soon as the original degree -p is: a functional of dual degree p sees only that piece of its argument.

theorem TauCeti.InternalGrading.finite_dualPiece_ne_bot {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] (G : InternalGrading R M) (hG : {p : ℤ | G.piece p ≠ ⊥}.Finite) : {p : ℤ | G.dualPiece p ≠ ⊥}.Finite

The dual grading has only finitely many nonzero pieces as soon as the original one does, the degree-p piece of the dual being carried by the original degree -p.

theorem TauCeti.InternalGrading.iSupIndep_dualPiece {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] (G : InternalGrading R M) : iSupIndep G.dualPiece

The pieces of the graded dual are independent, even when the original grading has infinitely many nonzero pieces.

noncomputable def TauCeti.InternalGrading.dual {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] (G : InternalGrading R M) (hG : {p : ℤ | G.piece p ≠ ⊥}.Finite) : InternalGrading R (Module.Dual R M)

The internal grading on the linear dual of a module whose grading has only finitely many nonzero pieces.

The degree is reversed: a functional of degree p is supported on the original degree -p piece.

Equations

• G.dual hG = { piece := G.dualPiece, isInternal := ⋯ }

@[simp]

theorem TauCeti.InternalGrading.dual_piece {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] (G : InternalGrading R M) (hG : {p : ℤ | G.piece p ≠ ⊥}.Finite) (p : ℤ) : (G.dual hG).piece p = G.dualPiece p

The degree-p piece of the dual grading is dualPiece G p.

theorem TauCeti.InternalGrading.dual_decompose_apply_of_mem_piece {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] (G : InternalGrading R M) (hG : {p : ℤ | G.piece p ≠ ⊥}.Finite) (φ : Module.Dual R M) {q : ℤ} {x : M} (hx : x ∈ G.piece q) : ↑(((DirectSum.decompose (G.dual hG).piece) φ) (-q)) x = φ x

On the degree-q piece a functional agrees with its own degree--q homogeneous component for the dual grading: all the other components vanish there.

@[simp]

theorem TauCeti.InternalGrading.dual_decompose_apply {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] (G : InternalGrading R M) (hG : {p : ℤ | G.piece p ≠ ⊥}.Finite) (φ : Module.Dual R M) (p : ℤ) (x : M) : ↑(((DirectSum.decompose (G.dual hG).piece) φ) p) x = φ ↑(((DirectSum.decompose G.piece) x) (-p))

The degree-p component of a functional evaluates an arbitrary vector by first taking its original degree--p homogeneous component.