A∞-functors

An A∞-functor F : A → B between A∞-categories consists of a map on objects together with, for each n ≥ 1, a multilinear map φₙ : Hom(X₀, X₁) ⊗ ⋯ ⊗ Hom(Xₙ₋₁, Xₙ) → Hom(F X₀, F Xₙ) of degree 1 - n, satisfying the A∞-functor equations ∑_{r + s + t = n, s ≥ 1} (-1)^(‖a_{r+s+1}‖ + ⋯ + ‖a_n‖) φ_{r+1+t}(a_1, …, a_r, m_s(a_{r+1}, …, a_{r+s}), a_{r+s+1}, …, a_n) = ∑_{k ≥ 1} ∑_{i₁ + ⋯ + iₖ = n} m'_k(φ_{i₁}(a_1, …, a_{i₁}), …, φ_{iₖ}(a_{n-iₖ+1}, …, a_n)).

The sign on the left is the Koszul sign stasheffSign of the Stasheff identities. There is no sign on the right: in reduced degrees ‖a‖ = |a| - 1 every φᵢ has degree 0, so no Koszul sign arises from moving it past the inputs (compare [Seidel, Fukaya categories and Picard–Lefschetz theory, (1.6)]).

The source and target may be graded by different grading types β and β'; the functor then carries a homomorphism of grading types β →+ᵍ β', which preserves the integer shifts and the Koszul signs.

Main definitions

• AInfinityTheory.AInfinityFunctorData β β' R Obj Obj': a map on objects, a grading homomorphism and functor components φₙ, not yet subject to any relations.
• AInfinityTheory.AInfinityFunctorData.mapCompSum: the left-hand side of the arity-n functor equation.
• AInfinityTheory.AInfinityFunctorData.compMapSum: the right-hand side of the arity-n functor equation.
• AInfinityTheory.AInfinityFunctorData.SatisfiesFunctorEquations: the functor equations in every arity.
• AInfinityTheory.AInfinityFunctor β β' R Obj Obj': an A∞-functor between A∞-categories.

Implementation notes

The component φₙ is a GradedMultilinearMap of degree shift (1 - n) in the source grading, into the pullback b ↦ Hom(F X₀, F Xₙ)(degMap b) of the target hom spaces. Both sides of the functor equation are stated pointwise on a composable string of inputs, in degree degMap d for any d equal to the degree of mₙ, as for indexedStasheffSum. Like the Stasheff sum, the left-hand side is a signedStasheffSum. Changes of objects are transported with homCongr. The ordered decompositions i₁ + ⋯ + iₖ = n on the right-hand side are Mathlib's Composition n.

theorem Composition.prod_prod_embedding {n : ℕ} {M : Type u_1} [CommMonoid M] (c : Composition n) (f : Fin n → M) : ∏ l : Fin c.length, ∏ j : Fin (c.blocksFun l), f ((c.embedding l) j) = ∏ i : Fin n, f i

Taking the product over each block of a composition c of n, and then over the blocks, is the same as taking the product over Fin n.

theorem Composition.sum_sum_embedding {n : ℕ} {M : Type u_1} [AddCommMonoid M] (c : Composition n) (f : Fin n → M) : ∑ l : Fin c.length, ∑ j : Fin (c.blocksFun l), f ((c.embedding l) j) = ∑ i : Fin n, f i

Summing over each block of a composition c of n, and then over the blocks, is the same as summing over Fin n.

@[reducible, inline]

abbrev AInfinityTheory.functorTargetDeg {n : ℕ} {β : Type u_1} [AddCommGroup β] [GradingType β] (deg : Fin n → β) : β

Target degree of the n-ary functor component φₙ, which has degree 1 - n.

Equations

• AInfinityTheory.functorTargetDeg deg = ∑ i : Fin n, deg i + AInfinityTheory.shift (1 - ↑n)

theorem AInfinityTheory.operationTargetDeg_eq_functorTargetDeg_add_shift_one {n : ℕ} {β : Type u_1} [AddCommGroup β] [GradingType β] (deg : Fin n → β) : operationTargetDeg deg = functorTargetDeg deg + shift 1

The n-ary operation mₙ has degree one more than the n-ary functor component φₙ.

theorem AInfinityTheory.functorTargetDeg_stasheffDegOut {n : ℕ} {β : Type u_1} [AddCommGroup β] [GradingType β] (deg : Fin n → β) (p : StasheffIndex n) : functorTargetDeg (stasheffDegOut deg p) = operationTargetDeg deg

In the term of the left-hand side of the functor equation indexed by p = (r, s, t), the outer functor component lands in the degree of mₙ.

