Signed insertion of graded multilinear maps

This file defines one-slot substitution of multilinear maps. The inputs are split into a prefix, the block consumed by the inserted map, and a suffix. Using sum types for these three blocks keeps the evaluation rule definitional and avoids transports between propositionally equal finite arities.

For graded maps, inserting a map of degree q after homogeneous prefix inputs of degrees d i contributes the Koszul coefficient

(-1) ^ (q * ∑ i, d i).

The signed operation takes the intended degrees of the homogeneous prefix inputs as an explicit parameter. The API does not enforce that these degrees correspond to the inputs; on the intended component the sign is a scalar, so the result is again a multilinear map. The homogeneity theorem proves that insertion adds the degrees of the outer and inner operations.

Main definitions

• MultilinearMap.evalNat: evaluate a finite-arity map on a natural-indexed input family.
• TauCeti.replaceBlock: collapse a consecutive block in a natural-indexed family.
• Fin.blockEquiv and Fin.oneSlotEquiv: canonical reindexings for one-slot substitution.
• MultilinearMap.oneSlot: substitute one multilinear map into a specified block of another.
• MultilinearMap.koszulSign: the sign acquired by crossing the prefix inputs.
• MultilinearMap.signedOneSlot: one-slot substitution scaled by the Koszul sign for supplied prefix degrees, correct when the prefix inputs have those degrees.

References

• Ezra Getzler and J. D. S. Jones, A-infinity algebras and the cyclic bar complex, Sections 1--2.
• Bernhard Keller, Introduction to A-infinity algebras and modules, Section 3.1.

def MultilinearMap.evalNat {R : Type uR} {M : Type uM} [Semiring R] [AddCommMonoid M] [Module R M] {k : ℕ} {N : Type uN} [AddCommMonoid N] [Module R N] (f : MultilinearMap R (fun (x : Fin k) => M) N) (x : ℕ → M) : N

Evaluate an arity-k operation on the first k entries of a family indexed by the naturals.

Equations

• f.evalNat x = f fun (i : Fin k) => x ↑i

theorem MultilinearMap.evalNat_def {R : Type uR} {M : Type uM} [Semiring R] [AddCommMonoid M] [Module R M] {k : ℕ} {N : Type uN} [AddCommMonoid N] [Module R N] (f : MultilinearMap R (fun (x : Fin k) => M) N) (x : ℕ → M) : f.evalNat x = f fun (i : Fin k) => x ↑i

theorem MultilinearMap.evalNat_congr {R : Type uR} {M : Type uM} [Semiring R] [AddCommMonoid M] [Module R M] {k : ℕ} {N : Type uN} [AddCommMonoid N] [Module R N] (f : MultilinearMap R (fun (x : Fin k) => M) N) {x y : ℕ → M} (h : ∀ i < k, x i = y i) : f.evalNat x = f.evalNat y

evalNat only reads the entries whose indices are below the operation's arity.

@[simp]

theorem MultilinearMap.evalNat_smul {R : Type uR} {M : Type uM} [Semiring R] [AddCommMonoid M] [Module R M] {k : ℕ} {N : Type uN} [AddCommMonoid N] [Module R N] [SMulCommClass R R N] (c : R) (f : MultilinearMap R (fun (x : Fin k) => M) N) (x : ℕ → M) : (c • f).evalNat x = c • f.evalNat x

@[simp]

theorem MultilinearMap.evalNat_one {R : Type uR} {M : Type uM} [Semiring R] [AddCommMonoid M] [Module R M] {N : Type uN} [AddCommMonoid N] [Module R N] (f : MultilinearMap R (fun (x : Fin 1) => M) N) (x : ℕ → M) : f.evalNat x = f ![x 0]

@[simp]

theorem MultilinearMap.evalNat_two {R : Type uR} {M : Type uM} [Semiring R] [AddCommMonoid M] [Module R M] {N : Type uN} [AddCommMonoid N] [Module R N] (f : MultilinearMap R (fun (x : Fin 2) => M) N) (x : ℕ → M) : f.evalNat x = f ![x 0, x 1]

@[simp]

theorem MultilinearMap.evalNat_three {R : Type uR} {M : Type uM} [Semiring R] [AddCommMonoid M] [Module R M] {N : Type uN} [AddCommMonoid N] [Module R N] (f : MultilinearMap R (fun (x : Fin 3) => M) N) (x : ℕ → M) : f.evalNat x = f ![x 0, x 1, x 2]

@[simp]

theorem MultilinearMap.evalNat_four {R : Type uR} {M : Type uM} [Semiring R] [AddCommMonoid M] [Module R M] {N : Type uN} [AddCommMonoid N] [Module R N] (f : MultilinearMap R (fun (x : Fin 4) => M) N) (x : ℕ → M) : f.evalNat x = f ![x 0, x 1, x 2, x 3]

