Comparing a vertex simple with its projective and its injective

For a vertex i of a quiver Q there are three representations attached to i: the vertex simple Sᵢ, the projective Pᵢ and the injective Iᵢ. This file builds the two comparison morphisms that tie them together, Pᵢ ↠ Sᵢ and Sᵢ ↪ Iᵢ, and proves that the first is an epimorphism, the second a monomorphism, and that each is unique up to a scalar.

Both morphisms come from universal properties already available: Pᵢ represents evaluation at i (TauCeti.indecProjRepHomEquiv) and Iᵢ represents the dual of evaluation at i (TauCeti.indecInjRepHomEquiv), so a morphism Pᵢ ⟶ Sᵢ is an element of the line (Sᵢ)ᵢ and a morphism Sᵢ ⟶ Iᵢ is a linear functional on it. The two canonical choices are the generator of that line and the functional dual to it, and both are read off the identification TauCeti.simpleRepSelfEquiv of (Sᵢ)ᵢ with the base field.

Main definitions

• TauCeti.indecProjRepToSimpleRep: the morphism Pᵢ ⟶ Sᵢ, sending the trivial path to the generator and killing every path of positive length.
• TauCeti.simpleRepToIndecInjRep: the morphism Sᵢ ⟶ Iᵢ, reading off the coefficient of an element of (Sᵢ)ᵢ on the trivial path.

Main results

• TauCeti.epi_indecProjRepToSimpleRep: Pᵢ ↠ Sᵢ is an epimorphism, and TauCeti.mono_simpleRepToIndecInjRep: Sᵢ ↪ Iᵢ is a monomorphism.
• TauCeti.indecProjRepToSimpleRep_app_self_apply: at the vertex i, Pᵢ ↠ Sᵢ reads off the coefficient of the trivial path.
• TauCeti.exists_eq_smul_indecProjRepToSimpleRep and TauCeti.exists_eq_smul_simpleRepToIndecInjRep: every morphism Pᵢ ⟶ Sᵢ, respectively Sᵢ ⟶ Iᵢ, is a scalar multiple of the canonical one, so each comparison morphism is unique up to a scalar.

Implementation notes

Only the two comparison morphisms and their formal properties are proved here. That Pᵢ ↠ Sᵢ is a projective cover in the technical sense (a superfluous kernel) and Sᵢ ↪ Iᵢ an injective envelope (an essential extension) is neither true nor claimed in this generality: for the quiver with one vertex and one loop the path algebra is k[X], the kernel of Pᵢ ↠ Sᵢ is the ideal (X), and (X) + (X - 1) = k[X] with (X - 1) proper, so that kernel is not superfluous. Ruling that loop out repairs both halves. The downstream module TauCeti.RepresentationTheory.Quiver.Representation.Projective.Cover proves TauCeti.epi_of_epi_comp_indecProjRepToSimpleRep, that Pᵢ ↠ Sᵢ is an essential epimorphism, and TauCeti.RepresentationTheory.Quiver.Representation.Injective.Envelope proves that Sᵢ ↪ Iᵢ is an essential monomorphism, under the same local hypothesis ∀ p : Quiver.Path i i, p = Quiver.Path.nil. What is recorded here instead is TauCeti.indecProjRepToSimpleRep_app_basis_eq_zero_of_length_ne_zero: the morphism kills the basis vector of every path of positive length, hence, by linearity, their whole span. The technical vocabulary is available as TauCeti.IsProjectiveCover on modules, TauCeti.IsEssentialEpi and TauCeti.IsEssentialMono categorically; the two downstream modules apply the categorical notions directly to these comparison morphisms.

The field lives in the universe max v w of the vertices and the arrows here, where the three files building Sᵢ, Pᵢ and Iᵢ let its universe be independent. The reason is that the vertex spaces of Pᵢ and Iᵢ are built on Quiver.Path i j, so for k : Type u they live in max u v w, whereas Sᵢ is built on the field itself and lives in u. The three objects therefore lie in a common category TauCeti.QuiverRep k Q exactly when v, w ≤ u, which Lean has no way to hypothesize; u = max v w is the least such u, and stating it that way leaves the vertex and the arrow universes independent of each other, so these declarations apply to a quiver whose vertices and arrows are in different universes as readily as to one where all three universes agree. What they do not cover is a field in a universe strictly larger than the vertices and the arrows; reaching that would mean rebuilding Sᵢ on a ULift of the field, re-indexing every existing statement about it. Sᵢ, Pᵢ and Iᵢ themselves are constructed with no relation between the universes, and only the statements comparing them are restricted here.

A vertex i : Q is used below as an object of the free category CategoryTheory.Paths Q, which is Q itself only by unfolding a semireducible definition; the (Paths.of Q).obj annotations record that identification, exactly as in the files this one builds on.

