Augmented A∞ algebras

An augmentation of a strictly unital A∞ algebra is a strict A∞ map to the ground ring in degree zero. Concretely, it is a degree-zero linear functional which sends the strict unit to one, intertwines the binary operation with multiplication, and annihilates every operation of arity other than two.

The kernel of the augmentation is the reduced augmentation ideal. It inherits the grading and all the operations, and the strict unit splits the underlying module into its scalar and reduced parts. This is the input used to form reduced bar constructions without unit-containing tensor words.

Main definitions

• TauCeti.AInfinityAlgebra.Augmentation: an augmentation together with its strict unit.
• TauCeti.AInfinityAlgebra.Augmentation.augmentationIdeal: the reduced augmentation ideal.
• TauCeti.AInfinityAlgebra.Augmentation.reducedGrading: its inherited internal grading.
• TauCeti.AInfinityAlgebra.Augmentation.reducedOperation: the operations restricted to the augmentation ideal.
• TauCeti.AInfinityAlgebra.Augmentation.reducedAlgebra: the induced A∞ algebra on the augmentation ideal.
• TauCeti.AInfinityAlgebra.Augmentation.splitLinearEquiv: the canonical splitting into scalar and reduced parts.

References

• B. Keller, Introduction to A-infinity algebras and modules, Sections 3.1 and 3.6.

structure TauCeti.AInfinityAlgebra.Augmentation {R : Type uR} {A : Type uA} [CommRing R] [AddCommGroup A] [Module R A] (𝒜 : AInfinityAlgebra R A) : Type (max uA uR)

An augmentation of an uncurved A∞ algebra over its ground ring.

The bundled element is a strict unit. The linear map is homogeneous of degree zero, where the target ring is concentrated in degree zero, and its operation equations say precisely that it is a strict A∞ map to that ground ring.

• unit : A

  The strict unit selected by the augmented structure.

• isStrictUnit : 𝒜.StrictUnit self.unit

  The selected element is a strict unit.

• toLinearMap : A →ₗ[R] R

  The augmentation as a linear functional to the ground ring.

• map_unit : self.toLinearMap self.unit = 1

  The augmentation sends the strict unit to one.

• map_of_mem_ne_zero (p : ℤ) (x : A) : x ∈ 𝒜.grading.piece p → p ≠ 0 → self.toLinearMap x = 0

  The augmentation vanishes on homogeneous elements of nonzero degree.

• map_binary (x y : A) : self.toLinearMap ((𝒜.m 2) ![x, y]) = self.toLinearMap x * self.toLinearMap y

  The augmentation intertwines the binary operation with multiplication in the ground ring.

• map_m_of_ne_two (n : ℕ) : 0 < n → n ≠ 2 → ∀ (x : Fin n → A), self.toLinearMap ((𝒜.m n) x) = 0

  The augmentation annihilates every positive-arity operation other than the binary one.

@[instance_reducible]

instance TauCeti.AInfinityAlgebra.Augmentation.instCoeFunForall {R : Type uR} {A : Type uA} [CommRing R] [AddCommGroup A] [Module R A] {𝒜 : AInfinityAlgebra R A} : CoeFun 𝒜.Augmentation fun (x : 𝒜.Augmentation) => A → R

Equations

• TauCeti.AInfinityAlgebra.Augmentation.instCoeFunForall = { coe := fun (ε : 𝒜.Augmentation) => ⇑ε.toLinearMap }

theorem TauCeti.AInfinityAlgebra.Augmentation.map_unary {R : Type uR} {A : Type uA} [CommRing R] [AddCommGroup A] [Module R A] {𝒜 : AInfinityAlgebra R A} (ε : 𝒜.Augmentation) (x : A) : ε.toLinearMap ((𝒜.m 1) ![x]) = 0

An augmentation annihilates the unary operation.

theorem TauCeti.AInfinityAlgebra.Augmentation.ext {R : Type uR} {A : Type uA} [CommRing R] [AddCommGroup A] [Module R A] {𝒜 : AInfinityAlgebra R A} {ε ε' : 𝒜.Augmentation} (h : ε.toLinearMap = ε'.toLinearMap) : ε = ε'

An augmentation is determined by its underlying linear map.

