Morphisms of right A-infinity modules

A morphism of right A∞ modules over a fixed algebra is a degree-zero morphism of their cofree bar comodules commuting with the bar differentials. Its Taylor map is obtained by applying the coalgebra counit. Cofreeness makes this map determine the morphism, and makes commutation with the differentials equivalent to the suspended Taylor-component equation. Thus AInfinityRightModuleHom.ofTaylor constructs a morphism from a degree-zero Taylor map satisfying that equation, without requiring a separate bar map. The construction uses Comodule.Hom.cofreeEquiv and Comodule.Hom.cofreeLift; its bar/Taylor interface parallels AInfinityHom for algebra morphisms.

Identities and composition use comodule morphisms. Taylor components and the unary chain map are developed in TauCeti.Algebra.Homology.AInfinity.Module.Right.Hom.Components.

References

• B. Keller, Introduction to A-infinity algebras and modules, Section 4.
• E. Getzler and J. D. S. Jones, A-infinity algebras and the cyclic bar complex, Sections 1--2.

structure TauCeti.AInfinityRightModuleHom {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) : Type (max (max (max uA uM) uN) uR)

A morphism of right A∞ modules over a fixed algebra, represented by a degree-zero morphism of the cofree bar comodules intertwining their differentials.

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

  The induced morphism of cofree bar comodules.

• isHomogeneous_barMap : LinearMap.IsHomogeneous self.barHom.toLinearMap (AInfinityRightModule.barGrading AA MM.grading).piece (AInfinityRightModule.barGrading AA NN.grading).piece 0

  The bar map preserves the total suspended degree.

• barDifferential_comp_barMap : NN.barDifferential ∘ₗ self.barHom.toLinearMap = self.barHom.toLinearMap ∘ₗ MM.barDifferential

  The bar map intertwines the module bar differentials.

@[reducible, inline]

abbrev TauCeti.AInfinityRightModuleHom.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 : AInfinityRightModuleHom MM NN) : TensorProduct R M (TensorWords R A) →ₗ[R] TensorProduct R N (TensorWords R A)

The underlying linear map of the bar-comodule morphism.

Equations

• f.barMap = f.barHom.toLinearMap

@[simp]

theorem TauCeti.AInfinityRightModuleHom.barDifferential_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 : AInfinityRightModuleHom MM NN) (z : TensorProduct R M (TensorWords R A)) : NN.barDifferential (f.barHom z) = f.barHom (MM.barDifferential z)

The intertwining of the module bar differentials, applied to an element.

noncomputable def TauCeti.AInfinityRightModuleHom.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 : AInfinityRightModuleHom MM NN) : TensorProduct R M (TensorWords R A) →ₗ[R] N

The suspended Taylor map: apply the coalgebra counit after the bar map.

Equations

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

theorem TauCeti.AInfinityRightModuleHom.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 : AInfinityRightModuleHom MM NN) : f.taylor = ↑(TensorProduct.rid R N) ∘ₗ LinearMap.lTensor N CoalgebraStruct.counit ∘ₗ f.barMap

theorem TauCeti.AInfinityRightModuleHom.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 : AInfinityRightModuleHom MM NN) : LinearMap.IsHomogeneous f.taylor (AInfinityRightModule.barGrading AA MM.grading).piece (NN.grading.shift 1).piece 0

The Taylor map preserves suspended degree.

theorem TauCeti.AInfinityRightModuleHom.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 : AInfinityRightModuleHom MM NN) : f.barMap = (Comodule.Hom.cofreeLift f.taylor).toLinearMap

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

theorem TauCeti.AInfinityRightModuleHom.barMap_injective {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} : Function.Injective barMap

Morphisms are determined by their underlying bar maps.

theorem TauCeti.AInfinityRightModuleHom.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 : f.taylor = g.taylor) : f = g

Morphisms are determined by their suspended Taylor maps.

theorem TauCeti.AInfinityRightModuleHom.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} : f = g ↔ f.taylor = g.taylor

@[simp]

theorem TauCeti.AInfinityRightModuleHom.taylor_comp_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 : AInfinityRightModuleHom MM NN) : NN.taylor ∘ₗ f.barMap = f.taylor ∘ₗ MM.barDifferential

The suspended module-morphism equation, expressed on Taylor maps.

theorem TauCeti.AInfinityRightModuleHom.barDifferential_comp_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 : Comodule.Hom R (TensorWords R A) (TensorProduct R M (TensorWords R A)) (TensorProduct R N (TensorWords R A))) (hF : LinearMap.IsHomogeneous F.toLinearMap (AInfinityRightModule.barGrading AA MM.grading).piece (AInfinityRightModule.barGrading AA NN.grading).piece 0) : NN.barDifferential ∘ₗ F.toLinearMap = F.toLinearMap ∘ₗ MM.barDifferential ↔ NN.taylor ∘ₗ F.toLinearMap = (↑(TensorProduct.rid R N) ∘ₗ LinearMap.lTensor N CoalgebraStruct.counit ∘ₗ F.toLinearMap) ∘ₗ MM.barDifferential

For a degree-zero bar-comodule map, differential compatibility can be checked after applying the coalgebra counit. This is the full suspended component equation.