References

This implements the comparison morphisms Pᵢ ↠ Sᵢ and Sᵢ ↪ Iᵢ of Layer 1 of TauCetiRoadmap/RepresentationTheory/QuiverRepresentations/README.md. See Assem--Simson-- Skowroński, Elements of the Representation Theory of Associative Algebras I, Ch. III.

The surjection from a vertex projective onto its vertex simple

noncomputable def TauCeti.indecProjRepToSimpleRep (k : Type (max v w)) {Q : Type v} [Field k] [Quiver Q] (i : Q) : indecProjRep k Q i ⟶ simpleRep k Q i

The canonical surjection Pᵢ ↠ Sᵢ: under the universal property of Pᵢ it is the generator of the line (Sᵢ)ᵢ. It sends the basis vector of the trivial path to that generator and kills the basis vector of every path of positive length.

Equations

• TauCeti.indecProjRepToSimpleRep k i = TauCeti.indecProjRepHom i (TauCeti.simpleRep k Q i) (TauCeti.simpleRepGenerator k i)

@[simp]

theorem TauCeti.indecProjRepToSimpleRep_app_basis (k : Type (max v w)) {Q : Type v} [Field k] [Quiver Q] {i j : Q} (p : Quiver.Path i j) : (CategoryTheory.ConcreteCategory.hom ((indecProjRepToSimpleRep k i).app ((CategoryTheory.Paths.of Q).obj j))) ((indecProjRepBasis k i j) p) = (CategoryTheory.ConcreteCategory.hom ((simpleRep k Q i).map p)) (simpleRepGenerator k i)

The surjection Pᵢ ↠ Sᵢ carries the basis vector of a path p : i → j to the action of p on the generator.

theorem TauCeti.indecProjRepToSimpleRep_app_nil (k : Type (max v w)) {Q : Type v} [Field k] [Quiver Q] (i : Q) : (CategoryTheory.ConcreteCategory.hom ((indecProjRepToSimpleRep k i).app ((CategoryTheory.Paths.of Q).obj i))) ((indecProjRepBasis k i i) Quiver.Path.nil) = simpleRepGenerator k i

The surjection Pᵢ ↠ Sᵢ sends the basis vector of the trivial path to the generator of (Sᵢ)ᵢ.

theorem TauCeti.indecProjRepHomEquiv_indecProjRepToSimpleRep (k : Type (max v w)) {Q : Type v} [Field k] [Quiver Q] (i : Q) : (indecProjRepHomEquiv i (simpleRep k Q i)) (indecProjRepToSimpleRep k i) = simpleRepGenerator k i

The surjection Pᵢ ↠ Sᵢ is the morphism that the universal property of Pᵢ attaches to the generator of the line (Sᵢ)ᵢ.

theorem TauCeti.indecProjRepToSimpleRep_app_basis_eq_zero_of_length_ne_zero (k : Type (max v w)) {Q : Type v} [Field k] [Quiver Q] {i j : Q} (p : Quiver.Path i j) (hp : p.length ≠ 0) : (CategoryTheory.ConcreteCategory.hom ((indecProjRepToSimpleRep k i).app ((CategoryTheory.Paths.of Q).obj j))) ((indecProjRepBasis k i j) p) = 0

The surjection Pᵢ ↠ Sᵢ kills every path of positive length: the basis vector of such a path goes to zero, and so, by linearity, does everything in the span of those basis vectors.

@[simp]

theorem TauCeti.indecProjRepToSimpleRep_app_self_apply (k : Type (max v w)) {Q : Type v} [Field k] [Quiver Q] (i : Q) (x : ↑((indecProjRep k Q i).obj ((CategoryTheory.Paths.of Q).obj i))) : (CategoryTheory.ConcreteCategory.hom ((indecProjRepToSimpleRep k i).app ((CategoryTheory.Paths.of Q).obj i))) x = ((indecProjRepBasis k i i).repr x) Quiver.Path.nil • simpleRepGenerator k i

At the vertex i, the surjection Pᵢ ↠ Sᵢ reads off the coefficient of the trivial path: an element of (Pᵢ)ᵢ goes to that coefficient times the generator of (Sᵢ)ᵢ. Every other path i → i is a cycle of positive length and is killed.

theorem TauCeti.indecProjRepToSimpleRep_app_surjective (k : Type (max v w)) {Q : Type v} [Field k] [Quiver Q] (i j : Q) : Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom ((indecProjRepToSimpleRep k i).app ((CategoryTheory.Paths.of Q).obj j)))

Every component of Pᵢ ⟶ Sᵢ is surjective: at i because the generator spans, and away from i because the target vanishes.