def MultilinearMap.oneSlot {R : Type uR} {M : Type uM} {N : Type uN} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {α : Type uα} {β : Type uβ} {γ : Type uγ} (f : MultilinearMap R (fun (x : α ⊕ Unit ⊕ γ) => M) N) (g : MultilinearMap R (fun (x : β) => M) M) : MultilinearMap R (fun (x : α ⊕ β ⊕ γ) => M) N

Substitute g into the middle input of f.

The domain is divided into prefix inputs α, the inputs β consumed by g, and suffix inputs γ. Correspondingly, f has prefix inputs, one middle input, and suffix inputs.

Equations

• f.oneSlot g = MultilinearMap.domDomCongr (MultilinearMap.oneSlotIndexEquiv✝ α β γ) (f.compMultilinearMap (MultilinearMap.oneSlotMaps✝ g))

@[simp]

theorem MultilinearMap.oneSlot_apply {R : Type uR} {M : Type uM} {N : Type uN} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {α : Type uα} {β : Type uβ} {γ : Type uγ} (f : MultilinearMap R (fun (x : α ⊕ Unit ⊕ γ) => M) N) (g : MultilinearMap R (fun (x : β) => M) M) (x : α ⊕ β ⊕ γ → M) : (f.oneSlot g) x = f (Sum.elim (fun (i : α) => x (Sum.inl i)) (Sum.elim (fun (x_1 : Unit) => g fun (j : β) => x (Sum.inr (Sum.inl j))) fun (i : γ) => x (Sum.inr (Sum.inr i))))

Evaluating oneSlot f g substitutes the value of g on the middle block between the unchanged prefix and suffix inputs of f.

def TauCeti.replaceBlock {α : Type u_1} (x : ℕ → α) (p s : ℕ) (v : α) : ℕ → α

Replace the block of s entries at position p of a natural-indexed family by v.

Equations

• TauCeti.replaceBlock x p s v i = if i < p then x i else if i = p then v else x (i + s - 1)

@[simp]

theorem TauCeti.replaceBlock_of_lt {α : Type u_1} (x : ℕ → α) (p s : ℕ) (v : α) {i : ℕ} (h : i < p) : replaceBlock x p s v i = x i

@[simp]

theorem TauCeti.replaceBlock_self {α : Type u_1} (x : ℕ → α) (p s : ℕ) (v : α) : replaceBlock x p s v p = v

@[simp]

theorem TauCeti.replaceBlock_of_gt {α : Type u_1} (x : ℕ → α) (p s : ℕ) (v : α) {i : ℕ} (h : p < i) : replaceBlock x p s v i = x (i + s - 1)

theorem TauCeti.apply_replaceBlock {α : Type u_1} {β : Type u_2} (g : α → β) (x : ℕ → α) (p s : ℕ) (v : α) (i : ℕ) : g (replaceBlock x p s v i) = replaceBlock (fun (j : ℕ) => g (x j)) p s (g v) i

A function applied entrywise commutes with replacing a block of entries.

def Fin.blockEquiv (p s t : ℕ) : Fin p ⊕ Fin s ⊕ Fin t ≃ Fin (p + s + t)

Identify a prefix, inserted block, and suffix with their total finite arity.

Equations

• Fin.blockEquiv p s t = ((Equiv.refl (Fin p)).sumCongr finSumFinEquiv).trans (finSumFinEquiv.trans (finCongr ⋯))

@[simp]

theorem Fin.blockEquiv_inl_val (p s t : ℕ) (i : Fin p) : ↑((blockEquiv p s t) (Sum.inl i)) = ↑i

@[simp]

theorem Fin.blockEquiv_middle_val (p s t : ℕ) (j : Fin s) : ↑((blockEquiv p s t) (Sum.inr (Sum.inl j))) = p + ↑j

@[simp]

theorem Fin.blockEquiv_suffix_val (p s t : ℕ) (j : Fin t) : ↑((blockEquiv p s t) (Sum.inr (Sum.inr j))) = p + s + ↑j

def Fin.oneSlotEquiv (p t : ℕ) : Fin p ⊕ Unit ⊕ Fin t ≃ Fin (p + 1 + t)

Identify a prefix, one collapsed slot, and suffix with their total finite arity.

Equations

• Fin.oneSlotEquiv p t = ((Equiv.refl (Fin p)).sumCongr (finOneEquiv.symm.sumCongr (Equiv.refl (Fin t)))).trans (Fin.blockEquiv p 1 t)

@[simp]

theorem Fin.oneSlotEquiv_inl_val (p t : ℕ) (i : Fin p) : ↑((oneSlotEquiv p t) (Sum.inl i)) = ↑i

@[simp]

theorem Fin.oneSlotEquiv_middle_val (p t : ℕ) : ↑((oneSlotEquiv p t) (Sum.inr (Sum.inl ()))) = p

@[simp]

theorem Fin.oneSlotEquiv_suffix_val (p t : ℕ) (j : Fin t) : ↑((oneSlotEquiv p t) (Sum.inr (Sum.inr j))) = p + 1 + ↑j

