Homological transfer for A-infinity categories

Let 𝒞 be an A∞ category on a graded linear quiver C, and let D be a graded linear quiver whose objects correspond to those of C through a bijection e : D ≃ C. A special contraction (i, p, h) of the total module of morphisms of C, with the differential m₁, onto the total module of morphisms of D is compatible with the hom modules (TauCeti.LinearSpecialContraction.IsHomCompatible) when i sends morphisms X ⟶ Y to morphisms e X ⟶ e Y, p sends morphisms U ⟶ V to morphisms e⁻¹ U ⟶ e⁻¹ V, and h preserves every hom module. This is the shape of a contraction assembled from special contractions of the individual Hom complexes of 𝒞.

Homological transfer of the total A∞ algebra of 𝒞 along such a contraction (TauCeti.AInfinityAlgebra.transfer) gives an A∞ structure on the total module of morphisms of D, and this structure is again an A∞ category, the transferred A∞ category TauCeti.AInfinityCategory.transfer. Indeed, every operator entering the transfer preserves the composable words from U to V and the non-composable words of the bar construction: the higher bar differential of 𝒞, because the Taylor map of 𝒞 is path-compatible; the tensor-trick homotopy K, because it acts letter by letter through h, i p and Koszul twists, which preserve every hom module; and therefore the perturbation operator X = (1 + δ K)⁻¹ δ, which is a pointwise finite geometric series in them. The letterwise inclusion and projection carry composable words along e and e⁻¹, and non-composable words to non-composable words since e is injective. So the Taylor map d_D + p X i of the transferred structure is path-compatible. The transferred differential is d_D and the transferred composition is g ∘ f = p m₂(i g, i f).

The Taylor maps of the extending morphism i' = i - K X i and of the projection morphism p' = p - p X K of the transfer are path-compatible along e and along e⁻¹ respectively (TauCeti.AInfinityCategory.isWordPathCompatible_taylor_transferInclusion and TauCeti.AInfinityCategory.isWordPathCompatible_taylor_transferProjection): they send composable words to morphisms between the corresponding objects, as the components of an A∞ functor must.

Main definitions

• TauCeti.LinearSpecialContraction.IsHomCompatible: a special contraction of total modules of morphisms compatible with the hom modules along a bijection of objects.
• TauCeti.AInfinityCategory.transfer: the transferred A∞ category.

Main results

• TauCeti.LinearSpecialContraction.reducedTensorWordsHomotopy_mem_composableWords and TauCeti.LinearSpecialContraction.reducedTensorWordsHomotopy_mem_nonComposableWords: the tensor-trick homotopy preserves composable and non-composable words.
• TauCeti.AInfinityCategory.higherBarDifferential_mem_composableWords and TauCeti.AInfinityCategory.higherBarDifferential_mem_nonComposableWords: so does the higher bar differential of an A∞ category.
• TauCeti.AInfinityCategory.isWordPathCompatible_taylor_transfer: the transferred operations are path-compatible.
• TauCeti.AInfinityCategory.homInclusion_homDifferential_transfer and TauCeti.AInfinityCategory.homInclusion_comp_transfer: the differential and the composition of the transferred category.
• TauCeti.AInfinityCategory.isWordPathCompatible_taylor_transferInclusion and TauCeti.AInfinityCategory.isWordPathCompatible_taylor_transferProjection: the Taylor maps of the extending and projection morphisms are path-compatible along e and e⁻¹.

References

• P. Seidel, Fukaya categories and Picard--Lefschetz theory, Zurich Lectures in Advanced Mathematics, EMS, 2008, Section (1i), for homological perturbation of A∞ categories along contractions of the morphism spaces.
• B. Keller, Introduction to A-infinity algebras and modules, Sections 3.3 and 7.

Contractions compatible with the hom modules