theorem AInfinityTheory.operationTargetDeg_functorTargetDeg_embedding {n : ℕ} {β : Type u_1} [AddCommGroup β] [GradingType β] (deg : Fin n → β) (c : Composition n) : (operationTargetDeg fun (l : Fin c.length) => functorTargetDeg fun (j : Fin (c.blocksFun l)) => deg ((c.embedding l) j)) = operationTargetDeg deg

Applying functor components to the blocks of a composition c of n and then the c.length-ary operation lands in the degree of mₙ.

theorem Composition.sizeUpTo_add_blocksFun_le {n : ℕ} (c : Composition n) (l : Fin c.length) : c.sizeUpTo ↑l + c.blocksFun l ≤ n

The l-th block of a composition c of n ends no later than n.

instance Composition.neZero_blocksFun {n : ℕ} (c : Composition n) (l : Fin c.length) : NeZero (c.blocksFun l)

Every block of a composition is nonempty, so the functor component φ_{iₗ} applied to it has positive arity.

instance Composition.neZero_length {n : ℕ} (c : Composition n) [NeZero n] : NeZero c.length

A composition of a positive integer has at least one block, so the outer operation m'_k applied to the blocks has positive arity.

def AInfinityTheory.compositionBlockObj {n : ℕ} {Obj : Type u_1} (obj : Fin (n + 1) → Obj) (c : Composition n) (l : Fin c.length) : Fin (c.blocksFun l + 1) → Obj

The object string obj iₗ, …, obj (iₗ + c.blocksFun l) of the l-th block of a composition c of n, where iₗ = c.sizeUpTo l is the start of the block.

Equations

• AInfinityTheory.compositionBlockObj obj c l i = obj (Fin.castLE ⋯ (Fin.natAdd (c.sizeUpTo ↑l) i))

@[simp]

theorem AInfinityTheory.compositionBlockObj_zero {n : ℕ} {Obj : Type u_1} (obj : Fin (n + 1) → Obj) (c : Composition n) (l : Fin c.length) : compositionBlockObj obj c l 0 = obj (c.boundary l.castSucc)

The l-th block of a composition starts at the l-th boundary.

@[simp]

theorem AInfinityTheory.compositionBlockObj_last {n : ℕ} {Obj : Type u_1} (obj : Fin (n + 1) → Obj) (c : Composition n) (l : Fin c.length) : compositionBlockObj obj c l (Fin.last (c.blocksFun l)) = obj (c.boundary l.succ)

The l-th block of a composition ends at the (l + 1)-st boundary.

structure AInfinityTheory.AInfinityFunctorData (β : Type u_1) (β' : Type u_2) [AddCommGroup β] [GradingType β] [AddCommGroup β'] [GradingType β'] (R : Type u_3) [CommRing R] (Obj : Type u_4) (Obj' : Type u_5) [GradedLinearQuiver β R Obj] [GradedLinearQuiver β' R Obj'] : Type (max (max (max (max (max u_1 u_2) u_4) u_5) u_6) u_7)

The data of an A∞-functor between graded R-linear quivers: a map on objects, a homomorphism of grading types and, for each n ≥ 1, a functor component φₙ of degree 1 - n. No relations are imposed.

• obj : Obj → Obj'

  The action of the functor on objects.

• degMap : β →+ᵍ β'

  The homomorphism of grading types translating source degrees into target degrees.

• map {n : ℕ} [NeZero n] (X : Fin (n + 1) → Obj) : GradedMultilinearMap R (GradedLinearQuiver.ComposableHomType R X) (fun (b : β) => GradedLinearQuiver.Hom R (self.obj (X 0)) (self.obj (X (Fin.last n))) (self.degMap b)) (shift (1 - ↑n))

  The action of the functor on hom spaces, i.e. the functor components φₙ, of degree 1 - n, landing in the hom spaces of the target in the translated degrees.

theorem AInfinityTheory.AInfinityFunctorData.operationTargetDeg_degMap {β : Type u_1} {β' : Type u_2} [AddCommGroup β] [GradingType β] [AddCommGroup β'] [GradingType β'] {R : Type u_3} [CommRing R] {Obj : Type u_4} {Obj' : Type u_5} [GradedLinearQuiver β R Obj] [GradedLinearQuiver β' R Obj'] (F : AInfinityFunctorData β β' R Obj Obj') {k : ℕ} (b : Fin k → β) : (operationTargetDeg fun (i : Fin k) => F.degMap (b i)) = F.degMap (operationTargetDeg b)

