Coalgebra morphisms of reduced tensor coalgebras

For R-modules M and N, a linear map F : Tᶜ(M) ⟶ Tᶜ(N) between the reduced tensor coalgebras ⨁_{n ≥ 1} M^{⊗n} and ⨁_{n ≥ 1} N^{⊗n} is a coalgebra morphism when it commutes with reduced deconcatenation: Δ ∘ F = (F ⊗ F) ∘ Δ. This file proves the concrete correspondence between coalgebra morphisms Tᶜ(M) ⟶ Tᶜ(N) and their families of Taylor components, obtained by composing with the projection Tᶜ(N) ⟶ N onto single letters.

That a coalgebra morphism is determined by its Taylor components is an induction along the conilpotence filtration, exactly as for coderivations. That every family f of components occurs is the Taylor expansion coalgHom f, which sends a word x₁ ⋯ xₙ to the sum, over all ways of cutting it into consecutive nonempty blocks B₁ ⋯ B_k, of the word f(B₁) ⋯ f(B_k). It is built recursively by splitting off the first block, coalgHom f (x₁ ⋯ xₙ) = f(x₁ ⋯ xₙ) + ∑_{0 < d < n} f(x₁ ⋯ x_d) · coalgHom f (x_{d+1} ⋯ xₙ), where · prepends a letter to a word (ReducedTensorWords.prepend). Deconcatenating a prepended word either separates the new letter or cuts the remaining word, which is what makes the coalgebra-morphism identity an induction on the length of the word.

No sign enters: a coalgebra morphism of a bar construction has degree zero, so this ungraded correspondence is the one describing A∞ morphisms through their components f_n.

Main definitions

• TauCeti.ReducedTensorWords.IsCoalgHom: a linear map commuting with reduced deconcatenation.
• TauCeti.ReducedTensorWords.coalgHom: the coalgebra morphism with prescribed Taylor components.
• TauCeti.ReducedTensorWords.coalgHomEquivTaylor: coalgebra morphisms are in bijection with their Taylor components.

Main results

• TauCeti.ReducedTensorWords.coalgHom_subword: the recursive evaluation rule of coalgHom f.
• TauCeti.ReducedTensorWords.isCoalgHom_coalgHom and TauCeti.ReducedTensorWords.letter_comp_coalgHom: coalgHom f is a coalgebra morphism with Taylor components f.
• TauCeti.ReducedTensorWords.IsCoalgHom.eq_of_letter_comp_eq: a coalgebra morphism is determined by its Taylor components.
• TauCeti.ReducedTensorWords.coalgHom_comp_letter: the letterwise map of a linear map is the coalgebra morphism whose only nonzero Taylor component is that map in arity one.
• TauCeti.ReducedTensorWords.IsCoalgHom.mem_filtration: a coalgebra morphism does not increase tensor length.
• TauCeti.ReducedTensorWords.IsCoalgHom.bijective_of_letter_comp_comp_ofLetter_bijective: a coalgebra morphism with bijective arity-one component is bijective, and TauCeti.ReducedTensorWords.IsCoalgHom.linearEquiv_symm: the inverse of a bijective coalgebra morphism is a coalgebra morphism.

References

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

noncomputable def TauCeti.ReducedTensorWords.coalgHom (R : Type uR) {M : Type uM} {N : Type uN} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (f : ReducedTensorWords R M →ₗ[R] N) : ReducedTensorWords R M →ₗ[R] ReducedTensorWords R N

The coalgebra morphism of reduced tensor coalgebras with Taylor components f: it sends a word x₁ ⋯ xₙ to the sum, over all ways of cutting it into consecutive nonempty blocks B₁ ⋯ B_k, of the word f(B₁) ⋯ f(B_k).

Equations

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

theorem TauCeti.ReducedTensorWords.coalgHom_subword {R : Type uR} {M : Type uM} {N : Type uN} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (f : ReducedTensorWords R M →ₗ[R] N) {n : ℕ} (x : Fin n → M) (a b : ℕ) : (coalgHom R f) (subword R x a b) = (ofLetter R N) (f (subword R x a b)) + ∑ d ∈ Finset.range b, ((prepend R N) (f (subword R x a d))) ((coalgHom R f) (subword R x (a + d) (b - d)))

The recursive evaluation rule of coalgHom f on a block of a tensor word: either the whole block is collapsed to the single letter f(B), or a nonempty first block of d letters is collapsed and prepended to the expansion of the rest. The summand d = 0 vanishes.

@[simp]

