Signed substitution of dependent graded multilinear maps

Substituting homogeneous operations gᵢ into an operation f uses the tensor-map Koszul rule. The operation gᵢ crosses all inputs belonging to earlier blocks. Here the outer slots are ordered by Fin n, while the input modules and the finite slot type of each inner operation may vary with the block. In particular, these modules can be Hom modules along composable strings in a graded linear quiver.

InternalGrading.signedCompMultilinearMap constructs this substitution on the total modules, not only on a specified tuple of degrees. It precomposes each input by the existing Koszul twist for the sum of the degrees of the operations to its right. The stored homogeneity of f and each gᵢ ensures that the degree parameters actually describe those operations. The result has degree deg f + ∑ᵢ deg gᵢ. Its homogeneous evaluation formula gives the exact Koszul sign, including the one-slot case, where a degree-q operation crosses the prefix.

The flattened input index is a dependent sum. Mathlib's domDomCongrLinearEquiv' and LinearEquiv.multilinearMapCongrLeft provide reindexing and coordinate changes without an interface based on equality casts. Empty input blocks are allowed.

The construction uses Mathlib's dependent MultilinearMap.compMultilinearMap and the homogeneous multilinear-map API of TauCeti.LinearAlgebra.Graded.Multilinear.

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.1 and 7.1.

noncomputable def TauCeti.InternalGrading.signedCompMultilinearMap {R : Type uR} [CommRing R] {n : ℕ} {β : Fin n → Type uβ} [(i : Fin n) → Fintype (β i)] {M : (i : Fin n) → β i → Type uM} {P : Fin n → Type uP} {N : Type uN} [(i : Fin n) → (j : β i) → AddCommMonoid (M i j)] [(i : Fin n) → (j : β i) → Module R (M i j)] [(i : Fin n) → AddCommMonoid (P i)] [(i : Fin n) → Module R (P i)] [AddCommMonoid N] [Module R N] (G : (i : Fin n) → (j : β i) → InternalGrading R (M i j)) (H : (i : Fin n) → ℤ → Submodule R (P i)) (ℬ : ℤ → Submodule R N) {p : ℤ} {q : Fin n → ℤ} (f : ↥(MultilinearMap.homogeneousSubmodule H ℬ p)) (g : (i : Fin n) → ↥(MultilinearMap.homogeneousSubmodule (fun (j : β i) => (G i j).piece) (H i) (q i))) : ↥(MultilinearMap.homogeneousSubmodule (fun (ij : (i : Fin n) × β i) => (G ij.fst ij.snd).piece) ℬ (∑ i : Fin n, q i + p))

Simultaneous Koszul-signed substitution of homogeneous multilinear maps with dependent input modules. Each input in block i is twisted by the sum of the degrees of operations in later blocks. The output degree is the sum of all inner degrees plus the outer degree.

Equations

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

theorem TauCeti.InternalGrading.signedCompMultilinearMap_val {R : Type uR} [CommRing R] {n : ℕ} {β : Fin n → Type uβ} [(i : Fin n) → Fintype (β i)] {M : (i : Fin n) → β i → Type uM} {P : Fin n → Type uP} {N : Type uN} [(i : Fin n) → (j : β i) → AddCommMonoid (M i j)] [(i : Fin n) → (j : β i) → Module R (M i j)] [(i : Fin n) → AddCommMonoid (P i)] [(i : Fin n) → Module R (P i)] [AddCommMonoid N] [Module R N] (G : (i : Fin n) → (j : β i) → InternalGrading R (M i j)) (H : (i : Fin n) → ℤ → Submodule R (P i)) (ℬ : ℤ → Submodule R N) {p : ℤ} {q : Fin n → ℤ} (f : ↥(MultilinearMap.homogeneousSubmodule H ℬ p)) (g : (i : Fin n) → ↥(MultilinearMap.homogeneousSubmodule (fun (j : β i) => (G i j).piece) (H i) (q i))) : ↑(signedCompMultilinearMap G H ℬ f g) = ((↑f).compMultilinearMap fun (i : Fin n) => ↑(g i)).compLinearMap fun (ij : (i : Fin n) × β i) => (G ij.fst ij.snd).koszulTwist (∑ k : Fin n, if ij.fst < k then q k else 0)

The underlying map is ordinary dependent substitution precomposed with Koszul twists.

