The total module of morphisms of a graded linear quiver

The total module of a graded linear quiver is the external direct sum ⨁ (X, Y), Hom(X, Y) of all of its hom modules, graded degreewise. Operations on composable strings of morphisms are conveniently encoded as multilinear operations on the total module which respect the decomposition into hom modules: a string aₙ, …, a₁ with aᵢ : Xᵢ₋₁ ⟶ Xᵢ is sent to a morphism X₀ ⟶ Xₙ, and a string that is not composable is sent to zero. This is the predicate TauCeti.GradedLinearQuiver.IsPathCompatible. It lets the structure on a many-object quiver be stated as structure on a single graded module, the many-object analogue of an algebra over the product of copies of the ground ring indexed by the objects.

The inclusion and projection of a single hom module are homInclusion and homProjection. They are DirectSum.lof and DirectSum.component; homInclusion is defined with classical decidable equality on objects, so that no decidability assumption on the objects enters the statements that use it.

Main definitions

• TauCeti.GradedLinearQuiver.TotalHom: the direct sum of all hom modules.
• TauCeti.GradedLinearQuiver.totalGrading: its degreewise grading.
• TauCeti.GradedLinearQuiver.homInclusion and TauCeti.GradedLinearQuiver.homProjection: the inclusion and projection of the hom module of a pair of objects.
• TauCeti.GradedLinearQuiver.IsPathCompatible: a multilinear operation on the total module sending composable strings to the hom module of their endpoints and other strings to zero.

Main results

• TauCeti.GradedLinearQuiver.mem_totalGrading_piece_iff: an element of the total module has degree n exactly when each of its components has.
• TauCeti.GradedLinearQuiver.homInclusion_homProjection_of_mem_range: an element of the image of a hom module is recovered from its component there.
• TauCeti.GradedLinearQuiver.IsPathCompatible.ext: a path-compatible operation is determined by its values on composable strings.

References

• B. Keller, Introduction to A-infinity algebras and modules, Section 7.1.

@[reducible, inline]

abbrev TauCeti.GradedLinearQuiver.TotalHom (R : Type w) [CommRing R] (C : Type u) [GradedLinearQuiver R C] : Type (max u v)

The total module of morphisms of a graded linear quiver: the external direct sum of the hom modules of all ordered pairs of objects.

Equations

• TauCeti.GradedLinearQuiver.TotalHom R C = DirectSum (C × C) fun (p : C × C) => ↑(TauCeti.GradedLinearQuiver.homModule p.1 p.2)

noncomputable def TauCeti.GradedLinearQuiver.totalGrading (R : Type w) [CommRing R] (C : Type u) [GradedLinearQuiver R C] : InternalGrading R (TotalHom R C)

The grading of the total module of morphisms: an element has degree n when each of its components has degree n.

Equations

• TauCeti.GradedLinearQuiver.totalGrading R C = TauCeti.InternalGrading.directSum fun (p : C × C) => TauCeti.GradedLinearQuiver.grading p.1 p.2

noncomputable def TauCeti.GradedLinearQuiver.homInclusion {R : Type w} [CommRing R] {C : Type u} [GradedLinearQuiver R C] (X Y : C) : ↑(homModule X Y) →ₗ[R] TotalHom R C

The inclusion of the morphisms X ⟶ Y into the total module of morphisms.

Equations

• TauCeti.GradedLinearQuiver.homInclusion X Y = DirectSum.lof R (C × C) (fun (p : C × C) => ↑(TauCeti.GradedLinearQuiver.homModule p.1 p.2)) (X, Y)

noncomputable def TauCeti.GradedLinearQuiver.homProjection {R : Type w} [CommRing R] {C : Type u} [GradedLinearQuiver R C] (X Y : C) : TotalHom R C →ₗ[R] ↑(homModule X Y)

The projection of the total module of morphisms onto the morphisms X ⟶ Y.

Equations

• TauCeti.GradedLinearQuiver.homProjection X Y = DirectSum.component R (C × C) (fun (p : C × C) => ↑(TauCeti.GradedLinearQuiver.homModule p.1 p.2)) (X, Y)

theorem TauCeti.GradedLinearQuiver.homInclusion_eq_lof {R : Type w} [CommRing R] {C : Type u} [GradedLinearQuiver R C] [DecidableEq C] (X Y : C) : homInclusion X Y = DirectSum.lof R (C × C) (fun (p : C × C) => ↑(homModule p.1 p.2)) (X, Y)

The inclusion of a hom module is the direct-sum inclusion of its summand, for any decidable equality on the objects.

@[simp]

theorem TauCeti.GradedLinearQuiver.homProjection_homInclusion {R : Type w} [CommRing R] {C : Type u} [GradedLinearQuiver R C] (X Y : C) (f : ↑(homModule X Y)) : (homProjection X Y) ((homInclusion X Y) f) = f

Projecting an included morphism back to its own hom module recovers it.

@[simp]

theorem TauCeti.GradedLinearQuiver.homProjection_homInclusion_of_ne {R : Type w} [CommRing R] {C : Type u} [GradedLinearQuiver R C] {X Y X' Y' : C} (h : (X, Y) ≠ (X', Y')) (f : ↑(homModule X Y)) : (homProjection X' Y') ((homInclusion X Y) f) = 0

