Multilinear operations on composable graded morphisms

For a string of objects X : Fin (n + 1) → C, inputs are ordered from left to right as Hom(Xₙ₋₁,Xₙ), …, Hom(X₀,X₁), and the output lies in Hom(X₀,Xₙ). Thus binary operations take (g,f) in the order used by m₂(g,f) = g ∘ f.

GradedLinearQuiver.PathOperation records an operation of degree q by its multilinear maps on each tuple of homogeneous pieces. GradedLinearQuiver.pathOperationEquiv identifies this with a homogeneous multilinear map on the total Hom modules: degreewise operations extend uniquely, and restricting the extension recovers every component. The representation accommodates the degree 2 - n operations of an A∞ category without assuming composition on the quiver.

Coordinate changes use linear equivalences of the input and output pieces, through Mathlib's LinearEquiv.multilinearMapCongrLeft and LinearEquiv.multilinearMapCongrRight. No equality cast of an operation is needed to change its homogeneous modules.

References

• B. Keller, Introduction to A-infinity algebras and modules, Section 7.1.

@[reducible, inline]

abbrev TauCeti.GradedLinearQuiver.PathMultilinear (R : Type w) [CommRing R] {C : Type u} [GradedLinearQuiver R C] {n : ℕ} (X : Fin (n + 1) → C) (d : Fin n → ℤ) (q : ℤ) : Type v

A degree-q operation on a composable string, on the input degrees d. The i-th input runs from X (n - 1 - i) to X (n - i), so binary inputs are (g,f). The degrees d follow this input order.

Equations

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

@[reducible, inline]

abbrev TauCeti.GradedLinearQuiver.PathOperation (R : Type w) [CommRing R] {C : Type u} [GradedLinearQuiver R C] {n : ℕ} (X : Fin (n + 1) → C) (q : ℤ) : Type v

A degree-q operation on a composable string, specified on every tuple of input degrees. All data are used: there is one component for each tuple and no choice of degree casts.

Equations

• TauCeti.GradedLinearQuiver.PathOperation R X q = ((d : Fin n → ℤ) → TauCeti.GradedLinearQuiver.PathMultilinear R X d q)

@[reducible, inline]

abbrev TauCeti.GradedLinearQuiver.HomogeneousPathOperation (R : Type w) [CommRing R] {C : Type u} [GradedLinearQuiver R C] {n : ℕ} (X : Fin (n + 1) → C) (q : ℤ) : Submodule R (MultilinearMap R (fun (i : Fin n) => ↑(homModule (X i.rev.castSucc) (X i.rev.succ))) ↑(homModule (X 0) (X (Fin.last n))))

Homogeneous multilinear operations on the total Hom modules of a composable string.

Equations

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

noncomputable def TauCeti.GradedLinearQuiver.pathOperationEquiv (R : Type w) [CommRing R] {C : Type u} [GradedLinearQuiver R C] {n : ℕ} (X : Fin (n + 1) → C) (q : ℤ) : ↥(HomogeneousPathOperation R X q) ≃ₗ[R] PathOperation R X q

Restriction to homogeneous pieces identifies total homogeneous operations with degreewise path operations. Its inverse is the unique multilinear extension to total Hom modules.

Equations

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

@[simp]

theorem TauCeti.GradedLinearQuiver.coe_pathOperationEquiv_apply (R : Type w) [CommRing R] {C : Type u} [GradedLinearQuiver R C] {n : ℕ} (X : Fin (n + 1) → C) (q : ℤ) (f : ↥(HomogeneousPathOperation R X q)) (d : Fin n → ℤ) (x : (i : Fin n) → grHom R (X i.rev.castSucc) (X i.rev.succ) (d i)) : ↑(((pathOperationEquiv R X q) f d) x) = ↑f fun (i : Fin n) => ↑(x i)

Restricting a total path operation evaluates it on the underlying homogeneous inputs.

@[simp]

theorem TauCeti.GradedLinearQuiver.pathOperationEquiv_symm_apply (R : Type w) [CommRing R] {C : Type u} [GradedLinearQuiver R C] {n : ℕ} (X : Fin (n + 1) → C) (q : ℤ) (f : PathOperation R X q) (d : Fin n → ℤ) (x : (i : Fin n) → grHom R (X i.rev.castSucc) (X i.rev.succ) (d i)) : (↑((pathOperationEquiv R X q).symm f) fun (i : Fin n) => ↑(x i)) = ↑((f d) x)

Extending degreewise path operations recovers their values on homogeneous inputs.