The morphism complex of right A-infinity modules

Let M and N be right A∞ modules over an A∞ algebra A, with module bar differentials b_M and b_N on the cofree bar comodules sM ⊗ Tᶜ(sA) and sN ⊗ Tᶜ(sA). A cochain of degree p from M to N is a morphism of these cofree comodules which is homogeneous of degree p for the total suspended gradings. The differential of a cochain is its graded commutator with the module bar differentials,

δF = b_N ∘ F - (-1)^p F ∘ b_M.

Both bar differentials are coderivations over the same algebra bar differential, so the commutator is again a comodule morphism (TauCeti.Comodule.Hom.coderivationComm); it has degree p + 1, and δ² = 0 because b_M² = 0 and b_N² = 0. This file packages these cochains and their differential as a cochain complex of modules over the ground ring. Composition of cochains adds degrees and satisfies the graded Leibniz rule, with the sign carried by the outer factor, so these complexes are the Hom complexes of a DG category of right A∞ modules.

The two existing notions of maps between modules sit inside this complex. Morphisms of right A∞ modules are exactly the closed cochains of degree zero, and a homotopy from f to g is exactly a cochain of degree -1 whose differential is the difference of their bar maps. As for module morphisms and homotopies, the differential of a cochain is detected by its Taylor map, TauCeti.AInfinityRightModule.homCochains.taylor_homDifferential.

Main definitions

• TauCeti.AInfinityRightModule.homCochains: the homogeneous comodule morphisms of degree p between the cofree bar comodules.
• TauCeti.AInfinityRightModule.homDifferential: the graded commutator with the module bar differentials.
• TauCeti.AInfinityRightModule.homComplex: the morphism complex.
• TauCeti.AInfinityRightModule.homCochains.id, TauCeti.AInfinityRightModule.homCochains.comp: the identity cochain, and the bilinear composition of cochains, which adds degrees.
• TauCeti.AInfinityRightModuleHom.equivZeroCocycles: module morphisms are the closed degree-zero cochains.
• TauCeti.AInfinityRightModuleHom.Homotopy.equivCochains: homotopies are the degree--1 cochains bounding the difference of two morphisms.

Main results

• TauCeti.AInfinityRightModule.homDifferential_homDifferential: the differential squares to zero.
• TauCeti.AInfinityRightModule.homCochains.taylor_homDifferential: the Taylor map of the differential of a cochain.
• TauCeti.AInfinityRightModule.homDifferential_comp: the graded Leibniz rule for composition of cochains.

Implementation notes

TauCeti.AInfinityRightModule.homComplex is exposed so that its terms remain definitionally the cochain modules homCochains MM NN p: the statement of homComplex_d already needs this to type-check, and so do downstream constructions which feed homCochains.comp and homCochains.id to the Hom complexes.

References

• B. Keller, Introduction to A-infinity algebras and modules, Section 4.

def TauCeti.AInfinityRightModule.homCochains {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) (p : ℤ) : Submodule R (TensorProduct R M (TensorWords R A) →ₗ[R] TensorProduct R N (TensorWords R A))

The cochains of degree p from MM to NN: the linear maps between the cofree bar comodules sM ⊗ Tᶜ(sA) and sN ⊗ Tᶜ(sA) which commute with the coactions and raise the total suspended degree by p.

Equations

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

theorem TauCeti.AInfinityRightModule.mem_homCochains_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} {p : ℤ} {F : TensorProduct R M (TensorWords R A) →ₗ[R] TensorProduct R N (TensorWords R A)} : F ∈ MM.homCochains NN p ↔ TensorProduct.map F LinearMap.id ∘ₗ Comodule.coact = Comodule.coact ∘ₗ F ∧ LinearMap.IsHomogeneous F (barGrading AA MM.grading).piece (barGrading AA NN.grading).piece p

Membership in the cochains of degree p: commuting with the coactions and having degree p.

theorem TauCeti.AInfinityRightModule.toLinearMap_mem_homCochains {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} {p : ℤ} (F : Comodule.Hom R (TensorWords R A) (TensorProduct R M (TensorWords R A)) (TensorProduct R N (TensorWords R A))) (hF : LinearMap.IsHomogeneous F.toLinearMap (barGrading AA MM.grading).piece (barGrading AA NN.grading).piece p) : F.toLinearMap ∈ MM.homCochains NN p