theorem TauCeti.LinearSpecialContraction.reducedTensorWordsHomotopy_mem_composableWords {R : Type w} [CommRing R] {C : Type u₁} [GradedLinearQuiver R C] {dC : Module.End R (GradedLinearQuiver.TotalHom R C)} {N : Type u_1} [AddCommGroup N] [Module R N] {dN : Module.End R N} (c : LinearSpecialContraction dC dN) (hh : ∀ (U V : C) (f : ↑(GradedLinearQuiver.homModule U V)), c.homotopy ((GradedLinearQuiver.homInclusion U V) f) ∈ (GradedLinearQuiver.homInclusion U V).range) (hip : ∀ (U V : C) (f : ↑(GradedLinearQuiver.homModule U V)), c.incl (c.proj ((GradedLinearQuiver.homInclusion U V) f)) ∈ (GradedLinearQuiver.homInclusion U V).range) (s : ℤ) {U V : C} {w : ReducedTensorWords R (GradedLinearQuiver.TotalHom R C)} (hw : w ∈ GradedLinearQuiver.composableWords R U V) : (c.reducedTensorWordsHomotopy ((GradedLinearQuiver.totalGrading R C).shift s)) w ∈ GradedLinearQuiver.composableWords R U V

The tensor-trick homotopy preserves composable words from U to V, for every shift of the total grading, when the homotopy and the idempotent i p preserve every hom module: on a word it is a sum of words obtained by applying a Koszul twist, the homotopy or i p to each letter.

theorem TauCeti.LinearSpecialContraction.reducedTensorWordsHomotopy_mem_nonComposableWords {R : Type w} [CommRing R] {C : Type u₁} [GradedLinearQuiver R C] {dC : Module.End R (GradedLinearQuiver.TotalHom R C)} {N : Type u_1} [AddCommGroup N] [Module R N] {dN : Module.End R N} (c : LinearSpecialContraction dC dN) (hh : ∀ (U V : C) (f : ↑(GradedLinearQuiver.homModule U V)), c.homotopy ((GradedLinearQuiver.homInclusion U V) f) ∈ (GradedLinearQuiver.homInclusion U V).range) (hip : ∀ (U V : C) (f : ↑(GradedLinearQuiver.homModule U V)), c.incl (c.proj ((GradedLinearQuiver.homInclusion U V) f)) ∈ (GradedLinearQuiver.homInclusion U V).range) (s : ℤ) {w : ReducedTensorWords R (GradedLinearQuiver.TotalHom R C)} (hw : w ∈ GradedLinearQuiver.nonComposableWords R C) : (c.reducedTensorWordsHomotopy ((GradedLinearQuiver.totalGrading R C).shift s)) w ∈ GradedLinearQuiver.nonComposableWords R C

The tensor-trick homotopy preserves non-composable words, for every shift of the total grading, when the homotopy and the idempotent i p preserve every hom module.

structure TauCeti.LinearSpecialContraction.IsHomCompatible {R : Type w} [CommRing R] {C : Type u₁} {D : Type u₂} [GradedLinearQuiver R C] [GradedLinearQuiver R D] {dC : Module.End R (GradedLinearQuiver.TotalHom R C)} {dD : Module.End R (GradedLinearQuiver.TotalHom R D)} (e : D ≃ C) (c : LinearSpecialContraction dC dD) : Prop

A special contraction of the total module of morphisms of C onto that of D is compatible with the hom modules along a bijection of objects e : D ≃ C when its inclusion sends morphisms X ⟶ Y to morphisms e X ⟶ e Y, its projection sends morphisms U ⟶ V to morphisms e⁻¹ U ⟶ e⁻¹ V, and its homotopy sends morphisms U ⟶ V to morphisms U ⟶ V. This is the shape of a contraction assembled from contractions of the individual hom modules.

• incl_homInclusion_mem (X Y : D) (f : ↑(GradedLinearQuiver.homModule X Y)) : c.incl ((GradedLinearQuiver.homInclusion X Y) f) ∈ (GradedLinearQuiver.homInclusion (e X) (e Y)).range

  The inclusion sends morphisms X ⟶ Y to morphisms e X ⟶ e Y.

• proj_homInclusion_mem (U V : C) (f : ↑(GradedLinearQuiver.homModule U V)) : c.proj ((GradedLinearQuiver.homInclusion U V) f) ∈ (GradedLinearQuiver.homInclusion (e.symm U) (e.symm V)).range

  The projection sends morphisms U ⟶ V to morphisms e⁻¹ U ⟶ e⁻¹ V.

