Cohomology and quasi-isomorphisms of right A-infinity modules

The linear part of a morphism of right A∞ modules commutes with the unary operations. It therefore sends cycles to cycles and boundaries to boundaries, inducing a linear map on module cohomology. These induced maps preserve identities and composition.

A module morphism is a quasi-isomorphism when its induced map on cohomology is bijective. The functorial laws immediately give identity, composition, and both two-out-of-three implications. This is the invariant inverted in the derived category of A∞ modules.

Main definitions

• TauCeti.AInfinityRightModuleHom.cohomologyMap: the map induced by the linear part.
• TauCeti.AInfinityRightModuleHom.IsQuasiIso: bijectivity of the induced cohomology map.
• TauCeti.AInfinityRightModuleHom.IsQuasiIso.cohomologyLinearEquiv: the resulting linear equivalence on cohomology.

References

• B. Keller, Introduction to A-infinity algebras and modules, Sections 4.1--4.2.

theorem TauCeti.AInfinityRightModuleHom.differential_comp_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 : AInfinityRightModuleHom MM NN) : NN.differential ∘ₗ f.linearPart = f.linearPart ∘ₗ MM.differential

The linear part of a module morphism commutes with the unary module differentials.

theorem TauCeti.AInfinityRightModuleHom.linearPart_mem_cycles {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) {x : M} (hx : x ∈ MM.cycles) : f.linearPart x ∈ NN.cycles

The linear part of a module morphism carries cycles to cycles.

theorem TauCeti.AInfinityRightModuleHom.linearPart_mem_boundaries {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) {x : M} (hx : x ∈ MM.boundaries) : f.linearPart x ∈ NN.boundaries

The linear part of a module morphism carries boundaries to boundaries.

noncomputable def TauCeti.AInfinityRightModuleHom.cyclesMap {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) : ↥MM.cycles →ₗ[R] ↥NN.cycles

The linear part of a module morphism, restricted to unary cycles.

Equations

• f.cyclesMap = f.linearPart.restrict ⋯

@[simp]

theorem TauCeti.AInfinityRightModuleHom.coe_cyclesMap {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) (x : ↥MM.cycles) : ↑(f.cyclesMap x) = f.linearPart ↑x

The underlying element of the image of a cycle is its image under the linear part.

noncomputable def TauCeti.AInfinityRightModuleHom.cohomologyMap {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) : MM.Cohomology →ₗ[R] NN.Cohomology

The linear map on cohomology induced by the linear part of a module morphism.

Equations

• f.cohomologyMap = MM.boundariesInCycles.mapQ NN.boundariesInCycles f.cyclesMap ⋯

@[simp]

theorem TauCeti.AInfinityRightModuleHom.cohomologyMap_cohomologyClass {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) {x : M} (hx : x ∈ MM.cycles) : f.cohomologyMap (MM.cohomologyClass hx) = NN.cohomologyClass ⋯

The induced map sends the class of a cycle to the class of its image under the linear part.

@[simp]

theorem TauCeti.AInfinityRightModuleHom.cohomologyMap_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).cohomologyMap = LinearMap.id

Passage to module cohomology sends the identity morphism to the identity map.

@[simp]

theorem TauCeti.AInfinityRightModuleHom.cohomologyMap_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).cohomologyMap = g.cohomologyMap ∘ₗ f.cohomologyMap

Passage to module cohomology preserves composition.

def TauCeti.AInfinityRightModuleHom.IsQuasiIso {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) : Prop

A morphism of right A∞ modules is a quasi-isomorphism when its linear part induces a bijection on cohomology.

Equations

• f.IsQuasiIso = Function.Bijective ⇑f.cohomologyMap

theorem TauCeti.AInfinityRightModuleHom.isQuasiIso_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.IsQuasiIso ↔ Function.Bijective ⇑f.cohomologyMap

A module morphism is a quasi-isomorphism exactly when its induced cohomology map is bijective.

@[simp]

theorem TauCeti.AInfinityRightModuleHom.isQuasiIso_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).IsQuasiIso

The identity morphism of a right A∞ module is a quasi-isomorphism.

theorem TauCeti.AInfinityRightModuleHom.IsQuasiIso.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} (hg : g.IsQuasiIso) (hf : f.IsQuasiIso) : (g.comp f).IsQuasiIso

Quasi-isomorphisms of right A∞ modules are closed under composition.

theorem TauCeti.AInfinityRightModuleHom.IsQuasiIso.of_precomp {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} (hf : f.IsQuasiIso) (hgf : (g.comp f).IsQuasiIso) : g.IsQuasiIso

Two out of three: if f and g ∘ f are quasi-isomorphisms, then so is g.

theorem TauCeti.AInfinityRightModuleHom.IsQuasiIso.of_postcomp {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} (hg : g.IsQuasiIso) (hgf : (g.comp f).IsQuasiIso) : f.IsQuasiIso

Two out of three: if g and g ∘ f are quasi-isomorphisms, then so is f.

noncomputable def TauCeti.AInfinityRightModuleHom.IsQuasiIso.cohomologyLinearEquiv {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} (hf : f.IsQuasiIso) : MM.Cohomology ≃ₗ[R] NN.Cohomology

The map induced on cohomology by a quasi-isomorphism, as a linear equivalence.

Equations

• hf.cohomologyLinearEquiv = LinearEquiv.ofBijective f.cohomologyMap ⋯

@[simp]

theorem TauCeti.AInfinityRightModuleHom.IsQuasiIso.cohomologyLinearEquiv_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 : AInfinityRightModuleHom MM NN} (hf : f.IsQuasiIso) (c : MM.Cohomology) : hf.cohomologyLinearEquiv c = f.cohomologyMap c

The cohomology equivalence of a quasi-isomorphism agrees with its induced map.