Naturality of homological transfer

A strict morphism of A∞ algebras, together with a degree-zero map of their retracts commuting with inclusion, projection and homotopy, induces a strict morphism of the transferred structures. The extending inclusion and projection morphisms form commuting squares with these maps. In particular the retract map preserves every transferred operation, not just the unary complex or the induced cohomology product.

The hypotheses express compatibility with the chosen contractions. No field or minimality assumption is required. This does not assert that arbitrary maps preserve arbitrary choices of transferred structures strictly.

References

• V. K. A. M. Gugenheim, L. A. Lambe, and J. D. Stasheff, Perturbation theory in differential homological algebra II, Illinois Journal of Mathematics 35 (1991), 357--373.
• B. Keller, Introduction to A-infinity algebras and modules, Section 3.3.

theorem TauCeti.AInfinityAlgebra.transferBarDifferential_naturality {R : Type uR} [CommRing R] {A : Type uA} {H : Type uH} {B : Type uB} {K : Type uK} [AddCommGroup A] [Module R A] [AddCommGroup H] [Module R H] [AddCommGroup B] [Module R B] [AddCommGroup K] [Module R K] {𝒜 : AInfinityAlgebra R A} {ℬ : AInfinityAlgebra R B} {GH : InternalGrading R H} {GK : InternalGrading R K} {dH : Module.End R H} {dK : Module.End R K} (c : LinearSpecialContraction 𝒜.differential dH) (c' : LinearSpecialContraction ℬ.differential dK) (hh : LinearMap.IsHomogeneous c.homotopy 𝒜.grading.piece 𝒜.grading.piece (-1)) (hi : LinearMap.IsHomogeneous c.incl GH.piece 𝒜.grading.piece 0) (hp : LinearMap.IsHomogeneous c.proj 𝒜.grading.piece GH.piece 0) (hh' : LinearMap.IsHomogeneous c'.homotopy ℬ.grading.piece ℬ.grading.piece (-1)) (hi' : LinearMap.IsHomogeneous c'.incl GK.piece ℬ.grading.piece 0) (hp' : LinearMap.IsHomogeneous c'.proj ℬ.grading.piece GK.piece 0) (f : AInfinityStrictHom 𝒜 ℬ) (g : H →ₗ[R] K) (hι : f.toLinearMap ∘ₗ c.incl = c'.incl ∘ₗ g) (hπ : g ∘ₗ c.proj = c'.proj ∘ₗ f.toLinearMap) (hη : f.toLinearMap ∘ₗ c.homotopy = c'.homotopy ∘ₗ f.toLinearMap) : ReducedTensorWords.map R g ∘ₗ 𝒜.transferBarDifferential c hh hi hp = ℬ.transferBarDifferential c' hh' hi' hp' ∘ₗ ReducedTensorWords.map R g

The letterwise retract map intertwines the transferred bar differentials.

noncomputable def TauCeti.AInfinityAlgebra.transferStrictHom {R : Type uR} [CommRing R] {A : Type uA} {H : Type uH} {B : Type uB} {K : Type uK} [AddCommGroup A] [Module R A] [AddCommGroup H] [Module R H] [AddCommGroup B] [Module R B] [AddCommGroup K] [Module R K] {𝒜 : AInfinityAlgebra R A} {ℬ : AInfinityAlgebra R B} {GH : InternalGrading R H} {GK : InternalGrading R K} {dH : Module.End R H} {dK : Module.End R K} (c : LinearSpecialContraction 𝒜.differential dH) (c' : LinearSpecialContraction ℬ.differential dK) (hh : LinearMap.IsHomogeneous c.homotopy 𝒜.grading.piece 𝒜.grading.piece (-1)) (hi : LinearMap.IsHomogeneous c.incl GH.piece 𝒜.grading.piece 0) (hp : LinearMap.IsHomogeneous c.proj 𝒜.grading.piece GH.piece 0) (hh' : LinearMap.IsHomogeneous c'.homotopy ℬ.grading.piece ℬ.grading.piece (-1)) (hi' : LinearMap.IsHomogeneous c'.incl GK.piece ℬ.grading.piece 0) (hp' : LinearMap.IsHomogeneous c'.proj ℬ.grading.piece GK.piece 0) (f : AInfinityStrictHom 𝒜 ℬ) (g : H →ₗ[R] K) (hι : f.toLinearMap ∘ₗ c.incl = c'.incl ∘ₗ g) (hπ : g ∘ₗ c.proj = c'.proj ∘ₗ f.toLinearMap) (hη : f.toLinearMap ∘ₗ c.homotopy = c'.homotopy ∘ₗ f.toLinearMap) : AInfinityStrictHom (𝒜.transfer c hh hi hp) (ℬ.transfer c' hh' hi' hp')