• homotopy_homInclusion_mem (U V : C) (f : ↑(GradedLinearQuiver.homModule U V)) : c.homotopy ((GradedLinearQuiver.homInclusion U V) f) ∈ (GradedLinearQuiver.homInclusion U V).range

  The homotopy sends morphisms U ⟶ V to morphisms U ⟶ V.

theorem TauCeti.LinearSpecialContraction.IsHomCompatible.incl_proj_homInclusion_mem {R : Type w} [CommRing R] {C : Type u₁} {D : Type u₂} [GradedLinearQuiver R C] [GradedLinearQuiver R D] {dC : Module.End R (GradedLinearQuiver.TotalHom R C)} {dD : Module.End R (GradedLinearQuiver.TotalHom R D)} {e : D ≃ C} {c : LinearSpecialContraction dC dD} (hc : IsHomCompatible e c) (U V : C) (f : ↑(GradedLinearQuiver.homModule U V)) : c.incl (c.proj ((GradedLinearQuiver.homInclusion U V) f)) ∈ (GradedLinearQuiver.homInclusion U V).range

The idempotent i p of a contraction compatible with the hom modules preserves every hom module.

theorem TauCeti.LinearSpecialContraction.IsHomCompatible.proj_mem_range {R : Type w} [CommRing R] {C : Type u₁} {D : Type u₂} [GradedLinearQuiver R C] [GradedLinearQuiver R D] {dC : Module.End R (GradedLinearQuiver.TotalHom R C)} {dD : Module.End R (GradedLinearQuiver.TotalHom R D)} {e : D ≃ C} {c : LinearSpecialContraction dC dD} (hc : IsHomCompatible e c) {X Y : D} {u : GradedLinearQuiver.TotalHom R C} (hu : u ∈ (GradedLinearQuiver.homInclusion (e X) (e Y)).range) : c.proj u ∈ (GradedLinearQuiver.homInclusion X Y).range

The projection sends morphisms e X ⟶ e Y to morphisms X ⟶ Y.

theorem TauCeti.LinearSpecialContraction.IsHomCompatible.map_incl_mem_composableWords {R : Type w} [CommRing R] {C : Type u₁} {D : Type u₂} [GradedLinearQuiver R C] [GradedLinearQuiver R D] {dC : Module.End R (GradedLinearQuiver.TotalHom R C)} {dD : Module.End R (GradedLinearQuiver.TotalHom R D)} {e : D ≃ C} {c : LinearSpecialContraction dC dD} (hc : IsHomCompatible e c) {X Y : D} {w : ReducedTensorWords R (GradedLinearQuiver.TotalHom R D)} (hw : w ∈ GradedLinearQuiver.composableWords R X Y) : (ReducedTensorWords.map R c.incl) w ∈ GradedLinearQuiver.composableWords R (e X) (e Y)

Applied letter by letter, the inclusion sends composable words from X to Y to composable words from e X to e Y.

theorem TauCeti.LinearSpecialContraction.IsHomCompatible.map_incl_mem_nonComposableWords {R : Type w} [CommRing R] {C : Type u₁} {D : Type u₂} [GradedLinearQuiver R C] [GradedLinearQuiver R D] {dC : Module.End R (GradedLinearQuiver.TotalHom R C)} {dD : Module.End R (GradedLinearQuiver.TotalHom R D)} {e : D ≃ C} {c : LinearSpecialContraction dC dD} (hc : IsHomCompatible e c) {w : ReducedTensorWords R (GradedLinearQuiver.TotalHom R D)} (hw : w ∈ GradedLinearQuiver.nonComposableWords R D) : (ReducedTensorWords.map R c.incl) w ∈ GradedLinearQuiver.nonComposableWords R C

Applied letter by letter, the inclusion sends non-composable words to non-composable words.

