Quadratic duality for path algebras

A quadratic algebra presented on a quiver Q is kQ / (R) for a space R of k-linear combinations of paths of length two. Its quadratic dual is presented on the opposite quiver by the orthogonal complement R^⊥ of R for the pairing which makes the paths of length two an orthonormal family: the arrow space of the opposite quiver is dual to the arrow space of Q through the dual basis of the arrows, and the induced pairing of length-two paths is the diagonal one.

The path algebra of the opposite quiver is the opposite algebra (kQ)ᵐᵒᵖ, and this file uses the latter directly, so that the orthogonal complement R^⊥ is a space of length-two elements of kQ and the dual algebra is

(kQ)ᵐᵒᵖ / (op R^⊥).

Working on the opposite side is not a convention that can be dropped: a length-two path b a of Q, read later-factor-first, pairs with the dual arrows in the order a* b*, which is a path of the opposite quiver. For a quiver with an involutive reversal of arrows the two sides are identified by TauCeti.PathAlgebra.reverseOpAlgEquiv, and the dual algebra can then be presented back on Q itself.

The pairing is defined on the whole path algebra, not just on its degree-two piece: it is the pairing of TauCeti.pathAlgebraBasis with itself, so the coordinate of an element on a path is its pairing with that path. Restricting the orthogonality condition to degree two is what TauCeti.PathAlgebra.quadraticOrthogonal does.

Implementation notes

TauCeti.PathAlgebra.pathPairing is Module.Basis.toDual of the path basis with the decidable equality of paths fixed classically. Fixing it is what keeps DecidableEq (Quiver.TotalPath Q) out of the signatures below, which no quiver supplies; the pairing itself does not depend on the choice.

Duality here is taken through the path basis: R^⊥ is the annihilator of R inside the degree-two part of kQ itself, and the degree-one part of (kQ)ᵐᵒᵖ is the span of the dual arrows. That span is all of the dual of the arrow module exactly when the quiver has finitely many arrows, [∀ a b : Q, Finite (a ⟶ b)]: a free module is identified with its full linear dual by its dual basis only in finite rank. Accordingly, the pairing and orthogonal-complement API is stated for arbitrary quivers, as Submodule.dualAnnihilator carries no finiteness hypothesis, while the named quadratic-dual ideal, algebra, and universal-property API assumes finite arrow types. That hypothesis delimits what those names mean rather than entering their construction, so it is carried as an underscore-named instance argument on TauCeti.PathAlgebra.quadraticDualIdeal, from which the rest of the dual API inherits it. The dual relation ideal needs nothing more, while the quadratic dual algebra and its universal property additionally assume [Finite Q], which the unit of the path algebra needs.

Main definitions

• TauCeti.PathAlgebra.pathPairing: the pairing of the path algebra with itself for which the paths are an orthonormal family.
• TauCeti.PathAlgebra.quadraticOrthogonal: the orthogonal complement R^⊥ inside the degree-two piece.
• TauCeti.PathAlgebra.quadraticDualIdeal and TauCeti.PathAlgebra.quadraticDual: the relation ideal of the quadratic dual inside (kQ)ᵐᵒᵖ, and the quadratic dual algebra, with quotient map TauCeti.PathAlgebra.quadraticDualMk and universal property TauCeti.PathAlgebra.quadraticDualLift.

Main results

• TauCeti.PathAlgebra.pathPairing_apply_ofPath and TauCeti.PathAlgebra.pathPairing_ofPath_apply: pairing with a path reads off the coordinate on it.
• TauCeti.PathAlgebra.mem_quadraticOrthogonal_span_iff: orthogonality to a spanning set of relations suffices.

References

Quadratic duality of quadratic algebras over a semisimple base, in the form used for quiver algebras, follows A. Polishchuk and L. Positselski, Quadratic algebras, Chapter 1, Section 2.

The pairing of the path basis with itself

noncomputable def TauCeti.PathAlgebra.pathPairing (k : Type w) (Q : Type u) [CommSemiring k] [Quiver Q] : pathAlgebra k Q →ₗ[k] Module.Dual k (pathAlgebra k Q)

The pairing of the path algebra with itself for which the paths of Q are an orthonormal family: ⟨f, g⟩ is the sum over the paths x of the product of the coordinates of f and g on x. It realizes the finite-support dual-basis pairing on the degree-two part of the path algebra, and so computes the relations of a quadratic dual.

@[simp]

theorem TauCeti.PathAlgebra.pathPairing_apply_ofPath {k : Type w} {Q : Type u} [CommSemiring k] [Quiver Q] (f : pathAlgebra k Q) (x : Quiver.TotalPath Q) : ((pathPairing k Q) f) (ofPath x) = ((pathAlgebraBasis k Q).repr f) x

Pairing with a path reads off the coordinate on that path.

@[simp]

theorem TauCeti.PathAlgebra.pathPairing_ofPath_apply {k : Type w} {Q : Type u} [CommSemiring k] [Quiver Q] (x : Quiver.TotalPath Q) (g : pathAlgebra k Q) : ((pathPairing k Q) (ofPath x)) g = ((pathAlgebraBasis k Q).repr g) x

