structure AInfinityCategoryTheory.AInfinityPreCategory {β : Type v} [AInfinityTheory.Grading β] (R : Type u) [CommRing R] (Obj : Type w) extends AInfinityTheory.RLinearGQuiver R Obj : Type (max (max (u + 1) v) w)

• Hom : Obj → Obj → GradedRModule R
• m {n : ℕ+} (obj : Fin (↑n + 1) → Obj) (deg : Fin ↑n → β) : MultilinearMap R (fun (i : Fin ↑n) => ↑(AInfinityTheory.composableHomType AInfinityTheory.RLinearGQuiver.Hom obj deg i)) ↑(AInfinityTheory.operationTargetType AInfinityTheory.RLinearGQuiver.Hom obj deg)

structure AInfinityCategoryTheory.AInfinityPreCategory.Chain {β : Type v} [AInfinityTheory.Grading β] {R : Type u} [CommRing R] {Obj : Type w} (X : AInfinityPreCategory R Obj) : Type (max v w)

• n : ℕ+
• obj : Fin (↑self.n + 1) → Obj
• deg : Fin ↑self.n → β

def AInfinityCategoryTheory.AInfinityPreCategory.Chain.source {β : Type v} [AInfinityTheory.Grading β] {R : Type u} [CommRing R] {Obj : Type w} {X : AInfinityPreCategory R Obj} (ch : X.Chain) : Obj

Equations

• ch.source = ch.obj 0

def AInfinityCategoryTheory.AInfinityPreCategory.Chain.target {β : Type v} [AInfinityTheory.Grading β] {R : Type u} [CommRing R] {Obj : Type w} {X : AInfinityPreCategory R Obj} (ch : X.Chain) : Obj

Equations

• ch.target = ch.obj (Fin.last ↑ch.n)

@[reducible, inline]

abbrev AInfinityCategoryTheory.AInfinityPreCategory.Chain.link {β : Type v} [AInfinityTheory.Grading β] {R : Type u} [CommRing R] {Obj : Type w} {X : AInfinityPreCategory R Obj} (ch : X.Chain) (i : Fin ↑ch.n) : ModuleCat R

Equations

• ch.link i = AInfinityTheory.composableHomType AInfinityTheory.RLinearGQuiver.Hom ch.obj ch.deg i

@[reducible, inline]

abbrev AInfinityCategoryTheory.AInfinityPreCategory.Chain.operationTarget {β : Type v} [AInfinityTheory.Grading β] {R : Type u} [CommRing R] {Obj : Type w} {X : AInfinityPreCategory R Obj} (ch : X.Chain) : ModuleCat R

Equations

• ch.operationTarget = AInfinityTheory.operationTargetType AInfinityTheory.RLinearGQuiver.Hom ch.obj ch.deg

def AInfinityCategoryTheory.AInfinityPreCategory.stasheffSum {β : Type v} [AInfinityTheory.Grading β] {R : Type u} [CommRing R] {Obj : Type w} (X : AInfinityPreCategory R Obj) {n : ℕ+} (obj : Fin (↑n + 1) → Obj) (deg : Fin ↑n → β) (x : (i : Fin ↑n) → ↑(AInfinityTheory.composableHomType AInfinityTheory.RLinearGQuiver.Hom obj deg i)) : ↑(AInfinityTheory.RLinearGQuiver.Hom (obj 0) (obj (Fin.last ↑n)) (AInfinityTheory.stasheffTargetDeg deg))

The full Stasheff sum in arity n, with Koszul signs.

Equations

• X.stasheffSum obj deg x = AInfinityTheory.indexedStasheffSum AInfinityTheory.RLinearGQuiver.Hom (fun {n : ℕ+} => X.m) obj deg x

def AInfinityCategoryTheory.AInfinityPreCategory.satisfiesStasheff {β : Type v} [AInfinityTheory.Grading β] {R : Type u} [CommRing R] {Obj : Type w} (X : AInfinityPreCategory R Obj) : Prop

The Stasheff identities as a property of the raw A∞ category data.

Equations

• X.satisfiesStasheff = AInfinityTheory.indexedSatisfiesStasheff AInfinityTheory.RLinearGQuiver.Hom fun {n : ℕ+} => X.m

structure AInfinityCategoryTheory.AInfinityCategory {β : Type v} [AInfinityTheory.Grading β] (R : Type u) [CommRing R] (Obj : Type w) extends AInfinityCategoryTheory.AInfinityPreCategory R Obj : Type (max (max (u + 1) v) w)

• Hom : Obj → Obj → GradedRModule R
• m {n : ℕ+} (obj : Fin (↑n + 1) → Obj) (deg : Fin ↑n → β) : MultilinearMap R (fun (i : Fin ↑n) => ↑(AInfinityTheory.composableHomType AInfinityTheory.RLinearGQuiver.Hom obj deg i)) ↑(AInfinityTheory.operationTargetType AInfinityTheory.RLinearGQuiver.Hom obj deg)
• stasheff : self.satisfiesStasheff

theorem AInfinityCategoryTheory.AInfinityCategory.stasheff_eq_zero {β : Type v} [AInfinityTheory.Grading β] {R : Type u} [CommRing R] {Obj : Type w} (X : AInfinityCategory R Obj) {n : ℕ+} (obj : Fin (↑n + 1) → Obj) (deg : Fin ↑n → β) (x : (i : Fin ↑n) → ↑(AInfinityTheory.composableHomType AInfinityTheory.RLinearGQuiver.Hom obj deg i)) : X.stasheffSum obj deg x = 0