The grading homomorphism commutes with taking the degree of an operation.

theorem AInfinityTheory.AInfinityFunctorData.operationTargetDeg_degMap_functorTargetDeg_embedding {n : ℕ} {β : Type u_1} {β' : Type u_2} [AddCommGroup β] [GradingType β] [AddCommGroup β'] [GradingType β'] {R : Type u_3} [CommRing R] {Obj : Type u_4} {Obj' : Type u_5} [GradedLinearQuiver β R Obj] [GradedLinearQuiver β' R Obj'] (F : AInfinityFunctorData β β' R Obj Obj') {deg : Fin n → β} (c : Composition n) (d : β) (hd : operationTargetDeg deg = d) : (operationTargetDeg fun (l : Fin c.length) => F.degMap (functorTargetDeg fun (j : Fin (c.blocksFun l)) => deg ((c.embedding l) j))) = F.degMap d

Applying functor components to the blocks of a composition c of n and then the c.length-ary operation of the target lands in the image of the degree of mₙ.

The left-hand side of the functor equation

def AInfinityTheory.AInfinityFunctorData.mapCompTerm {n : ℕ} {β : Type u_1} {β' : Type u_2} [AddCommGroup β] [GradingType β] [AddCommGroup β'] [GradingType β'] {R : Type u_3} [CommRing R] {Obj : Type u_4} {Obj' : Type u_5} [GradedLinearQuiver β R Obj] [GradedLinearQuiver β' R Obj'] (m : AInfinityComposition β R Obj) (F : AInfinityFunctorData β β' R Obj Obj') {obj : Fin (n + 1) → Obj} {deg : Fin n → β} (x : (i : Fin n) → GradedLinearQuiver.ComposableHomType R obj i (deg i)) (p : StasheffIndex n) (d : β) (hd : operationTargetDeg deg = d) : GradedLinearQuiver.Hom R (F.obj (obj 0)) (F.obj (obj (Fin.last n))) (F.degMap d)

The term φ_{r+1+t}(a_1, …, a_r, m_s(a_{r+1}, …, a_{r+s}), a_{r+s+1}, …, a_n) of the left-hand side of the functor equation indexed by p = (r, s, t), in degree F.degMap d for any d equal to the degree of mₙ.

Equations

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

def AInfinityTheory.AInfinityFunctorData.mapCompSum {n : ℕ} {β : Type u_1} {β' : Type u_2} [AddCommGroup β] [GradingType β] [AddCommGroup β'] [GradingType β'] {R : Type u_3} [CommRing R] {Obj : Type u_4} {Obj' : Type u_5} [GradedLinearQuiver β R Obj] [GradedLinearQuiver β' R Obj'] (m : AInfinityComposition β R Obj) (F : AInfinityFunctorData β β' R Obj Obj') {obj : Fin (n + 1) → Obj} {deg : Fin n → β} (x : (i : Fin n) → GradedLinearQuiver.ComposableHomType R obj i (deg i)) (d : β) (hd : operationTargetDeg deg = d) : GradedLinearQuiver.Hom R (F.obj (obj 0)) (F.obj (obj (Fin.last n))) (F.degMap d)

The left-hand side of the arity-n functor equation, with the Koszul signs of the Stasheff identities, in degree F.degMap d for any d equal to the degree of mₙ.

Equations

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

The right-hand side of the functor equation

def AInfinityTheory.AInfinityFunctorData.compositionBlockMap {n : ℕ} {β : Type u_1} {β' : Type u_2} [AddCommGroup β] [GradingType β] [AddCommGroup β'] [GradingType β'] {R : Type u_3} [CommRing R] {Obj : Type u_4} {Obj' : Type u_5} [GradedLinearQuiver β R Obj] [GradedLinearQuiver β' R Obj'] (F : AInfinityFunctorData β β' R Obj Obj') {obj : Fin (n + 1) → Obj} {deg : Fin n → β} (x : (i : Fin n) → GradedLinearQuiver.ComposableHomType R obj i (deg i)) (c : Composition n) (l : Fin c.length) : GradedLinearQuiver.ComposableHomType R (fun (k : Fin (c.length + 1)) => F.obj (obj (c.boundary k))) l (F.degMap (functorTargetDeg fun (j : Fin (c.blocksFun l)) => deg ((c.embedding l) j)))

The output φ_{iₗ} of the l-th block of a composition c = (i₁, …, iₖ) of n, as the l-th input of the outer operation m'_k.

Equations

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

