The one-object A-infinity category of an A-infinity algebra

An A∞ algebra 𝒜 on a graded module A is an A∞ category with a single object, whose endomorphisms are A. The graded linear quiver TauCeti.AInfinitySingleObj 𝒜 has one object TauCeti.AInfinitySingleObj.star 𝒜 with endomorphism module A, graded as 𝒜 is, and TauCeti.AInfinitySingleObj.aInfinityCategory 𝒜 is its A∞ structure: the operations of 𝒜, transported to the total module of morphisms along the inclusion of the single hom module, which is a linear equivalence.

The operation of the category on a string of endomorphisms is the operation of the algebra, TauCeti.AInfinitySingleObj.coe_pathOperation_aInfinityCategory_apply; in particular its differential and composition are m₁ and m₂ of 𝒜.

Main definitions

• TauCeti.AInfinitySingleObj: the one-object graded linear quiver of an A∞ algebra.
• TauCeti.AInfinitySingleObj.aInfinityCategory: its A∞ category structure.

Main results

• TauCeti.AInfinitySingleObj.coe_pathOperation_aInfinityCategory_apply: the operations of the one-object A∞ category are the operations of the algebra.
• TauCeti.AInfinitySingleObj.homDifferential_aInfinityCategory and TauCeti.AInfinitySingleObj.comp_aInfinityCategory: its differential and composition are m₁ and m₂.

References

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

structure TauCeti.AInfinitySingleObj {R : Type uR} {A : Type uA} [CommRing R] [AddCommGroup A] [Module R A] (𝒜 : AInfinityAlgebra R A) : Type

The objects of the one-object A∞ category of an A∞ algebra 𝒜: a single object TauCeti.AInfinitySingleObj.star 𝒜, whose endomorphisms are the underlying module of 𝒜.

The type is a structure indexed by 𝒜, so that the quivers of different A∞ algebras are not interchangeable.

def TauCeti.AInfinitySingleObj.star {R : Type uR} {A : Type uA} [CommRing R] [AddCommGroup A] [Module R A] (𝒜 : AInfinityAlgebra R A) : AInfinitySingleObj 𝒜

The unique object of the one-object A∞ category.

Equations

• TauCeti.AInfinitySingleObj.star 𝒜 = { }

@[instance_reducible]

instance TauCeti.AInfinitySingleObj.instUnique {R : Type uR} {A : Type uA} [CommRing R] [AddCommGroup A] [Module R A] (𝒜 : AInfinityAlgebra R A) : Unique (AInfinitySingleObj 𝒜)

Equations

• TauCeti.AInfinitySingleObj.instUnique 𝒜 = { default := TauCeti.AInfinitySingleObj.star 𝒜, uniq := ⋯ }

@[instance_reducible]

instance TauCeti.AInfinitySingleObj.instGradedLinearQuiver {R : Type uR} {A : Type uA} [CommRing R] [AddCommGroup A] [Module R A] (𝒜 : AInfinityAlgebra R A) : GradedLinearQuiver R (AInfinitySingleObj 𝒜)

The one-object graded linear quiver of an A∞ algebra: the endomorphisms of the single object are the underlying graded module of the algebra.

Equations

• TauCeti.AInfinitySingleObj.instGradedLinearQuiver 𝒜 = { homModule := fun (x x_1 : TauCeti.AInfinitySingleObj 𝒜) => ↧A, grading := fun (x x_1 : TauCeti.AInfinitySingleObj 𝒜) => 𝒜.grading }

noncomputable def TauCeti.AInfinitySingleObj.totalHomEquiv {R : Type uR} {A : Type uA} [CommRing R] [AddCommGroup A] [Module R A] (𝒜 : AInfinityAlgebra R A) : A ≃ₗ[R] GradedLinearQuiver.TotalHom R (AInfinitySingleObj 𝒜)

The inclusion of the endomorphisms of the single object into the total module of morphisms is a linear equivalence, with inverse the projection.

Equations

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

@[simp]