theorem TauCeti.LinearSpecialContraction.IsHomCompatible.map_proj_mem_composableWords {R : Type w} [CommRing R] {C : Type u₁} {D : Type u₂} [GradedLinearQuiver R C] [GradedLinearQuiver R D] {dC : Module.End R (GradedLinearQuiver.TotalHom R C)} {dD : Module.End R (GradedLinearQuiver.TotalHom R D)} {e : D ≃ C} {c : LinearSpecialContraction dC dD} (hc : IsHomCompatible e c) {U V : C} {w : ReducedTensorWords R (GradedLinearQuiver.TotalHom R C)} (hw : w ∈ GradedLinearQuiver.composableWords R U V) : (ReducedTensorWords.map R c.proj) w ∈ GradedLinearQuiver.composableWords R (e.symm U) (e.symm V)

Applied letter by letter, the projection sends composable words from U to V to composable words from e⁻¹ U to e⁻¹ V.

theorem TauCeti.LinearSpecialContraction.IsHomCompatible.map_proj_mem_nonComposableWords {R : Type w} [CommRing R] {C : Type u₁} {D : Type u₂} [GradedLinearQuiver R C] [GradedLinearQuiver R D] {dC : Module.End R (GradedLinearQuiver.TotalHom R C)} {dD : Module.End R (GradedLinearQuiver.TotalHom R D)} {e : D ≃ C} {c : LinearSpecialContraction dC dD} (hc : IsHomCompatible e c) {w : ReducedTensorWords R (GradedLinearQuiver.TotalHom R C)} (hw : w ∈ GradedLinearQuiver.nonComposableWords R C) : (ReducedTensorWords.map R c.proj) w ∈ GradedLinearQuiver.nonComposableWords R D

Applied letter by letter, the projection sends non-composable words to non-composable words.

The higher bar differential of an A∞ category

theorem TauCeti.AInfinityCategory.higherBarDifferential_mem_composableWords {R : Type w} [CommRing R] {C : Type u₁} [GradedLinearQuiver R C] (𝒞 : AInfinityCategory R C) {X Y : C} {w : ReducedTensorWords R (GradedLinearQuiver.TotalHom R C)} (hw : w ∈ GradedLinearQuiver.composableWords R X Y) : 𝒞.higherBarDifferential w ∈ GradedLinearQuiver.composableWords R X Y

The higher bar differential of an A∞ category preserves composable words from X to Y.

theorem TauCeti.AInfinityCategory.higherBarDifferential_mem_nonComposableWords {R : Type w} [CommRing R] {C : Type u₁} [GradedLinearQuiver R C] (𝒞 : AInfinityCategory R C) {w : ReducedTensorWords R (GradedLinearQuiver.TotalHom R C)} (hw : w ∈ GradedLinearQuiver.nonComposableWords R C) : 𝒞.higherBarDifferential w ∈ GradedLinearQuiver.nonComposableWords R C

The higher bar differential of an A∞ category preserves non-composable words.

The transferred A∞ category

theorem TauCeti.AInfinityCategory.isWordPathCompatible_taylor_transfer {R : Type w} [CommRing R] {C : Type u₁} {D : Type u₂} [GradedLinearQuiver R C] [GradedLinearQuiver R D] (𝒞 : AInfinityCategory R C) (e : D ≃ C) {dD : Module.End R (GradedLinearQuiver.TotalHom R D)} (c : LinearSpecialContraction 𝒞.differential dD) (hh : LinearMap.IsHomogeneous c.homotopy (𝒞.grading.piece ℤ) (𝒞.grading.piece ℤ) (-1)) (hincl : LinearMap.IsHomogeneous c.incl ((GradedLinearQuiver.totalGrading R D).piece ℤ) (𝒞.grading.piece ℤ) 0) (hproj : LinearMap.IsHomogeneous c.proj (𝒞.grading.piece ℤ) ((GradedLinearQuiver.totalGrading R D).piece ℤ) 0) (hc : LinearSpecialContraction.IsHomCompatible e c) : GradedLinearQuiver.IsWordPathCompatible id (𝒞.transfer c hh hincl hproj).taylor

The transferred operations are path-compatible. The Taylor map of the structure transferred from 𝒞 along a contraction compatible with the hom modules sends composable words of D from X to Y to morphisms X ⟶ Y, and non-composable words to zero.

