Cohomology of a right A-infinity module

The unary operation of a right A∞ module squares to zero. This file packages its cycles, boundaries, and total cohomology as modules over the ground ring. The quotient interface is stated using cycle representatives so morphisms can descend their linear parts without exposing the implementation of the quotient.

The higher module operations are not used to define the underlying cohomology module. Their arity-two identity will subsequently equip it with a right action of the cohomology algebra.

Main definitions

• TauCeti.AInfinityRightModule.differential: the unary module operation as a linear map.
• TauCeti.AInfinityRightModule.cycles and TauCeti.AInfinityRightModule.boundaries: its kernel and range.
• TauCeti.AInfinityRightModule.Cohomology: unary cycles modulo unary boundaries.
• TauCeti.AInfinityRightModule.cohomologyClass: the class represented by a cycle.

References

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

noncomputable def TauCeti.AInfinityRightModule.differential {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) : M →ₗ[R] M

The differential of a right A∞ module, namely its unary operation.

Equations

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

@[simp]

theorem TauCeti.AInfinityRightModule.differential_apply {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) (x : M) : MM.differential x = ((MM.m 1) x) fun (i : Fin (1 - 1)) => i.elim0

The module differential evaluates to the unary operation.

@[simp]

theorem TauCeti.AInfinityRightModule.differential_comp_self_eq_zero {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.differential ∘ₗ MM.differential = 0

The unary operation of a right A∞ module squares to zero.

noncomputable def TauCeti.AInfinityRightModule.cycles {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) : Submodule R M

The cycles of a right A∞ module are the kernel of its unary operation.

Equations

• MM.cycles = MM.differential.ker

theorem TauCeti.AInfinityRightModule.cycles_def {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.cycles = MM.differential.ker

The cycles are the kernel of the module differential.

@[simp]

theorem TauCeti.AInfinityRightModule.mem_cycles {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) {x : M} : x ∈ MM.cycles ↔ MM.differential x = 0

An element is a cycle exactly when its unary operation vanishes.

noncomputable def TauCeti.AInfinityRightModule.boundaries {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) : Submodule R M

The boundaries of a right A∞ module are the range of its unary operation.

Equations

• MM.boundaries = MM.differential.range

theorem TauCeti.AInfinityRightModule.boundaries_def {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.boundaries = MM.differential.range

The boundaries are the range of the module differential.

@[simp]

theorem TauCeti.AInfinityRightModule.mem_boundaries {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) {x : M} : x ∈ MM.boundaries ↔ ∃ (y : M), MM.differential y = x

An element is a boundary exactly when it is the unary operation of some element.

theorem TauCeti.AInfinityRightModule.boundaries_le_cycles {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.boundaries ≤ MM.cycles

Every boundary is a cycle.

theorem TauCeti.AInfinityRightModule.differential_mem_boundaries {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) (x : M) : MM.differential x ∈ MM.boundaries

The differential of every element is a boundary.

theorem TauCeti.AInfinityRightModule.differential_mem_cycles {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) (x : M) : MM.differential x ∈ MM.cycles

The differential of every element is a cycle.

theorem TauCeti.AInfinityRightModule.m_one_mem_boundaries {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) (x : M) : (((MM.m 1) x) fun (i : Fin (1 - 1)) => i.elim0) ∈ MM.boundaries

The unary operation of every element is a boundary.

theorem TauCeti.AInfinityRightModule.m_one_mem_cycles {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) (x : M) : (((MM.m 1) x) fun (i : Fin (1 - 1)) => i.elim0) ∈ MM.cycles

The unary operation of every element is a cycle.

noncomputable def TauCeti.AInfinityRightModule.boundariesInCycles {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) : Submodule R ↥MM.cycles

The boundaries, viewed as a submodule of the cycles.

Equations

• MM.boundariesInCycles = MM.boundaries.submoduleOf MM.cycles

@[simp]

theorem TauCeti.AInfinityRightModule.mem_boundariesInCycles {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) {x : ↥MM.cycles} : x ∈ MM.boundariesInCycles ↔ ↑x ∈ MM.boundaries

A cycle lies in boundariesInCycles exactly when its underlying element is a boundary.

@[reducible, inline]

abbrev TauCeti.AInfinityRightModule.Cohomology {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) : Type uM

The total cohomology module of a right A∞ module: unary cycles modulo unary boundaries.

Equations

• MM.Cohomology = (↥MM.cycles ⧸ MM.boundariesInCycles)

noncomputable def TauCeti.AInfinityRightModule.cohomologyClassLinearMap {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.cycles →ₗ[R] MM.Cohomology

The linear quotient map from cycles to module cohomology.

Equations

• MM.cohomologyClassLinearMap = MM.boundariesInCycles.mkQ

noncomputable def TauCeti.AInfinityRightModule.cohomologyClass {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) {x : M} (hx : x ∈ MM.cycles) : MM.Cohomology

The cohomology class represented by a module cycle.

Equations

• MM.cohomologyClass hx = MM.cohomologyClassLinearMap ⟨x, hx⟩

theorem TauCeti.AInfinityRightModule.cohomologyClass_eq_mk {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) {x : M} (hx : x ∈ MM.cycles) : MM.cohomologyClass hx = Submodule.Quotient.mk ⟨x, hx⟩

A cohomology class is the quotient class of its cycle representative.

@[simp]

theorem TauCeti.AInfinityRightModule.cohomologyClass_zero {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.cohomologyClass ⋯ = 0

Zero represents zero in module cohomology.

@[simp]

theorem TauCeti.AInfinityRightModule.cohomologyClass_add {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) {x y : M} (hx : x ∈ MM.cycles) (hy : y ∈ MM.cycles) : MM.cohomologyClass ⋯ = MM.cohomologyClass hx + MM.cohomologyClass hy

The class of a sum of module cycles is the sum of their classes.

@[simp]

theorem TauCeti.AInfinityRightModule.cohomologyClass_smul {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) (r : R) {x : M} (hx : x ∈ MM.cycles) : MM.cohomologyClass ⋯ = r • MM.cohomologyClass hx

The class of a scalar multiple of a module cycle is the scalar multiple of its class.

theorem TauCeti.AInfinityRightModule.exists_cohomologyClass_eq {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) (c : MM.Cohomology) : ∃ (x : M) (hx : x ∈ MM.cycles), MM.cohomologyClass hx = c

Every module cohomology class has a cycle representative.

@[simp]

theorem TauCeti.AInfinityRightModule.cohomologyClass_eq_iff {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) {x y : M} (hx : x ∈ MM.cycles) (hy : y ∈ MM.cycles) : MM.cohomologyClass hx = MM.cohomologyClass hy ↔ x - y ∈ MM.boundaries

Two module cycles represent the same cohomology class exactly when their difference is a boundary.

@[simp]

theorem TauCeti.AInfinityRightModule.cohomologyClass_eq_zero_iff {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) {x : M} (hx : x ∈ MM.cycles) : MM.cohomologyClass hx = 0 ↔ x ∈ MM.boundaries

A module cycle represents zero in cohomology exactly when it is a boundary.

@[simp]

theorem TauCeti.AInfinityRightModule.cohomologyClass_m_one_eq_zero {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) (x : M) : MM.cohomologyClass ⋯ = 0

The cohomology class of a unary operation is zero.