def AInfinityTheory.AInfinityFunctorData.compMapTerm {n : ℕ} {β : Type u_1} {β' : Type u_2} [AddCommGroup β] [GradingType β] [AddCommGroup β'] [GradingType β'] {R : Type u_3} [CommRing R] {Obj : Type u_4} {Obj' : Type u_5} [GradedLinearQuiver β R Obj] [GradedLinearQuiver β' R Obj'] (m' : AInfinityComposition β' R Obj') (F : AInfinityFunctorData β β' R Obj Obj') {obj : Fin (n + 1) → Obj} {deg : Fin n → β} (x : (i : Fin n) → GradedLinearQuiver.ComposableHomType R obj i (deg i)) [NeZero n] (c : Composition n) (d : β) (hd : operationTargetDeg deg = d) : GradedLinearQuiver.Hom R (F.obj (obj 0)) (F.obj (obj (Fin.last n))) (F.degMap d)

The term m'_k(φ_{i₁}(a_1, …, a_{i₁}), …, φ_{iₖ}(a_{n-iₖ+1}, …, a_n)) of the right-hand side of the functor equation indexed by a composition c = (i₁, …, iₖ) of n, in degree F.degMap d for any d equal to the degree of mₙ.

Equations

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

def AInfinityTheory.AInfinityFunctorData.compMapSum {n : ℕ} {β : Type u_1} {β' : Type u_2} [AddCommGroup β] [GradingType β] [AddCommGroup β'] [GradingType β'] {R : Type u_3} [CommRing R] {Obj : Type u_4} {Obj' : Type u_5} [GradedLinearQuiver β R Obj] [GradedLinearQuiver β' R Obj'] (m' : AInfinityComposition β' R Obj') (F : AInfinityFunctorData β β' R Obj Obj') {obj : Fin (n + 1) → Obj} {deg : Fin n → β} (x : (i : Fin n) → GradedLinearQuiver.ComposableHomType R obj i (deg i)) [NeZero n] (d : β) (hd : operationTargetDeg deg = d) : GradedLinearQuiver.Hom R (F.obj (obj 0)) (F.obj (obj (Fin.last n))) (F.degMap d)

The right-hand side of the arity-n functor equation, summed over all compositions of n, in degree F.degMap d for any d equal to the degree of mₙ.

Equations

• AInfinityTheory.AInfinityFunctorData.compMapSum m' F x d hd = ∑ c : Composition n, AInfinityTheory.AInfinityFunctorData.compMapTerm (fun {n : ℕ} [NeZero n] => m') F x c d hd

def AInfinityTheory.AInfinityFunctorData.SatisfiesFunctorEquations {β : Type u_1} {β' : Type u_2} [AddCommGroup β] [GradingType β] [AddCommGroup β'] [GradingType β'] {R : Type u_3} [CommRing R] {Obj : Type u_4} {Obj' : Type u_5} [GradedLinearQuiver β R Obj] [GradedLinearQuiver β' R Obj'] (m : AInfinityComposition β R Obj) (m' : AInfinityComposition β' R Obj') (F : AInfinityFunctorData β β' R Obj Obj') : Prop

The A∞-functor equations: in every arity n ≥ 1, the left-hand side and the right-hand side of the functor equation agree on every composable string of inputs.

Equations

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

structure AInfinityTheory.AInfinityFunctor (β : Type u_1) (β' : Type u_2) [AddCommGroup β] [GradingType β] [AddCommGroup β'] [GradingType β'] (R : Type u_3) [CommRing R] (Obj : Type u_4) (Obj' : Type u_5) [AInfinityCategory β R Obj] [AInfinityCategory β' R Obj'] extends AInfinityTheory.AInfinityFunctorData β β' R Obj Obj' : Type (max (max (max (max (max u_1 u_2) u_4) u_5) u_6) u_7)

An A∞-functor between A∞-categories: A∞-functor data satisfying the functor equations.

• obj : Obj → Obj'
• degMap : β →+ᵍ β'
• map {n : ℕ} [NeZero n] (X : Fin (n + 1) → Obj) : GradedMultilinearMap R (GradedLinearQuiver.ComposableHomType R X) (fun (b : β) => GradedLinearQuiver.Hom R (self.obj (X 0)) (self.obj (X (Fin.last n))) (self.degMap b)) (shift (1 - ↑n))
• satisfiesFunctorEquations : AInfinityFunctorData.SatisfiesFunctorEquations (fun {n : ℕ} [NeZero n] => AInfinityCategoryStruct.m) (fun {n : ℕ} [NeZero n] => AInfinityCategoryStruct.m) self.toAInfinityFunctorData

  The functor components satisfy the functor equations in every arity.