@[reducible, inline]

abbrev AInfinityAlgebraTheory.OneObj : Type

Equations

• AInfinityAlgebraTheory.OneObj = PUnit.{1}

structure AInfinityAlgebraTheory.AInfinityAlgStruct {β : Type v} [AInfinityTheory.Grading β] (R : Type u) [CommRing R] (A : AInfinityTheory.GradedRModule R) : Type (max u v)

• m {n : ℕ+} (deg : Fin ↑n → β) : MultilinearMap R (fun (i : Fin ↑n) => ↑(A (deg i))) ↑(A (AInfinityTheory.operationTargetDeg deg))

def AInfinityAlgebraTheory.AInfinityAlgStruct.toPreCategory {β : Type v} [AInfinityTheory.Grading β] {R : Type u} [CommRing R] {A : AInfinityTheory.GradedRModule R} (X : AInfinityAlgStruct R A) : AInfinityCategoryTheory.AInfinityPreCategory R OneObj

View an A∞-algebra as a one-object A∞-precategory.

Equations

• X.toPreCategory = { Hom := fun (x x_1 : AInfinityAlgebraTheory.OneObj) => A, m := fun {n : ℕ+} (obj : Fin (↑n + 1) → AInfinityAlgebraTheory.OneObj) (deg : Fin ↑n → β) => id (X.m deg) }

def AInfinityAlgebraTheory.AInfinityAlgStruct.stasheffSum {β : Type v} [AInfinityTheory.Grading β] {R : Type u} [CommRing R] {A : AInfinityTheory.GradedRModule R} (X : AInfinityAlgStruct R A) (n : ℕ+) (deg : Fin ↑n → β) (x : (i : Fin ↑n) → ↑(A (deg i))) : ↑(A (AInfinityTheory.stasheffTargetDeg deg))

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

Equations

• X.stasheffSum n deg x = X.toPreCategory.stasheffSum (fun (x : Fin (↑n + 1)) => PUnit.unit) deg x

def AInfinityAlgebraTheory.AInfinityAlgStruct.satisfiesStasheff {β : Type v} [AInfinityTheory.Grading β] {R : Type u} [CommRing R] {A : AInfinityTheory.GradedRModule R} (X : AInfinityAlgStruct R A) : Prop

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

Equations

• X.satisfiesStasheff = ∀ (n : ℕ+) (deg : Fin ↑n → β) (x : (i : Fin ↑n) → ↑(A (deg i))), X.stasheffSum n deg x = 0

class AInfinityAlgebraTheory.AInfinityAlgebra {β : Type v} [AInfinityTheory.Grading β] (R : Type u) [CommRing R] (A : AInfinityTheory.GradedRModule R) extends AInfinityAlgebraTheory.AInfinityAlgStruct R A : Type (max u v)

An A∞-algebra is raw data together with the Stasheff identities.

• m {n : ℕ+} (deg : Fin ↑n → β) : MultilinearMap R (fun (i : Fin ↑n) => ↑(A (deg i))) ↑(A (AInfinityTheory.operationTargetDeg deg))
• stasheff : self.satisfiesStasheff

theorem AInfinityAlgebraTheory.AInfinityAlgebra.stasheff_eq_zero {β : Type v} [AInfinityTheory.Grading β] {R : Type u} [CommRing R] {A : AInfinityTheory.GradedRModule R} (X : AInfinityAlgebra R A) (n : ℕ+) (deg : Fin ↑n → β) (x : (i : Fin ↑n) → ↑(A (deg i))) : X.stasheffSum n deg x = 0

Re-export the Stasheff identity in a convenient form.

def AInfinityAlgebraTheory.AInfinityAlgebra.toPreCategory {β : Type v} [AInfinityTheory.Grading β] {R : Type u} [CommRing R] {A : AInfinityTheory.GradedRModule R} (X : AInfinityAlgebra R A) : AInfinityCategoryTheory.AInfinityPreCategory R OneObj

View an A∞-algebra as a one-object A∞-precategory.

Equations

• X.toPreCategory = X.toPreCategory