Homotopies of morphisms of right A-infinity modules

Let f g : M ⟶ N be morphisms of right A∞ modules over a fixed algebra. A homotopy from f to g is a degree--1 morphism H of their cofree bar comodules satisfying

F - G = b_N H + H b_M.

The comodule morphism H is determined by its suspended Taylor map, obtained by applying the coalgebra counit. The homotopy equation can likewise be checked after applying the counit. Its component with no algebra inputs is an ordinary chain homotopy between the linear parts of f and g; consequently homotopic module morphisms induce the same map on cohomology and are quasi-isomorphisms together.

Homotopies are reflexive, symmetric, and transitive, and they are preserved by composition with module morphisms on either side.

Main definitions

• TauCeti.AInfinityRightModuleHom.Homotopy: a homotopy of right A∞ module morphisms.
• TauCeti.AInfinityRightModuleHom.Homotopy.taylor: its suspended Taylor map.
• TauCeti.AInfinityRightModuleHom.Homotopy.linearHomotopy: its unary component.
• TauCeti.AInfinityRightModuleHom.Homotopy.ofBarHomotopy: construction from a homogeneous comodule morphism satisfying the suspended component equation.

References

• B. Keller, Introduction to A-infinity algebras and modules, Section 4.
• K. Lefèvre-Hasegawa, Sur les A-infini catégories, thèse de doctorat, Université Paris 7 (2003), Chapter 1.

structure TauCeti.AInfinityRightModuleHom.Homotopy {R : Type uR} {A : Type uA} [CommRing R] [AddCommGroup A] [Module R A] {AA : AInfinityAlgebra R A} {M : Type uM} {N : Type uN} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {MM : AInfinityRightModule AA M} {NN : AInfinityRightModule AA N} (f g : AInfinityRightModuleHom MM NN) : Type (max (max (max uA uM) uN) uR)

A homotopy from f to g is a degree--1 morphism of their cofree bar comodules whose commutator with the module bar differentials is F - G.

• barHomotopy : Comodule.Hom R (TensorWords R A) (TensorProduct R M (TensorWords R A)) (TensorProduct R N (TensorWords R A))

  The degree--1 morphism of cofree bar comodules.

• isHomogeneous_barHomotopy : LinearMap.IsHomogeneous self.barHomotopy.toLinearMap (AInfinityRightModule.barGrading AA MM.grading).piece (AInfinityRightModule.barGrading AA NN.grading).piece (-1)

  The bar homotopy lowers the total suspended degree by one.

• barMap_sub_barMap : f.barMap - g.barMap = NN.barDifferential ∘ₗ self.barHomotopy.toLinearMap + self.barHomotopy.toLinearMap ∘ₗ MM.barDifferential

  The homotopy equation F - G = b_N H + H b_M.

@[reducible, inline]

abbrev TauCeti.AInfinityRightModuleHom.Homotopy.barMap {R : Type uR} {A : Type uA} [CommRing R] [AddCommGroup A] [Module R A] {AA : AInfinityAlgebra R A} {M : Type uM} {N : Type uN} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {MM : AInfinityRightModule AA M} {NN : AInfinityRightModule AA N} {f g : AInfinityRightModuleHom MM NN} (h : f.Homotopy g) : TensorProduct R M (TensorWords R A) →ₗ[R] TensorProduct R N (TensorWords R A)

The underlying linear map of the bar-comodule homotopy.

Equations

• h.barMap = h.barHomotopy.toLinearMap

theorem TauCeti.AInfinityRightModuleHom.Homotopy.barMap_sub_barMap_apply {R : Type uR} {A : Type uA} [CommRing R] [AddCommGroup A] [Module R A] {AA : AInfinityAlgebra R A} {M : Type uM} {N : Type uN} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {MM : AInfinityRightModule AA M} {NN : AInfinityRightModule AA N} {f g : AInfinityRightModuleHom MM NN} (h : f.Homotopy g) (z : TensorProduct R M (TensorWords R A)) : f.barMap z - g.barMap z = NN.barDifferential (h.barMap z) + h.barMap (MM.barDifferential z)

The homotopy equation, applied to one bar-comodule element.

noncomputable def TauCeti.AInfinityRightModuleHom.Homotopy.taylor {R : Type uR} {A : Type uA} [CommRing R] [AddCommGroup A] [Module R A] {AA : AInfinityAlgebra R A} {M : Type uM} {N : Type uN} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {MM : AInfinityRightModule AA M} {NN : AInfinityRightModule AA N} {f g : AInfinityRightModuleHom MM NN} (h : f.Homotopy g) : TensorProduct R M (TensorWords R A) →ₗ[R] N

