Subrepresentations of a quiver representation

A subrepresentation of a representation M of a quiver is a submodule of Mₐ at every vertex a, stable under the action of every path. This file packages that data as TauCeti.QuiverSubrep M, orders subrepresentations vertexwise — a bounded order, with ⊥ and ⊤ the zero subrepresentation and the whole of M — builds the representation a subrepresentation carries together with its monomorphism into M, and identifies when that monomorphism is zero or invertible. The payoff is TauCeti.QuiverSubrep.eq_bot_or_eq_top: over a simple representation there are no subrepresentations other than the two trivial ones.

The file also builds the subrepresentation TauCeti.QuiverSubrep.pathSpan x n spanned by the images of a single vector x : Mᵢ under all paths out of i of length at least n. Taking n = 0 gives the subrepresentation generated by x, and n = 1 the part of it reached along the paths of positive length; the two agree away from i, so they can differ only at i, where — as soon as the closed paths at i carry x into the line through x, respectively kill x — the first is that line and the second vanishes. That comparison is what forces a simple representation to be concentrated at one vertex.

Main definitions

• TauCeti.QuiverSubrep M: a subrepresentation of M, ordered vertexwise by TauCeti.QuiverSubrep.le_def and bounded by ⊥ and ⊤.
• TauCeti.QuiverSubrep.toQuiverRep and TauCeti.QuiverSubrep.ι: the representation a subrepresentation carries, and its inclusion into M.
• TauCeti.QuiverSubrep.pathSpan x n: the subrepresentation spanned by the images of x under the paths of length at least n.

Main results

• TauCeti.QuiverSubrep.ι_eq_zero_iff and TauCeti.QuiverSubrep.isIso_ι_iff: the inclusion is zero exactly when the subrepresentation is ⊥, and invertible exactly when it is ⊤.
• TauCeti.QuiverSubrep.eq_bot_or_eq_top: a subrepresentation of a simple representation is ⊥ or ⊤.
• TauCeti.QuiverSubrep.pathSpan_zero_self_of_forall_map_mem_span and TauCeti.QuiverSubrep.pathSpan_one_self_of_forall_map_eq_zero: if the closed paths at the base vertex carry x into the line through x, respectively kill x, the two spans there are that line and ⊥.

Implementation notes

The submodules are indexed by the vertices of Q, while a representation is a functor out of CategoryTheory.Paths Q; the two index types agree only by unfolding the semireducible CategoryTheory.Paths, so several proofs below have to change a goal into its vertex-indexed form before rewriting. The same device restates a goal about LinearMap.restrict or about path composition in CategoryTheory.Paths Q as the plain statement about M that the functoriality lemmas CategoryTheory.Functor.map_id and CategoryTheory.Functor.map_comp are phrased in; each such change carries a comment saying which reduction it performs.

References

This supports Layer 1 of TauCetiRoadmap/RepresentationTheory/QuiverRepresentations/README.md, where the category of representations is described as abelian with the pointwise structure and its subobjects are the subrepresentations.

structure TauCeti.QuiverSubrep {k : Type u} {Q : Type v} [Field k] [Quiver Q] (M : QuiverRep k Q) : Type (max u_1 v)

A subrepresentation of a representation M of a quiver: a submodule of the vector space that M puts at each vertex, stable under the action of every path.

• toSubmodule (a : Q) : Submodule k ↑(M.obj a)

  The submodule of Mₐ sitting at the vertex a.

• map_mem {a b : Q} (p : Quiver.Path a b) {x : ↑(M.obj a)} : x ∈ self.toSubmodule a → (CategoryTheory.ConcreteCategory.hom (M.map p)) x ∈ self.toSubmodule b

  Every path carries the submodule at its source into the submodule at its target.

theorem TauCeti.QuiverSubrep.ext {k : Type u} {Q : Type v} [Field k] [Quiver Q] {M : QuiverRep k Q} {N N' : QuiverSubrep M} (h : ∀ (a : Q), N.toSubmodule a = N'.toSubmodule a) : N = N'