noncomputable def TauCeti.AInfinityCategory.transfer {R : Type w} [CommRing R] {C : Type u₁} {D : Type u₂} [GradedLinearQuiver R C] [GradedLinearQuiver R D] (𝒞 : AInfinityCategory R C) (e : D ≃ C) {dD : Module.End R (GradedLinearQuiver.TotalHom R D)} (c : LinearSpecialContraction 𝒞.differential dD) (hh : LinearMap.IsHomogeneous c.homotopy (𝒞.grading.piece ℤ) (𝒞.grading.piece ℤ) (-1)) (hincl : LinearMap.IsHomogeneous c.incl ((GradedLinearQuiver.totalGrading R D).piece ℤ) (𝒞.grading.piece ℤ) 0) (hproj : LinearMap.IsHomogeneous c.proj (𝒞.grading.piece ℤ) ((GradedLinearQuiver.totalGrading R D).piece ℤ) 0) (hc : LinearSpecialContraction.IsHomCompatible e c) : AInfinityCategory R D

The transferred A∞ category: the A∞ structure transferred from the total algebra of morphisms of 𝒞 along a special contraction onto the total module of morphisms of D which is compatible with the hom modules along a bijection of objects e : D ≃ C. Its differential is the differential d_D of the retract (homInclusion_homDifferential_transfer), its composition is g ∘ f = p m₂(i g, i f) (homInclusion_comp_transfer), and its higher operations are those of the transferred A∞ algebra.

@[simp]

theorem TauCeti.AInfinityCategory.transfer_toAInfinityAlgebra {R : Type w} [CommRing R] {C : Type u₁} {D : Type u₂} [GradedLinearQuiver R C] [GradedLinearQuiver R D] (𝒞 : AInfinityCategory R C) (e : D ≃ C) {dD : Module.End R (GradedLinearQuiver.TotalHom R D)} (c : LinearSpecialContraction 𝒞.differential dD) (hh : LinearMap.IsHomogeneous c.homotopy (𝒞.grading.piece ℤ) (𝒞.grading.piece ℤ) (-1)) (hincl : LinearMap.IsHomogeneous c.incl ((GradedLinearQuiver.totalGrading R D).piece ℤ) (𝒞.grading.piece ℤ) 0) (hproj : LinearMap.IsHomogeneous c.proj (𝒞.grading.piece ℤ) ((GradedLinearQuiver.totalGrading R D).piece ℤ) 0) (hc : LinearSpecialContraction.IsHomCompatible e c) : (𝒞.transfer e c hh hincl hproj hc).toAInfinityAlgebra = 𝒞.transfer c hh hincl hproj

The total algebra of morphisms of the transferred category is the transferred A∞ algebra.

theorem TauCeti.AInfinityCategory.homInclusion_homDifferential_transfer {R : Type w} [CommRing R] {C : Type u₁} {D : Type u₂} [GradedLinearQuiver R C] [GradedLinearQuiver R D] (𝒞 : AInfinityCategory R C) (e : D ≃ C) {dD : Module.End R (GradedLinearQuiver.TotalHom R D)} (c : LinearSpecialContraction 𝒞.differential dD) (hh : LinearMap.IsHomogeneous c.homotopy (𝒞.grading.piece ℤ) (𝒞.grading.piece ℤ) (-1)) (hincl : LinearMap.IsHomogeneous c.incl ((GradedLinearQuiver.totalGrading R D).piece ℤ) (𝒞.grading.piece ℤ) 0) (hproj : LinearMap.IsHomogeneous c.proj (𝒞.grading.piece ℤ) ((GradedLinearQuiver.totalGrading R D).piece ℤ) 0) (hc : LinearSpecialContraction.IsHomCompatible e c) (X Y : D) (f : ↑(GradedLinearQuiver.homModule X Y)) : (GradedLinearQuiver.homInclusion X Y) (((𝒞.transfer e c hh hincl hproj hc).homDifferential X Y) f) = dD ((GradedLinearQuiver.homInclusion X Y) f)

The differential of the transferred category is the differential of the retract.

