Suspension of operations on composable paths

An arity-n operation of degree 2 - n on a graded linear quiver corresponds to a degree-one operation on its suspended Hom modules. GradedLinearQuiver.pathSuspensionEquiv implements this correspondence for each composable string, including both round trips. Inputs retain Keller's order (aₙ, …, a₁).

Both sides are families of multilinear maps on homogeneous pieces. The construction extends these families to total Hom modules, applies the dependent suspension equivalence, and restricts back to pieces. No casts of multilinear maps along equalities of degrees are part of the API. The evaluation formula measures the sign in the original degrees, so an input of suspended degree d contributes d + 1. The unary and binary formulas pin the differential and composition conventions used for higher categories.

References

• B. Keller, Introduction to A-infinity algebras and modules, Sections 3.6 and 7.1.
• E. Getzler and J. D. S. Jones, A-infinity algebras and the cyclic bar complex, Sections 1--2.

@[reducible, inline]

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

Degree-one path operations on suspended Hom modules. An input of suspended degree d i is an original morphism of degree d i + 1; the output has original degree ∑ i, d i + 2.

Equations

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

noncomputable def TauCeti.GradedLinearQuiver.pathSuspensionEquiv (R : Type w) [CommRing R] {C : Type u} [GradedLinearQuiver R C] {n : ℕ} (X : Fin (n + 1) → C) : PathOperation R X (2 - ↑n) ≃ₗ[R] SuspendedPathOperation R X

Suspension and unsuspension give mutually inverse linear correspondences between degree-2 - n path operations and degree-one operations on suspended Hom modules.

Equations

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

@[simp]

theorem TauCeti.GradedLinearQuiver.coe_pathSuspensionEquiv_apply (R : Type w) [CommRing R] {C : Type u} [GradedLinearQuiver R C] {n : ℕ} (X : Fin (n + 1) → C) (f : PathOperation R X (2 - ↑n)) (d : Fin n → ℤ) (x : (i : Fin n) → grHom R (X i.rev.castSucc) (X i.rev.succ) (d i + 1)) : ↑(((pathSuspensionEquiv R X) f d) x) = negOnePowCast R (∑ i : Fin n, (↑n - 1 - ↑↑i) * (d i + 1)) • ↑((f fun (i : Fin n) => d i + 1) x)

The path suspension square has the Koszul sign of moving each suspension past the inputs to its left. Degrees in the exponent are original, rather than suspended, degrees.

@[simp]

theorem TauCeti.GradedLinearQuiver.coe_pathSuspensionEquiv_symm_apply (R : Type w) [CommRing R] {C : Type u} [GradedLinearQuiver R C] {n : ℕ} (X : Fin (n + 1) → C) (b : SuspendedPathOperation R X) (d : Fin n → ℤ) (x : (i : Fin n) → grHom R (X i.rev.castSucc) (X i.rev.succ) (d i + 1)) : ↑(((pathSuspensionEquiv R X).symm b fun (i : Fin n) => d i + 1) x) = negOnePowCast R (∑ i : Fin n, (↑n - 1 - ↑↑i) * (d i + 1)) • ↑((b d) x)

Unsuspension uses the same sign as suspension when evaluated on the same original homogeneous morphisms.

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

Unary suspension introduces no sign: the suspended differential is the original operation viewed on regraded pieces.

theorem TauCeti.GradedLinearQuiver.coe_pathSuspensionEquiv_apply_two (R : Type w) [CommRing R] {C : Type u} [GradedLinearQuiver R C] (X : Fin 3 → C) (f : PathOperation R X 0) (d : Fin 2 → ℤ) (x : (i : Fin 2) → grHom R (X i.rev.castSucc) (X i.rev.succ) (d i + 1)) : ↑(((pathSuspensionEquiv R X) f d) x) = negOnePowCast R (d 0 + 1) • ↑((f fun (i : Fin 2) => d i + 1) x)

Binary suspension has sign (-1)^|g| on inputs (g,f), where |g| is the original degree of the first input. There is no change to the order of composable morphisms.