The suspended Taylor map of a module homotopy, obtained by applying the coalgebra counit.

Equations

• h.taylor = ↑(TensorProduct.rid R N) ∘ₗ LinearMap.lTensor N CoalgebraStruct.counit ∘ₗ h.barMap

theorem TauCeti.AInfinityRightModuleHom.Homotopy.taylor_def {R : Type uR} {A : Type uA} [CommRing R] [AddCommGroup A] [Module R A] {AA : AInfinityAlgebra R A} {M : Type uM} {N : Type uN} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {MM : AInfinityRightModule AA M} {NN : AInfinityRightModule AA N} {f g : AInfinityRightModuleHom MM NN} (h : f.Homotopy g) : h.taylor = ↑(TensorProduct.rid R N) ∘ₗ LinearMap.lTensor N CoalgebraStruct.counit ∘ₗ h.barMap

theorem TauCeti.AInfinityRightModuleHom.Homotopy.isHomogeneous_taylor {R : Type uR} {A : Type uA} [CommRing R] [AddCommGroup A] [Module R A] {AA : AInfinityAlgebra R A} {M : Type uM} {N : Type uN} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {MM : AInfinityRightModule AA M} {NN : AInfinityRightModule AA N} {f g : AInfinityRightModuleHom MM NN} (h : f.Homotopy g) : LinearMap.IsHomogeneous h.taylor (AInfinityRightModule.barGrading AA MM.grading).piece (NN.grading.shift 1).piece (-1)

The Taylor map of a homotopy lowers suspended degree by one.

theorem TauCeti.AInfinityRightModuleHom.Homotopy.barMap_eq_cofreeLift {R : Type uR} {A : Type uA} [CommRing R] [AddCommGroup A] [Module R A] {AA : AInfinityAlgebra R A} {M : Type uM} {N : Type uN} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {MM : AInfinityRightModule AA M} {NN : AInfinityRightModule AA N} {f g : AInfinityRightModuleHom MM NN} (h : f.Homotopy g) : h.barMap = (Comodule.Hom.cofreeLift h.taylor).toLinearMap

The bar homotopy is the cofree lift of its Taylor map.

theorem TauCeti.AInfinityRightModuleHom.Homotopy.ext {R : Type uR} {A : Type uA} [CommRing R] [AddCommGroup A] [Module R A] {AA : AInfinityAlgebra R A} {M : Type uM} {N : Type uN} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {MM : AInfinityRightModule AA M} {NN : AInfinityRightModule AA N} {f g : AInfinityRightModuleHom MM NN} {h h' : f.Homotopy g} (e : h.taylor = h'.taylor) : h = h'

Homotopies between fixed morphisms are determined by their Taylor maps.