A homogeneous comodule morphism of degree p is a cochain of degree p.

def TauCeti.AInfinityRightModule.homCochains.toComoduleHom {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} {p : ℤ} (F : ↥(MM.homCochains NN p)) : Comodule.Hom R (TensorWords R A) (TensorProduct R M (TensorWords R A)) (TensorProduct R N (TensorWords R A))

A cochain as a morphism of the cofree bar comodules.

Equations

• TauCeti.AInfinityRightModule.homCochains.toComoduleHom F = { toLinearMap := ↑F, map_coact := ⋯ }

@[simp]

theorem TauCeti.AInfinityRightModule.homCochains.toComoduleHom_toLinearMap {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} {p : ℤ} (F : ↥(MM.homCochains NN p)) : (toComoduleHom F).toLinearMap = ↑F

theorem TauCeti.AInfinityRightModule.homCochains.isHomogeneous {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} {p : ℤ} (F : ↥(MM.homCochains NN p)) : LinearMap.IsHomogeneous (↑F) (barGrading AA MM.grading).piece (barGrading AA NN.grading).piece p

A cochain of degree p raises the total suspended degree by p.

theorem TauCeti.AInfinityRightModule.homCochains.ext_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} {p : ℤ} {F G : ↥(MM.homCochains NN p)} (h : ↑(TensorProduct.rid R N) ∘ₗ LinearMap.lTensor N CoalgebraStruct.counit ∘ₗ ↑F = ↑(TensorProduct.rid R N) ∘ₗ LinearMap.lTensor N CoalgebraStruct.counit ∘ₗ ↑G) : F = G

Cochains are determined by their Taylor maps, the components obtained by applying the coalgebra counit.

theorem TauCeti.AInfinityRightModule.sub_negOnePow_smul_mem_homCochains {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} {p : ℤ} {F : TensorProduct R M (TensorWords R A) →ₗ[R] TensorProduct R N (TensorWords R A)} (hF : F ∈ MM.homCochains NN p) : NN.barDifferential ∘ₗ F - p.negOnePow • F ∘ₗ MM.barDifferential ∈ MM.homCochains NN (p + 1)

The graded commutator of a cochain of degree p with the module bar differentials, b_N ∘ F - (-1)^p F ∘ b_M, is a cochain of degree p + 1.

def TauCeti.AInfinityRightModule.homDifferential {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) (p : ℤ) : ↥(MM.homCochains NN p) →ₗ[R] ↥(MM.homCochains NN (p + 1))

The differential of the morphism complex: a cochain F of degree p is sent to its graded commutator b_N ∘ F - (-1)^p F ∘ b_M with the module bar differentials.

Equations

• MM.homDifferential NN p = { toFun := fun (F : ↥(MM.homCochains NN p)) => ⟨NN.barDifferential ∘ₗ ↑F - p.negOnePow • ↑F ∘ₗ MM.barDifferential, ⋯⟩, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem TauCeti.AInfinityRightModule.coe_homDifferential {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} (p : ℤ) (F : ↥(MM.homCochains NN p)) : ↑((MM.homDifferential NN p) F) = NN.barDifferential ∘ₗ ↑F - p.negOnePow • ↑F ∘ₗ MM.barDifferential

The differential of a cochain is its graded commutator with the module bar differentials.

@[simp]

theorem TauCeti.AInfinityRightModule.homDifferential_homDifferential {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} (p : ℤ) (F : ↥(MM.homCochains NN p)) : (MM.homDifferential NN (p + 1)) ((MM.homDifferential NN p) F) = 0

The differential of the morphism complex squares to zero.

theorem TauCeti.AInfinityRightModule.homDifferential_comp_homDifferential {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} (p : ℤ) : MM.homDifferential NN (p + 1) ∘ₗ MM.homDifferential NN p = 0

The differential of the morphism complex composed with itself is zero.

theorem TauCeti.AInfinityRightModule.homCochains.taylor_homDifferential {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} {p : ℤ} (F : ↥(MM.homCochains NN p)) : ↑(TensorProduct.rid R N) ∘ₗ LinearMap.lTensor N CoalgebraStruct.counit ∘ₗ ↑((MM.homDifferential NN p) F) = NN.taylor ∘ₗ ↑F - p.negOnePow • (↑(TensorProduct.rid R N) ∘ₗ LinearMap.lTensor N CoalgebraStruct.counit ∘ₗ ↑F) ∘ₗ MM.barDifferential

The Taylor map of the differential of a cochain: the counit component of b_N ∘ F - (-1)^p F ∘ b_M is taylor_N ∘ F - (-1)^p taylor(F) ∘ b_M.

theorem TauCeti.AInfinityRightModule.homDifferential_zero_eq_zero_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 : ↥(MM.homCochains NN 0)) : (MM.homDifferential NN 0) F = 0 ↔ NN.barDifferential ∘ₗ ↑F = ↑F ∘ₗ MM.barDifferential

