A-infinity categories induced along a map of objects

For an A∞ category 𝒞 on a graded linear quiver C and any map F : D → C, the induced A∞ category 𝒞.induced F lives on the induced quiver TauCeti.GradedLinearQuiver.InducedQuiver C F: its objects are those of D, its morphisms X ⟶ Y are the morphisms F X ⟶ F Y of 𝒞, and its operation on a composable string X₀, …, Xₙ is the operation of 𝒞 on the string F X₀, …, F Xₙ. When F is not injective, the same morphism of 𝒞 appears between several pairs of objects.

An A∞ functor from an A∞ category ℬ on D to 𝒞, with object map F, sends a composable string of morphisms of ℬ to a morphism of 𝒞 between the images of its endpoints, and its defining equation is imposed only on composable strings. It can therefore be stored as an A∞ morphism from the total algebra of ℬ to the total algebra of the induced category along F. This avoids an obstruction that the total algebra of 𝒞 itself can meet as a target when F is not injective: a string of morphisms which is not composable in ℬ can become composable after applying F, and the operations of 𝒞 need not vanish on it.

The total module of the induced quiver maps to that of C (TauCeti.GradedLinearQuiver.InducedQuiver.totalHomMap). In general this map need not be injective, and it intertwines the operations on composable strings (TauCeti.AInfinityCategory.totalHomMap_induced_m_of_chain) but in general not on other strings. So the induced structure is in general not a pullback of A∞ algebras. Instead its Stasheff identities are checked string by string: on a composable string each Stasheff term is the corresponding term of 𝒞, which lies in a single hom module where the map is injective, and on any other string every term vanishes. When F is injective, the map intertwines the operations on all strings (TauCeti.AInfinityCategory.totalHomMap_induced_m), so it is a strict A∞ morphism of total algebras (TauCeti.AInfinityCategory.inducedInclusion).

Main definitions

• TauCeti.AInfinityCategory.induced: the A∞ category induced along a map of objects.
• TauCeti.AInfinityCategory.inducedInclusion: along an injective map of objects, the inclusion of the total algebra of morphisms of the induced category into that of 𝒞, a strict A∞ morphism.
• TauCeti.AInfinityHom.liftInduced: along an injective map of objects, the factorization through the induced category of an A∞ morphism into the total algebra of 𝒞 whose Taylor map is path-compatible.

Main results

• TauCeti.AInfinityCategory.totalHomMap_induced_m_of_chain: on a composable string, the map of total modules intertwines the operations of the induced category with those of 𝒞.
• TauCeti.AInfinityCategory.induced_m_homInclusion and TauCeti.AInfinityCategory.coe_pathOperation_induced_apply: the operation of the induced category on a composable string is the operation of 𝒞 on its image.
• TauCeti.AInfinityCategory.eq_induced: the induced category is the unique A∞ category on the induced quiver with these operations.
• TauCeti.AInfinityCategory.homDifferential_induced and TauCeti.AInfinityCategory.comp_induced: its differential and composition are those of 𝒞.
• TauCeti.AInfinityCategory.totalHomMap_induced_m: along an injective map of objects, the map of total modules intertwines the operations on all strings.
• TauCeti.AInfinityHom.inducedInclusion_comp_liftInduced and TauCeti.AInfinityHom.eq_liftInduced: the factorization of a path-compatible A∞ morphism through the total algebra of the induced category recovers the morphism and is unique.

References

• B. Keller, Introduction to A-infinity algebras and modules, Section 7, for A∞ categories and functors.
• V. Lyubashenko, Category of A-infinity-categories, Homology, Homotopy and Applications 5 (2003), for A∞ functors as morphisms of bar constructions over a map of objects.

The operations of the induced category

The Stasheff identities