theorem TauCeti.indecProjRepToSimpleRep_ne_zero (k : Type (max v w)) {Q : Type v} [Field k] [Quiver Q] (i : Q) : indecProjRepToSimpleRep k i ≠ 0

The surjection Pᵢ ↠ Sᵢ is nonzero.

instance TauCeti.epi_indecProjRepToSimpleRep (k : Type (max v w)) {Q : Type v} [Field k] [Quiver Q] (i : Q) : CategoryTheory.Epi (indecProjRepToSimpleRep k i)

Pᵢ ↠ Sᵢ is an epimorphism. It is nonzero, and a nonzero morphism into a simple object is an epimorphism; Sᵢ is simple by TauCeti.simpleRep_simple.

theorem TauCeti.exists_eq_smul_indecProjRepToSimpleRep (k : Type (max v w)) {Q : Type v} [Field k] [Quiver Q] {i : Q} (f : indecProjRep k Q i ⟶ simpleRep k Q i) : ∃ (c : k), f = c • indecProjRepToSimpleRep k i

The surjection Pᵢ ↠ Sᵢ is unique up to a scalar: Hom(Pᵢ, Sᵢ) is the line spanned by TauCeti.indecProjRepToSimpleRep.

The embedding of a vertex simple into its vertex injective

noncomputable def TauCeti.simpleRepToIndecInjRep (k : Type (max v w)) {Q : Type v} [Field k] [Quiver Q] (i : Q) : simpleRep k Q i ⟶ indecInjRep k Q i

The canonical embedding Sᵢ ↪ Iᵢ: under the universal property of Iᵢ it is the linear functional identifying the line (Sᵢ)ᵢ with the base field.

Equations

• TauCeti.simpleRepToIndecInjRep k i = TauCeti.indecInjRepHom i (TauCeti.simpleRep k Q i) ↑(TauCeti.simpleRepSelfEquiv k i)

@[simp]

theorem TauCeti.simpleRepToIndecInjRep_app_apply (k : Type (max v w)) {Q : Type v} [Field k] [Quiver Q] {i j : Q} (x : ↑((simpleRep k Q i).obj ((CategoryTheory.Paths.of Q).obj j))) (q : Quiver.Path j i) : (CategoryTheory.ConcreteCategory.hom ((simpleRepToIndecInjRep k i).app ((CategoryTheory.Paths.of Q).obj j))) x q = (simpleRepSelfEquiv k i) ((CategoryTheory.ConcreteCategory.hom ((simpleRep k Q i).map q)) x)

The embedding Sᵢ ↪ Iᵢ sends x at the vertex j to the function whose value on a path q : j → i is the coefficient of the action of q on x.

@[simp]

theorem TauCeti.indecInjRepHomEquiv_simpleRepToIndecInjRep (k : Type (max v w)) {Q : Type v} [Field k] [Quiver Q] (i : Q) : (indecInjRepHomEquiv i (simpleRep k Q i)) (simpleRepToIndecInjRep k i) = ↑(simpleRepSelfEquiv k i)

The embedding Sᵢ ↪ Iᵢ is the morphism that the universal property of Iᵢ attaches to the functional identifying the line (Sᵢ)ᵢ with the base field.

theorem TauCeti.simpleRepToIndecInjRep_app_injective (k : Type (max v w)) {Q : Type v} [Field k] [Quiver Q] (i j : Q) : Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom ((simpleRepToIndecInjRep k i).app ((CategoryTheory.Paths.of Q).obj j)))

Every component of Sᵢ ⟶ Iᵢ is injective: at i because the coefficient on the trivial path recovers the element, and away from i because the source vanishes.

theorem TauCeti.simpleRepToIndecInjRep_ne_zero (k : Type (max v w)) {Q : Type v} [Field k] [Quiver Q] (i : Q) : simpleRepToIndecInjRep k i ≠ 0

The embedding Sᵢ ↪ Iᵢ is nonzero.

instance TauCeti.mono_simpleRepToIndecInjRep (k : Type (max v w)) {Q : Type v} [Field k] [Quiver Q] (i : Q) : CategoryTheory.Mono (simpleRepToIndecInjRep k i)

Sᵢ ↪ Iᵢ is a monomorphism. It is nonzero, and a nonzero morphism out of a simple object is a monomorphism; Sᵢ is simple by TauCeti.simpleRep_simple.

theorem TauCeti.exists_eq_smul_simpleRepToIndecInjRep (k : Type (max v w)) {Q : Type v} [Field k] [Quiver Q] {i : Q} (f : simpleRep k Q i ⟶ indecInjRep k Q i) : ∃ (c : k), f = c • simpleRepToIndecInjRep k i

The embedding Sᵢ ↪ Iᵢ is unique up to a scalar: Hom(Sᵢ, Iᵢ) is the line spanned by TauCeti.simpleRepToIndecInjRep.