Homogeneous multilinear maps #
This file records the degree of a multilinear map between modules equipped with families of
graded subobjects. A multilinear map has degree q when it maps inputs lying in 𝒜 i (d i)
into ℬ ((∑ i, d i) + q); as in the linear case
(TauCeti.LinearAlgebra.Graded.LinearMap) this is a containment condition, so no direct-sum
hypothesis is imposed and a map can have several degrees at once.
The main results show that degrees add under composition, both for precomposition by a family of
linear maps and for simultaneous substitution of multilinear maps. The composition operations are
Mathlib's MultilinearMap.compLinearMap and MultilinearMap.compMultilinearMap; this file supplies
their unsigned degree calculations, which underlie signed substitution for DG and A∞ structures.
Main definitions #
MultilinearMap.IsHomogeneous: a multilinear map shifts the sum of its input degrees.MultilinearMap.homogeneousSubmodule: the submodule of multilinear maps of a fixed degree.
Main results #
MultilinearMap.IsHomogeneous.compLinearMap: precomposing the inputs by homogeneous linear maps adds their degrees to the degree of the multilinear map.MultilinearMap.IsHomogeneous.compMultilinearMap: simultaneously substituting homogeneous multilinear maps adds their degrees to the degree of the outer map; the composite is indexed by the sigma typeΣ i, β i.MultilinearMap.IsHomogeneous.domDomCongrLinearEquiv': reindexing the inputs along an equivalence preserves the degree, which turns a sigma-indexed composite into one of any equivalent arity.LinearMap.IsHomogeneous.compMultilinearMap: postcomposing by a homogeneous linear map adds its degree.
References #
- B. Keller, Introduction to A-infinity algebras and modules, Section 3.1.
def
TauCeti.MultilinearMap.IsHomogeneous
{R : Type uR}
{ι : Type uι}
{κ : Type uκ}
{M : κ → Type uM}
{N : Type uN}
{σM : κ → Type u_1}
{σN : Type u_2}
[Semiring R]
[AddCommMonoid ι]
[Fintype κ]
[(i : κ) → AddCommMonoid (M i)]
[AddCommMonoid N]
[(i : κ) → Module R (M i)]
[Module R N]
[(i : κ) → SetLike (σM i) (M i)]
[SetLike σN N]
(f : MultilinearMap R M N)
(𝒜 : (i : κ) → ι → σM i)
(ℬ : ι → σN)
(q : ι)
:
A multilinear map is homogeneous of degree q if it maps inputs lying in 𝒜 i (d i) into
ℬ ((∑ i, d i) + q). No direct-sum hypothesis on the families is needed.
Equations
- TauCeti.MultilinearMap.IsHomogeneous f 𝒜 ℬ q = ∀ (d : κ → ι) (x : (i : κ) → M i), (∀ (i : κ), x i ∈ 𝒜 i (d i)) → f x ∈ ℬ (∑ i : κ, d i + q)
Instances For
theorem
TauCeti.MultilinearMap.isHomogeneous_def
{R : Type uR}
{ι : Type uι}
{κ : Type uκ}
{M : κ → Type uM}
{N : Type uN}
{σM : κ → Type u_1}
{σN : Type u_2}
[Semiring R]
[AddCommMonoid ι]
[Fintype κ]
[(i : κ) → AddCommMonoid (M i)]
[AddCommMonoid N]
[(i : κ) → Module R (M i)]
[Module R N]
[(i : κ) → SetLike (σM i) (M i)]
[SetLike σN N]
{f : MultilinearMap R M N}
{𝒜 : (i : κ) → ι → σM i}
{ℬ : ι → σN}
{q : ι}
:
IsHomogeneous f 𝒜 ℬ q ↔ ∀ (d : κ → ι) (x : (i : κ) → M i), (∀ (i : κ), x i ∈ 𝒜 i (d i)) → f x ∈ ℬ (∑ i : κ, d i + q)
Homogeneity of degree q is exactly the mapping condition on homogeneous inputs. This is a
convenient introduction rule, and IsHomogeneous.map_mem is the corresponding elimination rule.
theorem
TauCeti.MultilinearMap.IsHomogeneous.map_mem
{R : Type uR}
{ι : Type uι}
{κ : Type uκ}
{M : κ → Type uM}
{N : Type uN}
{σM : κ → Type u_1}
{σN : Type u_2}
[Semiring R]
[AddCommMonoid ι]
[Fintype κ]
[(i : κ) → AddCommMonoid (M i)]
[AddCommMonoid N]
[(i : κ) → Module R (M i)]
[Module R N]
[(i : κ) → SetLike (σM i) (M i)]
[SetLike σN N]
{f : MultilinearMap R M N}
{𝒜 : (i : κ) → ι → σM i}
{ℬ : ι → σN}
{q : ι}
(hf : IsHomogeneous f 𝒜 ℬ q)
(d : κ → ι)
(x : (i : κ) → M i)
(hx : ∀ (i : κ), x i ∈ 𝒜 i (d i))
:
Apply a homogeneous multilinear map to homogeneous inputs.
@[simp]
theorem
TauCeti.MultilinearMap.isHomogeneous_zero
{R : Type uR}
{ι : Type uι}
{κ : Type uκ}
{M : κ → Type uM}
{N : Type uN}
{σM : κ → Type u_1}
{σN : Type u_2}
[Semiring R]
[AddCommMonoid ι]
[Fintype κ]
[(i : κ) → AddCommMonoid (M i)]
[AddCommMonoid N]
[(i : κ) → Module R (M i)]
[Module R N]
[(i : κ) → SetLike (σM i) (M i)]
[SetLike σN N]
[ZeroMemClass σN N]
(𝒜 : (i : κ) → ι → σM i)
(ℬ : ι → σN)
(q : ι)
:
IsHomogeneous 0 𝒜 ℬ q
The zero multilinear map is homogeneous of every degree.
theorem
TauCeti.MultilinearMap.IsHomogeneous.add
{R : Type uR}
{ι : Type uι}
{κ : Type uκ}
{M : κ → Type uM}
{N : Type uN}
{σM : κ → Type u_1}
{σN : Type u_2}
[Semiring R]
[AddCommMonoid ι]
[Fintype κ]
[(i : κ) → AddCommMonoid (M i)]
[AddCommMonoid N]
[(i : κ) → Module R (M i)]
[Module R N]
[(i : κ) → SetLike (σM i) (M i)]
[SetLike σN N]
[AddMemClass σN N]
{f g : MultilinearMap R M N}
{𝒜 : (i : κ) → ι → σM i}
{ℬ : ι → σN}
{q : ι}
(hf : IsHomogeneous f 𝒜 ℬ q)
(hg : IsHomogeneous g 𝒜 ℬ q)
:
IsHomogeneous (f + g) 𝒜 ℬ q
A sum of multilinear maps of the same degree has that degree.
theorem
TauCeti.MultilinearMap.IsHomogeneous.compLinearMap
{R : Type uR}
{ι : Type uι}
{κ : Type uκ}
{M : κ → Type uM}
{N : Type uN}
{σM : κ → Type u_1}
{σN : Type u_2}
[Semiring R]
[AddCommMonoid ι]
[Fintype κ]
[(i : κ) → AddCommMonoid (M i)]
[AddCommMonoid N]
[(i : κ) → Module R (M i)]
[Module R N]
[(i : κ) → SetLike (σM i) (M i)]
[SetLike σN N]
{M' : κ → Type uP}
{σM' : κ → Type u_3}
[(i : κ) → AddCommMonoid (M' i)]
[(i : κ) → Module R (M' i)]
[(i : κ) → SetLike (σM' i) (M' i)]
{f : MultilinearMap R M N}
{g : (i : κ) → M' i →ₗ[R] M i}
{𝒜 : (i : κ) → ι → σM' i}
{ℬ : (i : κ) → ι → σM i}
{𝒞 : ι → σN}
{q : ι}
{r : κ → ι}
(hf : IsHomogeneous f ℬ 𝒞 q)
(hg : ∀ (i : κ), LinearMap.IsHomogeneous (g i) (𝒜 i) (ℬ i) (r i))
:
IsHomogeneous (f.compLinearMap g) 𝒜 𝒞 (∑ i : κ, r i + q)
Precomposing each input by a homogeneous linear map adds all of their degrees to the degree of the multilinear map.
theorem
TauCeti.MultilinearMap.IsHomogeneous.compMultilinearMap
{R : Type uR}
{ι : Type uι}
{κ : Type uκ}
{M : κ → Type uM}
{N : Type uN}
{σM : κ → Type u_1}
{σN : Type u_2}
[Semiring R]
[AddCommMonoid ι]
[Fintype κ]
[(i : κ) → AddCommMonoid (M i)]
[AddCommMonoid N]
[(i : κ) → Module R (M i)]
[Module R N]
[(i : κ) → SetLike (σM i) (M i)]
[SetLike σN N]
{β : κ → Type uβ}
[(i : κ) → Fintype (β i)]
{P : (i : κ) → β i → Type uP}
{σP : (i : κ) → β i → Type u_3}
[(i : κ) → (j : β i) → AddCommMonoid (P i j)]
[(i : κ) → (j : β i) → Module R (P i j)]
[(i : κ) → (j : β i) → SetLike (σP i j) (P i j)]
{f : MultilinearMap R M N}
{g : (i : κ) → MultilinearMap R (P i) (M i)}
{𝒜 : (i : κ) → (j : β i) → ι → σP i j}
{ℬ : (i : κ) → ι → σM i}
{𝒞 : ι → σN}
{q : ι}
{r : κ → ι}
(hf : IsHomogeneous f ℬ 𝒞 q)
(hg : ∀ (i : κ), IsHomogeneous (g i) (𝒜 i) (ℬ i) (r i))
:
IsHomogeneous (f.compMultilinearMap g) (fun (ij : (i : κ) × β i) => 𝒜 ij.fst ij.snd) 𝒞 (∑ i : κ, r i + q)
Simultaneous substitution of homogeneous multilinear maps adds the degrees of all substituted maps to the degree of the outer map.
theorem
TauCeti.MultilinearMap.IsHomogeneous.domDomCongrLinearEquiv'
{R : Type uR}
{ι : Type uι}
{κ : Type uκ}
{M : κ → Type uM}
{N : Type uN}
{σM : κ → Type u_1}
{σN : Type u_2}
[Semiring R]
[AddCommMonoid ι]
[Fintype κ]
[(i : κ) → AddCommMonoid (M i)]
[AddCommMonoid N]
[(i : κ) → Module R (M i)]
[Module R N]
[(i : κ) → SetLike (σM i) (M i)]
[SetLike σN N]
{κ' : Type u_3}
[Fintype κ']
(σ : κ ≃ κ')
{f : MultilinearMap R M N}
{𝒜 : (i : κ) → ι → σM i}
{ℬ : ι → σN}
{q : ι}
(hf : IsHomogeneous f 𝒜 ℬ q)
:
IsHomogeneous ((MultilinearMap.domDomCongrLinearEquiv' R ℕ M N σ) f) (fun (i : κ') => 𝒜 (σ.symm i)) ℬ q
Reindexing the inputs of a homogeneous multilinear map along an equivalence of index types preserves its degree.
theorem
TauCeti.MultilinearMap.IsHomogeneous.neg
{R : Type uR}
{ι : Type uι}
{κ : Type uκ}
{M : κ → Type uM}
{N : Type uN}
{σM : κ → Type u_1}
{σN : Type u_2}
[Semiring R]
[AddCommMonoid ι]
[Fintype κ]
[(i : κ) → AddCommMonoid (M i)]
[AddCommGroup N]
[(i : κ) → Module R (M i)]
[Module R N]
[(i : κ) → SetLike (σM i) (M i)]
[SetLike σN N]
[NegMemClass σN N]
{f : MultilinearMap R M N}
{𝒜 : (i : κ) → ι → σM i}
{ℬ : ι → σN}
{q : ι}
(hf : IsHomogeneous f 𝒜 ℬ q)
:
IsHomogeneous (-f) 𝒜 ℬ q
The negative of a homogeneous multilinear map has the same degree.
theorem
TauCeti.MultilinearMap.IsHomogeneous.sub
{R : Type uR}
{ι : Type uι}
{κ : Type uκ}
{M : κ → Type uM}
{N : Type uN}
{σM : κ → Type u_1}
{σN : Type u_2}
[Semiring R]
[AddCommMonoid ι]
[Fintype κ]
[(i : κ) → AddCommMonoid (M i)]
[AddCommGroup N]
[(i : κ) → Module R (M i)]
[Module R N]
[(i : κ) → SetLike (σM i) (M i)]
[SetLike σN N]
[AddMemClass σN N]
[NegMemClass σN N]
{f g : MultilinearMap R M N}
{𝒜 : (i : κ) → ι → σM i}
{ℬ : ι → σN}
{q : ι}
(hf : IsHomogeneous f 𝒜 ℬ q)
(hg : IsHomogeneous g 𝒜 ℬ q)
:
IsHomogeneous (f - g) 𝒜 ℬ q
A difference of multilinear maps of the same degree has that degree.
theorem
TauCeti.MultilinearMap.IsHomogeneous.smul
{R : Type uR}
{S : Type u_1}
{ι : Type uι}
{κ : Type uκ}
{M : κ → Type uM}
{N : Type uN}
{σM : κ → Type u_2}
{σN : Type u_3}
[Semiring R]
[AddCommMonoid ι]
[Fintype κ]
[(i : κ) → AddCommMonoid (M i)]
[AddCommMonoid N]
[(i : κ) → Module R (M i)]
[Module R N]
[(i : κ) → SetLike (σM i) (M i)]
[SetLike σN N]
[Monoid S]
[DistribMulAction S N]
[SMulCommClass R S N]
[SMulMemClass σN S N]
{f : MultilinearMap R M N}
{𝒜 : (i : κ) → ι → σM i}
{ℬ : ι → σN}
{q : ι}
(hf : IsHomogeneous f 𝒜 ℬ q)
(s : S)
:
IsHomogeneous (s • f) 𝒜 ℬ q
A scalar multiple of a homogeneous multilinear map has the same degree.
def
TauCeti.MultilinearMap.homogeneousSubmodule
{R : Type uR}
{S : Type u_1}
{ι : Type uι}
{κ : Type uκ}
{M : κ → Type uM}
{N : Type uN}
{σM : κ → Type u_2}
{σN : Type u_3}
[Semiring R]
[AddCommMonoid ι]
[Fintype κ]
[(i : κ) → AddCommMonoid (M i)]
[AddCommMonoid N]
[(i : κ) → Module R (M i)]
[Module R N]
[(i : κ) → SetLike (σM i) (M i)]
[SetLike σN N]
[Semiring S]
[Module S N]
[SMulCommClass R S N]
[AddSubmonoidClass σN N]
[SMulMemClass σN S N]
(𝒜 : (i : κ) → ι → σM i)
(ℬ : ι → σN)
(q : ι)
:
Submodule S (MultilinearMap R M N)
Multilinear maps of a fixed degree form a submodule over any scalar ring acting on the target.
Equations
- TauCeti.MultilinearMap.homogeneousSubmodule 𝒜 ℬ q = { carrier := {f : MultilinearMap R M N | TauCeti.MultilinearMap.IsHomogeneous f 𝒜 ℬ q}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }
Instances For
@[simp]
theorem
TauCeti.MultilinearMap.mem_homogeneousSubmodule
{R : Type uR}
{S : Type u_1}
{ι : Type uι}
{κ : Type uκ}
{M : κ → Type uM}
{N : Type uN}
{σM : κ → Type u_2}
{σN : Type u_3}
[Semiring R]
[AddCommMonoid ι]
[Fintype κ]
[(i : κ) → AddCommMonoid (M i)]
[AddCommMonoid N]
[(i : κ) → Module R (M i)]
[Module R N]
[(i : κ) → SetLike (σM i) (M i)]
[SetLike σN N]
[Semiring S]
[Module S N]
[SMulCommClass R S N]
[AddSubmonoidClass σN N]
[SMulMemClass σN S N]
{f : MultilinearMap R M N}
{𝒜 : (i : κ) → ι → σM i}
{ℬ : ι → σN}
{q : ι}
:
theorem
TauCeti.LinearMap.IsHomogeneous.compMultilinearMap
{R : Type uR}
{ι : Type uι}
{κ : Type uκ}
{M : κ → Type uM}
{N : Type uN}
{P : Type uP}
{σM : κ → Type u_1}
{σN : Type u_2}
{σP : Type u_3}
[Semiring R]
[AddCommMonoid ι]
[Fintype κ]
[(i : κ) → AddCommMonoid (M i)]
[AddCommMonoid N]
[AddCommMonoid P]
[(i : κ) → Module R (M i)]
[Module R N]
[Module R P]
[(i : κ) → SetLike (σM i) (M i)]
[SetLike σN N]
[SetLike σP P]
{f : MultilinearMap R M N}
{g : N →ₗ[R] P}
{𝒜 : (i : κ) → ι → σM i}
{ℬ : ι → σN}
{𝒞 : ι → σP}
{q r : ι}
(hg : IsHomogeneous g ℬ 𝒞 r)
(hf : MultilinearMap.IsHomogeneous f 𝒜 ℬ q)
:
MultilinearMap.IsHomogeneous (g.compMultilinearMap f) 𝒜 𝒞 (q + r)
Postcomposing a homogeneous multilinear map by a homogeneous linear map adds their degrees.