A cochain of degree zero is closed exactly when it intertwines the module bar differentials.

theorem TauCeti.AInfinityRightModule.coe_homDifferential_neg_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} (H : ↥(MM.homCochains NN (-1))) : ↑((MM.homDifferential NN (-1)) H) = NN.barDifferential ∘ₗ ↑H + ↑H ∘ₗ MM.barDifferential

For a cochain of degree -1, the differential is b_N ∘ H + H ∘ b_M.

Composition

theorem TauCeti.AInfinityRightModule.id_mem_homCochains {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} : LinearMap.id ∈ MM.homCochains MM 0

The identity of the cofree bar comodule is a cochain of degree zero.

theorem TauCeti.AInfinityRightModule.comp_mem_homCochains {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} {p q : ℤ} {G : TensorProduct R N (TensorWords R A) →ₗ[R] TensorProduct R P (TensorWords R A)} (hG : G ∈ NN.homCochains PP p) {F : TensorProduct R M (TensorWords R A) →ₗ[R] TensorProduct R N (TensorWords R A)} (hF : F ∈ MM.homCochains NN q) : G ∘ₗ F ∈ MM.homCochains PP (p + q)

The composite of a cochain of degree p after a cochain of degree q is a cochain of degree p + q.

def TauCeti.AInfinityRightModule.homCochains.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) : ↥(MM.homCochains MM 0)

The identity cochain of degree zero: the identity of the cofree bar comodule.

Equations

• TauCeti.AInfinityRightModule.homCochains.id MM = ⟨LinearMap.id, ⋯⟩

@[simp]

theorem TauCeti.AInfinityRightModule.homCochains.coe_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} : ↑(id MM) = LinearMap.id

The identity cochain is the identity map.

def TauCeti.AInfinityRightModule.homCochains.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} {p q n : ℤ} (h : p + q = n) : ↥(NN.homCochains PP p) →ₗ[R] ↥(MM.homCochains NN q) →ₗ[R] ↥(MM.homCochains PP n)

Composition of cochains, in Keller's order: a cochain G of degree p after a cochain F of degree q is the cochain G ∘ F of degree n = p + q. It is bilinear in G and F.

Equations

• TauCeti.AInfinityRightModule.homCochains.comp h = LinearMap.mk₂ R (fun (G : ↥(NN.homCochains PP p)) (F : ↥(MM.homCochains NN q)) => ⟨↑G ∘ₗ ↑F, ⋯⟩) ⋯ ⋯ ⋯ ⋯

@[simp]

theorem TauCeti.AInfinityRightModule.homCochains.coe_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} {p q n : ℤ} (h : p + q = n) (G : ↥(NN.homCochains PP p)) (F : ↥(MM.homCochains NN q)) : ↑(((comp h) G) F) = ↑G ∘ₗ ↑F

The composite of two cochains is the composite of the underlying maps.

@[simp]

theorem TauCeti.AInfinityRightModule.homCochains.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} {p : ℤ} (G : ↥(MM.homCochains NN p)) : ((comp ⋯) G) (id MM) = G

Composing with the identity cochain on the right changes nothing.

@[simp]

theorem TauCeti.AInfinityRightModule.homCochains.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} {p : ℤ} (F : ↥(MM.homCochains NN p)) : ((comp ⋯) (id NN)) F = F

Composing with the identity cochain on the left changes nothing.

theorem TauCeti.AInfinityRightModule.homCochains.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 u_1} [AddCommGroup Q] [Module R Q] {QQ : AInfinityRightModule AA Q} {r q p rq qp n : ℤ} (hrq : r + q = rq) (hqp : q + p = qp) (h : rq + p = n) (h' : r + qp = n) (K : ↥(PP.homCochains QQ r)) (G : ↥(NN.homCochains PP q)) (F : ↥(MM.homCochains NN p)) : ((comp h) (((comp hrq) K) G)) F = ((comp h') K) (((comp hqp) G) F)