The strict morphism between transferred structures induced by a strict morphism and compatible contractions. Its underlying linear map is the retract map.

Equations

• TauCeti.AInfinityAlgebra.transferStrictHom c c' hh hi hp hh' hi' hp' f g hι hπ hη = ⋯.toStrictHom

@[simp]

theorem TauCeti.AInfinityAlgebra.transferStrictHom_toLinearMap {R : Type uR} [CommRing R] {A : Type uA} {H : Type uH} {B : Type uB} {K : Type uK} [AddCommGroup A] [Module R A] [AddCommGroup H] [Module R H] [AddCommGroup B] [Module R B] [AddCommGroup K] [Module R K] {𝒜 : AInfinityAlgebra R A} {ℬ : AInfinityAlgebra R B} {GH : InternalGrading R H} {GK : InternalGrading R K} {dH : Module.End R H} {dK : Module.End R K} (c : LinearSpecialContraction 𝒜.differential dH) (c' : LinearSpecialContraction ℬ.differential dK) (hh : LinearMap.IsHomogeneous c.homotopy 𝒜.grading.piece 𝒜.grading.piece (-1)) (hi : LinearMap.IsHomogeneous c.incl GH.piece 𝒜.grading.piece 0) (hp : LinearMap.IsHomogeneous c.proj 𝒜.grading.piece GH.piece 0) (hh' : LinearMap.IsHomogeneous c'.homotopy ℬ.grading.piece ℬ.grading.piece (-1)) (hi' : LinearMap.IsHomogeneous c'.incl GK.piece ℬ.grading.piece 0) (hp' : LinearMap.IsHomogeneous c'.proj ℬ.grading.piece GK.piece 0) (f : AInfinityStrictHom 𝒜 ℬ) (g : H →ₗ[R] K) (hι : f.toLinearMap ∘ₗ c.incl = c'.incl ∘ₗ g) (hπ : g ∘ₗ c.proj = c'.proj ∘ₗ f.toLinearMap) (hη : f.toLinearMap ∘ₗ c.homotopy = c'.homotopy ∘ₗ f.toLinearMap) : (transferStrictHom c c' hh hi hp hh' hi' hp' f g hι hπ hη).toLinearMap = g

The underlying linear map of the induced strict morphism is the retract map.

@[simp]

theorem TauCeti.AInfinityAlgebra.coe_transferStrictHom {R : Type uR} [CommRing R] {A : Type uA} {H : Type uH} {B : Type uB} {K : Type uK} [AddCommGroup A] [Module R A] [AddCommGroup H] [Module R H] [AddCommGroup B] [Module R B] [AddCommGroup K] [Module R K] {𝒜 : AInfinityAlgebra R A} {ℬ : AInfinityAlgebra R B} {GH : InternalGrading R H} {GK : InternalGrading R K} {dH : Module.End R H} {dK : Module.End R K} (c : LinearSpecialContraction 𝒜.differential dH) (c' : LinearSpecialContraction ℬ.differential dK) (hh : LinearMap.IsHomogeneous c.homotopy 𝒜.grading.piece 𝒜.grading.piece (-1)) (hi : LinearMap.IsHomogeneous c.incl GH.piece 𝒜.grading.piece 0) (hp : LinearMap.IsHomogeneous c.proj 𝒜.grading.piece GH.piece 0) (hh' : LinearMap.IsHomogeneous c'.homotopy ℬ.grading.piece ℬ.grading.piece (-1)) (hi' : LinearMap.IsHomogeneous c'.incl GK.piece ℬ.grading.piece 0) (hp' : LinearMap.IsHomogeneous c'.proj ℬ.grading.piece GK.piece 0) (f : AInfinityStrictHom 𝒜 ℬ) (g : H →ₗ[R] K) (hι : f.toLinearMap ∘ₗ c.incl = c'.incl ∘ₗ g) (hπ : g ∘ₗ c.proj = c'.proj ∘ₗ f.toLinearMap) (hη : f.toLinearMap ∘ₗ c.homotopy = c'.homotopy ∘ₗ f.toLinearMap) : ⇑(transferStrictHom c c' hh hi hp hh' hi' hp' f g hι hπ hη) = ⇑g