theorem TauCeti.AInfinityRightModuleHom.Homotopy.ext_iff {R : Type uR} {A : Type uA} [CommRing R] [AddCommGroup A] [Module R A] {AA : AInfinityAlgebra R A} {M : Type uM} {N : Type uN} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {MM : AInfinityRightModule AA M} {NN : AInfinityRightModule AA N} {f g : AInfinityRightModuleHom MM NN} {h h' : f.Homotopy g} : h = h' ↔ h.taylor = h'.taylor

theorem TauCeti.AInfinityRightModuleHom.Homotopy.barMap_sub_barMap_iff {R : Type uR} {A : Type uA} [CommRing R] [AddCommGroup A] [Module R A] {AA : AInfinityAlgebra R A} {M : Type uM} {N : Type uN} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {MM : AInfinityRightModule AA M} {NN : AInfinityRightModule AA N} {f g : AInfinityRightModuleHom MM NN} (H : Comodule.Hom R (TensorWords R A) (TensorProduct R M (TensorWords R A)) (TensorProduct R N (TensorWords R A))) (hH : LinearMap.IsHomogeneous H.toLinearMap (AInfinityRightModule.barGrading AA MM.grading).piece (AInfinityRightModule.barGrading AA NN.grading).piece (-1)) : f.barMap - g.barMap = NN.barDifferential ∘ₗ H.toLinearMap + H.toLinearMap ∘ₗ MM.barDifferential ↔ f.taylor - g.taylor = NN.taylor ∘ₗ H.toLinearMap + (↑(TensorProduct.rid R N) ∘ₗ LinearMap.lTensor N CoalgebraStruct.counit ∘ₗ H.toLinearMap) ∘ₗ MM.barDifferential

For a degree--1 comodule morphism, the full homotopy equation is equivalent to its projection to the cogenerator.

theorem TauCeti.AInfinityRightModuleHom.Homotopy.taylor_sub_taylor {R : Type uR} {A : Type uA} [CommRing R] [AddCommGroup A] [Module R A] {AA : AInfinityAlgebra R A} {M : Type uM} {N : Type uN} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {MM : AInfinityRightModule AA M} {NN : AInfinityRightModule AA N} {f g : AInfinityRightModuleHom MM NN} (h : f.Homotopy g) : f.taylor - g.taylor = NN.taylor ∘ₗ h.barMap + h.taylor ∘ₗ MM.barDifferential

The suspended component equation of a module homotopy.

noncomputable def TauCeti.AInfinityRightModuleHom.Homotopy.ofBarHomotopy {R : Type uR} {A : Type uA} [CommRing R] [AddCommGroup A] [Module R A] {AA : AInfinityAlgebra R A} {M : Type uM} {N : Type uN} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {MM : AInfinityRightModule AA M} {NN : AInfinityRightModule AA N} {f g : AInfinityRightModuleHom MM NN} (H : Comodule.Hom R (TensorWords R A) (TensorProduct R M (TensorWords R A)) (TensorProduct R N (TensorWords R A))) (hH : LinearMap.IsHomogeneous H.toLinearMap (AInfinityRightModule.barGrading AA MM.grading).piece (AInfinityRightModule.barGrading AA NN.grading).piece (-1)) (e : f.taylor - g.taylor = NN.taylor ∘ₗ H.toLinearMap + (↑(TensorProduct.rid R N) ∘ₗ LinearMap.lTensor N CoalgebraStruct.counit ∘ₗ H.toLinearMap) ∘ₗ MM.barDifferential) : f.Homotopy g

Construct a homotopy from a degree--1 comodule morphism satisfying the suspended component equation.

Equations

• TauCeti.AInfinityRightModuleHom.Homotopy.ofBarHomotopy H hH e = { barHomotopy := H, isHomogeneous_barHomotopy := hH, barMap_sub_barMap := ⋯ }

@[simp]

theorem TauCeti.AInfinityRightModuleHom.Homotopy.barHomotopy_ofBarHomotopy {R : Type uR} {A : Type uA} [CommRing R] [AddCommGroup A] [Module R A] {AA : AInfinityAlgebra R A} {M : Type uM} {N : Type uN} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {MM : AInfinityRightModule AA M} {NN : AInfinityRightModule AA N} {f g : AInfinityRightModuleHom MM NN} (H : Comodule.Hom R (TensorWords R A) (TensorProduct R M (TensorWords R A)) (TensorProduct R N (TensorWords R A))) (hH : LinearMap.IsHomogeneous H.toLinearMap (AInfinityRightModule.barGrading AA MM.grading).piece (AInfinityRightModule.barGrading AA NN.grading).piece (-1)) (e : f.taylor - g.taylor = NN.taylor ∘ₗ H.toLinearMap + (↑(TensorProduct.rid R N) ∘ₗ LinearMap.lTensor N CoalgebraStruct.counit ∘ₗ H.toLinearMap) ∘ₗ MM.barDifferential) : (ofBarHomotopy H hH e).barHomotopy = H

@[simp]

theorem TauCeti.AInfinityRightModuleHom.Homotopy.taylor_ofBarHomotopy {R : Type uR} {A : Type uA} [CommRing R] [AddCommGroup A] [Module R A] {AA : AInfinityAlgebra R A} {M : Type uM} {N : Type uN} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {MM : AInfinityRightModule AA M} {NN : AInfinityRightModule AA N} {f g : AInfinityRightModuleHom MM NN} (H : Comodule.Hom R (TensorWords R A) (TensorProduct R M (TensorWords R A)) (TensorProduct R N (TensorWords R A))) (hH : LinearMap.IsHomogeneous H.toLinearMap (AInfinityRightModule.barGrading AA MM.grading).piece (AInfinityRightModule.barGrading AA NN.grading).piece (-1)) (e : f.taylor - g.taylor = NN.taylor ∘ₗ H.toLinearMap + (↑(TensorProduct.rid R N) ∘ₗ LinearMap.lTensor N CoalgebraStruct.counit ∘ₗ H.toLinearMap) ∘ₗ MM.barDifferential) : (ofBarHomotopy H hH e).taylor = ↑(TensorProduct.rid R N) ∘ₗ LinearMap.lTensor N CoalgebraStruct.counit ∘ₗ H.toLinearMap

The Taylor map of a homotopy constructed from a bar-comodule morphism is its counit component.

The unary component

noncomputable def TauCeti.AInfinityRightModuleHom.Homotopy.linearHomotopy {R : Type uR} {A : Type uA} [CommRing R] [AddCommGroup A] [Module R A] {AA : AInfinityAlgebra R A} {M : Type uM} {N : Type uN} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {MM : AInfinityRightModule AA M} {NN : AInfinityRightModule AA N} {f g : AInfinityRightModuleHom MM NN} (h : f.Homotopy g) : M →ₗ[R] N

The unary component of a module homotopy, evaluated on the empty algebra word.

Equations

• h.linearHomotopy = h.taylor ∘ₗ (TensorProduct.mk R M (TauCeti.TensorWords R A)).flip 1

@[simp]

theorem TauCeti.AInfinityRightModuleHom.Homotopy.linearHomotopy_apply {R : Type uR} {A : Type uA} [CommRing R] [AddCommGroup A] [Module R A] {AA : AInfinityAlgebra R A} {M : Type uM} {N : Type uN} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {MM : AInfinityRightModule AA M} {NN : AInfinityRightModule AA N} {f g : AInfinityRightModuleHom MM NN} (h : f.Homotopy g) (x : M) : h.linearHomotopy x = h.taylor (x ⊗ₜ[R] 1)

@[simp]

theorem TauCeti.AInfinityRightModuleHom.Homotopy.barMap_tmul_one {R : Type uR} {A : Type uA} [CommRing R] [AddCommGroup A] [Module R A] {AA : AInfinityAlgebra R A} {M : Type uM} {N : Type uN} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {MM : AInfinityRightModule AA M} {NN : AInfinityRightModule AA N} {f g : AInfinityRightModuleHom MM NN} (h : f.Homotopy g) (x : M) : h.barMap (x ⊗ₜ[R] 1) = h.linearHomotopy x ⊗ₜ[R] 1

A bar homotopy sends an empty algebra word to the empty word multiplied by its unary component.

theorem TauCeti.AInfinityRightModuleHom.Homotopy.linearHomotopy_mem {R : Type uR} {A : Type uA} [CommRing R] [AddCommGroup A] [Module R A] {AA : AInfinityAlgebra R A} {M : Type uM} {N : Type uN} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {MM : AInfinityRightModule AA M} {NN : AInfinityRightModule AA N} {f g : AInfinityRightModuleHom MM NN} (h : f.Homotopy g) {x : M} {p : ℤ} (hx : x ∈ MM.grading.piece p) : h.linearHomotopy x ∈ NN.grading.piece (p - 1)

The unary component of a module homotopy lowers the unsuspended degree by one.

theorem TauCeti.AInfinityRightModuleHom.Homotopy.linearPart_sub_linearPart {R : Type uR} {A : Type uA} [CommRing R] [AddCommGroup A] [Module R A] {AA : AInfinityAlgebra R A} {M : Type uM} {N : Type uN} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {MM : AInfinityRightModule AA M} {NN : AInfinityRightModule AA N} {f g : AInfinityRightModuleHom MM NN} (h : f.Homotopy g) (x : M) : f.linearPart x - g.linearPart x = NN.differential (h.linearHomotopy x) + h.linearHomotopy (MM.differential x)

The unary component is a chain homotopy between the linear parts.

Cohomology

theorem TauCeti.AInfinityRightModuleHom.Homotopy.cohomologyMap_eq {R : Type uR} {A : Type uA} [CommRing R] [AddCommGroup A] [Module R A] {AA : AInfinityAlgebra R A} {M : Type uM} {N : Type uN} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {MM : AInfinityRightModule AA M} {NN : AInfinityRightModule AA N} {f g : AInfinityRightModuleHom MM NN} (h : f.Homotopy g) : f.cohomologyMap = g.cohomologyMap

Homotopic module morphisms induce the same map on unary cohomology.

theorem TauCeti.AInfinityRightModuleHom.Homotopy.isQuasiIso_iff {R : Type uR} {A : Type uA} [CommRing R] [AddCommGroup A] [Module R A] {AA : AInfinityAlgebra R A} {M : Type uM} {N : Type uN} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {MM : AInfinityRightModule AA M} {NN : AInfinityRightModule AA N} {f g : AInfinityRightModuleHom MM NN} (h : f.Homotopy g) : f.IsQuasiIso ↔ g.IsQuasiIso

Homotopic module morphisms are quasi-isomorphisms together.

Equivalence and composition laws

noncomputable def TauCeti.AInfinityRightModuleHom.Homotopy.refl {R : Type uR} {A : Type uA} [CommRing R] [AddCommGroup A] [Module R A] {AA : AInfinityAlgebra R A} {M : Type uM} {N : Type uN} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {MM : AInfinityRightModule AA M} {NN : AInfinityRightModule AA N} (f : AInfinityRightModuleHom MM NN) : f.Homotopy f

The zero homotopy from a module morphism to itself.

Equations

• TauCeti.AInfinityRightModuleHom.Homotopy.refl f = { barHomotopy := 0, isHomogeneous_barHomotopy := ⋯, barMap_sub_barMap := ⋯ }

@[simp]

theorem TauCeti.AInfinityRightModuleHom.Homotopy.barMap_refl {R : Type uR} {A : Type uA} [CommRing R] [AddCommGroup A] [Module R A] {AA : AInfinityAlgebra R A} {M : Type uM} {N : Type uN} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {MM : AInfinityRightModule AA M} {NN : AInfinityRightModule AA N} (f : AInfinityRightModuleHom MM NN) : (refl f).barMap = 0

@[simp]

theorem TauCeti.AInfinityRightModuleHom.Homotopy.taylor_refl {R : Type uR} {A : Type uA} [CommRing R] [AddCommGroup A] [Module R A] {AA : AInfinityAlgebra R A} {M : Type uM} {N : Type uN} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {MM : AInfinityRightModule AA M} {NN : AInfinityRightModule AA N} (f : AInfinityRightModuleHom MM NN) : (refl f).taylor = 0

noncomputable def TauCeti.AInfinityRightModuleHom.Homotopy.symm {R : Type uR} {A : Type uA} [CommRing R] [AddCommGroup A] [Module R A] {AA : AInfinityAlgebra R A} {M : Type uM} {N : Type uN} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {MM : AInfinityRightModule AA M} {NN : AInfinityRightModule AA N} {f g : AInfinityRightModuleHom MM NN} (h : f.Homotopy g) : g.Homotopy f

Reverse a module homotopy.

Equations

• h.symm = { barHomotopy := -1 • h.barHomotopy, isHomogeneous_barHomotopy := ⋯, barMap_sub_barMap := ⋯ }

@[simp]

theorem TauCeti.AInfinityRightModuleHom.Homotopy.barMap_symm {R : Type uR} {A : Type uA} [CommRing R] [AddCommGroup A] [Module R A] {AA : AInfinityAlgebra R A} {M : Type uM} {N : Type uN} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {MM : AInfinityRightModule AA M} {NN : AInfinityRightModule AA N} {f g : AInfinityRightModuleHom MM NN} (h : f.Homotopy g) : h.symm.barMap = -h.barMap

noncomputable def TauCeti.AInfinityRightModuleHom.Homotopy.trans {R : Type uR} {A : Type uA} [CommRing R] [AddCommGroup A] [Module R A] {AA : AInfinityAlgebra R A} {M : Type uM} {N : Type uN} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {MM : AInfinityRightModule AA M} {NN : AInfinityRightModule AA N} {f g k : AInfinityRightModuleHom MM NN} (h : f.Homotopy g) (h' : g.Homotopy k) : f.Homotopy k

Concatenate two module homotopies.

Equations

• h.trans h' = { barHomotopy := h.barHomotopy + h'.barHomotopy, isHomogeneous_barHomotopy := ⋯, barMap_sub_barMap := ⋯ }

@[simp]

theorem TauCeti.AInfinityRightModuleHom.Homotopy.barMap_trans {R : Type uR} {A : Type uA} [CommRing R] [AddCommGroup A] [Module R A] {AA : AInfinityAlgebra R A} {M : Type uM} {N : Type uN} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {MM : AInfinityRightModule AA M} {NN : AInfinityRightModule AA N} {f g k : AInfinityRightModuleHom MM NN} (h : f.Homotopy g) (h' : g.Homotopy k) : (h.trans h').barMap = h.barMap + h'.barMap

noncomputable def TauCeti.AInfinityRightModuleHom.Homotopy.compRight {R : Type uR} {A : Type uA} [CommRing R] [AddCommGroup A] [Module R A] {AA : AInfinityAlgebra R A} {M : Type uM} {N : Type uN} {P : Type uP} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [AddCommGroup P] [Module R P] {MM : AInfinityRightModule AA M} {NN : AInfinityRightModule AA N} {PP : AInfinityRightModule AA P} {f g : AInfinityRightModuleHom MM NN} (h : f.Homotopy g) (l : AInfinityRightModuleHom NN PP) : (l.comp f).Homotopy (l.comp g)

Postcomposition of a homotopy by a module morphism.

Equations

• h.compRight l = { barHomotopy := l.barHom.comp h.barHomotopy, isHomogeneous_barHomotopy := ⋯, barMap_sub_barMap := ⋯ }

@[simp]

theorem TauCeti.AInfinityRightModuleHom.Homotopy.barMap_compRight {R : Type uR} {A : Type uA} [CommRing R] [AddCommGroup A] [Module R A] {AA : AInfinityAlgebra R A} {M : Type uM} {N : Type uN} {P : Type uP} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [AddCommGroup P] [Module R P] {MM : AInfinityRightModule AA M} {NN : AInfinityRightModule AA N} {PP : AInfinityRightModule AA P} {f g : AInfinityRightModuleHom MM NN} (h : f.Homotopy g) (l : AInfinityRightModuleHom NN PP) : (h.compRight l).barMap = l.barMap ∘ₗ h.barMap

theorem TauCeti.AInfinityRightModuleHom.Homotopy.taylor_compRight {R : Type uR} {A : Type uA} [CommRing R] [AddCommGroup A] [Module R A] {AA : AInfinityAlgebra R A} {M : Type uM} {N : Type uN} {P : Type uP} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [AddCommGroup P] [Module R P] {MM : AInfinityRightModule AA M} {NN : AInfinityRightModule AA N} {PP : AInfinityRightModule AA P} {f g : AInfinityRightModuleHom MM NN} (h : f.Homotopy g) (l : AInfinityRightModuleHom NN PP) : (h.compRight l).taylor = l.taylor ∘ₗ h.barMap

Postcomposition applies the Taylor map of the outer morphism to the bar homotopy.

noncomputable def TauCeti.AInfinityRightModuleHom.Homotopy.compLeft {R : Type uR} {A : Type uA} [CommRing R] [AddCommGroup A] [Module R A] {AA : AInfinityAlgebra R A} {L : Type uL} {M : Type uM} {N : Type uN} [AddCommGroup L] [Module R L] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {LL : AInfinityRightModule AA L} {MM : AInfinityRightModule AA M} {NN : AInfinityRightModule AA N} {f g : AInfinityRightModuleHom MM NN} (h : f.Homotopy g) (l : AInfinityRightModuleHom LL MM) : (f.comp l).Homotopy (g.comp l)

Precomposition of a homotopy by a module morphism.

Equations

• h.compLeft l = { barHomotopy := h.barHomotopy.comp l.barHom, isHomogeneous_barHomotopy := ⋯, barMap_sub_barMap := ⋯ }

@[simp]

theorem TauCeti.AInfinityRightModuleHom.Homotopy.barMap_compLeft {R : Type uR} {A : Type uA} [CommRing R] [AddCommGroup A] [Module R A] {AA : AInfinityAlgebra R A} {L : Type uL} {M : Type uM} {N : Type uN} [AddCommGroup L] [Module R L] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {LL : AInfinityRightModule AA L} {MM : AInfinityRightModule AA M} {NN : AInfinityRightModule AA N} {f g : AInfinityRightModuleHom MM NN} (h : f.Homotopy g) (l : AInfinityRightModuleHom LL MM) : (h.compLeft l).barMap = h.barMap ∘ₗ l.barMap

theorem TauCeti.AInfinityRightModuleHom.Homotopy.taylor_compLeft {R : Type uR} {A : Type uA} [CommRing R] [AddCommGroup A] [Module R A] {AA : AInfinityAlgebra R A} {L : Type uL} {M : Type uM} {N : Type uN} [AddCommGroup L] [Module R L] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {LL : AInfinityRightModule AA L} {MM : AInfinityRightModule AA M} {NN : AInfinityRightModule AA N} {f g : AInfinityRightModuleHom MM NN} (h : f.Homotopy g) (l : AInfinityRightModuleHom LL MM) : (h.compLeft l).taylor = h.taylor ∘ₗ l.barMap

Precomposition applies the Taylor map of the homotopy after the inner bar map.