The vertex simple representations of a quiver #
For a vertex i of a quiver Q, the vertex simple representation Sᵢ is the base field k at
i and the zero module at every other vertex, every arrow acting by zero. This file constructs
Sᵢ, proves that it is a simple object of the category of representations, and proves that over an
acyclic quiver these are all the simple objects.
The construction is a CategoryTheory.Paths.lift of the prefunctor sending i to k, every other
vertex to the zero module, and every arrow to the zero map; functoriality along path concatenation
is then supplied by Mathlib. Simplicity is checked pointwise, and uses only that Sᵢ is supported
at the single vertex i: a monomorphism into a representation that vanishes away from i is zero
there, so it is determined by its component at i, where k is a simple k-module. Lifting the
vertex spaces to a larger universe preserves both of those properties, so the lifted Sᵢ is simple
as well.
The converse classification runs through the subrepresentations of
TauCeti.RepresentationTheory.Quiver.Representation.Subrepresentation. A nonzero vector x of Mᵢ
spans two of them: the subrepresentation it generates, and the one generated by the images of x
along the paths of positive length. Over an acyclic quiver the second vanishes at i while the
first contains x, so simplicity makes the second zero and the first everything; M is then the
line through x at i and zero elsewhere, which is Sᵢ.
Main definitions #
TauCeti.simpleRep k Q i: the vertex simple representationSᵢ.TauCeti.simpleRepSelfEquiv: the identification(Sᵢ)ᵢ ≃ₗ[k] k, andTauCeti.simpleRepGenerator: the element of(Sᵢ)ᵢit sends to1.TauCeti.simpleRepHom: the morphismSᵢ ⟶ Msending the generator to a chosen vectorxofMᵢ, available whenever every path out ofiof positive length killsx.
Main results #
TauCeti.simple_of_simple_obj_of_isZero_obj: a representation whose vertex space at one vertex is a simple module and which vanishes at every other vertex is simple.TauCeti.simpleRep_simple:Sᵢis a simple object ofTauCeti.QuiverRep k Q.TauCeti.simple_simpleRep_comp_uliftFunctor: lifting the vertex spaces ofSᵢto a larger universe preserves simplicity.TauCeti.isIso_simpleRepHom: a representation spanned atiby a single nonzero vector and vanishing at every other vertex isSᵢ.TauCeti.exists_iso_simpleRep_of_simple: over an acyclic quiver every simple representation is isomorphic to someSᵢ.TauCeti.exists_eq_smul_simpleRepGenerator:(Sᵢ)ᵢis the line spanned by the generator.TauCeti.hom_simpleRep_eq_zero_iffandTauCeti.simpleRep_hom_eq_zero_iff: a morphism into or out ofSᵢis detected by its component ati.TauCeti.dimVector_simpleRep: the dimension vector ofSᵢisPi.single i 1.TauCeti.exists_mono_simpleRep_of_not_isZero: over a finite-vertex acyclic quiver, every nonzero representation contains a vertex simple.TauCeti.not_nonempty_simpleRep_iso: vertex simples at distinct vertices are not isomorphic.
Implementation notes #
simpleRep branches on equality of vertices. It is noncomputable in any case, so that branch is
decided classically and no DecidableEq Q instance appears in the interface; simpleRep_obj_self
and simpleRep_obj_of_ne describe the two cases without mentioning the branch. Only
dimVector_simpleRep assumes DecidableEq Q, because Pi.single needs one to be stated.
The objects of CategoryTheory.Paths Q are the vertices of Q, so the statements below use a
vertex directly as an object of the path category. The classification is the exception: rw and
simp build their motives at a transparency at which M.obj i for a vertex i : Q is not
type-correct, so simpleRepHom and everything downstream of it spell the base vertex as
(CategoryTheory.Paths.of Q).obj i, and pin the implicit vertex of the spanning
subrepresentations to match.
The roadmap pins the simplicity result as simpleRep_simple, so the instance carries that name
rather than the simple_simpleRep a Mathlib predicate prefix would give it.
References #
This implements the vertex simples of Layer 1 of
TauCetiRoadmap/RepresentationTheory/QuiverRepresentations/README.md.
The vertex simple representation Sᵢ of a quiver: the base field k at the vertex i,
the zero module at every other vertex, and the zero map along every arrow.
Equations
- TauCeti.simpleRep k Q i = CategoryTheory.Paths.lift { obj := fun (a : Q) => if a = i then ↧k else 0, map := fun {X Y : Q} (x : X ⟶ Y) => 0 }
Instances For
Away from i, the vertex simple Sᵢ vanishes.
At i, the vertex simple Sᵢ is the simple k-module k.
The vertex simple is a line at its vertex #
The vector space that the vertex simple Sᵢ puts at i is the base field.
Equations
Instances For
The canonical generator of the line (Sᵢ)ᵢ: the element corresponding to 1 : k.
Equations
- TauCeti.simpleRepGenerator k i = (TauCeti.simpleRepSelfEquiv k i).symm 1
Instances For
The generator of (Sᵢ)ᵢ corresponds to 1 : k.
The vertex simple is a line at its vertex: every element of (Sᵢ)ᵢ is a multiple of the
generator.
The generator of (Sᵢ)ᵢ is nonzero.
A path of positive length acts by zero on the vertex simple Sᵢ; only the trivial paths, which
act by the identity, survive.
A representation supported at a single vertex is simple as soon as its vertex space there
is: if M vanishes at every vertex other than j and the module Mⱼ is simple, then M is a
simple object of TauCeti.QuiverRep k Q. A monomorphism into such an M is zero away from j
because the target vanishes there, so it is determined by its component at j, where simplicity
of Mⱼ makes a nonzero monomorphism invertible.
The vertex simples are simple. The vertex representation Sᵢ = simpleRep k Q i is a simple
object of TauCeti.QuiverRep k Q.
Universe-lifting the vertex spaces of a vertex simple representation preserves its simplicity.
The vertex simples are the only simples over an acyclic quiver #
The morphism Sᵢ ⟶ M determined by a vector at i, for a vector x that every path out
of i of positive length annihilates. It carries the generator of the line (Sᵢ)ᵢ to x, and is
the zero map at every other vertex. The hypothesis hx is exactly what naturality asks for: a path
of positive length acts by zero on Sᵢ, so it must kill x as well.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Away from i, the morphism Sᵢ ⟶ M attached to x : Mᵢ vanishes.
The morphism Sᵢ ⟶ M attached to x : Mᵢ carries the generator of (Sᵢ)ᵢ to x.
A representation carried by a single vector at i is Sᵢ: the morphism Sᵢ ⟶ M attached
to a nonzero vector x spanning Mᵢ is an isomorphism, as soon as M vanishes at every other
vertex.
The vertex simples exhaust the simples. Over an acyclic quiver every simple representation
is isomorphic to a vertex simple Sᵢ.
The proof compares two subrepresentations attached to a nonzero vector x of Mᵢ: the one it
generates, and the one generated by its images under the paths of positive length. Simplicity forces
each to be everything or nothing; over an acyclic quiver the second vanishes at i while the first
contains x, so the second is nothing and the first everything. Away from i the two agree, so M
vanishes there, and at i it is the line through x.
Every nonzero representation of a finite-vertex acyclic quiver contains a vertex simple as a subrepresentation. No finite-dimensionality of the vertex spaces is needed.