theorem TauCeti.InternalGrading.signedCompMultilinearMap_apply {R : Type uR} [CommRing R] {n : ℕ} {β : Fin n → Type uβ} [(i : Fin n) → Fintype (β i)] {M : (i : Fin n) → β i → Type uM} {P : Fin n → Type uP} {N : Type uN} [(i : Fin n) → (j : β i) → AddCommMonoid (M i j)] [(i : Fin n) → (j : β i) → Module R (M i j)] [(i : Fin n) → AddCommMonoid (P i)] [(i : Fin n) → Module R (P i)] [AddCommMonoid N] [Module R N] (G : (i : Fin n) → (j : β i) → InternalGrading R (M i j)) (H : (i : Fin n) → ℤ → Submodule R (P i)) (ℬ : ℤ → Submodule R N) {p : ℤ} {q : Fin n → ℤ} (f : ↥(MultilinearMap.homogeneousSubmodule H ℬ p)) (g : (i : Fin n) → ↥(MultilinearMap.homogeneousSubmodule (fun (j : β i) => (G i j).piece) (H i) (q i))) (d : (i : Fin n) × β i → ℤ) (x : (ij : (i : Fin n) × β i) → M ij.fst ij.snd) (hx : ∀ (ij : (i : Fin n) × β i), x ij ∈ (G ij.fst ij.snd).piece (d ij)) : ↑(signedCompMultilinearMap G H ℬ f g) x = negOnePowCast R (∑ ij : (i : Fin n) × β i, (∑ k : Fin n, if ij.fst < k then q k else 0) * d ij) • ↑f fun (i : Fin n) => ↑(g i) fun (j : β i) => x ⟨i, j⟩

On homogeneous inputs, each later operation crosses every earlier input. This formula uses actual input degrees, not degrees supplied independently of the inputs.

theorem TauCeti.InternalGrading.signedCompMultilinearMap_apply_eq_prefix_sign {R : Type uR} [CommRing R] {n : ℕ} {β : Fin n → Type uβ} [(i : Fin n) → Fintype (β i)] {M : (i : Fin n) → β i → Type uM} {P : Fin n → Type uP} {N : Type uN} [(i : Fin n) → (j : β i) → AddCommMonoid (M i j)] [(i : Fin n) → (j : β i) → Module R (M i j)] [(i : Fin n) → AddCommMonoid (P i)] [(i : Fin n) → Module R (P i)] [AddCommMonoid N] [Module R N] (G : (i : Fin n) → (j : β i) → InternalGrading R (M i j)) (H : (i : Fin n) → ℤ → Submodule R (P i)) (ℬ : ℤ → Submodule R N) {p : ℤ} {q : Fin n → ℤ} (f : ↥(MultilinearMap.homogeneousSubmodule H ℬ p)) (g : (i : Fin n) → ↥(MultilinearMap.homogeneousSubmodule (fun (j : β i) => (G i j).piece) (H i) (q i))) (d : (i : Fin n) × β i → ℤ) (x : (ij : (i : Fin n) × β i) → M ij.fst ij.snd) (hx : ∀ (ij : (i : Fin n) × β i), x ij ∈ (G ij.fst ij.snd).piece (d ij)) : ↑(signedCompMultilinearMap G H ℬ f g) x = negOnePowCast R (∑ k : Fin n, q k * ∑ ij : (i : Fin n) × β i, if ij.fst < k then d ij else 0) • ↑f fun (i : Fin n) => ↑(g i) fun (j : β i) => x ⟨i, j⟩

The Koszul exponent can equivalently be summed over operations and their preceding blocks.

theorem TauCeti.InternalGrading.signedCompMultilinearMap_apply_of_single_degree {R : Type uR} [CommRing R] {n : ℕ} {β : Fin n → Type uβ} [(i : Fin n) → Fintype (β i)] {M : (i : Fin n) → β i → Type uM} {P : Fin n → Type uP} {N : Type uN} [(i : Fin n) → (j : β i) → AddCommMonoid (M i j)] [(i : Fin n) → (j : β i) → Module R (M i j)] [(i : Fin n) → AddCommMonoid (P i)] [(i : Fin n) → Module R (P i)] [AddCommMonoid N] [Module R N] (G : (i : Fin n) → (j : β i) → InternalGrading R (M i j)) (H : (i : Fin n) → ℤ → Submodule R (P i)) (ℬ : ℤ → Submodule R N) {p : ℤ} {q : Fin n → ℤ} (f : ↥(MultilinearMap.homogeneousSubmodule H ℬ p)) (g : (i : Fin n) → ↥(MultilinearMap.homogeneousSubmodule (fun (j : β i) => (G i j).piece) (H i) (q i))) (k : Fin n) (r : ℤ) (hq : q = fun (i : Fin n) => if i = k then r else 0) (d : (i : Fin n) × β i → ℤ) (x : (ij : (i : Fin n) × β i) → M ij.fst ij.snd) (hx : ∀ (ij : (i : Fin n) × β i), x ij ∈ (G ij.fst ij.snd).piece (d ij)) : ↑(signedCompMultilinearMap G H ℬ f g) x = negOnePowCast R (r * ∑ ij : (i : Fin n) × β i, if ij.fst < k then d ij else 0) • ↑f fun (i : Fin n) => ↑(g i) fun (j : β i) => x ⟨i, j⟩

