Graded linear maps

This file defines graded linear maps of a fixed degree between externally graded modules, i.e. families of modules M N : β → Type* indexed by a grading type β.

A graded linear map f of degree d consists of one linear map M i →ₗ[R] N j for each pair of degrees with i + d = j.

Main definitions

• AInfinityTheory.GradedLinearMap R M N d: graded R-linear maps of degree d from M to N.
• AInfinityTheory.GradedLinearMap.id: the identity graded linear map, of degree 0.
• AInfinityTheory.GradedLinearMap.comp: the composite of graded linear maps of degrees d and e, of any degree de with d + e = de.
• AInfinityTheory.GradedMultilinearMap R M N d: graded R-multilinear maps of degree d from the families M j, j : ι, to N. For input degrees deg : ι → β, the component lands in any degree i with (∑ j, deg j) + d = i.

Main results

• GradedLinearMap and GradedMultilinearMap are additive commutative monoids (groups if N is), and modules over any semiring S whose action on each N i commutes with that of R.
• GradedLinearMap.comp_assoc, GradedLinearMap.id_comp, GradedLinearMap.comp_id: graded linear maps compose associatively and unitally.

Implementation notes

Following CochainComplex.HomComplex.Cochain, components are indexed by a source degree i, a target degree j and a proof of i + d = j, rather than by i alone with target N (i + d). The terms i + 0 and i + d + e are not definitionally equal to i and i + (d + e), so the latter choice would force casts into id and comp. With the proof as an argument, any two choices of proof are definitionally equal, and a composite factors through any middle degree (GradedLinearMap.comp_apply).

The algebraic structure is transferred from a Pi type along toPi, which reindexes the components by the type of pairs (i, j) with i + d = j; the Pi instances in Mathlib do not apply to the Prop-valued binder i + d = j directly.

The structures only need an addition on β; comp needs AddSemigroup β and id needs AddZeroClass β.

structure AInfinityTheory.GradedLinearMap (R : Type u) [Semiring R] {β : Type v} [Add β] (M : β → Type w₁) (N : β → Type w₂) [(i : β) → AddCommMonoid (M i)] [(i : β) → Module R (M i)] [(i : β) → AddCommMonoid (N i)] [(i : β) → Module R (N i)] (d : β) : Type (max (max v w₁) w₂)

A graded R-linear map of degree d from M to N is a family of R-linear maps M i →ₗ[R] N j, one for each pair of degrees with i + d = j. It raises the degree of every homogeneous element by d.

• toLinearMap (i j : β) : i + d = j → M i →ₗ[R] N j

  The component of the graded linear map from degree i to degree j, where i + d = j.

@[implicit_reducible]

instance AInfinityTheory.GradedLinearMap.instCoeFunForallForallForallEqHAddLinearMapId {R : Type u} [Semiring R] {β : Type v} {M : β → Type w₁} {N : β → Type w₂} [(i : β) → AddCommMonoid (M i)] [(i : β) → Module R (M i)] [(i : β) → AddCommMonoid (N i)] [(i : β) → Module R (N i)] [Add β] {d : β} : CoeFun (GradedLinearMap R M N d) fun (x : GradedLinearMap R M N d) => (i j : β) → i + d = j → M i →ₗ[R] N j

A graded linear map is applied to degrees i and j with i + d = j to get its linear component from degree i to degree j.

Equations

• AInfinityTheory.GradedLinearMap.instCoeFunForallForallForallEqHAddLinearMapId = { coe := AInfinityTheory.GradedLinearMap.toLinearMap }

@[simp]

theorem AInfinityTheory.GradedLinearMap.toLinearMap_eq_coe {R : Type u} [Semiring R] {β : Type v} {M : β → Type w₁} {N : β → Type w₂} [(i : β) → AddCommMonoid (M i)] [(i : β) → Module R (M i)] [(i : β) → AddCommMonoid (N i)] [(i : β) → Module R (N i)] [Add β] {d : β} (f : GradedLinearMap R M N d) : ↑f = ↑f

@[simp]

theorem AInfinityTheory.GradedLinearMap.coe_mk {R : Type u} [Semiring R] {β : Type v} {M : β → Type w₁} {N : β → Type w₂} [(i : β) → AddCommMonoid (M i)] [(i : β) → Module R (M i)] [(i : β) → AddCommMonoid (N i)] [(i : β) → Module R (N i)] [Add β] {d : β} (f : (i j : β) → i + d = j → M i →ₗ[R] N j) : ↑{ toLinearMap := f } = f

theorem AInfinityTheory.GradedLinearMap.coe_injective {R : Type u} [Semiring R] {β : Type v} {M : β → Type w₁} {N : β → Type w₂} [(i : β) → AddCommMonoid (M i)] [(i : β) → Module R (M i)] [(i : β) → AddCommMonoid (N i)] [(i : β) → Module R (N i)] [Add β] {d : β} : Function.Injective fun (f : GradedLinearMap R M N d) => ↑f

A graded linear map is determined by its components.

theorem AInfinityTheory.GradedLinearMap.ext {R : Type u} [Semiring R] {β : Type v} {M : β → Type w₁} {N : β → Type w₂} [(i : β) → AddCommMonoid (M i)] [(i : β) → Module R (M i)] [(i : β) → AddCommMonoid (N i)] [(i : β) → Module R (N i)] [Add β] {d : β} {f g : GradedLinearMap R M N d} (h : ∀ (i j : β) (hij : i + d = j) (x : M i), (↑f i j hij) x = (↑g i j hij) x) : f = g