theorem TauCeti.AInfinityAlgebra.Augmentation.ext_iff {R : Type uR} {A : Type uA} [CommRing R] [AddCommGroup A] [Module R A] {𝒜 : AInfinityAlgebra R A} {ε ε' : 𝒜.Augmentation} : ε = ε' ↔ ε.toLinearMap = ε'.toLinearMap

noncomputable def TauCeti.AInfinityAlgebra.Augmentation.unitHom {R : Type uR} {A : Type uA} [CommRing R] [AddCommGroup A] [Module R A] {𝒜 : AInfinityAlgebra R A} (ε : 𝒜.Augmentation) : R →ₗ[R] A

The linear inclusion of the ground ring generated by the strict unit.

Equations

• ε.unitHom = LinearMap.toSpanSingleton R A ε.unit

@[simp]

theorem TauCeti.AInfinityAlgebra.Augmentation.unitHom_apply {R : Type uR} {A : Type uA} [CommRing R] [AddCommGroup A] [Module R A] {𝒜 : AInfinityAlgebra R A} (ε : 𝒜.Augmentation) (r : R) : ε.unitHom r = r • ε.unit

@[simp]

theorem TauCeti.AInfinityAlgebra.Augmentation.comp_unitHom {R : Type uR} {A : Type uA} [CommRing R] [AddCommGroup A] [Module R A] {𝒜 : AInfinityAlgebra R A} (ε : 𝒜.Augmentation) : ε.toLinearMap ∘ₗ ε.unitHom = LinearMap.id

The augmentation is a retraction of the strict-unit inclusion.

theorem TauCeti.AInfinityAlgebra.Augmentation.surjective {R : Type uR} {A : Type uA} [CommRing R] [AddCommGroup A] [Module R A] {𝒜 : AInfinityAlgebra R A} (ε : 𝒜.Augmentation) : Function.Surjective ⇑ε.toLinearMap

An augmentation is surjective because it maps the strict unit to one.

def TauCeti.AInfinityAlgebra.Augmentation.augmentationIdeal {R : Type uR} {A : Type uA} [CommRing R] [AddCommGroup A] [Module R A] {𝒜 : AInfinityAlgebra R A} (ε : 𝒜.Augmentation) : Submodule R A

The reduced augmentation ideal, as a submodule of the underlying graded module.

Equations

• ε.augmentationIdeal = ε.toLinearMap.ker

@[simp]

theorem TauCeti.AInfinityAlgebra.Augmentation.mem_augmentationIdeal {R : Type uR} {A : Type uA} [CommRing R] [AddCommGroup A] [Module R A] {𝒜 : AInfinityAlgebra R A} (ε : 𝒜.Augmentation) {x : A} : x ∈ ε.augmentationIdeal ↔ ε.toLinearMap x = 0

Membership in the augmentation ideal is equivalent to vanishing under the augmentation.

theorem TauCeti.AInfinityAlgebra.Augmentation.binary_mem_augmentationIdeal_left {R : Type uR} {A : Type uA} [CommRing R] [AddCommGroup A] [Module R A] {𝒜 : AInfinityAlgebra R A} (ε : 𝒜.Augmentation) (x : A) {y : A} (hy : y ∈ ε.augmentationIdeal) : (𝒜.m 2) ![x, y] ∈ ε.augmentationIdeal

The binary operation remains in the augmentation ideal when its second input lies there.

theorem TauCeti.AInfinityAlgebra.Augmentation.binary_mem_augmentationIdeal_right {R : Type uR} {A : Type uA} [CommRing R] [AddCommGroup A] [Module R A] {𝒜 : AInfinityAlgebra R A} (ε : 𝒜.Augmentation) {x : A} (hx : x ∈ ε.augmentationIdeal) (y : A) : (𝒜.m 2) ![x, y] ∈ ε.augmentationIdeal

The binary operation remains in the augmentation ideal when its first input lies there.

theorem TauCeti.AInfinityAlgebra.Augmentation.decompose_mem_augmentationIdeal {R : Type uR} {A : Type uA} [CommRing R] [AddCommGroup A] [Module R A] {𝒜 : AInfinityAlgebra R A} (ε : 𝒜.Augmentation) (x : ↥ε.augmentationIdeal) (p : ℤ) : ↑(((DirectSum.decompose 𝒜.grading.piece) ↑x) p) ∈ ε.augmentationIdeal

Every homogeneous projection of an element of the augmentation ideal remains in the ideal.

noncomputable def TauCeti.AInfinityAlgebra.Augmentation.reducedGrading {R : Type uR} {A : Type uA} [CommRing R] [AddCommGroup A] [Module R A] {𝒜 : AInfinityAlgebra R A} (ε : 𝒜.Augmentation) : InternalGrading R ↥ε.augmentationIdeal

The internal grading on the reduced augmentation ideal obtained by intersecting it with each homogeneous piece of the original algebra.

Equations

• ε.reducedGrading = 𝒜.grading.submodule ε.augmentationIdeal ⋯

@[simp]

theorem TauCeti.AInfinityAlgebra.Augmentation.reducedGrading_piece {R : Type uR} {A : Type uA} [CommRing R] [AddCommGroup A] [Module R A] {𝒜 : AInfinityAlgebra R A} (ε : 𝒜.Augmentation) (p : ℤ) : ε.reducedGrading.piece p = Submodule.comap ε.augmentationIdeal.subtype (𝒜.grading.piece p)

theorem TauCeti.AInfinityAlgebra.Augmentation.m_mem_augmentationIdeal {R : Type uR} {A : Type uA} [CommRing R] [AddCommGroup A] [Module R A] {𝒜 : AInfinityAlgebra R A} (ε : 𝒜.Augmentation) (n : ℕ) (x : Fin n → ↥ε.augmentationIdeal) : ((𝒜.m n) fun (i : Fin n) => ↑(x i)) ∈ ε.augmentationIdeal

Every A∞ operation preserves the reduced augmentation ideal when all its inputs lie there.

noncomputable def TauCeti.AInfinityAlgebra.Augmentation.reducedOperation {R : Type uR} {A : Type uA} [CommRing R] [AddCommGroup A] [Module R A] {𝒜 : AInfinityAlgebra R A} (ε : 𝒜.Augmentation) (n : ℕ) : MultilinearMap R (fun (x : Fin n) => ↥ε.augmentationIdeal) ↥ε.augmentationIdeal

The arity-n operation restricted to the reduced augmentation ideal.

Equations

• ε.reducedOperation n = ((𝒜.m n).compLinearMap fun (x : Fin n) => ε.augmentationIdeal.subtype).codRestrict ε.augmentationIdeal ⋯

@[simp]

theorem TauCeti.AInfinityAlgebra.Augmentation.coe_reducedOperation {R : Type uR} {A : Type uA} [CommRing R] [AddCommGroup A] [Module R A] {𝒜 : AInfinityAlgebra R A} (ε : 𝒜.Augmentation) (n : ℕ) (x : Fin n → ↥ε.augmentationIdeal) : ↑((ε.reducedOperation n) x) = (𝒜.m n) fun (i : Fin n) => ↑(x i)

The restricted operation agrees with the original operation after inclusion.

@[simp]

theorem TauCeti.AInfinityAlgebra.Augmentation.reducedOperation_zero {R : Type uR} {A : Type uA} [CommRing R] [AddCommGroup A] [Module R A] {𝒜 : AInfinityAlgebra R A} (ε : 𝒜.Augmentation) : ε.reducedOperation 0 = 0

The nullary restricted operation vanishes.

theorem TauCeti.AInfinityAlgebra.Augmentation.isHomogeneous_reducedOperation {R : Type uR} {A : Type uA} [CommRing R] [AddCommGroup A] [Module R A] {𝒜 : AInfinityAlgebra R A} (ε : 𝒜.Augmentation) (n : ℕ) (hn : 0 < n) : MultilinearMap.IsHomogeneous (ε.reducedOperation n) (fun (x : Fin n) => ε.reducedGrading.piece) ε.reducedGrading.piece (2 - ↑n)

The operation on the reduced augmentation ideal has the same degree as the original operation.

theorem TauCeti.AInfinityAlgebra.Augmentation.sub_smul_unit_mem_augmentationIdeal {R : Type uR} {A : Type uA} [CommRing R] [AddCommGroup A] [Module R A] {𝒜 : AInfinityAlgebra R A} (ε : 𝒜.Augmentation) (x : A) : x - ε.toLinearMap x • ε.unit ∈ ε.augmentationIdeal

Removing the scalar part of an element leaves an element of the augmentation ideal.

noncomputable def TauCeti.AInfinityAlgebra.Augmentation.reducedPart {R : Type uR} {A : Type uA} [CommRing R] [AddCommGroup A] [Module R A] {𝒜 : AInfinityAlgebra R A} (ε : 𝒜.Augmentation) : A →ₗ[R] ↥ε.augmentationIdeal

The linear projection onto the reduced augmentation ideal, obtained by subtracting the scalar part of an element.

Equations

• ε.reducedPart = LinearMap.codRestrict ε.augmentationIdeal (LinearMap.id - ε.unitHom ∘ₗ ε.toLinearMap) ⋯

@[simp]

theorem TauCeti.AInfinityAlgebra.Augmentation.coe_reducedPart {R : Type uR} {A : Type uA} [CommRing R] [AddCommGroup A] [Module R A] {𝒜 : AInfinityAlgebra R A} (ε : 𝒜.Augmentation) (x : A) : ↑(ε.reducedPart x) = x - ε.toLinearMap x • ε.unit

@[simp]

theorem TauCeti.AInfinityAlgebra.Augmentation.reducedPart_coe {R : Type uR} {A : Type uA} [CommRing R] [AddCommGroup A] [Module R A] {𝒜 : AInfinityAlgebra R A} (ε : 𝒜.Augmentation) (x : ↥ε.augmentationIdeal) : ε.reducedPart ↑x = x

The reduced-part projection fixes the augmentation ideal pointwise.

noncomputable def TauCeti.AInfinityAlgebra.Augmentation.reducedAlgebra {R : Type uR} {A : Type uA} [CommRing R] [AddCommGroup A] [Module R A] {𝒜 : AInfinityAlgebra R A} (ε : 𝒜.Augmentation) : AInfinityAlgebra R ↥ε.augmentationIdeal

The A∞ algebra induced on the reduced augmentation ideal.

Equations

• ε.reducedAlgebra = TauCeti.AInfinityAlgebra.ofStasheff ε.reducedGrading ε.reducedOperation ⋯ ⋯ (TauCeti.AInfinityAlgebra.Augmentation.reducedTaylor✝ ε) ⋯ ⋯

@[simp]

theorem TauCeti.AInfinityAlgebra.Augmentation.reducedAlgebra_grading {R : Type uR} {A : Type uA} [CommRing R] [AddCommGroup A] [Module R A] {𝒜 : AInfinityAlgebra R A} (ε : 𝒜.Augmentation) : ε.reducedAlgebra.grading = ε.reducedGrading

The grading of the reduced A∞ algebra is the inherited grading.

@[simp]

theorem TauCeti.AInfinityAlgebra.Augmentation.reducedAlgebra_m {R : Type uR} {A : Type uA} [CommRing R] [AddCommGroup A] [Module R A] {𝒜 : AInfinityAlgebra R A} (ε : 𝒜.Augmentation) : ε.reducedAlgebra.m = ε.reducedOperation

The operations of the reduced A∞ algebra are the restricted operations.

@[simp]

theorem TauCeti.AInfinityAlgebra.Augmentation.reducedAlgebra_taylor {R : Type uR} {A : Type uA} [CommRing R] [AddCommGroup A] [Module R A] {𝒜 : AInfinityAlgebra R A} (ε : 𝒜.Augmentation) : ε.reducedAlgebra.taylor = ε.reducedPart ∘ₗ 𝒜.taylor ∘ₗ ReducedTensorWords.map R ε.augmentationIdeal.subtype

The Taylor map of the reduced A∞ algebra includes reduced tensor words, applies the ambient Taylor map, and projects to the reduced part.

noncomputable def TauCeti.AInfinityAlgebra.Augmentation.splitLinearEquiv {R : Type uR} {A : Type uA} [CommRing R] [AddCommGroup A] [Module R A] {𝒜 : AInfinityAlgebra R A} (ε : 𝒜.Augmentation) : A ≃ₗ[R] R × ↥ε.augmentationIdeal

The canonical linear splitting of an augmented A∞ algebra into its scalar and reduced parts.

Equations

• ε.splitLinearEquiv = ε.toLinearMap.equivProdOfSurjectiveOfIsCompl ε.reducedPart ⋯ ⋯ ⋯

@[simp]

theorem TauCeti.AInfinityAlgebra.Augmentation.splitLinearEquiv_apply {R : Type uR} {A : Type uA} [CommRing R] [AddCommGroup A] [Module R A] {𝒜 : AInfinityAlgebra R A} (ε : 𝒜.Augmentation) (x : A) : ε.splitLinearEquiv x = (ε.toLinearMap x, ε.reducedPart x)

@[simp]

theorem TauCeti.AInfinityAlgebra.Augmentation.splitLinearEquiv_symm_apply {R : Type uR} {A : Type uA} [CommRing R] [AddCommGroup A] [Module R A] {𝒜 : AInfinityAlgebra R A} (ε : 𝒜.Augmentation) (x : R × ↥ε.augmentationIdeal) : ε.splitLinearEquiv.symm x = x.1 • ε.unit + ↑x.2

The inverse splitting adds the scalar multiple of the unit to the reduced part.