Gradings of a path algebra by arrow weights

The path algebra kQ is free on the paths of Q. Give every arrow e a weight wt e in an additive monoid M, and give a path the sum Quiver.Path.addWeight wt of the weights of its arrows. Concatenating paths adds their weights, so the span TauCeti.PathAlgebra.gradeBy k wt m of the paths of weight m makes kQ an M-graded k-algebra once M is commutative. This file constructs that grading in the internal sense: the graded pieces are submodules of kQ itself and the decomposition compares them with kQ, rather than with a separate graded copy of it.

The path-length grading TauCeti.PathAlgebra.grade k Q is the case of the constant weight 1 : ℕ. Degree 0 is the span of the vertex idempotents and degree 1 is the span of the arrows. Each piece is free on the paths of that length, and each sits inside the corresponding step TauCeti.pathSpan k Q n of the length filtration of TauCeti.RepresentationTheory.Quiver.Radical, which spans the paths of length at least n.

Other weights give the underlying gradings of DG path algebras. The (uncompleted) Ginzburg DG algebra has as underlying graded algebra the path algebra of a quiver whose added loops sit in a negative cohomological degree, and its Adams grading is a second, independent weight on the same arrows (Etgü--Lekili; Keller); the standard construction further completes this graded path algebra and equips it with a differential, neither of which is part of gradeBy.

Main definitions

• TauCeti.PathAlgebra.gradeBy: the degree-m piece of the grading by an arrow weight, the span of the paths of weight m.
• TauCeti.PathAlgebra.gradeByBasis: the paths of weight m as a k-basis of that piece.
• TauCeti.PathAlgebra.decomposeAlgHom: the algebra homomorphism to the direct sum decomposing elements by weight, which is DirectSum.decompose for the grading below.
• TauCeti.PathAlgebra.grade: the degree-n piece of the path-length grading, the span of the paths of length n.
• TauCeti.PathAlgebra.gradeBasis: the paths of length n as a k-basis of that piece.
• TauCeti.PathAlgebra.integerGrade: the path-length grading extended by zero to integer degrees, for use with internal grading shifts.

Main results

• TauCeti.PathAlgebra.gradeBy.gradedAlgebra: the grading by an arrow weight, the GradedAlgebra instance on TauCeti.PathAlgebra.gradeBy. Its multiplicative half, TauCeti.PathAlgebra.gradeBy_mul_gradeBy_le, is the statement that multiplication adds weights, and TauCeti.PathAlgebra.isInternal_gradeBy is the comparison of the direct sum of the pieces with kQ itself.
• TauCeti.PathAlgebra.mem_gradeBy_iff: an element is homogeneous of weight m exactly when its path coordinates are supported on the paths of weight m.
• TauCeti.PathAlgebra.ofArrow_mem_gradeBy: an arrow is homogeneous of its own weight, and TauCeti.PathAlgebra.ofArrow_mem_gradeBy_iff and TauCeti.PathAlgebra.vertexIdempotent_mem_gradeBy_iff read off the degree of an arrow and of a vertex idempotent.
• TauCeti.PathAlgebra.gradedAlgebra: the path-length grading, the GradedAlgebra instance on TauCeti.PathAlgebra.grade, with TauCeti.PathAlgebra.grade_mul_grade_le and TauCeti.PathAlgebra.isInternal_grade its two halves.
• TauCeti.PathAlgebra.grade_zero_eq_span_range_vertexIdempotent and TauCeti.PathAlgebra.grade_one_eq_span_range_ofArrow: the vertex idempotents span degree 0 and the arrows span degree 1.
• TauCeti.PathAlgebra.grade_le_pathSpan: the degree-n piece lies in the n-th step of the length filtration.
• TauCeti.PathAlgebra.isInternal_integerGrade: the integer-indexed pieces still form an internal direct sum.

Implementation notes