Two graded linear maps are equal if they agree on every homogeneous element.

theorem AInfinityTheory.GradedLinearMap.ext_iff {R : Type u} [Semiring R] {β : Type v} {M : β → Type w₁} {N : β → Type w₂} [(i : β) → AddCommMonoid (M i)] [(i : β) → Module R (M i)] [(i : β) → AddCommMonoid (N i)] [(i : β) → Module R (N i)] [Add β] {d : β} {f g : GradedLinearMap R M N d} : f = g ↔ ∀ (i j : β) (hij : i + d = j) (x : M i), (↑f i j hij) x = (↑g i j hij) x

def AInfinityTheory.GradedLinearMap.toPi {R : Type u} [Semiring R] {β : Type v} {M : β → Type w₁} {N : β → Type w₂} [(i : β) → AddCommMonoid (M i)] [(i : β) → Module R (M i)] [(i : β) → AddCommMonoid (N i)] [(i : β) → Module R (N i)] [Add β] {d : β} (f : GradedLinearMap R M N d) (p : { p : β × β // p.1 + d = p.2 }) : M (↑p).1 →ₗ[R] N (↑p).2

The components of a graded linear map, indexed by the type of pairs of degrees (i, j) with i + d = j. The Pi instances apply to this indexing, so it is used to transfer algebraic structure to graded linear maps.

Equations

• f.toPi p = ↑f (↑p).1 (↑p).2 ⋯

@[simp]

theorem AInfinityTheory.GradedLinearMap.toPi_apply {R : Type u} [Semiring R] {β : Type v} {M : β → Type w₁} {N : β → Type w₂} [(i : β) → AddCommMonoid (M i)] [(i : β) → Module R (M i)] [(i : β) → AddCommMonoid (N i)] [(i : β) → Module R (N i)] [Add β] {d : β} (f : GradedLinearMap R M N d) (p : { p : β × β // p.1 + d = p.2 }) : f.toPi p = ↑f (↑p).1 (↑p).2 ⋯

theorem AInfinityTheory.GradedLinearMap.toPi_injective {R : Type u} [Semiring R] {β : Type v} {M : β → Type w₁} {N : β → Type w₂} [(i : β) → AddCommMonoid (M i)] [(i : β) → Module R (M i)] [(i : β) → AddCommMonoid (N i)] [(i : β) → Module R (N i)] [Add β] {d : β} : Function.Injective toPi

@[implicit_reducible]

instance AInfinityTheory.GradedLinearMap.instZero {R : Type u} [Semiring R] {β : Type v} {M : β → Type w₁} {N : β → Type w₂} [(i : β) → AddCommMonoid (M i)] [(i : β) → Module R (M i)] [(i : β) → AddCommMonoid (N i)] [(i : β) → Module R (N i)] [Add β] {d : β} : Zero (GradedLinearMap R M N d)

The zero graded linear map sends every homogeneous element to zero.

Equations

• AInfinityTheory.GradedLinearMap.instZero = { zero := { toLinearMap := fun (x x_1 : β) (x_2 : x + d = x_1) => 0 } }

@[implicit_reducible]

instance AInfinityTheory.GradedLinearMap.instAdd {R : Type u} [Semiring R] {β : Type v} {M : β → Type w₁} {N : β → Type w₂} [(i : β) → AddCommMonoid (M i)] [(i : β) → Module R (M i)] [(i : β) → AddCommMonoid (N i)] [(i : β) → Module R (N i)] [Add β] {d : β} : Add (GradedLinearMap R M N d)

Graded linear maps of the same degree are added componentwise.

Equations

• AInfinityTheory.GradedLinearMap.instAdd = { add := fun (f g : AInfinityTheory.GradedLinearMap R M N d) => { toLinearMap := fun (i j : β) (hij : i + d = j) => ↑f i j hij + ↑g i j hij } }

@[implicit_reducible]

instance AInfinityTheory.GradedLinearMap.instSMulOfSMulCommClass {R : Type u} [Semiring R] {β : Type v} {M : β → Type w₁} {N : β → Type w₂} [(i : β) → AddCommMonoid (M i)] [(i : β) → Module R (M i)] [(i : β) → AddCommMonoid (N i)] [(i : β) → Module R (N i)] [Add β] {d : β} {S : Type u_1} [Monoid S] [(i : β) → DistribMulAction S (N i)] [∀ (i : β), SMulCommClass R S (N i)] : SMul S (GradedLinearMap R M N d)

Scalar multiplication on graded linear maps is defined componentwise.

Equations

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

@[simp]

theorem AInfinityTheory.GradedLinearMap.zero_apply {R : Type u} [Semiring R] {β : Type v} {M : β → Type w₁} {N : β → Type w₂} [(i : β) → AddCommMonoid (M i)] [(i : β) → Module R (M i)] [(i : β) → AddCommMonoid (N i)] [(i : β) → Module R (N i)] [Add β] {d : β} (i j : β) (hij : i + d = j) : ↑0 i j hij = 0

@[simp]

theorem AInfinityTheory.GradedLinearMap.add_apply {R : Type u} [Semiring R] {β : Type v} {M : β → Type w₁} {N : β → Type w₂} [(i : β) → AddCommMonoid (M i)] [(i : β) → Module R (M i)] [(i : β) → AddCommMonoid (N i)] [(i : β) → Module R (N i)] [Add β] {d : β} (f g : GradedLinearMap R M N d) (i j : β) (hij : i + d = j) : ↑(f + g) i j hij = ↑f i j hij + ↑g i j hij

@[simp]

theorem AInfinityTheory.GradedLinearMap.smul_apply {R : Type u} [Semiring R] {β : Type v} {M : β → Type w₁} {N : β → Type w₂} [(i : β) → AddCommMonoid (M i)] [(i : β) → Module R (M i)] [(i : β) → AddCommMonoid (N i)] [(i : β) → Module R (N i)] [Add β] {d : β} {S : Type u_1} [Monoid S] [(i : β) → DistribMulAction S (N i)] [∀ (i : β), SMulCommClass R S (N i)] (c : S) (f : GradedLinearMap R M N d) (i j : β) (hij : i + d = j) : ↑(c • f) i j hij = c • ↑f i j hij

@[implicit_reducible]

instance AInfinityTheory.GradedLinearMap.instSMulNat {R : Type u} [Semiring R] {β : Type v} {M : β → Type w₁} {N : β → Type w₂} [(i : β) → AddCommMonoid (M i)] [(i : β) → Module R (M i)] [(i : β) → AddCommMonoid (N i)] [(i : β) → Module R (N i)] [Add β] {d : β} : SMul ℕ (GradedLinearMap R M N d)

The components of the natural-number multiple n • f are the multiples n • f i j hij.

Equations

• AInfinityTheory.GradedLinearMap.instSMulNat = { smul := fun (n : ℕ) (f : AInfinityTheory.GradedLinearMap R M N d) => { toLinearMap := fun (i j : β) (hij : i + d = j) => n • ↑f i j hij } }

@[implicit_reducible]

instance AInfinityTheory.GradedLinearMap.instAddCommMonoid {R : Type u} [Semiring R] {β : Type v} {M : β → Type w₁} {N : β → Type w₂} [(i : β) → AddCommMonoid (M i)] [(i : β) → Module R (M i)] [(i : β) → AddCommMonoid (N i)] [(i : β) → Module R (N i)] [Add β] {d : β} : AddCommMonoid (GradedLinearMap R M N d)

Graded linear maps of degree d form an additive commutative monoid under componentwise addition.

Equations

• AInfinityTheory.GradedLinearMap.instAddCommMonoid = Function.Injective.addCommMonoid AInfinityTheory.GradedLinearMap.toPi ⋯ ⋯ ⋯ ⋯

@[implicit_reducible]

instance AInfinityTheory.GradedLinearMap.instModuleOfSMulCommClass {R : Type u} [Semiring R] {β : Type v} {M : β → Type w₁} {N : β → Type w₂} [(i : β) → AddCommMonoid (M i)] [(i : β) → Module R (M i)] [(i : β) → AddCommMonoid (N i)] [(i : β) → Module R (N i)] [Add β] {d : β} {S : Type u_1} [Semiring S] [(i : β) → Module S (N i)] [∀ (i : β), SMulCommClass R S (N i)] : Module S (GradedLinearMap R M N d)

Graded linear maps of degree d form a module over any semiring S acting on the target compatibly with R.

Equations

• AInfinityTheory.GradedLinearMap.instModuleOfSMulCommClass = Function.Injective.module S { toFun := AInfinityTheory.GradedLinearMap.toPi, map_zero' := ⋯, map_add' := ⋯ } ⋯ ⋯

@[implicit_reducible]

instance AInfinityTheory.GradedLinearMap.instNeg {R : Type u} [Semiring R] {β : Type v} {M : β → Type w₁} [(i : β) → AddCommMonoid (M i)] [(i : β) → Module R (M i)] [Add β] {d : β} {N : β → Type w₂} [(i : β) → AddCommGroup (N i)] [(i : β) → Module R (N i)] : Neg (GradedLinearMap R M N d)

The negation of a graded linear map is taken componentwise.

Equations

• AInfinityTheory.GradedLinearMap.instNeg = { neg := fun (f : AInfinityTheory.GradedLinearMap R M N d) => { toLinearMap := fun (i j : β) (hij : i + d = j) => -↑f i j hij } }

@[implicit_reducible]

instance AInfinityTheory.GradedLinearMap.instSub {R : Type u} [Semiring R] {β : Type v} {M : β → Type w₁} [(i : β) → AddCommMonoid (M i)] [(i : β) → Module R (M i)] [Add β] {d : β} {N : β → Type w₂} [(i : β) → AddCommGroup (N i)] [(i : β) → Module R (N i)] : Sub (GradedLinearMap R M N d)

The difference of two graded linear maps is taken componentwise.

Equations

• AInfinityTheory.GradedLinearMap.instSub = { sub := fun (f g : AInfinityTheory.GradedLinearMap R M N d) => { toLinearMap := fun (i j : β) (hij : i + d = j) => ↑f i j hij - ↑g i j hij } }

@[implicit_reducible]

instance AInfinityTheory.GradedLinearMap.instSMulInt {R : Type u} [Semiring R] {β : Type v} {M : β → Type w₁} [(i : β) → AddCommMonoid (M i)] [(i : β) → Module R (M i)] [Add β] {d : β} {N : β → Type w₂} [(i : β) → AddCommGroup (N i)] [(i : β) → Module R (N i)] : SMul ℤ (GradedLinearMap R M N d)

The components of the integer multiple n • f are the multiples n • f i j hij.

Equations

• AInfinityTheory.GradedLinearMap.instSMulInt = { smul := fun (n : ℤ) (f : AInfinityTheory.GradedLinearMap R M N d) => { toLinearMap := fun (i j : β) (hij : i + d = j) => n • ↑f i j hij } }

@[simp]

theorem AInfinityTheory.GradedLinearMap.neg_apply {R : Type u} [Semiring R] {β : Type v} {M : β → Type w₁} [(i : β) → AddCommMonoid (M i)] [(i : β) → Module R (M i)] [Add β] {d : β} {N : β → Type w₂} [(i : β) → AddCommGroup (N i)] [(i : β) → Module R (N i)] (f : GradedLinearMap R M N d) (i j : β) (hij : i + d = j) : ↑(-f) i j hij = -↑f i j hij

@[simp]

theorem AInfinityTheory.GradedLinearMap.sub_apply {R : Type u} [Semiring R] {β : Type v} {M : β → Type w₁} [(i : β) → AddCommMonoid (M i)] [(i : β) → Module R (M i)] [Add β] {d : β} {N : β → Type w₂} [(i : β) → AddCommGroup (N i)] [(i : β) → Module R (N i)] (f g : GradedLinearMap R M N d) (i j : β) (hij : i + d = j) : ↑(f - g) i j hij = ↑f i j hij - ↑g i j hij

@[implicit_reducible]

instance AInfinityTheory.GradedLinearMap.instAddCommGroup {R : Type u} [Semiring R] {β : Type v} {M : β → Type w₁} [(i : β) → AddCommMonoid (M i)] [(i : β) → Module R (M i)] [Add β] {d : β} {N : β → Type w₂} [(i : β) → AddCommGroup (N i)] [(i : β) → Module R (N i)] : AddCommGroup (GradedLinearMap R M N d)

Graded linear maps of degree d into a family of additive groups form an additive commutative group.

Equations

• AInfinityTheory.GradedLinearMap.instAddCommGroup = Function.Injective.addCommGroup AInfinityTheory.GradedLinearMap.toPi ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

def AInfinityTheory.GradedLinearMap.comp {R : Type u} [Semiring R] {β : Type v} {M : β → Type w₁} {N : β → Type w₂} {P : β → Type w₃} [(i : β) → AddCommMonoid (M i)] [(i : β) → Module R (M i)] [(i : β) → AddCommMonoid (N i)] [(i : β) → Module R (N i)] [(i : β) → AddCommMonoid (P i)] [(i : β) → Module R (P i)] [AddSemigroup β] {d e de : β} (g : GradedLinearMap R N P e) (f : GradedLinearMap R M N d) (h : d + e = de) : GradedLinearMap R M P de

The composite of graded linear maps of degrees d and e is a graded linear map of any degree de with d + e = de. Its component from degree i factors through degree i + d.

Equations

• g.comp f h = { toLinearMap := fun (i k : β) (hik : i + de = k) => ↑g (i + d) k ⋯ ∘ₗ ↑f i (i + d) ⋯ }

theorem AInfinityTheory.GradedLinearMap.comp_apply {R : Type u} [Semiring R] {β : Type v} {M : β → Type w₁} {N : β → Type w₂} {P : β → Type w₃} [(i : β) → AddCommMonoid (M i)] [(i : β) → Module R (M i)] [(i : β) → AddCommMonoid (N i)] [(i : β) → Module R (N i)] [(i : β) → AddCommMonoid (P i)] [(i : β) → Module R (P i)] [AddSemigroup β] {d e de : β} (g : GradedLinearMap R N P e) (f : GradedLinearMap R M N d) (h : d + e = de) {i j k : β} (hij : i + d = j) (hjk : j + e = k) (hik : i + de = k) : ↑(g.comp f h) i k hik = ↑g j k hjk ∘ₗ ↑f i j hij

A component of a composite of graded linear maps factors through any middle degree j.

theorem AInfinityTheory.GradedLinearMap.comp_assoc {R : Type u} [Semiring R] {β : Type v} {M : β → Type w₁} {N : β → Type w₂} {P : β → Type w₃} {Q : β → Type w₄} [(i : β) → AddCommMonoid (M i)] [(i : β) → Module R (M i)] [(i : β) → AddCommMonoid (N i)] [(i : β) → Module R (N i)] [(i : β) → AddCommMonoid (P i)] [(i : β) → Module R (P i)] [(i : β) → AddCommMonoid (Q i)] [(i : β) → Module R (Q i)] [AddSemigroup β] {d₁ d₂ d₃ d₁₂ d₂₃ d₁₂₃ : β} (f₁ : GradedLinearMap R M N d₁) (f₂ : GradedLinearMap R N P d₂) (f₃ : GradedLinearMap R P Q d₃) (h₁₂ : d₁ + d₂ = d₁₂) (h₂₃ : d₂ + d₃ = d₂₃) (h₁₂₃ : d₁₂ + d₃ = d₁₂₃) (h₁₂₃' : d₁ + d₂₃ = d₁₂₃) : (f₃.comp f₂ h₂₃).comp f₁ h₁₂₃' = f₃.comp (f₂.comp f₁ h₁₂) h₁₂₃

Composition of graded linear maps is associative, for any choice of degrees of the intermediate composites.

def AInfinityTheory.GradedLinearMap.id {R : Type u} [Semiring R] {β : Type v} {M : β → Type w₁} [(i : β) → AddCommMonoid (M i)] [(i : β) → Module R (M i)] [AddZeroClass β] : GradedLinearMap R M M 0

The identity graded linear map, of degree 0. Its component from degree i to degree j is the identity, transported along i = i + 0 = j.

Equations

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

@[simp]

theorem AInfinityTheory.GradedLinearMap.id_apply {R : Type u} [Semiring R] {β : Type v} {M : β → Type w₁} [(i : β) → AddCommMonoid (M i)] [(i : β) → Module R (M i)] [AddZeroClass β] (i : β) (h : i + 0 = i := ⋯) : ↑id i i h = LinearMap.id

@[simp]

theorem AInfinityTheory.GradedLinearMap.id_comp {R : Type u} [Semiring R] {β : Type v} {M : β → Type w₁} {N : β → Type w₂} [(i : β) → AddCommMonoid (M i)] [(i : β) → Module R (M i)] [(i : β) → AddCommMonoid (N i)] [(i : β) → Module R (N i)] [AddMonoid β] {d : β} (f : GradedLinearMap R M N d) : id.comp f ⋯ = f

@[simp]

theorem AInfinityTheory.GradedLinearMap.comp_id {R : Type u} [Semiring R] {β : Type v} {M : β → Type w₁} {N : β → Type w₂} [(i : β) → AddCommMonoid (M i)] [(i : β) → Module R (M i)] [(i : β) → AddCommMonoid (N i)] [(i : β) → Module R (N i)] [AddMonoid β] {d : β} (f : GradedLinearMap R M N d) : f.comp id ⋯ = f

structure AInfinityTheory.GradedMultilinearMap (R : Type u) [Semiring R] {ι : Type u_1} [Fintype ι] {β : Type v} [AddCommMonoid β] (M : ι → β → Type w₁) (N : β → Type w₂) [(j : ι) → (i : β) → AddCommMonoid (M j i)] [(j : ι) → (i : β) → Module R (M j i)] [(i : β) → AddCommMonoid (N i)] [(i : β) → Module R (N i)] (d : β) : Type (max (max (max u_1 v) w₁) w₂)

A graded R-multilinear map of degree d from the families M j (for j : ι) to N consists of, for each choice of input degrees deg : ι → β and each output degree i with (∑ j, deg j) + d = i, an R-multilinear map from ∀ j, M j (deg j) to N i. The output degree is the total input degree shifted by d.

• toMultilinearMap (deg : ι → β) (i : β) : ∑ j : ι, deg j + d = i → MultilinearMap R (fun (j : ι) => M j (deg j)) (N i)

  The component of the graded multilinear map with input degrees deg and output degree i, where (∑ j, deg j) + d = i.

@[implicit_reducible]

instance AInfinityTheory.GradedMultilinearMap.instCoeFunForallForallForallEqHAddSumUnivMultilinearMap {R : Type u} [Semiring R] {ι : Type u_1} [Fintype ι] {β : Type v} [AddCommMonoid β] {M : ι → β → Type w₁} {N : β → Type w₂} [(j : ι) → (i : β) → AddCommMonoid (M j i)] [(j : ι) → (i : β) → Module R (M j i)] [(i : β) → AddCommMonoid (N i)] [(i : β) → Module R (N i)] {d : β} : CoeFun (GradedMultilinearMap R M N d) fun (x : GradedMultilinearMap R M N d) => (deg : ι → β) → (i : β) → ∑ j : ι, deg j + d = i → MultilinearMap R (fun (j : ι) => M j (deg j)) (N i)

A graded multilinear map is applied to input degrees deg and an output degree i with (∑ j, deg j) + d = i to get the corresponding multilinear component.

Equations

• AInfinityTheory.GradedMultilinearMap.instCoeFunForallForallForallEqHAddSumUnivMultilinearMap = { coe := AInfinityTheory.GradedMultilinearMap.toMultilinearMap }

@[simp]

theorem AInfinityTheory.GradedMultilinearMap.toMultilinearMap_eq_coe {R : Type u} [Semiring R] {ι : Type u_1} [Fintype ι] {β : Type v} [AddCommMonoid β] {M : ι → β → Type w₁} {N : β → Type w₂} [(j : ι) → (i : β) → AddCommMonoid (M j i)] [(j : ι) → (i : β) → Module R (M j i)] [(i : β) → AddCommMonoid (N i)] [(i : β) → Module R (N i)] {d : β} (f : GradedMultilinearMap R M N d) : ↑f = ↑f

@[simp]

theorem AInfinityTheory.GradedMultilinearMap.coe_mk {R : Type u} [Semiring R] {ι : Type u_1} [Fintype ι] {β : Type v} [AddCommMonoid β] {M : ι → β → Type w₁} {N : β → Type w₂} [(j : ι) → (i : β) → AddCommMonoid (M j i)] [(j : ι) → (i : β) → Module R (M j i)] [(i : β) → AddCommMonoid (N i)] [(i : β) → Module R (N i)] {d : β} (f : (deg : ι → β) → (i : β) → ∑ j : ι, deg j + d = i → MultilinearMap R (fun (j : ι) => M j (deg j)) (N i)) : ↑{ toMultilinearMap := f } = f

theorem AInfinityTheory.GradedMultilinearMap.coe_injective {R : Type u} [Semiring R] {ι : Type u_1} [Fintype ι] {β : Type v} [AddCommMonoid β] {M : ι → β → Type w₁} {N : β → Type w₂} [(j : ι) → (i : β) → AddCommMonoid (M j i)] [(j : ι) → (i : β) → Module R (M j i)] [(i : β) → AddCommMonoid (N i)] [(i : β) → Module R (N i)] {d : β} : Function.Injective fun (f : GradedMultilinearMap R M N d) => ↑f

A graded multilinear map is determined by its components.

theorem AInfinityTheory.GradedMultilinearMap.ext {R : Type u} [Semiring R] {ι : Type u_1} [Fintype ι] {β : Type v} [AddCommMonoid β] {M : ι → β → Type w₁} {N : β → Type w₂} [(j : ι) → (i : β) → AddCommMonoid (M j i)] [(j : ι) → (i : β) → Module R (M j i)] [(i : β) → AddCommMonoid (N i)] [(i : β) → Module R (N i)] {d : β} {f g : GradedMultilinearMap R M N d} (h : ∀ (deg : ι → β) (i : β) (hi : ∑ j : ι, deg j + d = i) (x : (i : ι) → M i (deg i)), (↑f deg i hi) x = (↑g deg i hi) x) : f = g

Two graded multilinear maps are equal if they agree on every tuple of homogeneous elements.

theorem AInfinityTheory.GradedMultilinearMap.ext_iff {R : Type u} [Semiring R] {ι : Type u_1} [Fintype ι] {β : Type v} [AddCommMonoid β] {M : ι → β → Type w₁} {N : β → Type w₂} [(j : ι) → (i : β) → AddCommMonoid (M j i)] [(j : ι) → (i : β) → Module R (M j i)] [(i : β) → AddCommMonoid (N i)] [(i : β) → Module R (N i)] {d : β} {f g : GradedMultilinearMap R M N d} : f = g ↔ ∀ (deg : ι → β) (i : β) (hi : ∑ j : ι, deg j + d = i) (x : (i : ι) → M i (deg i)), (↑f deg i hi) x = (↑g deg i hi) x

def AInfinityTheory.GradedMultilinearMap.toPi {R : Type u} [Semiring R] {ι : Type u_1} [Fintype ι] {β : Type v} [AddCommMonoid β] {M : ι → β → Type w₁} {N : β → Type w₂} [(j : ι) → (i : β) → AddCommMonoid (M j i)] [(j : ι) → (i : β) → Module R (M j i)] [(i : β) → AddCommMonoid (N i)] [(i : β) → Module R (N i)] {d : β} (f : GradedMultilinearMap R M N d) (p : { p : (ι → β) × β // ∑ j : ι, p.1 j + d = p.2 }) : MultilinearMap R (fun (j : ι) => M j ((↑p).1 j)) (N (↑p).2)

The components of a graded multilinear map, indexed by the type of pairs (deg, i) with (∑ j, deg j) + d = i. The Pi instances apply to this indexing, so it is used to transfer algebraic structure to graded multilinear maps.

Equations

• f.toPi p = ↑f (↑p).1 (↑p).2 ⋯

@[simp]

theorem AInfinityTheory.GradedMultilinearMap.toPi_apply {R : Type u} [Semiring R] {ι : Type u_1} [Fintype ι] {β : Type v} [AddCommMonoid β] {M : ι → β → Type w₁} {N : β → Type w₂} [(j : ι) → (i : β) → AddCommMonoid (M j i)] [(j : ι) → (i : β) → Module R (M j i)] [(i : β) → AddCommMonoid (N i)] [(i : β) → Module R (N i)] {d : β} (f : GradedMultilinearMap R M N d) (p : { p : (ι → β) × β // ∑ j : ι, p.1 j + d = p.2 }) : f.toPi p = ↑f (↑p).1 (↑p).2 ⋯

theorem AInfinityTheory.GradedMultilinearMap.toPi_injective {R : Type u} [Semiring R] {ι : Type u_1} [Fintype ι] {β : Type v} [AddCommMonoid β] {M : ι → β → Type w₁} {N : β → Type w₂} [(j : ι) → (i : β) → AddCommMonoid (M j i)] [(j : ι) → (i : β) → Module R (M j i)] [(i : β) → AddCommMonoid (N i)] [(i : β) → Module R (N i)] {d : β} : Function.Injective toPi

@[implicit_reducible]

instance AInfinityTheory.GradedMultilinearMap.instZero {R : Type u} [Semiring R] {ι : Type u_1} [Fintype ι] {β : Type v} [AddCommMonoid β] {M : ι → β → Type w₁} {N : β → Type w₂} [(j : ι) → (i : β) → AddCommMonoid (M j i)] [(j : ι) → (i : β) → Module R (M j i)] [(i : β) → AddCommMonoid (N i)] [(i : β) → Module R (N i)] {d : β} : Zero (GradedMultilinearMap R M N d)

The zero graded multilinear map sends every tuple of homogeneous elements to zero.

Equations

• AInfinityTheory.GradedMultilinearMap.instZero = { zero := { toMultilinearMap := fun (x : ι → β) (x_1 : β) (x_2 : ∑ j : ι, x j + d = x_1) => 0 } }

@[implicit_reducible]

instance AInfinityTheory.GradedMultilinearMap.instAdd {R : Type u} [Semiring R] {ι : Type u_1} [Fintype ι] {β : Type v} [AddCommMonoid β] {M : ι → β → Type w₁} {N : β → Type w₂} [(j : ι) → (i : β) → AddCommMonoid (M j i)] [(j : ι) → (i : β) → Module R (M j i)] [(i : β) → AddCommMonoid (N i)] [(i : β) → Module R (N i)] {d : β} : Add (GradedMultilinearMap R M N d)

Graded multilinear maps of the same degree are added componentwise.

Equations

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

@[implicit_reducible]

instance AInfinityTheory.GradedMultilinearMap.instSMulOfSMulCommClass {R : Type u} [Semiring R] {ι : Type u_1} [Fintype ι] {β : Type v} [AddCommMonoid β] {M : ι → β → Type w₁} {N : β → Type w₂} [(j : ι) → (i : β) → AddCommMonoid (M j i)] [(j : ι) → (i : β) → Module R (M j i)] [(i : β) → AddCommMonoid (N i)] [(i : β) → Module R (N i)] {d : β} {S : Type u_2} [(i : β) → DistribSMul S (N i)] [∀ (i : β), SMulCommClass R S (N i)] : SMul S (GradedMultilinearMap R M N d)

Scalar multiplication on graded multilinear maps is defined componentwise.

Equations

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

@[simp]

theorem AInfinityTheory.GradedMultilinearMap.zero_apply {R : Type u} [Semiring R] {ι : Type u_1} [Fintype ι] {β : Type v} [AddCommMonoid β] {M : ι → β → Type w₁} {N : β → Type w₂} [(j : ι) → (i : β) → AddCommMonoid (M j i)] [(j : ι) → (i : β) → Module R (M j i)] [(i : β) → AddCommMonoid (N i)] [(i : β) → Module R (N i)] {d : β} (deg : ι → β) (i : β) (hi : ∑ j : ι, deg j + d = i) : ↑0 deg i hi = 0

@[simp]

theorem AInfinityTheory.GradedMultilinearMap.add_apply {R : Type u} [Semiring R] {ι : Type u_1} [Fintype ι] {β : Type v} [AddCommMonoid β] {M : ι → β → Type w₁} {N : β → Type w₂} [(j : ι) → (i : β) → AddCommMonoid (M j i)] [(j : ι) → (i : β) → Module R (M j i)] [(i : β) → AddCommMonoid (N i)] [(i : β) → Module R (N i)] {d : β} (f g : GradedMultilinearMap R M N d) (deg : ι → β) (i : β) (hi : ∑ j : ι, deg j + d = i) : ↑(f + g) deg i hi = ↑f deg i hi + ↑g deg i hi

@[simp]

theorem AInfinityTheory.GradedMultilinearMap.smul_apply {R : Type u} [Semiring R] {ι : Type u_1} [Fintype ι] {β : Type v} [AddCommMonoid β] {M : ι → β → Type w₁} {N : β → Type w₂} [(j : ι) → (i : β) → AddCommMonoid (M j i)] [(j : ι) → (i : β) → Module R (M j i)] [(i : β) → AddCommMonoid (N i)] [(i : β) → Module R (N i)] {d : β} {S : Type u_2} [(i : β) → DistribSMul S (N i)] [∀ (i : β), SMulCommClass R S (N i)] (c : S) (f : GradedMultilinearMap R M N d) (deg : ι → β) (i : β) (hi : ∑ j : ι, deg j + d = i) : ↑(c • f) deg i hi = c • ↑f deg i hi

@[implicit_reducible]

instance AInfinityTheory.GradedMultilinearMap.instSMulNat {R : Type u} [Semiring R] {ι : Type u_1} [Fintype ι] {β : Type v} [AddCommMonoid β] {M : ι → β → Type w₁} {N : β → Type w₂} [(j : ι) → (i : β) → AddCommMonoid (M j i)] [(j : ι) → (i : β) → Module R (M j i)] [(i : β) → AddCommMonoid (N i)] [(i : β) → Module R (N i)] {d : β} : SMul ℕ (GradedMultilinearMap R M N d)

The components of the natural-number multiple n • f are the multiples n • f deg i hi.

Equations

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

@[implicit_reducible]

instance AInfinityTheory.GradedMultilinearMap.instAddCommMonoid {R : Type u} [Semiring R] {ι : Type u_1} [Fintype ι] {β : Type v} [AddCommMonoid β] {M : ι → β → Type w₁} {N : β → Type w₂} [(j : ι) → (i : β) → AddCommMonoid (M j i)] [(j : ι) → (i : β) → Module R (M j i)] [(i : β) → AddCommMonoid (N i)] [(i : β) → Module R (N i)] {d : β} : AddCommMonoid (GradedMultilinearMap R M N d)

Graded multilinear maps of degree d form an additive commutative monoid under componentwise addition.

Equations

• AInfinityTheory.GradedMultilinearMap.instAddCommMonoid = Function.Injective.addCommMonoid AInfinityTheory.GradedMultilinearMap.toPi ⋯ ⋯ ⋯ ⋯

@[implicit_reducible]

instance AInfinityTheory.GradedMultilinearMap.instModuleOfSMulCommClass {R : Type u} [Semiring R] {ι : Type u_1} [Fintype ι] {β : Type v} [AddCommMonoid β] {M : ι → β → Type w₁} {N : β → Type w₂} [(j : ι) → (i : β) → AddCommMonoid (M j i)] [(j : ι) → (i : β) → Module R (M j i)] [(i : β) → AddCommMonoid (N i)] [(i : β) → Module R (N i)] {d : β} {S : Type u_2} [Semiring S] [(i : β) → Module S (N i)] [∀ (i : β), SMulCommClass R S (N i)] : Module S (GradedMultilinearMap R M N d)

Graded multilinear maps of degree d form a module over any semiring S acting on the target compatibly with R.

Equations

• AInfinityTheory.GradedMultilinearMap.instModuleOfSMulCommClass = Function.Injective.module S { toFun := AInfinityTheory.GradedMultilinearMap.toPi, map_zero' := ⋯, map_add' := ⋯ } ⋯ ⋯

@[implicit_reducible]

instance AInfinityTheory.GradedMultilinearMap.instNeg {R : Type u} [Semiring R] {ι : Type u_1} [Fintype ι] {β : Type v} [AddCommMonoid β] {M : ι → β → Type w₁} [(j : ι) → (i : β) → AddCommMonoid (M j i)] [(j : ι) → (i : β) → Module R (M j i)] {d : β} {N : β → Type w₂} [(i : β) → AddCommGroup (N i)] [(i : β) → Module R (N i)] : Neg (GradedMultilinearMap R M N d)

The negation of a graded multilinear map is taken componentwise.

Equations

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

@[implicit_reducible]

instance AInfinityTheory.GradedMultilinearMap.instSub {R : Type u} [Semiring R] {ι : Type u_1} [Fintype ι] {β : Type v} [AddCommMonoid β] {M : ι → β → Type w₁} [(j : ι) → (i : β) → AddCommMonoid (M j i)] [(j : ι) → (i : β) → Module R (M j i)] {d : β} {N : β → Type w₂} [(i : β) → AddCommGroup (N i)] [(i : β) → Module R (N i)] : Sub (GradedMultilinearMap R M N d)

The difference of two graded multilinear maps is taken componentwise.

Equations

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

@[implicit_reducible]

instance AInfinityTheory.GradedMultilinearMap.instSMulInt {R : Type u} [Semiring R] {ι : Type u_1} [Fintype ι] {β : Type v} [AddCommMonoid β] {M : ι → β → Type w₁} [(j : ι) → (i : β) → AddCommMonoid (M j i)] [(j : ι) → (i : β) → Module R (M j i)] {d : β} {N : β → Type w₂} [(i : β) → AddCommGroup (N i)] [(i : β) → Module R (N i)] : SMul ℤ (GradedMultilinearMap R M N d)

The components of the integer multiple n • f are the multiples n • f deg i hi.

Equations

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

@[simp]

theorem AInfinityTheory.GradedMultilinearMap.neg_apply {R : Type u} [Semiring R] {ι : Type u_1} [Fintype ι] {β : Type v} [AddCommMonoid β] {M : ι → β → Type w₁} [(j : ι) → (i : β) → AddCommMonoid (M j i)] [(j : ι) → (i : β) → Module R (M j i)] {d : β} {N : β → Type w₂} [(i : β) → AddCommGroup (N i)] [(i : β) → Module R (N i)] (f : GradedMultilinearMap R M N d) (deg : ι → β) (i : β) (hi : ∑ j : ι, deg j + d = i) : ↑(-f) deg i hi = -↑f deg i hi

@[simp]

theorem AInfinityTheory.GradedMultilinearMap.sub_apply {R : Type u} [Semiring R] {ι : Type u_1} [Fintype ι] {β : Type v} [AddCommMonoid β] {M : ι → β → Type w₁} [(j : ι) → (i : β) → AddCommMonoid (M j i)] [(j : ι) → (i : β) → Module R (M j i)] {d : β} {N : β → Type w₂} [(i : β) → AddCommGroup (N i)] [(i : β) → Module R (N i)] (f g : GradedMultilinearMap R M N d) (deg : ι → β) (i : β) (hi : ∑ j : ι, deg j + d = i) : ↑(f - g) deg i hi = ↑f deg i hi - ↑g deg i hi

@[implicit_reducible]

instance AInfinityTheory.GradedMultilinearMap.instAddCommGroup {R : Type u} [Semiring R] {ι : Type u_1} [Fintype ι] {β : Type v} [AddCommMonoid β] {M : ι → β → Type w₁} [(j : ι) → (i : β) → AddCommMonoid (M j i)] [(j : ι) → (i : β) → Module R (M j i)] {d : β} {N : β → Type w₂} [(i : β) → AddCommGroup (N i)] [(i : β) → Module R (N i)] : AddCommGroup (GradedMultilinearMap R M N d)

Graded multilinear maps of degree d into a family of additive groups form an additive commutative group.

Equations

• AInfinityTheory.GradedMultilinearMap.instAddCommGroup = Function.Injective.addCommGroup AInfinityTheory.GradedMultilinearMap.toPi ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