theorem TauCeti.ReducedTensorWords.letter_comp_coalgHom {R : Type uR} {M : Type uM} {N : Type uN} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (f : ReducedTensorWords R M →ₗ[R] N) : letter R N ∘ₗ coalgHom R f = f

The Taylor expansion of f has Taylor components f: every word it produces from more than one block has length at least two.

@[simp]

theorem TauCeti.ReducedTensorWords.coalgHom_ofLetter {R : Type uR} {M : Type uM} {N : Type uN} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (f : ReducedTensorWords R M →ₗ[R] N) (a : M) : (coalgHom R f) ((ofLetter R M) a) = (ofLetter R N) (f ((ofLetter R M) a))

On a single letter, coalgHom f is the single letter given by the arity-one component.

def TauCeti.ReducedTensorWords.IsCoalgHom (R : Type uR) {M : Type uM} {N : Type uN} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (F : ReducedTensorWords R M →ₗ[R] ReducedTensorWords R N) : Prop

A linear map of reduced tensor coalgebras is a coalgebra morphism when it commutes with reduced deconcatenation: cutting its value is the same as cutting first and mapping both halves.

Equations

• TauCeti.ReducedTensorWords.IsCoalgHom R F = (TauCeti.ReducedTensorWords.deconcatenation R N ∘ₗ F = TensorProduct.map F F ∘ₗ TauCeti.ReducedTensorWords.deconcatenation R M)

theorem TauCeti.ReducedTensorWords.isCoalgHom_iff {R : Type uR} {M : Type uM} {N : Type uN} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {F : ReducedTensorWords R M →ₗ[R] ReducedTensorWords R N} : IsCoalgHom R F ↔ deconcatenation R N ∘ₗ F = TensorProduct.map F F ∘ₗ deconcatenation R M

The defining identity of a coalgebra morphism, as a reusable Iff: this exposes the body of IsCoalgHom to consumers in other modules, for which the definition's body is not exposed.

theorem TauCeti.ReducedTensorWords.IsCoalgHom.deconcatenation_apply {R : Type uR} {M : Type uM} {N : Type uN} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {F : ReducedTensorWords R M →ₗ[R] ReducedTensorWords R N} (hF : IsCoalgHom R F) (z : ReducedTensorWords R M) : (deconcatenation R N) (F z) = (TensorProduct.map F F) ((deconcatenation R M) z)

The defining identity of a coalgebra morphism, applied to an element.

theorem TauCeti.ReducedTensorWords.isCoalgHom_coalgHom {R : Type uR} {M : Type uM} {N : Type uN} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (f : ReducedTensorWords R M →ₗ[R] N) : IsCoalgHom R (coalgHom R f)

The Taylor expansion coalgHom f is a coalgebra morphism.

theorem TauCeti.ReducedTensorWords.IsCoalgHom.eq_of_letter_comp_eq {R : Type uR} {M : Type uM} {N : Type uN} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {F₁ F₂ : ReducedTensorWords R M →ₗ[R] ReducedTensorWords R N} (h₁ : IsCoalgHom R F₁) (h₂ : IsCoalgHom R F₂) (hl : letter R N ∘ₗ F₁ = letter R N ∘ₗ F₂) : F₁ = F₂

A coalgebra morphism of reduced tensor coalgebras is determined by its Taylor components, that is by its composite with the projection onto single letters. Two coalgebra morphisms agreeing there agree on every tensor word, by induction along the conilpotence filtration.

theorem TauCeti.ReducedTensorWords.IsCoalgHom.eq_coalgHom {R : Type uR} {M : Type uM} {N : Type uN} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {F : ReducedTensorWords R M →ₗ[R] ReducedTensorWords R N} (hF : IsCoalgHom R F) : F = coalgHom R (letter R N ∘ₗ F)

A coalgebra morphism is the Taylor expansion of its own Taylor components.