Projecting an included morphism to the hom module of another pair of objects gives zero.

theorem TauCeti.GradedLinearQuiver.homInclusion_injective {R : Type w} [CommRing R] {C : Type u} [GradedLinearQuiver R C] (X Y : C) : Function.Injective ⇑(homInclusion X Y)

The inclusion of a hom module into the total module is injective.

theorem TauCeti.GradedLinearQuiver.totalHom_ext {R : Type w} [CommRing R] {C : Type u} [GradedLinearQuiver R C] {x y : TotalHom R C} (h : ∀ (X Y : C), (homProjection X Y) x = (homProjection X Y) y) : x = y

Two elements of the total module of morphisms are equal when all of their components are.

theorem TauCeti.GradedLinearQuiver.homInclusion_homProjection_of_mem_range {R : Type w} [CommRing R] {C : Type u} [GradedLinearQuiver R C] {X Y : C} {x : TotalHom R C} (hx : x ∈ (homInclusion X Y).range) : (homInclusion X Y) ((homProjection X Y) x) = x

An element of the image of the morphisms X ⟶ Y is the inclusion of its component there.

theorem TauCeti.GradedLinearQuiver.mem_totalGrading_piece_iff {R : Type w} [CommRing R] {C : Type u} [GradedLinearQuiver R C] (n : ℤ) (x : TotalHom R C) : x ∈ (totalGrading R C).piece n ↔ ∀ (X Y : C), (homProjection X Y) x ∈ (grading X Y).piece n

An element of the total module of morphisms has degree n exactly when each of its components has degree n.

theorem TauCeti.GradedLinearQuiver.homProjection_mem_piece {R : Type w} [CommRing R] {C : Type u} [GradedLinearQuiver R C] {n : ℤ} {x : TotalHom R C} (hx : x ∈ (totalGrading R C).piece n) (X Y : C) : (homProjection X Y) x ∈ (grading X Y).piece n

The component of an element of degree n of the total module has degree n.

@[simp]

theorem TauCeti.GradedLinearQuiver.homInclusion_mem_totalGrading_piece_iff {R : Type w} [CommRing R] {C : Type u} [GradedLinearQuiver R C] {X Y : C} (n : ℤ) (f : ↑(homModule X Y)) : (homInclusion X Y) f ∈ (totalGrading R C).piece n ↔ f ∈ (grading X Y).piece n

An included morphism has degree n in the total module exactly when it has degree n.

structure TauCeti.GradedLinearQuiver.IsPathCompatible {R : Type w} [CommRing R] {C : Type u} [GradedLinearQuiver R C] {n : ℕ} (f : MultilinearMap R (fun (x : Fin n) => TotalHom R C) (TotalHom R C)) : Prop

A multilinear operation on the total module of morphisms is path-compatible when it is an operation on composable strings of morphisms. Inputs are ordered aₙ, …, a₁ with aᵢ : Xᵢ₋₁ ⟶ Xᵢ, as for TauCeti.GradedLinearQuiver.PathOperation: the i-th input of a string X : Fin (n + 1) → C runs from X (n - 1 - i) to X (n - i). A path-compatible operation sends such a composable string to a morphism X₀ ⟶ Xₙ, and sends every string of morphisms which is not composable to zero.

Since a multilinear map on a direct sum is determined by its values on the summands, a path-compatible operation is determined by its values on composable strings.

• mem_range_homInclusion (X : Fin (n + 1) → C) (x : (i : Fin n) → ↑(homModule (X i.rev.castSucc) (X i.rev.succ))) : (f fun (i : Fin n) => (homInclusion (X i.rev.castSucc) (X i.rev.succ)) (x i)) ∈ (homInclusion (X 0) (X (Fin.last n))).range

  A composable string is sent to a morphism between the endpoints of the string.

• eq_zero_of_ne (s t : Fin n → C) (x : (i : Fin n) → ↑(homModule (s i) (t i))) (i j : Fin n) (hij : ↑j = ↑i + 1) (hne : t j ≠ s i) : (f fun (k : Fin n) => (homInclusion (s k) (t k)) (x k)) = 0

  A string in which the target of the j-th morphism is not the source of the i-th, for j = i + 1, is sent to zero.

theorem TauCeti.GradedLinearQuiver.IsPathCompatible.ext {R : Type w} [CommRing R] {C : Type u} [GradedLinearQuiver R C] {n : ℕ} {f g : MultilinearMap R (fun (x : Fin n) => TotalHom R C) (TotalHom R C)} (hf : IsPathCompatible f) (hg : IsPathCompatible g) (h : ∀ (X : Fin (n + 1) → C) (x : (i : Fin n) → ↑(homModule (X i.rev.castSucc) (X i.rev.succ))), (f fun (i : Fin n) => (homInclusion (X i.rev.castSucc) (X i.rev.succ)) (x i)) = g fun (i : Fin n) => (homInclusion (X i.rev.castSucc) (X i.rev.succ)) (x i)) : f = g

Path-compatible operations are determined by their values on composable strings.