The pairing is symmetric on the path basis: pairing a path with an element reads off the coordinate of that element on the path.

The orthogonal complement of a space of quadratic relations

noncomputable def TauCeti.PathAlgebra.quadraticOrthogonal (k : Type w) (Q : Type u) [CommSemiring k] [Quiver Q] (R : Submodule k (pathAlgebra k Q)) : Submodule k (pathAlgebra k Q)

The orthogonal complement of a space of quadratic relations: the degree-two elements of the path algebra pairing to zero with every element of R. It is the relation space of the quadratic dual, read on the path algebra of Q rather than of its opposite.

theorem TauCeti.PathAlgebra.mem_quadraticOrthogonal_iff {k : Type w} {Q : Type u} [CommSemiring k] [Quiver Q] {R : Submodule k (pathAlgebra k Q)} {f : pathAlgebra k Q} : f ∈ quadraticOrthogonal k Q R ↔ f ∈ grade k Q 2 ∧ ∀ g ∈ R, ((pathPairing k Q) f) g = 0

Membership of the orthogonal complement: degree two, and orthogonality to every relation.

theorem TauCeti.PathAlgebra.mem_quadraticOrthogonal_span_iff {k : Type w} {Q : Type u} [CommSemiring k] [Quiver Q] {S : Set (pathAlgebra k Q)} {f : pathAlgebra k Q} : f ∈ quadraticOrthogonal k Q (Submodule.span k S) ↔ f ∈ grade k Q 2 ∧ ∀ g ∈ S, ((pathPairing k Q) f) g = 0

Orthogonality to a spanning set of relations suffices: for a relation space presented by generators, only the generators have to be tested.

theorem TauCeti.PathAlgebra.quadraticOrthogonal_le_grade_two {k : Type w} {Q : Type u} [CommSemiring k] [Quiver Q] (R : Submodule k (pathAlgebra k Q)) : quadraticOrthogonal k Q R ≤ grade k Q 2

The orthogonal complement consists of degree-two elements.

theorem TauCeti.PathAlgebra.quadraticOrthogonal_antitone {k : Type w} {Q : Type u} [CommSemiring k] [Quiver Q] : Antitone (quadraticOrthogonal k Q)

The orthogonal complement is antitone in the space of relations.

The quadratic dual algebra

noncomputable def TauCeti.PathAlgebra.quadraticDualIdeal (k : Type w) (Q : Type u) [CommRing k] [Quiver Q] (R : Submodule k (pathAlgebra k Q)) [_finiteArrows : ∀ (a b : Q), Finite (a ⟶ b)] : TwoSidedIdeal (pathAlgebra k Q)ᵐᵒᵖ

The relation ideal of the quadratic dual: the two-sided ideal of the opposite path algebra generated by the orthogonal complement of R.

theorem TauCeti.PathAlgebra.quadraticDualIdeal_eq_span (k : Type w) (Q : Type u) [CommRing k] [Quiver Q] (R : Submodule k (pathAlgebra k Q)) [∀ (a b : Q), Finite (a ⟶ b)] : quadraticDualIdeal k Q R = TwoSidedIdeal.span (MulOpposite.op '' ↑(quadraticOrthogonal k Q R))

The dual relation ideal is the two-sided span of the orthogonal complement.

theorem TauCeti.PathAlgebra.op_mem_quadraticDualIdeal {k : Type w} {Q : Type u} [CommRing k] [Quiver Q] {R : Submodule k (pathAlgebra k Q)} [∀ (a b : Q), Finite (a ⟶ b)] {f : pathAlgebra k Q} (hf : f ∈ quadraticOrthogonal k Q R) : MulOpposite.op f ∈ quadraticDualIdeal k Q R

Every orthogonal relation lies in the dual relation ideal.

@[reducible, inline]

noncomputable abbrev TauCeti.PathAlgebra.quadraticDual (k : Type w) (Q : Type u) [CommRing k] [Quiver Q] (R : Submodule k (pathAlgebra k Q)) [Finite Q] [∀ (a b : Q), Finite (a ⟶ b)] : Type (max (max (max u v) w) (max w v) u)

The quadratic dual algebra of the quadratic algebra kQ / (R): the opposite path algebra modulo the orthogonal complement of R.

noncomputable def TauCeti.PathAlgebra.quadraticDualMk (k : Type w) (Q : Type u) [CommRing k] [Quiver Q] (R : Submodule k (pathAlgebra k Q)) [Finite Q] [∀ (a b : Q), Finite (a ⟶ b)] : (pathAlgebra k Q)ᵐᵒᵖ →ₐ[k] quadraticDual k Q R

The quotient map onto the quadratic dual algebra.

theorem TauCeti.PathAlgebra.quadraticDualMk_apply (k : Type w) (Q : Type u) [CommRing k] [Quiver Q] (R : Submodule k (pathAlgebra k Q)) [Finite Q] [∀ (a b : Q), Finite (a ⟶ b)] (f : (pathAlgebra k Q)ᵐᵒᵖ) : (quadraticDualMk k Q R) f = (Ideal.Quotient.mk (TwoSidedIdeal.asIdeal (quadraticDualIdeal k Q R))) f