The induced strict morphism acts by the retract map.

@[simp]

theorem TauCeti.AInfinityAlgebra.barMap_transferStrictHom {R : Type uR} [CommRing R] {A : Type uA} {H : Type uH} {B : Type uB} {K : Type uK} [AddCommGroup A] [Module R A] [AddCommGroup H] [Module R H] [AddCommGroup B] [Module R B] [AddCommGroup K] [Module R K] {𝒜 : AInfinityAlgebra R A} {ℬ : AInfinityAlgebra R B} {GH : InternalGrading R H} {GK : InternalGrading R K} {dH : Module.End R H} {dK : Module.End R K} (c : LinearSpecialContraction 𝒜.differential dH) (c' : LinearSpecialContraction ℬ.differential dK) (hh : LinearMap.IsHomogeneous c.homotopy 𝒜.grading.piece 𝒜.grading.piece (-1)) (hi : LinearMap.IsHomogeneous c.incl GH.piece 𝒜.grading.piece 0) (hp : LinearMap.IsHomogeneous c.proj 𝒜.grading.piece GH.piece 0) (hh' : LinearMap.IsHomogeneous c'.homotopy ℬ.grading.piece ℬ.grading.piece (-1)) (hi' : LinearMap.IsHomogeneous c'.incl GK.piece ℬ.grading.piece 0) (hp' : LinearMap.IsHomogeneous c'.proj ℬ.grading.piece GK.piece 0) (f : AInfinityStrictHom 𝒜 ℬ) (g : H →ₗ[R] K) (hι : f.toLinearMap ∘ₗ c.incl = c'.incl ∘ₗ g) (hπ : g ∘ₗ c.proj = c'.proj ∘ₗ f.toLinearMap) (hη : f.toLinearMap ∘ₗ c.homotopy = c'.homotopy ∘ₗ f.toLinearMap) : (transferStrictHom c c' hh hi hp hh' hi' hp' f g hι hπ hη).barMap = ReducedTensorWords.map R g

The induced strict morphism acts letterwise on the bar construction.

theorem TauCeti.AInfinityAlgebra.map_m_transfer {R : Type uR} [CommRing R] {A : Type uA} {H : Type uH} {B : Type uB} {K : Type uK} [AddCommGroup A] [Module R A] [AddCommGroup H] [Module R H] [AddCommGroup B] [Module R B] [AddCommGroup K] [Module R K] {𝒜 : AInfinityAlgebra R A} {ℬ : AInfinityAlgebra R B} {GH : InternalGrading R H} {GK : InternalGrading R K} {dH : Module.End R H} {dK : Module.End R K} (c : LinearSpecialContraction 𝒜.differential dH) (c' : LinearSpecialContraction ℬ.differential dK) (hh : LinearMap.IsHomogeneous c.homotopy 𝒜.grading.piece 𝒜.grading.piece (-1)) (hi : LinearMap.IsHomogeneous c.incl GH.piece 𝒜.grading.piece 0) (hp : LinearMap.IsHomogeneous c.proj 𝒜.grading.piece GH.piece 0) (hh' : LinearMap.IsHomogeneous c'.homotopy ℬ.grading.piece ℬ.grading.piece (-1)) (hi' : LinearMap.IsHomogeneous c'.incl GK.piece ℬ.grading.piece 0) (hp' : LinearMap.IsHomogeneous c'.proj ℬ.grading.piece GK.piece 0) (f : AInfinityStrictHom 𝒜 ℬ) (g : H →ₗ[R] K) (hι : f.toLinearMap ∘ₗ c.incl = c'.incl ∘ₗ g) (hπ : g ∘ₗ c.proj = c'.proj ∘ₗ f.toLinearMap) (hη : f.toLinearMap ∘ₗ c.homotopy = c'.homotopy ∘ₗ f.toLinearMap) (n : ℕ) (x : Fin n → H) : g (((𝒜.transfer c hh hi hp).m n) x) = ((ℬ.transfer c' hh' hi' hp').m n) fun (i : Fin n) => g (x i)