The grading is constructed from TauCeti.PathAlgebra.decomposeAlgHom, built from the universal property TauCeti.PathAlgebra.liftAlgHom in the same way as AddMonoidAlgebra.gradeBy.gradedAlgebra is built from the universal property of an additive monoid algebra: an assignment of a homogeneous summand to each basis path is an algebra map to the direct sum as soon as it respects the three defining products of kQ. It is what GradedAlgebra.ofAlgHom installs as DirectSum.decompose; the two maps are definitionally equal. As for AddMonoidAlgebra.grade and AddMonoidAlgebra.gradeBy, the length grading is the weight grading at one particular weight, so its graded-algebra structure is that of TauCeti.PathAlgebra.gradeBy.

The unit of kQ is the sum of the vertex idempotents, which exists only for a finite vertex type, so the graded pieces are defined for every quiver while the grading itself asks for [Finite Q].

References

• Assem--Simson--Skowroński, Elements of the Representation Theory of Associative Algebras I, Ch. II, for the path-length grading.
• T. Etgü and Y. Lekili, Koszul duality patterns in Floer theory, and B. Keller, Deformed Calabi--Yau completions, for Ginzburg DG algebras, path algebras graded by arrow degrees.

The pieces of the grading by an arrow weight

noncomputable def TauCeti.PathAlgebra.gradeBy (k : Type w) [Semiring k] {Q : Type u} [Quiver Q] {M : Type u_1} [AddMonoid M] (wt : {a b : Q} → (a ⟶ b) → M) (m : M) : Submodule k (pathAlgebra k Q)

The degree-m piece of the grading of the path algebra by the arrow weight wt: the k-span of the paths whose arrows have weights summing to m.

Equations

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

theorem TauCeti.PathAlgebra.gradeBy_eq_span_image_basis (k : Type w) [Semiring k] {Q : Type u} [Quiver Q] {M : Type u_1} [AddMonoid M] (wt : {a b : Q} → (a ⟶ b) → M) (m : M) : gradeBy k (fun {a b : Q} => wt) m = Submodule.span k (⇑(pathAlgebraBasis k Q) '' {x : Quiver.TotalPath Q | Quiver.Path.addWeight (fun {i j : Q} => wt) x.snd.snd = m})

The degree-m piece is the span of the image of the weight-m paths under the path basis. This is the form the Module.Basis API reads.