theorem TauCeti.PathAlgebra.quadraticDualMk_surjective (k : Type w) (Q : Type u) [CommRing k] [Quiver Q] (R : Submodule k (pathAlgebra k Q)) [Finite Q] [∀ (a b : Q), Finite (a ⟶ b)] : Function.Surjective ⇑(quadraticDualMk k Q R)

@[simp]

theorem TauCeti.PathAlgebra.quadraticDualMk_eq_zero_iff (k : Type w) (Q : Type u) [CommRing k] [Quiver Q] (R : Submodule k (pathAlgebra k Q)) [Finite Q] [∀ (a b : Q), Finite (a ⟶ b)] {f : (pathAlgebra k Q)ᵐᵒᵖ} : (quadraticDualMk k Q R) f = 0 ↔ f ∈ quadraticDualIdeal k Q R

@[simp]

theorem TauCeti.PathAlgebra.quadraticDualMk_op_eq_zero {k : Type w} {Q : Type u} [CommRing k] [Quiver Q] {R : Submodule k (pathAlgebra k Q)} [Finite Q] [∀ (a b : Q), Finite (a ⟶ b)] {f : pathAlgebra k Q} (hf : f ∈ quadraticOrthogonal k Q R) : (quadraticDualMk k Q R) (MulOpposite.op f) = 0

The defining relations of the quadratic dual: every orthogonal relation dies in it.

The universal property of the quadratic dual

theorem TauCeti.PathAlgebra.quadraticDualIdeal_le_ker {k : Type w} {Q : Type u} {B : Type u_1} [CommRing k] [Quiver Q] [Finite Q] [Semiring B] [Algebra k B] {R : Submodule k (pathAlgebra k Q)} (f : (pathAlgebra k Q)ᵐᵒᵖ →ₐ[k] B) [∀ (a b : Q), Finite (a ⟶ b)] (hf : ∀ x ∈ quadraticOrthogonal k Q R, f (MulOpposite.op x) = 0) : quadraticDualIdeal k Q R ≤ TwoSidedIdeal.ker f

An algebra map out of the opposite path algebra which kills every orthogonal relation kills the dual relation ideal.

noncomputable def TauCeti.PathAlgebra.quadraticDualLift {k : Type w} {Q : Type u} {B : Type u_1} [CommRing k] [Quiver Q] [Finite Q] [Semiring B] [Algebra k B] {R : Submodule k (pathAlgebra k Q)} (f : (pathAlgebra k Q)ᵐᵒᵖ →ₐ[k] B) [∀ (a b : Q), Finite (a ⟶ b)] (hf : ∀ x ∈ quadraticOrthogonal k Q R, f (MulOpposite.op x) = 0) : quadraticDual k Q R →ₐ[k] B

The universal property of the quadratic dual: an algebra map out of the opposite path algebra which kills every orthogonal relation descends to the quadratic dual.

theorem TauCeti.PathAlgebra.quadraticDualLift_comp_quadraticDualMk {k : Type w} {Q : Type u} {B : Type u_1} [CommRing k] [Quiver Q] [Finite Q] [Semiring B] [Algebra k B] {R : Submodule k (pathAlgebra k Q)} (f : (pathAlgebra k Q)ᵐᵒᵖ →ₐ[k] B) [∀ (a b : Q), Finite (a ⟶ b)] (hf : ∀ x ∈ quadraticOrthogonal k Q R, f (MulOpposite.op x) = 0) : (quadraticDualLift f hf).comp (quadraticDualMk k Q R) = f

The lift descends f: composing it with the quotient map recovers f.

@[simp]

theorem TauCeti.PathAlgebra.quadraticDualLift_quadraticDualMk {k : Type w} {Q : Type u} {B : Type u_1} [CommRing k] [Quiver Q] [Finite Q] [Semiring B] [Algebra k B] {R : Submodule k (pathAlgebra k Q)} (f : (pathAlgebra k Q)ᵐᵒᵖ →ₐ[k] B) [∀ (a b : Q), Finite (a ⟶ b)] (hf : ∀ x ∈ quadraticOrthogonal k Q R, f (MulOpposite.op x) = 0) (x : (pathAlgebra k Q)ᵐᵒᵖ) : (quadraticDualLift f hf) ((quadraticDualMk k Q R) x) = f x

Pointwise, the lift sends the quadratic dual class of x to f x.

theorem TauCeti.PathAlgebra.quadraticDualLift_unique {k : Type w} {Q : Type u} {B : Type u_1} [CommRing k] [Quiver Q] [Finite Q] [Semiring B] [Algebra k B] {R : Submodule k (pathAlgebra k Q)} (f : (pathAlgebra k Q)ᵐᵒᵖ →ₐ[k] B) [∀ (a b : Q), Finite (a ⟶ b)] (hf : ∀ x ∈ quadraticOrthogonal k Q R, f (MulOpposite.op x) = 0) (g : quadraticDual k Q R →ₐ[k] B) (hg : g.comp (quadraticDualMk k Q R) = f) : g = quadraticDualLift f hf

The lift is the only algebra map whose composite with the quotient map is f.