noncomputable def TauCeti.ReducedTensorWords.coalgHomEquivTaylor (R : Type uR) (M : Type uM) (N : Type uN) [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] : { F : ReducedTensorWords R M →ₗ[R] ReducedTensorWords R N // IsCoalgHom R F } ≃ (ReducedTensorWords R M →ₗ[R] N)

Coalgebra morphisms of reduced tensor coalgebras are in bijection with their Taylor components, the linear maps from tensor words to letters.

Its body is sealed; reason about it through TauCeti.ReducedTensorWords.coalgHomEquivTaylor_apply and TauCeti.ReducedTensorWords.coalgHomEquivTaylor_symm_apply.

Equations

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

@[simp]

theorem TauCeti.ReducedTensorWords.coalgHomEquivTaylor_apply {R : Type uR} {M : Type uM} {N : Type uN} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (F : { F : ReducedTensorWords R M →ₗ[R] ReducedTensorWords R N // IsCoalgHom R F }) : (coalgHomEquivTaylor R M N) F = letter R N ∘ₗ ↑F

@[simp]

theorem TauCeti.ReducedTensorWords.coalgHomEquivTaylor_symm_apply {R : Type uR} {M : Type uM} {N : Type uN} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (f : ReducedTensorWords R M →ₗ[R] N) : ↑((coalgHomEquivTaylor R M N).symm f) = coalgHom R f

theorem TauCeti.ReducedTensorWords.isCoalgHom_id {R : Type uR} (M : Type uM) [CommSemiring R] [AddCommMonoid M] [Module R M] : IsCoalgHom R LinearMap.id

The identity is a coalgebra morphism.

theorem TauCeti.ReducedTensorWords.IsCoalgHom.comp {R : Type uR} {M : Type uM} {N : Type uN} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {P : Type uP} [AddCommMonoid P] [Module R P] {G : ReducedTensorWords R N →ₗ[R] ReducedTensorWords R P} {F : ReducedTensorWords R M →ₗ[R] ReducedTensorWords R N} (hG : IsCoalgHom R G) (hF : IsCoalgHom R F) : IsCoalgHom R (G ∘ₗ F)

A composite of coalgebra morphisms is a coalgebra morphism.

theorem TauCeti.ReducedTensorWords.isCoalgHom_map {R : Type uR} {M : Type uM} {N : Type uN} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (g : M →ₗ[R] N) : IsCoalgHom R (map R g)

Applying a linear map to every letter is a coalgebra morphism.

@[simp]

theorem TauCeti.ReducedTensorWords.coalgHom_comp_letter {R : Type uR} {M : Type uM} {N : Type uN} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (g : M →ₗ[R] N) : coalgHom R (g ∘ₗ letter R M) = map R g

The letterwise map of g is the coalgebra morphism whose Taylor components are g in arity one and zero in every higher arity.

The length filtration and bijectivity

A coalgebra morphism of reduced tensor coalgebras never increases tensor length, and it is bijective as soon as its arity-one Taylor component is. The proof reduces, by correcting with the letterwise inverse of that component, to a coalgebra endomorphism fixing every single letter; such an endomorphism differs from the identity by a map lowering the length filtration, hence is bijective by induction along the filtration.

theorem TauCeti.ReducedTensorWords.coalgHom_subword_mem_filtration {R : Type uR} {M : Type uM} {N : Type uN} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (f : ReducedTensorWords R M →ₗ[R] N) {n : ℕ} (x : Fin n → M) (a b : ℕ) : (coalgHom R f) (subword R x a b) ∈ filtration R N b

The Taylor expansion of f does not increase tensor length: it sends a block of b letters into the words of length at most b.

theorem TauCeti.ReducedTensorWords.coalgHom_mem_filtration {R : Type uR} {M : Type uM} {N : Type uN} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (f : ReducedTensorWords R M →ₗ[R] N) {n : ℕ} {z : ReducedTensorWords R M} (hz : z ∈ filtration R M n) : (coalgHom R f) z ∈ filtration R N n

The Taylor expansion of f preserves the conilpotence filtration.

theorem TauCeti.ReducedTensorWords.IsCoalgHom.mem_filtration {R : Type uR} {M : Type uM} {N : Type uN} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {F : ReducedTensorWords R M →ₗ[R] ReducedTensorWords R N} (hF : IsCoalgHom R F) {n : ℕ} {z : ReducedTensorWords R M} (hz : z ∈ filtration R M n) : F z ∈ filtration R N n

A coalgebra morphism preserves the conilpotence filtration.

theorem TauCeti.ReducedTensorWords.IsCoalgHom.apply_ofLetter {R : Type uR} {M : Type uM} {N : Type uN} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {F : ReducedTensorWords R M →ₗ[R] ReducedTensorWords R N} (hF : IsCoalgHom R F) (a : M) : F ((ofLetter R M) a) = (ofLetter R N) ((letter R N) (F ((ofLetter R M) a)))

A coalgebra morphism sends a single letter to the single letter given by its arity-one Taylor component.

theorem TauCeti.ReducedTensorWords.IsCoalgHom.linearEquiv_symm {R : Type uR} {M : Type uM} {N : Type uN} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {e : ReducedTensorWords R M ≃ₗ[R] ReducedTensorWords R N} (he : IsCoalgHom R ↑e) : IsCoalgHom R ↑e.symm

The inverse of a linear equivalence of reduced tensor coalgebras which is a coalgebra morphism is again a coalgebra morphism.

theorem TauCeti.ReducedTensorWords.IsCoalgHom.letter_comp_comp_ofLetter_bijective {R : Type uR} {M : Type uM} {N : Type uN} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {e : ReducedTensorWords R M ≃ₗ[R] ReducedTensorWords R N} (he : IsCoalgHom R ↑e) : Function.Bijective ⇑(letter R N ∘ₗ ↑e ∘ₗ ofLetter R M)

The arity-one Taylor component of a linear equivalence of reduced tensor coalgebras which is a coalgebra morphism is bijective, with inverse the arity-one component of the inverse.

theorem TauCeti.ReducedTensorWords.IsCoalgHom.map_symm_comp_comp_ofLetter {R : Type uR} {M : Type uM} {N : Type uN} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {F : ReducedTensorWords R M →ₗ[R] ReducedTensorWords R N} (hF : IsCoalgHom R F) (hf : Function.Bijective ⇑(letter R N ∘ₗ F ∘ₗ ofLetter R M)) : (map R ↑(LinearEquiv.ofBijective (letter R N ∘ₗ F ∘ₗ ofLetter R M) hf).symm ∘ₗ F) ∘ₗ ofLetter R M = ofLetter R M

Correcting a coalgebra morphism with bijective arity-one component by the letterwise inverse of that component yields a coalgebra endomorphism fixing every single letter.

theorem TauCeti.ReducedTensorWords.IsCoalgHom.sub_subword_mem_filtration {R : Type uR} {M : Type uM} [CommRing R] [AddCommGroup M] [Module R M] {G : ReducedTensorWords R M →ₗ[R] ReducedTensorWords R M} (hG : IsCoalgHom R G) (h₁ : G ∘ₗ ofLetter R M = ofLetter R M) {l : ℕ} (x : Fin l → M) (a b : ℕ) : G (subword R x a b) - subword R x a b ∈ filtration R M (b - 1)

A coalgebra endomorphism of the reduced tensor coalgebra fixing every single letter moves a block of b letters by a word of length at most b - 1.

theorem TauCeti.ReducedTensorWords.IsCoalgHom.sub_mem_filtration {R : Type uR} {M : Type uM} [CommRing R] [AddCommGroup M] [Module R M] {G : ReducedTensorWords R M →ₗ[R] ReducedTensorWords R M} (hG : IsCoalgHom R G) (h₁ : G ∘ₗ ofLetter R M = ofLetter R M) {n : ℕ} {z : ReducedTensorWords R M} (hz : z ∈ filtration R M (n + 1)) : G z - z ∈ filtration R M n

A coalgebra endomorphism of the reduced tensor coalgebra fixing every single letter moves a word of length at most n + 1 by a word of length at most n: it is the identity plus a map lowering the length filtration.

theorem TauCeti.ReducedTensorWords.IsCoalgHom.bijective_of_comp_ofLetter_eq {R : Type uR} {M : Type uM} [CommRing R] [AddCommGroup M] [Module R M] {G : ReducedTensorWords R M →ₗ[R] ReducedTensorWords R M} (hG : IsCoalgHom R G) (h₁ : G ∘ₗ ofLetter R M = ofLetter R M) : Function.Bijective ⇑G

A coalgebra endomorphism of the reduced tensor coalgebra fixing every single letter is bijective.

theorem TauCeti.ReducedTensorWords.IsCoalgHom.map_eq_of_map_le {R : Type uR} {M : Type uM} [CommRing R] [AddCommGroup M] [Module R M] {G : ReducedTensorWords R M →ₗ[R] ReducedTensorWords R M} (hG : IsCoalgHom R G) (h₁ : G ∘ₗ ofLetter R M = ofLetter R M) {p : Submodule R (ReducedTensorWords R M)} (hp : Submodule.map G p ≤ p) : Submodule.map G p = p

A coalgebra endomorphism of the reduced tensor coalgebra fixing every single letter maps every submodule it preserves onto itself.

theorem TauCeti.ReducedTensorWords.IsCoalgHom.bijective_of_letter_comp_comp_ofLetter_bijective {R : Type uR} {M : Type uM} {N : Type uN} [CommRing R] [AddCommGroup M] [Module R M] [AddCommMonoid N] [Module R N] {F : ReducedTensorWords R M →ₗ[R] ReducedTensorWords R N} (hF : IsCoalgHom R F) (hf : Function.Bijective ⇑(letter R N ∘ₗ F ∘ₗ ofLetter R M)) : Function.Bijective ⇑F

A coalgebra morphism of reduced tensor coalgebras whose arity-one Taylor component is bijective is bijective.