noncomputable def TauCeti.AInfinityCategory.induced {R : Type w} [CommRing R] {C : Type u} [GradedLinearQuiver R C] {D : Type u'} (𝒞 : AInfinityCategory R C) (F : D → C) : AInfinityCategory R (GradedLinearQuiver.InducedQuiver C F)

The A∞ category induced by 𝒞 along a map of objects F : D → C: the A∞ category on the induced quiver whose operation on a composable string X₀, …, Xₙ is the operation of 𝒞 on F X₀, …, F Xₙ (TauCeti.AInfinityCategory.coe_pathOperation_induced_apply).

theorem TauCeti.AInfinityCategory.totalHomMap_induced_m_of_chain {R : Type w} [CommRing R] {C : Type u} [GradedLinearQuiver R C] {D : Type u'} (𝒞 : AInfinityCategory R C) (F : D → C) {n : ℕ} (s t : Fin n → GradedLinearQuiver.InducedQuiver C F) {x : Fin n → GradedLinearQuiver.TotalHom R (GradedLinearQuiver.InducedQuiver C F)} (hx : ∀ (i : Fin n), x i ∈ (GradedLinearQuiver.homInclusion (s i) (t i)).range) (h : ∀ (i j : Fin n), ↑j = ↑i + 1 → t j = s i) : (GradedLinearQuiver.InducedQuiver.totalHomMap R F) (((𝒞.induced F).m n) x) = (𝒞.m n) fun (i : Fin n) => (GradedLinearQuiver.InducedQuiver.totalHomMap R F) (x i)

The induced category has the operations of 𝒞 on composable strings. On a string of morphisms sᵢ ⟶ tᵢ of the induced quiver in which the source of each morphism is the target of the next one, the map of total modules sends the operation of the induced category to the operation of 𝒞 on the images of the morphisms.

theorem TauCeti.AInfinityCategory.induced_m_homInclusion {R : Type w} [CommRing R] {C : Type u} [GradedLinearQuiver R C] {D : Type u'} (𝒞 : AInfinityCategory R C) (F : D → C) {n : ℕ} (X : Fin (n + 1) → GradedLinearQuiver.InducedQuiver C F) (x : (i : Fin n) → ↑(GradedLinearQuiver.homModule (X i.rev.castSucc) (X i.rev.succ))) : (((𝒞.induced F).m n) fun (i : Fin n) => (GradedLinearQuiver.homInclusion (X i.rev.castSucc) (X i.rev.succ)) (x i)) = (GradedLinearQuiver.homInclusion (X 0) (X (Fin.last n))) ((GradedLinearQuiver.homProjection (F (X 0).obj) (F (X (Fin.last n)).obj)) ((𝒞.m n) fun (i : Fin n) => (GradedLinearQuiver.homInclusion (F (X i.rev.castSucc).obj) (F (X i.rev.succ).obj)) (x i)))

On a composable string X₀, …, Xₙ, the operation of the induced category is the component between F X₀ and F Xₙ of the operation of 𝒞 on the same morphisms.

@[simp]

theorem TauCeti.AInfinityCategory.coe_pathOperation_induced_apply {R : Type w} [CommRing R] {C : Type u} [GradedLinearQuiver R C] {D : Type u'} (𝒞 : AInfinityCategory R C) (F : D → C) {n : ℕ} (X : Fin (n + 1) → GradedLinearQuiver.InducedQuiver C F) (d : Fin n → ℤ) (x : (i : Fin n) → GradedLinearQuiver.grHom R (X i.rev.castSucc) (X i.rev.succ) (d i)) : ↑(((𝒞.induced F).pathOperation X d) x) = ↑((𝒞.pathOperation (fun (k : Fin (n + 1)) => F (X k).obj) d) x)

The operation of the induced category on a composable string X₀, …, Xₙ is the operation of 𝒞 on the string F X₀, …, F Xₙ.

theorem TauCeti.AInfinityCategory.eq_induced {R : Type w} [CommRing R] {C : Type u} [GradedLinearQuiver R C] {D : Type u'} (𝒞 : AInfinityCategory R C) (F : D → C) {𝒟 : AInfinityCategory R (GradedLinearQuiver.InducedQuiver C F)} (h : ∀ (n : ℕ) (X : Fin (n + 1) → GradedLinearQuiver.InducedQuiver C F) (x : (i : Fin n) → ↑(GradedLinearQuiver.homModule (X i.rev.castSucc) (X i.rev.succ))), (GradedLinearQuiver.InducedQuiver.totalHomMap R F) ((𝒟.m n) fun (i : Fin n) => (GradedLinearQuiver.homInclusion (X i.rev.castSucc) (X i.rev.succ)) (x i)) = (𝒞.m n) fun (i : Fin n) => (GradedLinearQuiver.homInclusion (F (X i.rev.castSucc).obj) (F (X i.rev.succ).obj)) (x i)) : 𝒟 = 𝒞.induced F

The induced category is the unique A∞ category on the induced quiver whose operations on composable strings the map of total modules sends to the operations of 𝒞.

theorem TauCeti.AInfinityCategory.totalHomMap_taylor_induced {R : Type w} [CommRing R] {C : Type u} [GradedLinearQuiver R C] {D : Type u'} (𝒞 : AInfinityCategory R C) (F : D → C) {X Y : GradedLinearQuiver.InducedQuiver C F} {w : ReducedTensorWords R (GradedLinearQuiver.TotalHom R (GradedLinearQuiver.InducedQuiver C F))} (hw : w ∈ GradedLinearQuiver.composableWords R X Y) : (GradedLinearQuiver.InducedQuiver.totalHomMap R F) ((𝒞.induced F).taylor w) = 𝒞.taylor ((ReducedTensorWords.map R (GradedLinearQuiver.InducedQuiver.totalHomMap R F)) w)

The induced category has the Taylor map of 𝒞 on composable words. On a composable word, the map of total modules sends the Taylor map of the induced category to the Taylor map of 𝒞 on the letterwise image of the word.

@[simp]

theorem TauCeti.AInfinityCategory.homDifferential_induced {R : Type w} [CommRing R] {C : Type u} [GradedLinearQuiver R C] {D : Type u'} (𝒞 : AInfinityCategory R C) (F : D → C) (X Y : GradedLinearQuiver.InducedQuiver C F) (f : ↑(GradedLinearQuiver.homModule X Y)) : ((𝒞.induced F).homDifferential X Y) f = (𝒞.homDifferential (F X.obj) (F Y.obj)) f

The differential of the induced category is the differential of 𝒞.

@[simp]

theorem TauCeti.AInfinityCategory.comp_induced {R : Type w} [CommRing R] {C : Type u} [GradedLinearQuiver R C] {D : Type u'} (𝒞 : AInfinityCategory R C) (F : D → C) (X Y Z : GradedLinearQuiver.InducedQuiver C F) (g : ↑(GradedLinearQuiver.homModule Y Z)) (f : ↑(GradedLinearQuiver.homModule X Y)) : (((𝒞.induced F).comp X Y Z) g) f = ((𝒞.comp (F X.obj) (F Y.obj) (F Z.obj)) g) f

The composition of the induced category is the composition of 𝒞.

@[simp]

theorem TauCeti.AInfinityCategory.totalHomMap_induced_m {R : Type w} [CommRing R] {C : Type u} [GradedLinearQuiver R C] {D : Type u'} (𝒞 : AInfinityCategory R C) {F : D → C} (hF : Function.Injective F) (n : ℕ) (x : Fin n → GradedLinearQuiver.TotalHom R (GradedLinearQuiver.InducedQuiver C F)) : (GradedLinearQuiver.InducedQuiver.totalHomMap R F) (((𝒞.induced F).m n) x) = (𝒞.m n) fun (i : Fin n) => (GradedLinearQuiver.InducedQuiver.totalHomMap R F) (x i)

Along an injective map of objects, the map of total modules intertwines the operations. Including the value of an operation of the induced category into the total module of 𝒞 gives the operation of 𝒞 on the included morphisms, on all strings: a string which is not composable in the induced quiver is not composable in C.

noncomputable def TauCeti.AInfinityCategory.inducedInclusion {R : Type w} [CommRing R] {C : Type u} [GradedLinearQuiver R C] {D : Type u'} (𝒞 : AInfinityCategory R C) {F : D → C} (hF : Function.Injective F) : AInfinityStrictHom (𝒞.induced F).toAInfinityAlgebra 𝒞.toAInfinityAlgebra

The inclusion of the total algebra of morphisms of the category induced along an injective map of objects into that of 𝒞, a strict A∞ morphism.

@[simp]

theorem TauCeti.AInfinityCategory.inducedInclusion_toLinearMap {R : Type w} [CommRing R] {C : Type u} [GradedLinearQuiver R C] {D : Type u'} (𝒞 : AInfinityCategory R C) {F : D → C} (hF : Function.Injective F) : (𝒞.inducedInclusion hF).toLinearMap = GradedLinearQuiver.InducedQuiver.totalHomMap R F

The underlying linear map of the inclusion of total algebras of an induced category is the map of total modules.

@[simp]

theorem TauCeti.AInfinityCategory.coe_inducedInclusion {R : Type w} [CommRing R] {C : Type u} [GradedLinearQuiver R C] {D : Type u'} (𝒞 : AInfinityCategory R C) {F : D → C} (hF : Function.Injective F) : ⇑(𝒞.inducedInclusion hF) = ⇑(GradedLinearQuiver.InducedQuiver.totalHomMap R F)

The inclusion of total algebras of an induced category is the map of total modules.

The factorization of a path-compatible A∞ morphism through the induced category

noncomputable def TauCeti.AInfinityHom.liftInduced {R : Type w} [CommRing R] {C : Type u} [GradedLinearQuiver R C] {D : Type u'} [GradedLinearQuiver R D] {ℬ : AInfinityCategory R D} {𝒞 : AInfinityCategory R C} {F : D → C} (f : AInfinityHom ℬ.toAInfinityAlgebra 𝒞.toAInfinityAlgebra) (hF : Function.Injective F) (hf : GradedLinearQuiver.IsWordPathCompatible F f.taylor) : AInfinityHom ℬ.toAInfinityAlgebra (𝒞.induced F).toAInfinityAlgebra

The factorization of a path-compatible A∞ morphism through the induced category. If F : D → C is injective and the Taylor map of f : ℬ.toAInfinityAlgebra ⟶ 𝒞.toAInfinityAlgebra sends composable words from X to Y to morphisms F X ⟶ F Y and non-composable words to zero, then f factors uniquely through the inclusion of the total algebra of 𝒞.induced F (TauCeti.AInfinityHom.inducedInclusion_comp_liftInduced and TauCeti.AInfinityHom.eq_liftInduced).

theorem TauCeti.AInfinityHom.totalHomMap_comp_taylor_liftInduced {R : Type w} [CommRing R] {C : Type u} [GradedLinearQuiver R C] {D : Type u'} [GradedLinearQuiver R D] {ℬ : AInfinityCategory R D} {𝒞 : AInfinityCategory R C} {F : D → C} (f : AInfinityHom ℬ.toAInfinityAlgebra 𝒞.toAInfinityAlgebra) (hF : Function.Injective F) (hf : GradedLinearQuiver.IsWordPathCompatible F f.taylor) : GradedLinearQuiver.InducedQuiver.totalHomMap R F ∘ₗ (f.liftInduced hF hf).taylor = f.taylor

The Taylor map of the factorization of f through the induced category is characterized by recovering the Taylor map of f after the map of total modules.

@[simp]

theorem TauCeti.AInfinityHom.inducedInclusion_comp_liftInduced {R : Type w} [CommRing R] {C : Type u} [GradedLinearQuiver R C] {D : Type u'} [GradedLinearQuiver R D] {ℬ : AInfinityCategory R D} {𝒞 : AInfinityCategory R C} {F : D → C} (f : AInfinityHom ℬ.toAInfinityAlgebra 𝒞.toAInfinityAlgebra) (hF : Function.Injective F) (hf : GradedLinearQuiver.IsWordPathCompatible F f.taylor) : (𝒞.inducedInclusion hF).toAInfinityHom.comp (f.liftInduced hF hf) = f

The factorization of f through the induced category recovers f after the inclusion of the total algebra of the induced category.

theorem TauCeti.AInfinityHom.eq_liftInduced {R : Type w} [CommRing R] {C : Type u} [GradedLinearQuiver R C] {D : Type u'} [GradedLinearQuiver R D] {ℬ : AInfinityCategory R D} {𝒞 : AInfinityCategory R C} {F : D → C} (f : AInfinityHom ℬ.toAInfinityAlgebra 𝒞.toAInfinityAlgebra) (hF : Function.Injective F) (hf : GradedLinearQuiver.IsWordPathCompatible F f.taylor) (ψ : AInfinityHom ℬ.toAInfinityAlgebra (𝒞.induced F).toAInfinityAlgebra) (hψ : (𝒞.inducedInclusion hF).toAInfinityHom.comp ψ = f) : ψ = f.liftInduced hF hf

Uniqueness of the factorization: the factorization of f is the only A∞ morphism into the total algebra of the induced category which recovers f after the inclusion of total algebras.

theorem TauCeti.AInfinityHom.totalHomMap_linearPart_liftInduced {R : Type w} [CommRing R] {C : Type u} [GradedLinearQuiver R C] {D : Type u'} [GradedLinearQuiver R D] {ℬ : AInfinityCategory R D} {𝒞 : AInfinityCategory R C} {F : D → C} (f : AInfinityHom ℬ.toAInfinityAlgebra 𝒞.toAInfinityAlgebra) (hF : Function.Injective F) (hf : GradedLinearQuiver.IsWordPathCompatible F f.taylor) (a : GradedLinearQuiver.TotalHom R D) : (GradedLinearQuiver.InducedQuiver.totalHomMap R F) ((f.liftInduced hF hf).linearPart a) = f.linearPart a

The linear part of the factorization of f through the induced category is the linear part of f after the map of total modules.