theorem TauCeti.PathAlgebra.gradeBy_eq_span_range (k : Type w) [Semiring k] {Q : Type u} [Quiver Q] {M : Type u_1} [AddMonoid M] (wt : {a b : Q} → (a ⟶ b) → M) (m : M) : gradeBy k (fun {a b : Q} => wt) m = Submodule.span k (Set.range fun (x : { x : Quiver.TotalPath Q // Quiver.Path.addWeight (fun {i j : Q} => wt) x.snd.snd = m }) => ofPath ↑x)

The degree-m piece is the span of the weight-m paths, indexed by the subtype they form.

theorem TauCeti.PathAlgebra.mem_gradeBy_iff {k : Type w} [Semiring k] {Q : Type u} [Quiver Q] {M : Type u_1} [AddMonoid M] {wt : {a b : Q} → (a ⟶ b) → M} {m : M} {f : pathAlgebra k Q} : f ∈ gradeBy k (fun {a b : Q} => wt) m ↔ ∀ x ∈ ((pathAlgebraBasis k Q).repr f).support, Quiver.Path.addWeight (fun {i j : Q} => wt) x.snd.snd = m

Homogeneity is a condition on path coordinates: an element has weight m exactly when every path carrying a nonzero coordinate has weight m.

theorem TauCeti.PathAlgebra.ofPath_mem_gradeBy {k : Type w} [Semiring k] {Q : Type u} [Quiver Q] {M : Type u_1} [AddMonoid M] (wt : {a b : Q} → (a ⟶ b) → M) (x : Quiver.TotalPath Q) : ofPath x ∈ gradeBy k (fun {a b : Q} => wt) (Quiver.Path.addWeight (fun {i j : Q} => wt) x.snd.snd)

A basis path is homogeneous of its own weight.

theorem TauCeti.PathAlgebra.ofPath_mem_gradeBy_of_addWeight {k : Type w} [Semiring k] {Q : Type u} [Quiver Q] {M : Type u_1} [AddMonoid M] {wt : {a b : Q} → (a ⟶ b) → M} {m : M} {x : Quiver.TotalPath Q} (hx : Quiver.Path.addWeight (fun {i j : Q} => wt) x.snd.snd = m) : ofPath x ∈ gradeBy k (fun {a b : Q} => wt) m

A path of weight m is homogeneous of degree m.

@[simp]

theorem TauCeti.PathAlgebra.ofPath_mem_gradeBy_iff {k : Type w} [Semiring k] {Q : Type u} [Quiver Q] {M : Type u_1} [AddMonoid M] {wt : {a b : Q} → (a ⟶ b) → M} [Nontrivial k] {m : M} {x : Quiver.TotalPath Q} : ofPath x ∈ gradeBy k (fun {a b : Q} => wt) m ↔ Quiver.Path.addWeight (fun {i j : Q} => wt) x.snd.snd = m

A basis path has degree m exactly when its weight is m.

theorem TauCeti.PathAlgebra.single_mem_gradeBy_of_addWeight {k : Type w} [Semiring k] {Q : Type u} [Quiver Q] {M : Type u_1} [AddMonoid M] {wt : {a b : Q} → (a ⟶ b) → M} {m : M} {x : Quiver.TotalPath Q} (hx : Quiver.Path.addWeight (fun {i j : Q} => wt) x.snd.snd = m) (c : k) : single x c ∈ gradeBy k (fun {a b : Q} => wt) m

A scaled basis path is homogeneous of the weight of that path.

theorem TauCeti.PathAlgebra.vertexIdempotent_mem_gradeBy_zero {k : Type w} [Semiring k] {Q : Type u} [Quiver Q] {M : Type u_1} [AddMonoid M] (wt : {a b : Q} → (a ⟶ b) → M) (v : Q) : vertexIdempotent k v ∈ gradeBy k (fun {a b : Q} => wt) 0

A vertex idempotent is homogeneous of degree 0.

theorem TauCeti.PathAlgebra.ofArrow_mem_gradeBy {k : Type w} [Semiring k] {Q : Type u} [Quiver Q] {M : Type u_1} [AddMonoid M] (wt : {a b : Q} → (a ⟶ b) → M) {a b : Q} (e : a ⟶ b) : ofArrow e ∈ gradeBy k (fun {a b : Q} => wt) (wt e)

An arrow is homogeneous of its own weight.

@[simp]

theorem TauCeti.PathAlgebra.vertexIdempotent_mem_gradeBy_iff {k : Type w} [Semiring k] {Q : Type u} [Quiver Q] {M : Type u_1} [AddMonoid M] {wt : {a b : Q} → (a ⟶ b) → M} [Nontrivial k] {m : M} (v : Q) : vertexIdempotent k v ∈ gradeBy k (fun {a b : Q} => wt) m ↔ m = 0

A vertex idempotent has degree m exactly when m = 0.

theorem TauCeti.PathAlgebra.ofArrow_mem_gradeBy_iff {k : Type w} [Semiring k] {Q : Type u} [Quiver Q] {M : Type u_1} [AddMonoid M] {wt : {a b : Q} → (a ⟶ b) → M} [Nontrivial k] {m : M} {a b : Q} (e : a ⟶ b) : ofArrow e ∈ gradeBy k (fun {a b : Q} => wt) m ↔ wt e = m

An arrow has degree m exactly when its weight is m. Deliberately not a simp lemma: ofArrow_eq_ofPath and ofPath_mem_gradeBy_iff already normalize its left-hand side.

noncomputable def TauCeti.PathAlgebra.gradeByBasis (k : Type w) [Semiring k] {Q : Type u} [Quiver Q] {M : Type u_1} [AddMonoid M] (wt : {a b : Q} → (a ⟶ b) → M) (m : M) : Module.Basis { x : Quiver.TotalPath Q // Quiver.Path.addWeight (fun {i j : Q} => wt) x.snd.snd = m } k ↥(gradeBy k (fun {a b : Q} => wt) m)

The paths of weight m are a k-basis of the degree-m piece: every graded piece is free.

Equations

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

@[simp]

theorem TauCeti.PathAlgebra.coe_gradeByBasis_apply {k : Type w} [Semiring k] {Q : Type u} [Quiver Q] {M : Type u_1} [AddMonoid M] {wt : {a b : Q} → (a ⟶ b) → M} {m : M} (x : { x : Quiver.TotalPath Q // Quiver.Path.addWeight (fun {i j : Q} => wt) x.snd.snd = m }) : ↑((gradeByBasis k (fun {a b : Q} => wt) m) x) = ofPath ↑x

The basis of the degree-m piece consists of the paths of weight m.

theorem TauCeti.PathAlgebra.ofPath_mul_ofPath_mem_gradeBy {k : Type w} {Q : Type u} [Semiring k] [Quiver Q] {M : Type u_1} [AddCommMonoid M] {wt : {a b : Q} → (a ⟶ b) → M} (x y : Quiver.TotalPath Q) : ofPath x * ofPath y ∈ gradeBy k (fun {a b : Q} => wt) (Quiver.Path.addWeight (fun {i j : Q} => wt) x.snd.snd + Quiver.Path.addWeight (fun {i j : Q} => wt) y.snd.snd)

Two paths multiply in the sum of their weights, whether or not they are composable.

theorem TauCeti.PathAlgebra.gradeBy_mul_gradeBy_le {k : Type w} {Q : Type u} [CommSemiring k] [Quiver Q] {M : Type u_1} [AddCommMonoid M] {wt : {a b : Q} → (a ⟶ b) → M} [Finite Q] (i j : M) : gradeBy k (fun {a b : Q} => wt) i * gradeBy k (fun {a b : Q} => wt) j ≤ gradeBy k (fun {a b : Q} => wt) (i + j)

Multiplication adds weights.

The graded algebra structure of an arrow weight

instance TauCeti.PathAlgebra.gradeBy.gradedMonoid (k : Type w) {Q : Type u} [CommSemiring k] [Quiver Q] [Finite Q] {M : Type u_1} [AddCommMonoid M] (wt : {a b : Q} → (a ⟶ b) → M) : SetLike.GradedMonoid (gradeBy k fun {a b : Q} => wt)

The graded pieces form a graded monoid: the unit is the degree-zero sum of the vertex idempotents, and multiplication adds weights.

noncomputable def TauCeti.PathAlgebra.decomposeAlgHom (k : Type w) {Q : Type u} [CommSemiring k] [Quiver Q] [Finite Q] {M : Type u_1} [AddCommMonoid M] (wt : {a b : Q} → (a ⟶ b) → M) [DecidableEq M] : pathAlgebra k Q →ₐ[k] DirectSum M fun (m : M) => ↥(gradeBy k (fun {a b : Q} => wt) m)

The algebra homomorphism into the direct sum of graded pieces that decomposes elements by weight. This is the map GradedAlgebra.ofAlgHom installs as DirectSum.decompose for the grading below, as AddMonoidAlgebra.decomposeAux is for the grading of a monoid algebra; the two maps are definitionally equal.

Equations

• TauCeti.PathAlgebra.decomposeAlgHom k wt = TauCeti.PathAlgebra.liftAlgHom k (TauCeti.PathAlgebra.gradeBySummand✝ k fun {a b : Q} => wt) ⋯ ⋯ ⋯

theorem TauCeti.PathAlgebra.decomposeAlgHom_ofPath (k : Type w) {Q : Type u} [CommSemiring k] [Quiver Q] [Finite Q] {M : Type u_1} [AddCommMonoid M] (wt : {a b : Q} → (a ⟶ b) → M) [DecidableEq M] (x : Quiver.TotalPath Q) : (decomposeAlgHom k fun {a b : Q} => wt) (ofPath x) = (DirectSum.of (fun (m : M) => ↥(gradeBy k (fun {a b : Q} => wt) m)) (Quiver.Path.addWeight (fun {i j : Q} => wt) x.snd.snd)) ⟨ofPath x, ⋯⟩

The decomposition map sends a basis path to the summand its weight names.

theorem TauCeti.PathAlgebra.decomposeAlgHom_of_mem (k : Type w) {Q : Type u} [CommSemiring k] [Quiver Q] [Finite Q] {M : Type u_1} [AddCommMonoid M] (wt : {a b : Q} → (a ⟶ b) → M) [DecidableEq M] {m : M} {f : pathAlgebra k Q} (hf : f ∈ gradeBy k (fun {a b : Q} => wt) m) : (decomposeAlgHom k fun {a b : Q} => wt) f = (DirectSum.of (fun (m' : M) => ↥(gradeBy k (fun {a b : Q} => wt) m')) m) ⟨f, hf⟩

The decomposition map is the identity on a homogeneous element, placing it in the summand its degree names.

@[instance_reducible]

noncomputable instance TauCeti.PathAlgebra.gradeBy.gradedAlgebra (k : Type w) {Q : Type u} [CommSemiring k] [Quiver Q] [Finite Q] {M : Type u_1} [AddCommMonoid M] (wt : {a b : Q} → (a ⟶ b) → M) [DecidableEq M] : GradedAlgebra (gradeBy k fun {a b : Q} => wt)

The grading by an arrow weight: the path algebra of a finite quiver is M-graded by the weight wt, with the span of the paths of weight m in degree m.

Equations

• TauCeti.PathAlgebra.gradeBy.gradedAlgebra k wt = GradedAlgebra.ofAlgHom (TauCeti.PathAlgebra.gradeBy k fun {a b : Q} => wt) (TauCeti.PathAlgebra.decomposeAlgHom k fun {a b : Q} => wt) ⋯ ⋯

theorem TauCeti.PathAlgebra.isInternal_gradeBy (k : Type w) {Q : Type u} [CommSemiring k] [Quiver Q] [Finite Q] {M : Type u_1} [AddCommMonoid M] (wt : {a b : Q} → (a ⟶ b) → M) [DecidableEq M] : DirectSum.IsInternal (gradeBy k fun {a b : Q} => wt)

The path algebra is the internal direct sum of its weight pieces: the direct-sum graded algebra is compared with kQ itself, not with a separate graded copy.

@[simp]

theorem TauCeti.PathAlgebra.decompose_ofPath_gradeBy (k : Type w) {Q : Type u} [CommSemiring k] [Quiver Q] [Finite Q] {M : Type u_1} [AddCommMonoid M] (wt : {a b : Q} → (a ⟶ b) → M) [DecidableEq M] (x : Quiver.TotalPath Q) : (DirectSum.decompose (gradeBy k fun {a b : Q} => wt)) (ofPath x) = (DirectSum.of (fun (m : M) => ↥(gradeBy k (fun {a b : Q} => wt) m)) (Quiver.Path.addWeight (fun {i j : Q} => wt) x.snd.snd)) ⟨ofPath x, ⋯⟩

The decomposition sends a basis path to the summand its weight names.

theorem TauCeti.PathAlgebra.isHomogeneous_gradeBy_gradeBy (k : Type w) {Q : Type u} [CommSemiring k] [Quiver Q] [Finite Q] {M : Type u_1} [AddCommMonoid M] (wt : {a b : Q} → (a ⟶ b) → M) [DecidableEq M] {M' : Type u_2} [AddMonoid M'] (wt' : {a b : Q} → (a ⟶ b) → M') (m : M') : DirectSum.SetLike.IsHomogeneous (gradeBy k fun {a b : Q} => wt) (gradeBy k (fun {a b : Q} => wt') m)

Two arrow weights are compatible: the wt-homogeneous components of an element which is homogeneous of degree m for a second weight wt' are again homogeneous of degree m for wt', because every basis path is homogeneous for both weights at once.

The path-length grading

noncomputable def TauCeti.PathAlgebra.grade (k : Type w) (Q : Type u) [Semiring k] [Quiver Q] (n : ℕ) : Submodule k (pathAlgebra k Q)

The degree-n piece of the path-length grading of the path algebra: the k-span of the paths of length n. It is the grading by the constant arrow weight 1.

Equations

• TauCeti.PathAlgebra.grade k Q n = TauCeti.PathAlgebra.gradeBy k (fun {a b : Q} (x : a ⟶ b) => 1) n

theorem TauCeti.PathAlgebra.gradeBy_const_one (k : Type w) (Q : Type u) [Semiring k] [Quiver Q] : (gradeBy k fun {a b : Q} (x : a ⟶ b) => 1) = grade k Q

The path-length grading is the grading by the constant arrow weight 1.

theorem TauCeti.PathAlgebra.grade_eq_span_image_basis (k : Type w) (Q : Type u) [Semiring k] [Quiver Q] (n : ℕ) : grade k Q n = Submodule.span k (⇑(pathAlgebraBasis k Q) '' {x : Quiver.TotalPath Q | x.snd.snd.length = n})

The degree-n piece is the span of the image of the length-n paths under the path basis. This is the form the Module.Basis API reads.

theorem TauCeti.PathAlgebra.grade_eq_span_range (k : Type w) (Q : Type u) [Semiring k] [Quiver Q] (n : ℕ) : grade k Q n = Submodule.span k (Set.range fun (x : { x : Quiver.TotalPath Q // x.snd.snd.length = n }) => ofPath ↑x)

The degree-n piece is the span of the length-n paths, indexed by the subtype they form.

theorem TauCeti.PathAlgebra.mem_grade_iff {k : Type w} {Q : Type u} [Semiring k] [Quiver Q] {n : ℕ} {f : pathAlgebra k Q} : f ∈ grade k Q n ↔ ∀ x ∈ ((pathAlgebraBasis k Q).repr f).support, x.snd.snd.length = n

Homogeneity is a condition on path coordinates: an element has degree n exactly when every path carrying a nonzero coordinate has length n.

theorem TauCeti.PathAlgebra.ofPath_mem_grade_of_length {k : Type w} {Q : Type u} [Semiring k] [Quiver Q] {n : ℕ} {x : Quiver.TotalPath Q} (hx : x.snd.snd.length = n) : ofPath x ∈ grade k Q n

A path of length n is homogeneous of degree n.

theorem TauCeti.PathAlgebra.ofPath_mem_grade {k : Type w} {Q : Type u} [Semiring k] [Quiver Q] (x : Quiver.TotalPath Q) : ofPath x ∈ grade k Q x.snd.snd.length

A basis path is homogeneous of its own length.

@[simp]

theorem TauCeti.PathAlgebra.ofPath_mem_grade_iff {k : Type w} {Q : Type u} [Semiring k] [Quiver Q] [Nontrivial k] {n : ℕ} {x : Quiver.TotalPath Q} : ofPath x ∈ grade k Q n ↔ x.snd.snd.length = n

A basis path has degree n exactly when its length is n.

theorem TauCeti.PathAlgebra.single_mem_grade_of_length {k : Type w} {Q : Type u} [Semiring k] [Quiver Q] {n : ℕ} {x : Quiver.TotalPath Q} (hx : x.snd.snd.length = n) (c : k) : single x c ∈ grade k Q n

A scaled basis path is homogeneous of the length of that path.

theorem TauCeti.PathAlgebra.vertexIdempotent_mem_grade_zero {k : Type w} {Q : Type u} [Semiring k] [Quiver Q] (v : Q) : vertexIdempotent k v ∈ grade k Q 0

A vertex idempotent is homogeneous of degree 0.

theorem TauCeti.PathAlgebra.ofPath_mul_ofPath_mem_grade {k : Type w} {Q : Type u} [Semiring k] [Quiver Q] (x y : Quiver.TotalPath Q) : ofPath x * ofPath y ∈ grade k Q (x.snd.snd.length + y.snd.snd.length)

Two paths multiply in the sum of their degrees, whether or not they are composable.

noncomputable def TauCeti.PathAlgebra.gradeBasis (k : Type w) (Q : Type u) [Semiring k] [Quiver Q] (n : ℕ) : Module.Basis { x : Quiver.TotalPath Q // x.snd.snd.length = n } k ↥(grade k Q n)

The paths of length n are a k-basis of the degree-n piece: every graded piece is free.

Equations

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

@[simp]

theorem TauCeti.PathAlgebra.coe_gradeBasis_apply {k : Type w} {Q : Type u} [Semiring k] [Quiver Q] {n : ℕ} (x : { x : Quiver.TotalPath Q // x.snd.snd.length = n }) : ↑((gradeBasis k Q n) x) = ofPath ↑x

The basis of the degree-n piece consists of the paths of length n.

theorem TauCeti.PathAlgebra.grade_zero_eq_span_range_vertexIdempotent (k : Type w) (Q : Type u) [Semiring k] [Quiver Q] : grade k Q 0 = Submodule.span k (Set.range (vertexIdempotent k))

Degree 0 is the span of the vertex idempotents: the trivial paths are exactly the paths of length zero.

theorem TauCeti.PathAlgebra.grade_le_pathSpan (k : Type w) (Q : Type u) [Semiring k] [Quiver Q] (n : ℕ) : grade k Q n ≤ pathSpan k Q n

The degree-n piece lies in the n-th step of the length filtration: a path of length exactly n is in particular a path of length at least n.

theorem TauCeti.PathAlgebra.ofArrow_mem_grade_one {k : Type w} {Q : Type u} [Semiring k] [Quiver Q] {a b : Q} (e : a ⟶ b) : ofArrow e ∈ grade k Q 1

An arrow is homogeneous of degree 1.

theorem TauCeti.PathAlgebra.grade_one_eq_span_range_ofArrow {k : Type w} {Q : Type u} [Semiring k] [Quiver Q] : grade k Q 1 = Submodule.span k (Set.range fun (e : (a : Q) × (b : Q) × (a ⟶ b)) => ofArrow e.snd.snd)

Degree 1 is the span of the arrows: the length-one paths are exactly the arrows.

noncomputable def TauCeti.PathAlgebra.arrowBasis (k : Type w) (Q : Type u) [Semiring k] [Quiver Q] : Module.Basis ((a : Q) × (b : Q) × (a ⟶ b)) k ↥(grade k Q 1)

The arrows form a basis of the degree-one part of the path algebra.

Equations

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

@[simp]

theorem TauCeti.PathAlgebra.coe_arrowBasis_apply (k : Type w) (Q : Type u) [Semiring k] [Quiver Q] (e : (a : Q) × (b : Q) × (a ⟶ b)) : ↑((arrowBasis k Q) e) = ofArrow e.snd.snd

A degree-one basis vector is the corresponding arrow in the path algebra.

theorem TauCeti.PathAlgebra.pathSpan_eq_grade_sup_pathSpan_succ (k : Type w) (Q : Type u) [Semiring k] [Quiver Q] (n : ℕ) : pathSpan k Q n = grade k Q n ⊔ pathSpan k Q (n + 1)

Each step of the length filtration splits into its lowest degree and the next step.

theorem TauCeti.PathAlgebra.grade_mul_grade_le {k : Type w} {Q : Type u} [CommSemiring k] [Quiver Q] [Finite Q] (i j : ℕ) : grade k Q i * grade k Q j ≤ grade k Q (i + j)

Multiplication adds degrees.

instance TauCeti.PathAlgebra.gradedMonoid (k : Type w) (Q : Type u) [CommSemiring k] [Quiver Q] [Finite Q] : SetLike.GradedMonoid (grade k Q)

The length pieces form a graded monoid, transported from the graded monoid of the constant weight 1 along TauCeti.PathAlgebra.gradeBy_const_one.

@[instance_reducible]

noncomputable instance TauCeti.PathAlgebra.gradedAlgebra (k : Type w) (Q : Type u) [CommSemiring k] [Quiver Q] [Finite Q] : GradedAlgebra (grade k Q)

The path-length grading: the path algebra of a finite quiver is ℕ-graded by path length, with the span of the paths of length n in degree n. It is the grading by the constant weight 1, transported along TauCeti.PathAlgebra.gradeBy_const_one.

Equations

• TauCeti.PathAlgebra.gradedAlgebra k Q = ⋯ ▸ TauCeti.PathAlgebra.gradeBy.gradedAlgebra k fun {a b : Q} (x : a ⟶ b) => 1

theorem TauCeti.PathAlgebra.isInternal_grade (k : Type w) (Q : Type u) [CommSemiring k] [Quiver Q] [Finite Q] : DirectSum.IsInternal (grade k Q)

The path algebra is the internal direct sum of its graded pieces: the direct-sum graded algebra is compared with kQ itself, not with a separate graded copy.

@[simp]

theorem TauCeti.PathAlgebra.decompose_ofPath (k : Type w) (Q : Type u) [CommSemiring k] [Quiver Q] [Finite Q] (x : Quiver.TotalPath Q) : (DirectSum.decompose (grade k Q)) (ofPath x) = (DirectSum.of (fun (n : ℕ) => ↥(grade k Q n)) x.snd.snd.length) ⟨ofPath x, ⋯⟩

The decomposition sends a basis path to the summand indexed by its length.

Integer-indexed path-length grading

noncomputable def TauCeti.PathAlgebra.integerGrade (k : Type w) (Q : Type u) [CommSemiring k] [Quiver Q] (d : ℤ) : Submodule k (pathAlgebra k Q)

The path-length grading of kQ, extended by zero from natural to integer degrees. This is the indexing used by graded-module shifts.

Equations

• TauCeti.PathAlgebra.integerGrade k Q d = TauCeti.Graded.extendByZero (TauCeti.PathAlgebra.grade k Q) d

@[simp]

theorem TauCeti.PathAlgebra.integerGrade_ofNat (k : Type w) (Q : Type u) [CommSemiring k] [Quiver Q] (n : ℕ) : integerGrade k Q ↑n = grade k Q n

Extending the path-length grading to the integer degree n recovers its natural-degree piece.

@[simp]

theorem TauCeti.PathAlgebra.integerGrade_eq_bot_of_neg (k : Type w) (Q : Type u) [CommSemiring k] [Quiver Q] {d : ℤ} (hd : d < 0) : integerGrade k Q d = ⊥

The integer path-length grading vanishes in negative degrees.

theorem TauCeti.PathAlgebra.vertexIdempotent_mem_integerGrade_zero (k : Type w) (Q : Type u) [CommSemiring k] [Quiver Q] (i : Q) : vertexIdempotent k i ∈ integerGrade k Q 0

A vertex idempotent has integer degree zero.

theorem TauCeti.PathAlgebra.isInternal_integerGrade (k : Type w) (Q : Type u) [CommSemiring k] [Quiver Q] [Finite Q] : DirectSum.IsInternal (integerGrade k Q)

The integer-indexed path-length pieces form an internal direct sum.

@[instance_reducible]

noncomputable def TauCeti.PathAlgebra.integerGradedAlgebra (k : Type w) (Q : Type u) [CommSemiring k] [Quiver Q] [Finite Q] : GradedAlgebra (integerGrade k Q)

The path algebra is integer graded by path length, with zero pieces in negative degrees.

Equations

• TauCeti.PathAlgebra.integerGradedAlgebra k Q = { toGradedMonoid := ⋯, toDecomposition := DirectSum.IsInternal.chooseDecomposition (TauCeti.PathAlgebra.integerGrade k Q) ⋯ }