Inserting one operation of degree r in slot k, with degree-zero operations in every other slot, gives precisely (-1)^(r * prefix degree). In particular, the other operations may be unary identity maps.

@[simp]

theorem TauCeti.InternalGrading.signedCompMultilinearMap_val_of_degree_zero {R : Type uR} [CommRing R] {n : ℕ} {β : Fin n → Type uβ} [(i : Fin n) → Fintype (β i)] {M : (i : Fin n) → β i → Type uM} {P : Fin n → Type uP} {N : Type uN} [(i : Fin n) → (j : β i) → AddCommMonoid (M i j)] [(i : Fin n) → (j : β i) → Module R (M i j)] [(i : Fin n) → AddCommMonoid (P i)] [(i : Fin n) → Module R (P i)] [AddCommMonoid N] [Module R N] (G : (i : Fin n) → (j : β i) → InternalGrading R (M i j)) (H : (i : Fin n) → ℤ → Submodule R (P i)) (ℬ : ℤ → Submodule R N) {p : ℤ} {q : Fin n → ℤ} (f : ↥(MultilinearMap.homogeneousSubmodule H ℬ p)) (g : (i : Fin n) → ↥(MultilinearMap.homogeneousSubmodule (fun (j : β i) => (G i j).piece) (H i) (q i))) (hq : q = 0) : ↑(signedCompMultilinearMap G H ℬ f g) = (↑f).compMultilinearMap fun (i : Fin n) => ↑(g i)

Substitution by degree-zero operations has no Koszul correction.

@[simp]

theorem TauCeti.InternalGrading.signedCompMultilinearMap_add {R : Type uR} [CommRing R] {n : ℕ} {β : Fin n → Type uβ} [(i : Fin n) → Fintype (β i)] {M : (i : Fin n) → β i → Type uM} {P : Fin n → Type uP} {N : Type uN} [(i : Fin n) → (j : β i) → AddCommMonoid (M i j)] [(i : Fin n) → (j : β i) → Module R (M i j)] [(i : Fin n) → AddCommMonoid (P i)] [(i : Fin n) → Module R (P i)] [AddCommMonoid N] [Module R N] (G : (i : Fin n) → (j : β i) → InternalGrading R (M i j)) (H : (i : Fin n) → ℤ → Submodule R (P i)) (ℬ : ℤ → Submodule R N) {p : ℤ} {q : Fin n → ℤ} (f : ↥(MultilinearMap.homogeneousSubmodule H ℬ p)) (g : (i : Fin n) → ↥(MultilinearMap.homogeneousSubmodule (fun (j : β i) => (G i j).piece) (H i) (q i))) (f' : ↥(MultilinearMap.homogeneousSubmodule H ℬ p)) : signedCompMultilinearMap G H ℬ (f + f') g = signedCompMultilinearMap G H ℬ f g + signedCompMultilinearMap G H ℬ f' g

Signed substitution is additive in the outer operation.

@[simp]

theorem TauCeti.InternalGrading.signedCompMultilinearMap_smul {R : Type uR} [CommRing R] {n : ℕ} {β : Fin n → Type uβ} [(i : Fin n) → Fintype (β i)] {M : (i : Fin n) → β i → Type uM} {P : Fin n → Type uP} {N : Type uN} [(i : Fin n) → (j : β i) → AddCommMonoid (M i j)] [(i : Fin n) → (j : β i) → Module R (M i j)] [(i : Fin n) → AddCommMonoid (P i)] [(i : Fin n) → Module R (P i)] [AddCommMonoid N] [Module R N] (G : (i : Fin n) → (j : β i) → InternalGrading R (M i j)) (H : (i : Fin n) → ℤ → Submodule R (P i)) (ℬ : ℤ → Submodule R N) {p : ℤ} {q : Fin n → ℤ} (f : ↥(MultilinearMap.homogeneousSubmodule H ℬ p)) (g : (i : Fin n) → ↥(MultilinearMap.homogeneousSubmodule (fun (j : β i) => (G i j).piece) (H i) (q i))) (c : R) : signedCompMultilinearMap G H ℬ (c • f) g = c • signedCompMultilinearMap G H ℬ f g

Signed substitution respects scalars in the outer operation.

@[simp]

theorem TauCeti.InternalGrading.signedCompMultilinearMap_zero {R : Type uR} [CommRing R] {n : ℕ} {β : Fin n → Type uβ} [(i : Fin n) → Fintype (β i)] {M : (i : Fin n) → β i → Type uM} {P : Fin n → Type uP} {N : Type uN} [(i : Fin n) → (j : β i) → AddCommMonoid (M i j)] [(i : Fin n) → (j : β i) → Module R (M i j)] [(i : Fin n) → AddCommMonoid (P i)] [(i : Fin n) → Module R (P i)] [AddCommMonoid N] [Module R N] (G : (i : Fin n) → (j : β i) → InternalGrading R (M i j)) (H : (i : Fin n) → ℤ → Submodule R (P i)) (ℬ : ℤ → Submodule R N) {p : ℤ} {q : Fin n → ℤ} (g : (i : Fin n) → ↥(MultilinearMap.homogeneousSubmodule (fun (j : β i) => (G i j).piece) (H i) (q i))) : signedCompMultilinearMap G H ℬ 0 g = 0