theorem TauCeti.AInfinitySingleObj.totalHomEquiv_apply {R : Type uR} {A : Type uA} [CommRing R] [AddCommGroup A] [Module R A] (𝒜 : AInfinityAlgebra R A) (a : A) : (totalHomEquiv 𝒜) a = (GradedLinearQuiver.homInclusion (star 𝒜) (star 𝒜)) a

The equivalence totalHomEquiv is the inclusion of the endomorphisms of the single object.

@[simp]

theorem TauCeti.AInfinitySingleObj.totalHomEquiv_symm_apply {R : Type uR} {A : Type uA} [CommRing R] [AddCommGroup A] [Module R A] (𝒜 : AInfinityAlgebra R A) (x : GradedLinearQuiver.TotalHom R (AInfinitySingleObj 𝒜)) : (totalHomEquiv 𝒜).symm x = (GradedLinearQuiver.homProjection (star 𝒜) (star 𝒜)) x

The inverse of totalHomEquiv is the projection onto the endomorphisms of the single object.

noncomputable def TauCeti.AInfinitySingleObj.aInfinityCategory {R : Type uR} {A : Type uA} [CommRing R] [AddCommGroup A] [Module R A] (𝒜 : AInfinityAlgebra R A) : AInfinityCategory R (AInfinitySingleObj 𝒜)

The one-object A∞ category of an A∞ algebra: the operations of the algebra, transported to the total module of morphisms of its one-object graded linear quiver.

Equations

• TauCeti.AInfinitySingleObj.aInfinityCategory 𝒜 = { toAInfinityAlgebra := 𝒜.map (TauCeti.AInfinitySingleObj.totalHomEquiv 𝒜), grading_eq := ⋯, isPathCompatible_m_of_pos := ⋯ }

theorem TauCeti.AInfinitySingleObj.toAInfinityAlgebra_aInfinityCategory {R : Type uR} {A : Type uA} [CommRing R] [AddCommGroup A] [Module R A] (𝒜 : AInfinityAlgebra R A) : (aInfinityCategory 𝒜).toAInfinityAlgebra = 𝒜.map (totalHomEquiv 𝒜)

The total A∞ algebra of the one-object A∞ category is the algebra, transported to the total module of morphisms.

@[simp]

theorem TauCeti.AInfinitySingleObj.coe_pathOperation_aInfinityCategory_apply {R : Type uR} {A : Type uA} [CommRing R] [AddCommGroup A] [Module R A] (𝒜 : AInfinityAlgebra R A) {n : ℕ} (X : Fin (n + 1) → AInfinitySingleObj 𝒜) (d : Fin n → ℤ) (x : (i : Fin n) → GradedLinearQuiver.grHom R (X i.rev.castSucc) (X i.rev.succ) (d i)) : ↑(((aInfinityCategory 𝒜).pathOperation X d) x) = (𝒜.m n) fun (i : Fin n) => ↑(x i)

The operations of the one-object A∞ category are the operations of the algebra.

@[simp]

theorem TauCeti.AInfinitySingleObj.homDifferential_aInfinityCategory {R : Type uR} {A : Type uA} [CommRing R] [AddCommGroup A] [Module R A] (𝒜 : AInfinityAlgebra R A) (X Y : AInfinitySingleObj 𝒜) (a : A) : ((aInfinityCategory 𝒜).homDifferential X Y) a = (𝒜.m 1) ![a]

The differential of the one-object A∞ category is the unary operation of the algebra.

@[simp]

theorem TauCeti.AInfinitySingleObj.comp_aInfinityCategory {R : Type uR} {A : Type uA} [CommRing R] [AddCommGroup A] [Module R A] (𝒜 : AInfinityAlgebra R A) (X Y Z : AInfinitySingleObj 𝒜) (a b : A) : (((aInfinityCategory 𝒜).comp X Y Z) a) b = (𝒜.m 2) ![a, b]

The composition of the one-object A∞ category is the binary operation of the algebra.