theorem TauCeti.QuiverSubrep.ext_iff {k : Type u} {Q : Type v} [Field k] [Quiver Q] {M : QuiverRep k Q} {N N' : QuiverSubrep M} : N = N' ↔ ∀ (a : Q), N.toSubmodule a = N'.toSubmodule a

The vertexwise order

@[instance_reducible]

instance TauCeti.QuiverSubrep.instPartialOrder {k : Type u} {Q : Type v} [Field k] [Quiver Q] {M : QuiverRep k Q} : PartialOrder (QuiverSubrep M)

Subrepresentations are ordered vertexwise, by inclusion of the submodules they put at each vertex.

Equations

• TauCeti.QuiverSubrep.instPartialOrder = PartialOrder.lift TauCeti.QuiverSubrep.toSubmodule ⋯

theorem TauCeti.QuiverSubrep.le_def {k : Type u} {Q : Type v} [Field k] [Quiver Q] {M : QuiverRep k Q} {N N' : QuiverSubrep M} : N ≤ N' ↔ ∀ (a : Q), N.toSubmodule a ≤ N'.toSubmodule a

One subrepresentation is contained in another exactly when that holds at every vertex.

@[instance_reducible]

instance TauCeti.QuiverSubrep.instBot {k : Type u} {Q : Type v} [Field k] [Quiver Q] {M : QuiverRep k Q} : Bot (QuiverSubrep M)

The zero subrepresentation: ⊥ at every vertex.

Equations

• TauCeti.QuiverSubrep.instBot = { bot := { toSubmodule := fun (x : Q) => ⊥, map_mem := ⋯ } }

@[instance_reducible]

instance TauCeti.QuiverSubrep.instTop {k : Type u} {Q : Type v} [Field k] [Quiver Q] {M : QuiverRep k Q} : Top (QuiverSubrep M)

The whole representation, viewed as a subrepresentation of itself: ⊤ at every vertex.

Equations

• TauCeti.QuiverSubrep.instTop = { top := { toSubmodule := fun (x : Q) => ⊤, map_mem := ⋯ } }

@[simp]

theorem TauCeti.QuiverSubrep.toSubmodule_bot {k : Type u} {Q : Type v} [Field k] [Quiver Q] {M : QuiverRep k Q} (a : Q) : ⊥.toSubmodule a = ⊥

@[simp]

theorem TauCeti.QuiverSubrep.toSubmodule_top {k : Type u} {Q : Type v} [Field k] [Quiver Q] {M : QuiverRep k Q} (a : Q) : ⊤.toSubmodule a = ⊤

@[instance_reducible]

instance TauCeti.QuiverSubrep.instBoundedOrder {k : Type u} {Q : Type v} [Field k] [Quiver Q] {M : QuiverRep k Q} : BoundedOrder (QuiverSubrep M)

Equations

• TauCeti.QuiverSubrep.instBoundedOrder = { toTop := TauCeti.QuiverSubrep.instTop, le_top := ⋯, toBot := TauCeti.QuiverSubrep.instBot, bot_le := ⋯ }

def TauCeti.QuiverSubrep.toQuiverRep {k : Type u} {Q : Type v} [Field k] [Quiver Q] {M : QuiverRep k Q} (N : QuiverSubrep M) : QuiverRep k Q

The representation carried by a subrepresentation: the submodule at each vertex, with a path acting by the restriction of its action on M.

Equations

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

theorem TauCeti.QuiverSubrep.toQuiverRep_obj {k : Type u} {Q : Type v} [Field k] [Quiver Q] {M : QuiverRep k Q} (N : QuiverSubrep M) (a : Q) : N.toQuiverRep.obj a = ↧↥(N.toSubmodule a)

A subrepresentation puts its submodule at each vertex.

def TauCeti.QuiverSubrep.ι {k : Type u} {Q : Type v} [Field k] [Quiver Q] {M : QuiverRep k Q} (N : QuiverSubrep M) : N.toQuiverRep ⟶ M

The inclusion of a subrepresentation into the ambient representation.

Equations

• N.ι = { app := fun (a : CategoryTheory.Paths Q) => ModuleCat.ofHom (N.toSubmodule a).subtype, naturality := ⋯ }

@[simp]

theorem TauCeti.QuiverSubrep.ι_app_apply {k : Type u} {Q : Type v} [Field k] [Quiver Q] {M : QuiverRep k Q} (N : QuiverSubrep M) (a : Q) (x : ↥(N.toSubmodule a)) : (CategoryTheory.ConcreteCategory.hom (N.ι.app a)) x = ↑x

@[simp]

theorem TauCeti.QuiverSubrep.coe_toQuiverRep_map_apply {k : Type u} {Q : Type v} [Field k] [Quiver Q] {M : QuiverRep k Q} (N : QuiverSubrep M) {a b : Q} (p : Quiver.Path a b) (x : ↥(N.toSubmodule a)) : ↑((CategoryTheory.ConcreteCategory.hom (N.toQuiverRep.map p)) x) = (CategoryTheory.ConcreteCategory.hom (M.map p)) ↑x

A path acts on a subrepresentation by its action on M: the value of the path action, read in the ambient representation, is the ambient action on the value.

instance TauCeti.QuiverSubrep.mono_ι {k : Type u} {Q : Type v} [Field k] [Quiver Q] {M : QuiverRep k Q} (N : QuiverSubrep M) : CategoryTheory.Mono N.ι

theorem TauCeti.QuiverSubrep.isZero_toQuiverRep {k : Type u} {Q : Type v} [Field k] [Quiver Q] {M : QuiverRep k Q} {N : QuiverSubrep M} (h : N = ⊥) : CategoryTheory.Limits.IsZero N.toQuiverRep

The zero subrepresentation carries the zero representation.

theorem TauCeti.QuiverSubrep.ι_eq_zero_iff {k : Type u} {Q : Type v} [Field k] [Quiver Q] {M : QuiverRep k Q} (N : QuiverSubrep M) : N.ι = 0 ↔ N = ⊥

The inclusion of a subrepresentation is the zero morphism exactly when the subrepresentation is ⊥.

theorem TauCeti.QuiverSubrep.isIso_ι_iff {k : Type u} {Q : Type v} [Field k] [Quiver Q] {M : QuiverRep k Q} (N : QuiverSubrep M) : CategoryTheory.IsIso N.ι ↔ N = ⊤

The inclusion of a subrepresentation is an isomorphism exactly when the subrepresentation is ⊤.

theorem TauCeti.QuiverSubrep.eq_bot_or_eq_top {k : Type u} {Q : Type v} [Field k] [Quiver Q] {M : QuiverRep k Q} [CategoryTheory.Simple M] (N : QuiverSubrep M) : N = ⊥ ∨ N = ⊤

A simple representation has no proper nonzero subrepresentation: a subrepresentation of a simple representation is ⊥ or ⊤.

The subrepresentation spanned by a vector

def TauCeti.QuiverSubrep.pathImages {k : Type u} {Q : Type v} [Field k] [Quiver Q] {M : QuiverRep k Q} {i : Q} (x : ↑(M.obj i)) (n : ℕ) (a : Q) : Set ↑(M.obj a)

The set of images of x : Mᵢ under the paths out of i of length at least n.

Equations

• TauCeti.QuiverSubrep.pathImages x n a = {y : ↑(M.obj a) | ∃ (p : Quiver.Path i a), n ≤ p.length ∧ (CategoryTheory.ConcreteCategory.hom (M.map p)) x = y}

@[simp]

theorem TauCeti.QuiverSubrep.mem_pathImages {k : Type u} {Q : Type v} [Field k] [Quiver Q] {M : QuiverRep k Q} {i : Q} {x : ↑(M.obj i)} {n : ℕ} {a : Q} {y : ↑(M.obj a)} : y ∈ pathImages x n a ↔ ∃ (p : Quiver.Path i a), n ≤ p.length ∧ (CategoryTheory.ConcreteCategory.hom (M.map p)) x = y

Membership in TauCeti.QuiverSubrep.pathImages: the elements are exactly the images of x under the paths i → a of length at least n.

def TauCeti.QuiverSubrep.pathSpan {k : Type u} {Q : Type v} [Field k] [Quiver Q] {M : QuiverRep k Q} {i : Q} (x : ↑(M.obj i)) (n : ℕ) : QuiverSubrep M

The subrepresentation spanned by a vector along the long paths: at the vertex a it is the span of the images of x : Mᵢ under the paths i → a of length at least n. For n = 0 this is the subrepresentation generated by x, and for n = 1 the part of it reached along the paths of positive length.

Equations

• TauCeti.QuiverSubrep.pathSpan x n = { toSubmodule := fun (a : Q) => Submodule.span k (TauCeti.QuiverSubrep.pathImages x n a), map_mem := ⋯ }

@[simp]

theorem TauCeti.QuiverSubrep.toSubmodule_pathSpan {k : Type u} {Q : Type v} [Field k] [Quiver Q] {M : QuiverRep k Q} {i : Q} (x : ↑(M.obj i)) (n : ℕ) (a : Q) : (pathSpan x n).toSubmodule a = Submodule.span k (pathImages x n a)

The submodule that TauCeti.QuiverSubrep.pathSpan puts at a vertex.

theorem TauCeti.QuiverSubrep.pathSpan_zero_eq_pathSpan_one_of_ne {k : Type u} {Q : Type v} [Field k] [Quiver Q] {M : QuiverRep k Q} {i : Q} (x : ↑(M.obj i)) {a : Q} (h : a ≠ i) : (pathSpan x 0).toSubmodule a = (pathSpan x 1).toSubmodule a

Away from the base vertex, the span along all paths and the span along the paths of positive length agree: every path out of i that lands elsewhere already has positive length.

theorem TauCeti.QuiverSubrep.mem_pathSpan_zero {k : Type u} {Q : Type v} [Field k] [Quiver Q] {M : QuiverRep k Q} {i : Q} (x : ↑(M.obj i)) : x ∈ (pathSpan x 0).toSubmodule i

The vector x lies in the subrepresentation it generates.

theorem TauCeti.QuiverSubrep.pathSpan_zero_self_of_forall_map_mem_span {k : Type u} {Q : Type v} [Field k] [Quiver Q] {M : QuiverRep k Q} {i : Q} (x : ↑(M.obj i)) (hx : ∀ (p : Quiver.Path i i), (CategoryTheory.ConcreteCategory.hom (M.map p)) x ∈ k ∙ x) : (pathSpan x 0).toSubmodule i = k ∙ x

If every closed path at i carries x into the line through x, the span at i along all paths is that line.

theorem TauCeti.QuiverSubrep.pathSpan_one_self_of_forall_map_eq_zero {k : Type u} {Q : Type v} [Field k] [Quiver Q] {M : QuiverRep k Q} {i : Q} (x : ↑(M.obj i)) (hx : ∀ (p : Quiver.Path i i), p.length ≠ 0 → (CategoryTheory.ConcreteCategory.hom (M.map p)) x = 0) : (pathSpan x 1).toSubmodule i = ⊥

If every closed path at i of positive length kills x, the span at i along the paths of positive length vanishes.