Composition of cochains is associative.

@[simp]

theorem TauCeti.AInfinityRightModule.homDifferential_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} : (MM.homDifferential MM 0) (homCochains.id MM) = 0

The identity cochain is closed.

theorem TauCeti.AInfinityRightModule.homDifferential_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} {p q n : ℤ} (h : p + q = n) (G : ↥(NN.homCochains PP p)) (F : ↥(MM.homCochains NN q)) : (MM.homDifferential PP n) (((homCochains.comp h) G) F) = ((homCochains.comp ⋯) ((NN.homDifferential PP p) G)) F + p.negOnePow • ((homCochains.comp ⋯) G) ((MM.homDifferential NN q) F)

The graded Leibniz rule: for cochains G of degree p and F of degree q, δ(G ∘ F) = δG ∘ F + (-1)^p G ∘ δF. The sign is carried by the outer factor, as in Keller's composition order.

def TauCeti.AInfinityRightModule.homComplex {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) : CochainComplex (ModuleCat R) ℤ

The morphism complex between two right A∞ modules. Its degree-p term is the module of cochains of degree p, and its differential is the graded commutator with the module bar differentials.

Equations

• MM.homComplex NN = CochainComplex.of (fun (p : ℤ) => ↧↥(MM.homCochains NN p)) (fun (p : ℤ) => ModuleCat.ofHom (MM.homDifferential NN p)) ⋯

@[simp]

theorem TauCeti.AInfinityRightModule.homComplex_X {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) (p : ℤ) : (MM.homComplex NN).X p = ↧↥(MM.homCochains NN p)

The degree-p term of the morphism complex is the module of cochains of degree p.

@[simp]

theorem TauCeti.AInfinityRightModule.homComplex_d {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) (p : ℤ) : (MM.homComplex NN).d p (p + 1) = ModuleCat.ofHom (MM.homDifferential NN p)

The differential of the morphism complex is induced by homDifferential.

theorem TauCeti.AInfinityRightModuleHom.barMap_mem_homCochains {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 ∈ MM.homCochains NN 0

The bar map of a module morphism is a cochain of degree zero.

def TauCeti.AInfinityRightModuleHom.equivZeroCocycles {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} : AInfinityRightModuleHom MM NN ≃ ↥(MM.homDifferential NN 0).ker

Morphisms of right A∞ modules are exactly the closed cochains of degree zero in the morphism complex.

Equations

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

@[simp]

theorem TauCeti.AInfinityRightModuleHom.coe_equivZeroCocycles {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) : ↑↑(equivZeroCocycles f) = f.barMap

The closed cochain of a module morphism is its bar map.

@[simp]

theorem TauCeti.AInfinityRightModuleHom.barMap_equivZeroCocycles_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 : ↥(MM.homDifferential NN 0).ker) : (equivZeroCocycles.symm F).barMap = ↑↑F

The module morphism of a closed cochain has that cochain as its bar map.

theorem TauCeti.AInfinityRightModuleHom.Homotopy.barMap_mem_homCochains {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 ∈ MM.homCochains NN (-1)

The bar homotopy of a module homotopy is a cochain of degree -1.

def TauCeti.AInfinityRightModuleHom.Homotopy.equivCochains {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.Homotopy g ≃ { H : ↥(MM.homCochains NN (-1)) // ↑((MM.homDifferential NN (-1)) H) = f.barMap - g.barMap }

Homotopies from f to g are exactly the cochains of degree -1 whose differential is the difference of the bar maps of f and g.

Equations

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

@[simp]

theorem TauCeti.AInfinityRightModuleHom.Homotopy.coe_equivCochains {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) : ↑↑(equivCochains h) = h.barMap

The cochain of a homotopy is its bar homotopy.

@[simp]

theorem TauCeti.AInfinityRightModuleHom.Homotopy.barMap_equivCochains_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 : { H : ↥(MM.homCochains NN (-1)) // ↑((MM.homDifferential NN (-1)) H) = f.barMap - g.barMap }) : (equivCochains.symm H).barMap = ↑↑H

The homotopy of a bounding cochain has that cochain as its bar homotopy.