theorem TauCeti.AInfinityCategory.homInclusion_comp_transfer {R : Type w} [CommRing R] {C : Type u₁} {D : Type u₂} [GradedLinearQuiver R C] [GradedLinearQuiver R D] (𝒞 : AInfinityCategory R C) (e : D ≃ C) {dD : Module.End R (GradedLinearQuiver.TotalHom R D)} (c : LinearSpecialContraction 𝒞.differential dD) (hh : LinearMap.IsHomogeneous c.homotopy (𝒞.grading.piece ℤ) (𝒞.grading.piece ℤ) (-1)) (hincl : LinearMap.IsHomogeneous c.incl ((GradedLinearQuiver.totalGrading R D).piece ℤ) (𝒞.grading.piece ℤ) 0) (hproj : LinearMap.IsHomogeneous c.proj (𝒞.grading.piece ℤ) ((GradedLinearQuiver.totalGrading R D).piece ℤ) 0) (hc : LinearSpecialContraction.IsHomCompatible e c) (X Y Z : D) (g : ↑(GradedLinearQuiver.homModule Y Z)) (f : ↑(GradedLinearQuiver.homModule X Y)) : (GradedLinearQuiver.homInclusion X Z) ((((𝒞.transfer e c hh hincl hproj hc).comp X Y Z) g) f) = c.proj ((𝒞.m 2) ![c.incl ((GradedLinearQuiver.homInclusion Y Z) g), c.incl ((GradedLinearQuiver.homInclusion X Y) f)])

The composition of the transferred category is g ∘ f = p m₂(i g, i f).

The extending and projection morphisms

theorem TauCeti.AInfinityCategory.isWordPathCompatible_taylor_transferInclusion {R : Type w} [CommRing R] {C : Type u₁} {D : Type u₂} [GradedLinearQuiver R C] [GradedLinearQuiver R D] (𝒞 : AInfinityCategory R C) (e : D ≃ C) {dD : Module.End R (GradedLinearQuiver.TotalHom R D)} (c : LinearSpecialContraction 𝒞.differential dD) (hh : LinearMap.IsHomogeneous c.homotopy (𝒞.grading.piece ℤ) (𝒞.grading.piece ℤ) (-1)) (hincl : LinearMap.IsHomogeneous c.incl ((GradedLinearQuiver.totalGrading R D).piece ℤ) (𝒞.grading.piece ℤ) 0) (hproj : LinearMap.IsHomogeneous c.proj (𝒞.grading.piece ℤ) ((GradedLinearQuiver.totalGrading R D).piece ℤ) 0) (hc : LinearSpecialContraction.IsHomCompatible e c) : GradedLinearQuiver.IsWordPathCompatible (⇑e) (𝒞.transferInclusion c hh hincl hproj).taylor

The extending morphism of the transfer is path-compatible along e: its Taylor map sends composable words of D from X to Y to morphisms e X ⟶ e Y of C, and non-composable words to zero.

theorem TauCeti.AInfinityCategory.isWordPathCompatible_taylor_transferProjection {R : Type w} [CommRing R] {C : Type u₁} {D : Type u₂} [GradedLinearQuiver R C] [GradedLinearQuiver R D] (𝒞 : AInfinityCategory R C) (e : D ≃ C) {dD : Module.End R (GradedLinearQuiver.TotalHom R D)} (c : LinearSpecialContraction 𝒞.differential dD) (hh : LinearMap.IsHomogeneous c.homotopy (𝒞.grading.piece ℤ) (𝒞.grading.piece ℤ) (-1)) (hincl : LinearMap.IsHomogeneous c.incl ((GradedLinearQuiver.totalGrading R D).piece ℤ) (𝒞.grading.piece ℤ) 0) (hproj : LinearMap.IsHomogeneous c.proj (𝒞.grading.piece ℤ) ((GradedLinearQuiver.totalGrading R D).piece ℤ) 0) (hc : LinearSpecialContraction.IsHomCompatible e c) : GradedLinearQuiver.IsWordPathCompatible (⇑e.symm) (𝒞.transferProjection c hh hincl hproj).taylor

The projection morphism of the transfer is path-compatible along e⁻¹: its Taylor map sends composable words of C from U to V to morphisms e⁻¹ U ⟶ e⁻¹ V of D, and non-composable words to zero.