noncomputable def TauCeti.AInfinityRightModuleHom.ofTaylor {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 : TensorProduct R M (TensorWords R A) →ₗ[R] N) (hF : LinearMap.IsHomogeneous F (AInfinityRightModule.barGrading AA MM.grading).piece (NN.grading.shift 1).piece 0) (h : NN.taylor ∘ₗ (Comodule.Hom.cofreeLift F).toLinearMap = F ∘ₗ MM.barDifferential) : AInfinityRightModuleHom MM NN

Construct a module morphism from a degree-zero Taylor map satisfying the suspended component equation. Cofreeness supplies the bar map and reduces its differential law to this equation.

Equations

• TauCeti.AInfinityRightModuleHom.ofTaylor F hF h = { barHom := TauCeti.Comodule.Hom.cofreeLift F, isHomogeneous_barMap := ⋯, barDifferential_comp_barMap := ⋯ }

@[simp]

theorem TauCeti.AInfinityRightModuleHom.barMap_ofTaylor {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 : TensorProduct R M (TensorWords R A) →ₗ[R] N) (hF : LinearMap.IsHomogeneous F (AInfinityRightModule.barGrading AA MM.grading).piece (NN.grading.shift 1).piece 0) (h : NN.taylor ∘ₗ (Comodule.Hom.cofreeLift F).toLinearMap = F ∘ₗ MM.barDifferential) : (ofTaylor F hF h).barMap = (Comodule.Hom.cofreeLift F).toLinearMap

The bar map of the constructed morphism is the cofree lift.

@[simp]

theorem TauCeti.AInfinityRightModuleHom.taylor_ofTaylor {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 : TensorProduct R M (TensorWords R A) →ₗ[R] N) (hF : LinearMap.IsHomogeneous F (AInfinityRightModule.barGrading AA MM.grading).piece (NN.grading.shift 1).piece 0) (h : NN.taylor ∘ₗ (Comodule.Hom.cofreeLift F).toLinearMap = F ∘ₗ MM.barDifferential) : (ofTaylor F hF h).taylor = F

The constructed morphism has the prescribed Taylor map.

@[simp]

theorem TauCeti.AInfinityRightModuleHom.ofTaylor_self {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) : ofTaylor f.taylor ⋯ ⋯ = f

Every morphism is recovered from its Taylor map and component equation.

noncomputable def TauCeti.AInfinityRightModuleHom.id {R : Type uR} {A : Type uA} [CommRing R] [AddCommGroup A] [Module R A] {AA : AInfinityAlgebra R A} {M : Type uM} [AddCommGroup M] [Module R M] (MM : AInfinityRightModule AA M) : AInfinityRightModuleHom MM MM

The identity module morphism.

Equations

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

@[simp]

theorem TauCeti.AInfinityRightModuleHom.barMap_id {R : Type uR} {A : Type uA} [CommRing R] [AddCommGroup A] [Module R A] {AA : AInfinityAlgebra R A} {M : Type uM} [AddCommGroup M] [Module R M] (MM : AInfinityRightModule AA M) : (AInfinityRightModuleHom.id MM).barMap = LinearMap.id

@[simp]

theorem TauCeti.AInfinityRightModuleHom.taylor_id {R : Type uR} {A : Type uA} [CommRing R] [AddCommGroup A] [Module R A] {AA : AInfinityAlgebra R A} {M : Type uM} [AddCommGroup M] [Module R M] (MM : AInfinityRightModule AA M) : (AInfinityRightModuleHom.id MM).taylor = ↑(TensorProduct.rid R M) ∘ₗ LinearMap.lTensor M CoalgebraStruct.counit

The Taylor map of the identity is the counit projection onto the module factor.

noncomputable def TauCeti.AInfinityRightModuleHom.comp {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} (g : AInfinityRightModuleHom NN PP) (f : AInfinityRightModuleHom MM NN) : AInfinityRightModuleHom MM PP

Composition of module morphisms is composition of bar-comodule maps.

Equations

• g.comp f = { barHom := g.barHom.comp f.barHom, isHomogeneous_barMap := ⋯, barDifferential_comp_barMap := ⋯ }

@[simp]

theorem TauCeti.AInfinityRightModuleHom.barMap_comp {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} (g : AInfinityRightModuleHom NN PP) (f : AInfinityRightModuleHom MM NN) : (g.comp f).barMap = g.barMap ∘ₗ f.barMap

@[simp]

theorem TauCeti.AInfinityRightModuleHom.taylor_comp {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} (g : AInfinityRightModuleHom NN PP) (f : AInfinityRightModuleHom MM NN) : (g.comp f).taylor = g.taylor ∘ₗ f.barMap

Taylor components of a composite are obtained by applying the second Taylor map to the first bar map.

@[simp]

theorem TauCeti.AInfinityRightModuleHom.comp_id {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.comp (AInfinityRightModuleHom.id MM) = f

The identity module morphism is a right identity for composition.

@[simp]

theorem TauCeti.AInfinityRightModuleHom.id_comp {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) : (AInfinityRightModuleHom.id NN).comp f = f

The identity module morphism is a left identity for composition.

@[simp]

theorem TauCeti.AInfinityRightModuleHom.comp_assoc {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} {Q : Type uQ} [AddCommGroup Q] [Module R Q] {QQ : AInfinityRightModule AA Q} (h : AInfinityRightModuleHom PP QQ) (g : AInfinityRightModuleHom NN PP) (f : AInfinityRightModuleHom MM NN) : (h.comp g).comp f = h.comp (g.comp f)

Composition of module morphisms is associative.