A∞-categories

An A∞-category is a graded R-linear quiver together with higher compositions mₙ : Hom(X₀, X₁) ⊗ ⋯ ⊗ Hom(Xₙ₋₁, Xₙ) → Hom(X₀, Xₙ) of degree 2 - n, one for each n ≥ 1, satisfying the Stasheff identities.

Main definitions

• AInfinityTheory.AInfinityCategoryStruct β R Obj: a graded R-linear quiver with higher compositions mₙ, not yet subject to any relations.
• AInfinityTheory.AInfinityCategory β R Obj: an A∞-category structure whose higher compositions satisfy the Stasheff identities.

Implementation notes

The ring of scalars R is an ordinary class parameter, so an object type may carry several rings of scalars. It is passed explicitly wherever it cannot be inferred from later arguments: to the hom spaces (X →ᵍ[R] Y) i, ComposableHomType, AInfinityComposition and homCongr.

class AInfinityTheory.AInfinityCategoryStruct (β : Type v) (R : Type u) [CommRing R] (Obj : Type w) [AddCommGroup β] [GradingType β] extends AInfinityTheory.GradedLinearQuiver β R Obj : Type (max (max (max u (u_1 + 1)) v) w)

The data of an A∞-category: a graded R-linear quiver together with, for each n ≥ 1, a higher composition mₙ of degree 2 - n. No relations are imposed.

• Hom : Obj → Obj → β → Type u_1
• homGroup (X Y : Obj) (i : β) : AddCommGroup (Hom R X Y i)
• homModule (X Y : Obj) (i : β) : Module R (Hom R X Y i)
• m : AInfinityComposition β R Obj

  The higher compositions mₙ.

class AInfinityTheory.AInfinityCategory (β : Type v) (R : Type u) [CommRing R] (Obj : Type w) [AddCommGroup β] [GradingType β] extends AInfinityTheory.AInfinityCategoryStruct β R Obj : Type (max (max (max u (u_1 + 1)) v) w)

An A∞-category: an A∞-category structure whose higher compositions satisfy the Stasheff identities in every arity.

• Hom : Obj → Obj → β → Type u_1
• homGroup (X Y : Obj) (i : β) : AddCommGroup (Hom R X Y i)
• homModule (X Y : Obj) (i : β) : Module R (Hom R X Y i)
• m : AInfinityComposition β R Obj
• stasheff : IndexedSatisfiesStasheff fun {n : ℕ} [NeZero n] => AInfinityCategoryStruct.m

  The higher compositions satisfy the Stasheff identities.

theorem AInfinityTheory.AInfinityCategory.indexedStasheffSum_eq_zero {β : Type v} [AddCommGroup β] [GradingType β] {R : Type u} [CommRing R] {Obj : Type w} [AInfinityCategory β R Obj] {n : ℕ} [NeZero n] {obj : Fin (n + 1) → Obj} {deg : Fin n → β} (x : (i : Fin n) → GradedLinearQuiver.ComposableHomType R obj i (deg i)) {d : β} (hd : stasheffTargetDeg deg = d) : indexedStasheffSum (fun {n : ℕ} [NeZero n] => AInfinityCategoryStruct.m) x d hd = 0

In an A∞-category, the Stasheff sum of any composable string of morphisms vanishes.