Substituting the zero outer operation gives zero.

theorem TauCeti.InternalGrading.signedCompMultilinearMap_update_add {R : Type uR} [CommRing R] {n : ℕ} {β : Fin n → Type uβ} [(i : Fin n) → Fintype (β i)] {M : (i : Fin n) → β i → Type uM} {P : Fin n → Type uP} {N : Type uN} [(i : Fin n) → (j : β i) → AddCommMonoid (M i j)] [(i : Fin n) → (j : β i) → Module R (M i j)] [(i : Fin n) → AddCommMonoid (P i)] [(i : Fin n) → Module R (P i)] [AddCommMonoid N] [Module R N] (G : (i : Fin n) → (j : β i) → InternalGrading R (M i j)) (H : (i : Fin n) → ℤ → Submodule R (P i)) (ℬ : ℤ → Submodule R N) {p : ℤ} {q : Fin n → ℤ} (f : ↥(MultilinearMap.homogeneousSubmodule H ℬ p)) (g : (i : Fin n) → ↥(MultilinearMap.homogeneousSubmodule (fun (j : β i) => (G i j).piece) (H i) (q i))) (k : Fin n) (a b : ↥(MultilinearMap.homogeneousSubmodule (fun (j : β k) => (G k j).piece) (H k) (q k))) : signedCompMultilinearMap G H ℬ f (Function.update g k (a + b)) = signedCompMultilinearMap G H ℬ f (Function.update g k a) + signedCompMultilinearMap G H ℬ f (Function.update g k b)

Signed substitution is additive in each inner operation separately.

theorem TauCeti.InternalGrading.signedCompMultilinearMap_update_smul {R : Type uR} [CommRing R] {n : ℕ} {β : Fin n → Type uβ} [(i : Fin n) → Fintype (β i)] {M : (i : Fin n) → β i → Type uM} {P : Fin n → Type uP} {N : Type uN} [(i : Fin n) → (j : β i) → AddCommMonoid (M i j)] [(i : Fin n) → (j : β i) → Module R (M i j)] [(i : Fin n) → AddCommMonoid (P i)] [(i : Fin n) → Module R (P i)] [AddCommMonoid N] [Module R N] (G : (i : Fin n) → (j : β i) → InternalGrading R (M i j)) (H : (i : Fin n) → ℤ → Submodule R (P i)) (ℬ : ℤ → Submodule R N) {p : ℤ} {q : Fin n → ℤ} (f : ↥(MultilinearMap.homogeneousSubmodule H ℬ p)) (g : (i : Fin n) → ↥(MultilinearMap.homogeneousSubmodule (fun (j : β i) => (G i j).piece) (H i) (q i))) (k : Fin n) (c : R) (a : ↥(MultilinearMap.homogeneousSubmodule (fun (j : β k) => (G k j).piece) (H k) (q k))) : signedCompMultilinearMap G H ℬ f (Function.update g k (c • a)) = c • signedCompMultilinearMap G H ℬ f (Function.update g k a)

Signed substitution respects scalars in each inner operation separately.

@[simp]

theorem TauCeti.InternalGrading.signedCompMultilinearMap_update_zero {R : Type uR} [CommRing R] {n : ℕ} {β : Fin n → Type uβ} [(i : Fin n) → Fintype (β i)] {M : (i : Fin n) → β i → Type uM} {P : Fin n → Type uP} {N : Type uN} [(i : Fin n) → (j : β i) → AddCommMonoid (M i j)] [(i : Fin n) → (j : β i) → Module R (M i j)] [(i : Fin n) → AddCommMonoid (P i)] [(i : Fin n) → Module R (P i)] [AddCommMonoid N] [Module R N] (G : (i : Fin n) → (j : β i) → InternalGrading R (M i j)) (H : (i : Fin n) → ℤ → Submodule R (P i)) (ℬ : ℤ → Submodule R N) {p : ℤ} {q : Fin n → ℤ} (f : ↥(MultilinearMap.homogeneousSubmodule H ℬ p)) (g : (i : Fin n) → ↥(MultilinearMap.homogeneousSubmodule (fun (j : β i) => (G i j).piece) (H i) (q i))) (k : Fin n) : signedCompMultilinearMap G H ℬ f (Function.update g k 0) = 0

If any inner operation is zero, the signed substitution is zero.