The retract map preserves all transferred operations.

theorem TauCeti.AInfinityAlgebra.transferInclusion_naturality {R : Type uR} [CommRing R] {A : Type uA} {H : Type uH} {B : Type uB} {K : Type uK} [AddCommGroup A] [Module R A] [AddCommGroup H] [Module R H] [AddCommGroup B] [Module R B] [AddCommGroup K] [Module R K] {𝒜 : AInfinityAlgebra R A} {ℬ : AInfinityAlgebra R B} {GH : InternalGrading R H} {GK : InternalGrading R K} {dH : Module.End R H} {dK : Module.End R K} (c : LinearSpecialContraction 𝒜.differential dH) (c' : LinearSpecialContraction ℬ.differential dK) (hh : LinearMap.IsHomogeneous c.homotopy 𝒜.grading.piece 𝒜.grading.piece (-1)) (hi : LinearMap.IsHomogeneous c.incl GH.piece 𝒜.grading.piece 0) (hp : LinearMap.IsHomogeneous c.proj 𝒜.grading.piece GH.piece 0) (hh' : LinearMap.IsHomogeneous c'.homotopy ℬ.grading.piece ℬ.grading.piece (-1)) (hi' : LinearMap.IsHomogeneous c'.incl GK.piece ℬ.grading.piece 0) (hp' : LinearMap.IsHomogeneous c'.proj ℬ.grading.piece GK.piece 0) (f : AInfinityStrictHom 𝒜 ℬ) (g : H →ₗ[R] K) (hι : f.toLinearMap ∘ₗ c.incl = c'.incl ∘ₗ g) (hπ : g ∘ₗ c.proj = c'.proj ∘ₗ f.toLinearMap) (hη : f.toLinearMap ∘ₗ c.homotopy = c'.homotopy ∘ₗ f.toLinearMap) : f.toAInfinityHom.comp (𝒜.transferInclusion c hh hi hp) = (ℬ.transferInclusion c' hh' hi' hp').comp (transferStrictHom c c' hh hi hp hh' hi' hp' f g hι hπ hη).toAInfinityHom

The extending inclusion is natural under maps compatible with the contractions.

theorem TauCeti.AInfinityAlgebra.transferProjection_naturality {R : Type uR} [CommRing R] {A : Type uA} {H : Type uH} {B : Type uB} {K : Type uK} [AddCommGroup A] [Module R A] [AddCommGroup H] [Module R H] [AddCommGroup B] [Module R B] [AddCommGroup K] [Module R K] {𝒜 : AInfinityAlgebra R A} {ℬ : AInfinityAlgebra R B} {GH : InternalGrading R H} {GK : InternalGrading R K} {dH : Module.End R H} {dK : Module.End R K} (c : LinearSpecialContraction 𝒜.differential dH) (c' : LinearSpecialContraction ℬ.differential dK) (hh : LinearMap.IsHomogeneous c.homotopy 𝒜.grading.piece 𝒜.grading.piece (-1)) (hi : LinearMap.IsHomogeneous c.incl GH.piece 𝒜.grading.piece 0) (hp : LinearMap.IsHomogeneous c.proj 𝒜.grading.piece GH.piece 0) (hh' : LinearMap.IsHomogeneous c'.homotopy ℬ.grading.piece ℬ.grading.piece (-1)) (hi' : LinearMap.IsHomogeneous c'.incl GK.piece ℬ.grading.piece 0) (hp' : LinearMap.IsHomogeneous c'.proj ℬ.grading.piece GK.piece 0) (f : AInfinityStrictHom 𝒜 ℬ) (g : H →ₗ[R] K) (hι : f.toLinearMap ∘ₗ c.incl = c'.incl ∘ₗ g) (hπ : g ∘ₗ c.proj = c'.proj ∘ₗ f.toLinearMap) (hη : f.toLinearMap ∘ₗ c.homotopy = c'.homotopy ∘ₗ f.toLinearMap) : (transferStrictHom c c' hh hi hp hh' hi' hp' f g hι hπ hη).toAInfinityHom.comp (𝒜.transferProjection c hh hi hp) = (ℬ.transferProjection c' hh' hi' hp').comp f.toAInfinityHom

The projection onto the transferred structure is natural under compatible maps.