theorem TauCeti.MultilinearMap.IsHomogeneous.oneSlot {R : Type uR} {M : Type uM} {N : Type uN} {ι : Type u_1} [Semiring R] [AddCommMonoid ι] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {σM : Type u_2} {σN : Type u_3} [SetLike σM M] [SetLike σN N] {α : Type uα} {β : Type uβ} {γ : Type uγ} [Fintype α] [Fintype β] [Fintype γ] {f : MultilinearMap R (fun (x : α ⊕ Unit ⊕ γ) => M) N} {g : MultilinearMap R (fun (x : β) => M) M} {A : α → ι → σM} {B : β → ι → σM} {C : γ → ι → σM} {D : ι → σM} {E : ι → σN} {p q : ι} (hf : IsHomogeneous f (Sum.elim A (Sum.elim (fun (x : Unit) => D) C)) E p) (hg : IsHomogeneous g B D q) : IsHomogeneous (f.oneSlot g) (Sum.elim A (Sum.elim B C)) E (q + p)

One-slot substitution adds the degree of the inserted map to the degree of the outer map.

def MultilinearMap.koszulSign {R : Type uR} [Ring R] {α : Type uα} [Fintype α] (q : ℤ) (d : α → ℤ) : R

The Koszul coefficient acquired when a degree-q operation crosses homogeneous inputs with degrees d i.

Equations

• MultilinearMap.koszulSign q d = TauCeti.negOnePowCast R (q * ∑ i : α, d i)

@[simp]

theorem MultilinearMap.koszulSign_eq_negOnePowCast {R : Type uR} [Ring R] {α : Type uα} [Fintype α] (q : ℤ) (d : α → ℤ) : koszulSign q d = TauCeti.negOnePowCast R (q * ∑ i : α, d i)

The Koszul coefficient is the ground-ring power of negative one.

theorem MultilinearMap.koszulSign_add_degree {R : Type uR} [Ring R] {α : Type uα} [Fintype α] (q q' : ℤ) (d : α → ℤ) : koszulSign (q + q') d = koszulSign q d * koszulSign q' d

def MultilinearMap.signedOneSlot {R : Type uR} [CommRing R] {M : Type uM} {N : Type uN} [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {α : Type uα} [Fintype α] {β : Type uβ} {γ : Type uγ} (q : ℤ) (d : α → ℤ) (f : MultilinearMap R (fun (x : α ⊕ Unit ⊕ γ) => M) N) (g : MultilinearMap R (fun (x : β) => M) M) : MultilinearMap R (fun (x : α ⊕ β ⊕ γ) => M) N

Signed one-slot substitution using d as the supplied degrees of the homogeneous prefix inputs.

The API does not enforce that d corresponds to the input components. On the intended component the sign is constant, so scalar multiplication preserves multilinearity.

Equations

• MultilinearMap.signedOneSlot q d f g = MultilinearMap.koszulSign q d • f.oneSlot g

@[simp]

theorem MultilinearMap.signedOneSlot_apply {R : Type uR} [CommRing R] {M : Type uM} {N : Type uN} [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {α : Type uα} [Fintype α] {β : Type uβ} {γ : Type uγ} (q : ℤ) (d : α → ℤ) (f : MultilinearMap R (fun (x : α ⊕ Unit ⊕ γ) => M) N) (g : MultilinearMap R (fun (x : β) => M) M) (x : α ⊕ β ⊕ γ → M) : (signedOneSlot q d f g) x = koszulSign q d • f (Sum.elim (fun (i : α) => x (Sum.inl i)) (Sum.elim (fun (x_1 : Unit) => g fun (j : β) => x (Sum.inr (Sum.inl j))) fun (i : γ) => x (Sum.inr (Sum.inr i))))

Evaluating signedOneSlot q d f g gives the one-slot substitution formula multiplied by the Koszul sign determined by q and the supplied prefix degrees d.

theorem TauCeti.MultilinearMap.IsHomogeneous.signedOneSlot {R : Type uR} {M : Type uM} {N : Type uN} [CommRing R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {σM : Type u_1} {σN : Type u_2} [SetLike σM M] [SetLike σN N] [SMulMemClass σN R N] {α : Type uα} {β : Type uβ} {γ : Type uγ} [Fintype α] [Fintype β] [Fintype γ] {f : MultilinearMap R (fun (x : α ⊕ Unit ⊕ γ) => M) N} {g : MultilinearMap R (fun (x : β) => M) M} {A : α → ℤ → σM} {B : β → ℤ → σM} {C : γ → ℤ → σM} {D : ℤ → σM} {E : ℤ → σN} {p q : ℤ} (d : α → ℤ) (hf : IsHomogeneous f (Sum.elim A (Sum.elim (fun (x : Unit) => D) C)) E p) (hg : IsHomogeneous g B D q) : IsHomogeneous (MultilinearMap.signedOneSlot q d f g) (Sum.elim A (Sum.elim B C)) E (q + p)

Signed one-slot substitution has the sum of the degrees of its two operations.