The module over the path algebra carried by a representation of a quiver

TauCeti.RepresentationTheory.Quiver.Representation.OfModule turns a left module over the path algebra kQ of a finite quiver into a representation of Q, and proves that functor fully faithful. This file supplies the other half: the kQ-module TauCeti.QuiverRep.asModule carried by a representation, the identification of its vertex components with the vertex spaces of the representation one started from, and hence the essential surjectivity that completes the equivalence

TauCeti.quiverRepEquivalence : QuiverRep k Q ≌ ModuleCat (pathAlgebra k Q).

The construction

The carrier is the direct sum ⨁ᵥ Mᵥ of the vertex spaces. A basis path p : a ⟶ b of kQ acts on it by the endomorphism TauCeti.QuiverRep.pathEnd that reads off the a-component, applies the structure map M.map p, and puts the result in the b-component; two such endomorphisms compose to the endomorphism of the concatenated path when the paths meet (TauCeti.QuiverRep.pathEnd_mul_pathEnd_of_comp) and to zero when they do not (TauCeti.QuiverRep.pathEnd_mul_pathEnd_of_not_composable), while the trivial paths give the component projections, which sum to the identity (TauCeti.QuiverRep.sum_pathEnd_nil). Those are exactly the three hypotheses of the universal property TauCeti.PathAlgebra.liftAlgHom, so the assignment extends to an algebra homomorphism TauCeti.QuiverRep.toEnd : kQ →ₐ[k] End_k (⨁ᵥ Mᵥ), and TauCeti.QuiverRep.asModule is ⨁ᵥ Mᵥ with the module structure it induces.

With that in hand the vertex idempotent eᵥ acts as the composite of the projection to Mᵥ and the inclusion back (TauCeti.QuiverRep.vertexIdempotent_smul), so the vertex component eᵥ · asModule is exactly the image of Mᵥ (TauCeti.QuiverRep.vertexComponent_asModule) and the inclusion is a k-linear isomorphism onto it, TauCeti.QuiverRep.vertexComponentEquiv. Those isomorphisms are natural in the path, because a path acts on the image of Mₐ through M.map p (TauCeti.QuiverRep.smul_ofVertex, whence TauCeti.QuiverRep.pathMap_vertexComponentEquiv); assembling them with CategoryTheory.NatIso.ofComponents gives the natural isomorphism TauCeti.QuiverRep.asModuleIso. Transported to the model TauCeti.QuiverRep.asModuleShrink of the carrier in the universe of the representation itself, that isomorphism becomes TauCeti.QuiverRep.asModuleShrinkIso, the essential surjectivity of TauCeti.quiverRepFunctor.

Main definitions

• TauCeti.QuiverRep.pathEnd: the endomorphism of ⨁ᵥ Mᵥ by which a basis path of kQ acts, and TauCeti.QuiverRep.toEnd: that action extended along the path basis as a k-algebra homomorphism into End_k (⨁ᵥ Mᵥ).
• TauCeti.QuiverRep.asModule: the kQ-module carried by a representation of Q, the direct sum ⨁ᵥ Mᵥ with the action of TauCeti.QuiverRep.toEnd.
• TauCeti.QuiverRep.ofVertex and TauCeti.QuiverRep.toVertex: the inclusion of a vertex space into that module and the projection onto it.
• TauCeti.QuiverRep.asModuleShrink: the model of that module in the universe of the representation, TauCeti.QuiverRep.asModuleShrinkEquiv identifying the two.
• TauCeti.quiverRepEquivalence: representations of a quiver are modules over its path algebra, with TauCeti.quiverRepEquivalenceFunctorObjShrinkIso identifying the module it sends a representation to with TauCeti.QuiverRep.asModuleShrink, and TauCeti.quiverRepEquivalenceFunctorObjIso identifying it with TauCeti.QuiverRep.asModule itself in the universe where the direct sum lives.

Main results

• TauCeti.QuiverRep.smul_ofPath: a basis path acts on asModule by reading off the component at its source, applying the structure map and putting the result in the component at its target; the two cases used below are TauCeti.QuiverRep.smul_ofVertex and TauCeti.QuiverRep.vertexIdempotent_smul, the latter saying that the vertex idempotent eᵥ acts as the projection onto the summand Mᵥ, whence TauCeti.QuiverRep.vertexComponent_asModule: the vertex component of asModule at v is the image of Mᵥ.
• TauCeti.QuiverRep.vertexComponentEquiv: the vertex space Mᵥ is that vertex component, and TauCeti.QuiverRep.pathMap_vertexComponentEquiv: the identification is natural in the path.
• TauCeti.QuiverRep.asModuleIso: the representation carried by asModule M is M, whence TauCeti.QuiverRep.asModuleShrinkIso says the same of the small model, so TauCeti.quiverRepFunctor is essentially surjective, and being fully faithful already it is an equivalence. TauCeti.QuiverRep.dimVector_asModule records that the dimension vector is unchanged.

Implementation notes

The vertex spaces are used through the family TauCeti.QuiverRep.vertexSpace of TauCeti.RepresentationTheory.Quiver.Representation.Basic rather than as M.obj v directly, because instance search does not see the objects of CategoryTheory.Paths Q as vertices when it is asked for the family of instances that a direct sum indexed by the vertices needs; that file's implementation notes say more. For the same reason the naturality squares of TauCeti.QuiverRep.asModuleIso and TauCeti.QuiverRep.asModuleShrinkIso open with change Q at a, restating their quantified objects as vertices.

The k-module structure on TauCeti.QuiverRep.asModule is deliberately not the one the direct sum already carries: it is Module.restrictScalars k (pathAlgebra k Q), restriction of scalars along algebraMap. That is exactly the structure ModuleCat.moduleOfAlgebraModule puts on an object of ModuleCat (kQ), which is the one TauCeti.quiverRepFunctor uses; taking the direct sum's own structure instead would give a second, only propositionally equal, Module k instance and the essential-surjectivity isomorphism would not typecheck against the functor. That the two agree is what makes the identification TauCeti.QuiverRep.asModuleEquiv with the direct sum k-linear; the identity additive equivalence it upgrades is private, asModuleEquiv being the identification consumers use.

DecidableEq Q is needed to write down the summand inclusions DirectSum.lof, so it is carried through the construction; the essential-surjectivity instance is a Prop and discharges it with classical, so neither it nor TauCeti.quiverRepEquivalence asks for it.

The concrete carrier is indexed by Q : Type v with summands in Type t, so ⨁ᵥ Mᵥ : Type (max v t): TauCeti.QuiverRep.asModule lands in a larger universe than the representation it is built from whenever the vertex type does. TauCeti.quiverRepEquivalence is nevertheless stated at an arbitrary representation universe t, because over a finite vertex set that direct sum is a finite product of the vertex spaces and so has a model in Type t (TauCeti.QuiverRep.small_asModule); the model TauCeti.QuiverRep.asModuleShrink of it, whose vertex components are those of asModule because TauCeti.QuiverRep.asModuleShrinkEquiv is kQ-linear, is what witnesses essential surjectivity there; TauCeti.quiverRepEquivalence's forward direction is identified with that model by TauCeti.quiverRepEquivalenceFunctorObjShrinkIso. The concrete direct-sum API is kept at max v t, and TauCeti.quiverRepEquivalenceFunctorObjIso identifies the forward direction with asModule itself at that universe.

References

This is the essential-surjectivity half of quiverRepEquivalence, Layer 1 of TauCetiRoadmap/RepresentationTheory/QuiverRepresentations/README.md, which asks for the equivalence "sending a module M to the representation v ↦ eᵥ M, with an arrow acting by left multiplication, and inverting through the idempotent decomposition M = ⨁ᵥ eᵥ M"; the fully faithful half is TauCeti.quiverRepFunctorFullyFaithful.

The plan of the file follows Mathlib's group-algebra analogue: the type synonym carrying a module structure through Module.compHom, the equivalence with the underlying type and the shape of the final ≌ ModuleCat (algebra) statement are those of Representation.asModule, Representation.asModuleEquiv and Rep.equivalenceModuleMonoidAlgebra for k[G].

See I. Assem, D. Simson, A. Skowroński, Elements of the Representation Theory of Associative Algebras, Vol. 1, Ch. III, or R. Schiffler, Quiver Representations, Ch. 5.

noncomputable def TauCeti.QuiverRep.pathEnd (k : Type u) (Q : Type v) [Field k] [Quiver Q] [DecidableEq Q] (M : QuiverRep k Q) (x : Quiver.TotalPath Q) : Module.End k (DirectSum Q (vertexSpace k Q M))

The endomorphism of ⨁ᵥ Mᵥ by which a path acts.

Equations

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

theorem TauCeti.QuiverRep.pathEnd_apply (k : Type u) (Q : Type v) [Field k] [Quiver Q] [DecidableEq Q] (M : QuiverRep k Q) (x : Quiver.TotalPath Q) (z : DirectSum Q (vertexSpace k Q M)) : (pathEnd k Q M x) z = (DirectSum.lof k Q (vertexSpace k Q M) x.snd.fst) ((mapₗ k Q M x.snd.snd) ((DirectSum.component k Q (vertexSpace k Q M) x.fst) z))

The endomorphism of a path reads off the component at its source, applies the structure map, and puts the result in the component at its target.

theorem TauCeti.QuiverRep.pathEnd_mk_apply (k : Type u) (Q : Type v) [Field k] [Quiver Q] [DecidableEq Q] (M : QuiverRep k Q) {a b : Q} (p : Quiver.Path a b) (z : DirectSum Q (vertexSpace k Q M)) : (pathEnd k Q M ⟨a, ⟨b, p⟩⟩) z = (DirectSum.lof k Q (vertexSpace k Q M) b) ((mapₗ k Q M p) ((DirectSum.component k Q (vertexSpace k Q M) a) z))

TauCeti.QuiverRep.pathEnd_apply on a path given by its source, target and underlying path, the form in which the endpoints are available for rewriting.

theorem TauCeti.QuiverRep.pathEnd_mul_pathEnd_of_comp (k : Type u) (Q : Type v) [Field k] [Quiver Q] [DecidableEq Q] (M : QuiverRep k Q) {a b c : Q} (p : Quiver.Path a b) (q : Quiver.Path c a) : pathEnd k Q M ⟨a, ⟨b, p⟩⟩ * pathEnd k Q M ⟨c, ⟨a, q⟩⟩ = pathEnd k Q M ⟨c, ⟨b, q.comp p⟩⟩

Composable paths compose: the endomorphisms of two paths that meet multiply to the endomorphism of their concatenation, later factor first, as the path algebra multiplies them.

theorem TauCeti.QuiverRep.pathEnd_mul_pathEnd_of_not_composable (k : Type u) (Q : Type v) [Field k] [Quiver Q] [DecidableEq Q] (M : QuiverRep k Q) {x y : Quiver.TotalPath Q} (h : y.snd.fst ≠ x.fst) : pathEnd k Q M x * pathEnd k Q M y = 0

Paths that do not meet annihilate one another, because the second lands in a summand the first reads as zero. This is the other half of the multiplicativity of TauCeti.QuiverRep.toEnd.

theorem TauCeti.QuiverRep.sum_pathEnd_nil (k : Type u) (Q : Type v) [Field k] [Quiver Q] [DecidableEq Q] (M : QuiverRep k Q) [Fintype Q] : ∑ v : Q, pathEnd k Q M ⟨v, ⟨v, Quiver.Path.nil⟩⟩ = 1

The trivial paths give the summand projections, and those sum to the identity: this is what makes TauCeti.QuiverRep.toEnd unital, the unit of the path algebra being the sum of the vertex idempotents.

noncomputable def TauCeti.QuiverRep.toEnd (k : Type u) (Q : Type v) [Field k] [Quiver Q] [Finite Q] [DecidableEq Q] (M : QuiverRep k Q) : pathAlgebra k Q →ₐ[k] Module.End k (DirectSum Q (vertexSpace k Q M))

The action of the path algebra on ⨁ᵥ Mᵥ: the universal property TauCeti.PathAlgebra.liftAlgHom applied to TauCeti.QuiverRep.pathEnd, whose three hypotheses are the two composition laws and the completeness of the summand projections proved above.

Equations

• TauCeti.QuiverRep.toEnd k Q M = TauCeti.PathAlgebra.liftAlgHom k (TauCeti.QuiverRep.pathEnd k Q M) ⋯ ⋯ ⋯

@[simp]

theorem TauCeti.QuiverRep.toEnd_ofPath (k : Type u) (Q : Type v) [Field k] [Quiver Q] [Finite Q] [DecidableEq Q] (M : QuiverRep k Q) (x : Quiver.TotalPath Q) : (toEnd k Q M) (PathAlgebra.ofPath x) = pathEnd k Q M x

The action of a basis path is the endomorphism it was assigned.

theorem TauCeti.QuiverRep.toEnd_ofPath_loop (k : Type u) (Q : Type v) [Field k] [Quiver Q] [Finite Q] [DecidableEq Q] (M : QuiverRep k Q) {v : Q} (p : Quiver.Path v v) : (toEnd k Q M) (PathAlgebra.ofPath ⟨v, ⟨v, p⟩⟩) = DirectSum.lof k Q (vertexSpace k Q M) v ∘ₗ mapₗ k Q M p ∘ₗ DirectSum.component k Q (vertexSpace k Q M) v

A loop at v acts on ⨁_u M_u through the summand M_v only.

@[simp]

theorem TauCeti.QuiverRep.toEnd_single (k : Type u) (Q : Type v) [Field k] [Quiver Q] [Finite Q] [DecidableEq Q] (M : QuiverRep k Q) (x : Quiver.TotalPath Q) (c : k) : (toEnd k Q M) (PathAlgebra.single x c) = c • pathEnd k Q M x

The action of a scaled basis path scales its endomorphism.

theorem TauCeti.QuiverRep.toEnd_vertexIdempotent (k : Type u) (Q : Type v) [Field k] [Quiver Q] [Finite Q] [DecidableEq Q] (M : QuiverRep k Q) (v : Q) : (toEnd k Q M) (PathAlgebra.vertexIdempotent k v) = pathEnd k Q M ⟨v, ⟨v, Quiver.Path.nil⟩⟩

The action of a vertex idempotent is the endomorphism of the trivial path there, which by TauCeti.QuiverRep.mapₗ_nil is the projection onto that summand.

def TauCeti.QuiverRep.asModule (k : Type u) (Q : Type v) [Field k] [Quiver Q] (M : QuiverRep k Q) : Type (max v t)

The module over the path algebra carried by a representation of Q.

@[expose] is load-bearing rather than a leak: the Module (pathAlgebra k Q) instance below is Module.compHom on the underlying direct sum, and the naturality square of TauCeti.QuiverRep.asModuleIso is stated on elements of it, neither of which elaborates against this type until the body is unfolded. Consumers should still go through TauCeti.QuiverRep.asModuleEquiv, since the direct sum's own k-action is only propositionally the one carried here.

Equations

• TauCeti.QuiverRep.asModule k Q M = DirectSum Q (TauCeti.QuiverRep.vertexSpace k Q M)

@[instance_reducible]

instance TauCeti.QuiverRep.instAddCommGroupAsModule (k : Type u) (Q : Type v) [Field k] [Quiver Q] (M : QuiverRep k Q) : AddCommGroup (asModule k Q M)

Equations

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

@[instance_reducible]

noncomputable instance TauCeti.QuiverRep.instModulePathAlgebraAsModule (k : Type u) (Q : Type v) [Field k] [Quiver Q] [Finite Q] [DecidableEq Q] (M : QuiverRep k Q) : Module (pathAlgebra k Q) (asModule k Q M)

The defining kQ-action: the path algebra acts on ⨁ᵥ Mᵥ through the algebra map TauCeti.QuiverRep.toEnd into its k-linear endomorphisms.

Equations

• TauCeti.QuiverRep.instModulePathAlgebraAsModule k Q M = Module.compHom (DirectSum Q (TauCeti.QuiverRep.vertexSpace k Q M)) (TauCeti.QuiverRep.toEnd k Q M).toRingHom

@[instance_reducible]

noncomputable instance TauCeti.QuiverRep.instModuleAsModule (k : Type u) (Q : Type v) [Field k] [Quiver Q] [Finite Q] [DecidableEq Q] (M : QuiverRep k Q) : Module k (asModule k Q M)

The k-action, by restriction of scalars along algebraMap k (kQ) — deliberately not the direct sum's own k-action, though the two agree, which is what makes TauCeti.QuiverRep.asModuleEquiv k-linear; see the implementation notes.

Equations

• TauCeti.QuiverRep.instModuleAsModule k Q M = Module.restrictScalars k (TauCeti.pathAlgebra k Q) (TauCeti.QuiverRep.asModule k Q M)

instance TauCeti.QuiverRep.instIsScalarTowerPathAlgebraAsModule (k : Type u) (Q : Type v) [Field k] [Quiver Q] [Finite Q] [DecidableEq Q] (M : QuiverRep k Q) : IsScalarTower k (pathAlgebra k Q) (asModule k Q M)

The k-action on TauCeti.QuiverRep.asModule is the restriction of the kQ-action, so the two are compatible by construction.

noncomputable def TauCeti.QuiverRep.asModuleEquiv (k : Type u) (Q : Type v) [Field k] [Quiver Q] [Finite Q] [DecidableEq Q] (M : QuiverRep k Q) : asModule k Q M ≃ₗ[k] DirectSum Q (vertexSpace k Q M)

The module carried by a representation is its direct sum of vertex spaces, k-linearly. This is the identification consumers should go through, the k-action on TauCeti.QuiverRep.asModule being only propositionally the direct sum's own.

Equations

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

theorem TauCeti.QuiverRep.smul_asModule_def (k : Type u) (Q : Type v) [Field k] [Quiver Q] [Finite Q] [DecidableEq Q] (M : QuiverRep k Q) (f : pathAlgebra k Q) (x : asModule k Q M) : f • x = ((toEnd k Q M) f) ((asModuleEquiv k Q M) x)

The defining action on TauCeti.QuiverRep.asModule: an element of the path algebra acts through TauCeti.QuiverRep.toEnd.

noncomputable def TauCeti.QuiverRep.ofVertex (k : Type u) (Q : Type v) [Field k] [Quiver Q] [Finite Q] [DecidableEq Q] (M : QuiverRep k Q) (v : Q) : vertexSpace k Q M v →ₗ[k] asModule k Q M

The inclusion of a vertex space into the module carried by a representation.

Equations

• TauCeti.QuiverRep.ofVertex k Q M v = ↑(TauCeti.QuiverRep.asModuleEquiv k Q M).symm ∘ₗ DirectSum.lof k Q (TauCeti.QuiverRep.vertexSpace k Q M) v

noncomputable def TauCeti.QuiverRep.toVertex (k : Type u) (Q : Type v) [Field k] [Quiver Q] [Finite Q] [DecidableEq Q] (M : QuiverRep k Q) (v : Q) : asModule k Q M →ₗ[k] vertexSpace k Q M v

The projection of the module carried by a representation onto a vertex space.

Equations

• TauCeti.QuiverRep.toVertex k Q M v = DirectSum.component k Q (TauCeti.QuiverRep.vertexSpace k Q M) v ∘ₗ ↑(TauCeti.QuiverRep.asModuleEquiv k Q M)

@[simp]

theorem TauCeti.QuiverRep.asModuleEquiv_ofVertex (k : Type u) (Q : Type v) [Field k] [Quiver Q] [Finite Q] [DecidableEq Q] (M : QuiverRep k Q) (v : Q) (z : vertexSpace k Q M v) : (asModuleEquiv k Q M) ((ofVertex k Q M v) z) = (DirectSum.lof k Q (vertexSpace k Q M) v) z

The inclusion of a vertex space is the inclusion of the corresponding summand.

theorem TauCeti.QuiverRep.toVertex_apply (k : Type u) (Q : Type v) [Field k] [Quiver Q] [Finite Q] [DecidableEq Q] (M : QuiverRep k Q) (v : Q) (x : asModule k Q M) : (toVertex k Q M v) x = (DirectSum.component k Q (vertexSpace k Q M) v) ((asModuleEquiv k Q M) x)

The projection onto a vertex space reads off the corresponding component.

@[simp]

theorem TauCeti.QuiverRep.toVertex_ofVertex (k : Type u) (Q : Type v) [Field k] [Quiver Q] [Finite Q] [DecidableEq Q] (M : QuiverRep k Q) (v : Q) (z : vertexSpace k Q M v) : (toVertex k Q M v) ((ofVertex k Q M v) z) = z

The projection onto a vertex space undoes its inclusion.

@[simp]

theorem TauCeti.QuiverRep.toVertex_ofVertex_of_ne (k : Type u) (Q : Type v) [Field k] [Quiver Q] [Finite Q] [DecidableEq Q] (M : QuiverRep k Q) {u v : Q} (h : u ≠ v) (z : vertexSpace k Q M v) : (toVertex k Q M u) ((ofVertex k Q M v) z) = 0

The summands are independent: the projection onto a vertex space kills the image of every other one.

theorem TauCeti.QuiverRep.sum_ofVertex_toVertex (k : Type u) (Q : Type v) [Field k] [Quiver Q] [Finite Q] [DecidableEq Q] (M : QuiverRep k Q) [Fintype Q] (x : asModule k Q M) : ∑ v : Q, (ofVertex k Q M v) ((toVertex k Q M v) x) = x

The summands exhaust the module: every element of TauCeti.QuiverRep.asModule is the sum of the images of its vertex components.

theorem TauCeti.QuiverRep.ofVertex_injective (k : Type u) (Q : Type v) [Field k] [Quiver Q] [Finite Q] [DecidableEq Q] (M : QuiverRep k Q) (v : Q) : Function.Injective ⇑(ofVertex k Q M v)

The inclusion of a vertex space is injective.

theorem TauCeti.QuiverRep.smul_ofPath (k : Type u) (Q : Type v) [Field k] [Quiver Q] [Finite Q] [DecidableEq Q] (M : QuiverRep k Q) {a b : Q} (p : Quiver.Path a b) (x : asModule k Q M) : PathAlgebra.ofPath ⟨a, ⟨b, p⟩⟩ • x = (ofVertex k Q M b) ((mapₗ k Q M p) ((toVertex k Q M a) x))

A basis path acts by transporting the component at its source: it reads off that component, applies the structure map, and puts the result in the component at its target. This is TauCeti.QuiverRep.pathEnd read on TauCeti.QuiverRep.asModule.

@[simp]

theorem TauCeti.QuiverRep.smul_ofVertex (k : Type u) (Q : Type v) [Field k] [Quiver Q] [Finite Q] [DecidableEq Q] (M : QuiverRep k Q) {a b : Q} (p : Quiver.Path a b) (z : vertexSpace k Q M a) : PathAlgebra.ofPath ⟨a, ⟨b, p⟩⟩ • (ofVertex k Q M a) z = (ofVertex k Q M b) ((mapₗ k Q M p) z)

A path acts on the image of its source through the structure map: this is the naturality that makes TauCeti.QuiverRep.asModuleIso a morphism of representations.

@[simp]

theorem TauCeti.QuiverRep.vertexIdempotent_smul (k : Type u) (Q : Type v) [Field k] [Quiver Q] [Finite Q] [DecidableEq Q] (M : QuiverRep k Q) (v : Q) (x : asModule k Q M) : PathAlgebra.vertexIdempotent k v • x = (ofVertex k Q M v) ((toVertex k Q M v) x)

The vertex idempotent acts as the projection onto its summand, the fact from which the vertex component of TauCeti.QuiverRep.asModule is read off.

theorem TauCeti.QuiverRep.vertexComponent_asModule (k : Type u) (Q : Type v) [Field k] [Quiver Q] [Finite Q] [DecidableEq Q] (M : QuiverRep k Q) (v : Q) : vertexComponent k (asModule k Q M) v = (ofVertex k Q M v).range

The vertex component is the image of the vertex space: the piece of TauCeti.QuiverRep.asModule that the vertex idempotent fixes is the summand Mᵥ.

noncomputable def TauCeti.QuiverRep.vertexComponentEquiv (k : Type u) (Q : Type v) [Field k] [Quiver Q] [Finite Q] [DecidableEq Q] (M : QuiverRep k Q) (v : Q) : vertexSpace k Q M v ≃ₗ[k] ↥(vertexComponent k (asModule k Q M) v)

The vertex space of a representation is the vertex component of the module it carries.

Equations

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

@[simp]

theorem TauCeti.QuiverRep.coe_vertexComponentEquiv (k : Type u) (Q : Type v) [Field k] [Quiver Q] [Finite Q] [DecidableEq Q] (M : QuiverRep k Q) (v : Q) (z : vertexSpace k Q M v) : ↑((vertexComponentEquiv k Q M v) z) = (ofVertex k Q M v) z

The identification of a vertex space with a vertex component is the inclusion of the summand.

@[simp]

theorem TauCeti.QuiverRep.pathMap_vertexComponentEquiv (k : Type u) (Q : Type v) [Field k] [Quiver Q] [Finite Q] [DecidableEq Q] (M : QuiverRep k Q) {a b : Q} (p : Quiver.Path a b) (z : vertexSpace k Q M a) : (pathMap k (asModule k Q M) p) ((vertexComponentEquiv k Q M a) z) = (vertexComponentEquiv k Q M b) ((mapₗ k Q M p) z)

The identification is natural in the path: the action of a path on the vertex components of TauCeti.QuiverRep.asModule is the structure map of the representation.

noncomputable def TauCeti.QuiverRep.asModuleIso (k : Type u) (Q : Type v) [Field k] [Quiver Q] [Finite Q] [DecidableEq Q] (M : QuiverRep k Q) : quiverRepOfModule k Q (asModule k Q M) ≅ M

Essential surjectivity, as an isomorphism: the representation carried by the module carried by M is M again.

Equations

• TauCeti.QuiverRep.asModuleIso k Q M = CategoryTheory.NatIso.ofComponents (fun (a : CategoryTheory.Paths Q) => (TauCeti.QuiverRep.vertexComponentEquiv k Q M a).toModuleIso.symm) ⋯

theorem TauCeti.QuiverRep.dimVector_asModule (k : Type u) (Q : Type v) [Field k] [Quiver Q] [Finite Q] [DecidableEq Q] (M : QuiverRep k Q) : dimVector (quiverRepOfModule k Q (asModule k Q M)) = dimVector M

The dimension vector is unchanged by passing to the module a representation carries and back.

instance TauCeti.QuiverRep.small_asModule (k : Type u) (Q : Type v) [Field k] [Quiver Q] [Finite Q] (M : QuiverRep k Q) : Small.{t, max t v} (asModule k Q M)

The module carried by a representation is no larger than the representation: over a finite vertex set the direct sum ⨁ᵥ Mᵥ is a finite product of the vertex spaces, so it has a model in their universe even though it is indexed by a vertex type that may live in a larger one.

noncomputable def TauCeti.QuiverRep.asModuleShrink (k : Type u) (Q : Type v) [Field k] [Quiver Q] [Finite Q] [DecidableEq Q] (M : QuiverRep k Q) : ModuleCat (pathAlgebra k Q)

The module carried by a representation, in the universe of the representation: a model of TauCeti.QuiverRep.asModule in Type t, as an object of ModuleCat (kQ). It is bundled as an object rather than as a type so that its k-structure is the restriction of scalars that ModuleCat.moduleOfAlgebraModule puts on it, and not the one Shrink transports; that is the structure TauCeti.quiverRepFunctor reads it with.

Equations

• TauCeti.QuiverRep.asModuleShrink k Q M = ↧(Shrink.{?u.1, max ?u.1 ?u.3} (TauCeti.QuiverRep.asModule k Q M))

noncomputable def TauCeti.QuiverRep.asModuleShrinkEquiv (k : Type u) (Q : Type v) [Field k] [Quiver Q] [Finite Q] [DecidableEq Q] (M : QuiverRep k Q) : ↑(asModuleShrink k Q M) ≃ₗ[pathAlgebra k Q] asModule k Q M

The small model is the module carried by the representation, kQ-linearly.

Equations

• TauCeti.QuiverRep.asModuleShrinkEquiv k Q M = Shrink.linearEquiv (TauCeti.pathAlgebra k Q) (TauCeti.QuiverRep.asModule k Q M)

noncomputable def TauCeti.QuiverRep.asModuleShrinkIso (k : Type u) (Q : Type v) [Field k] [Quiver Q] [Finite Q] [DecidableEq Q] (M : QuiverRep k Q) : quiverRepOfModule k Q ↑(asModuleShrink k Q M) ≅ M

Essential surjectivity in the universe of the representation: the representation carried by the small model of the module carried by M is M again. This is TauCeti.QuiverRep.asModuleIso transported along TauCeti.QuiverRep.asModuleShrinkEquiv, and it is what makes TauCeti.quiverRepEquivalence an equivalence at an arbitrary representation universe.

Equations

• TauCeti.QuiverRep.asModuleShrinkIso k Q M = CategoryTheory.NatIso.ofComponents (fun (a : CategoryTheory.Paths Q) => (TauCeti.QuiverRep.vertexShrinkEquiv✝ k Q M a).toModuleIso) ⋯

instance TauCeti.QuiverRep.instEssSurjModuleCatPathAlgebraQuiverRepFunctor (k : Type u) (Q : Type v) [Field k] [Quiver Q] [Finite Q] : (quiverRepFunctor k Q).EssSurj

The module-to-representation functor is essentially surjective: every representation is carried by the kQ-module TauCeti.QuiverRep.asModule built from it, read in the universe of the representation through TauCeti.QuiverRep.asModuleShrink.

instance TauCeti.QuiverRep.instIsEquivalenceModuleCatPathAlgebraQuiverRepFunctor (k : Type u) (Q : Type v) [Field k] [Quiver Q] [Finite Q] : (quiverRepFunctor k Q).IsEquivalence

The module-to-representation functor is an equivalence: it is fully faithful by TauCeti.quiverRepFunctorFullyFaithful and essentially surjective by the instance above.

noncomputable def TauCeti.quiverRepEquivalence (k : Type u) (Q : Type v) [Field k] [Quiver Q] [Finite Q] : QuiverRep k Q ≌ ModuleCat (pathAlgebra k Q)

Representations of a quiver are modules over its path algebra.

Equations

• TauCeti.quiverRepEquivalence k Q = (TauCeti.quiverRepFunctor k Q).asEquivalence.symm

theorem TauCeti.quiverRepEquivalence_inverse (k : Type u) (Q : Type v) [Field k] [Quiver Q] [Finite Q] : (quiverRepEquivalence k Q).inverse = quiverRepFunctor k Q

The inverse of TauCeti.quiverRepEquivalence is TauCeti.quiverRepFunctor: the equivalence is the module-to-representation functor of TauCeti.RepresentationTheory.Quiver.Representation.OfModule, turned around.

noncomputable def TauCeti.quiverRepEquivalenceFunctorObjShrinkIso (k : Type u) (Q : Type v) [Field k] [Quiver Q] [Finite Q] [DecidableEq Q] (M : QuiverRep k Q) : (quiverRepEquivalence k Q).functor.obj M ≅ QuiverRep.asModuleShrink k Q M

The forward direction of TauCeti.quiverRepEquivalence is TauCeti.QuiverRep.asModuleShrink. The functor of the equivalence is CategoryTheory.Functor.inv, so on objects it is a choice of preimage; this identifies that choice with the model of TauCeti.QuiverRep.asModule built here, at the arbitrary representation universe t the equivalence is stated at, which is what a consumer transporting a representation across it needs. For a representation valued in the universe max v t where the direct sum ⨁ᵥ Mᵥ itself lives, TauCeti.quiverRepEquivalenceFunctorObjIso identifies the preimage with that sum directly.

Equations

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

noncomputable def TauCeti.quiverRepEquivalenceFunctorObjIso (k : Type u) (Q : Type v) [Field k] [Quiver Q] [Finite Q] [DecidableEq Q] (M : QuiverRep k Q) : (quiverRepEquivalence k Q).functor.obj M ≅ ↧(QuiverRep.asModule k Q M)

The forward direction of TauCeti.quiverRepEquivalence is TauCeti.QuiverRep.asModule, at the universe max v t where the direct sum ⨁ᵥ Mᵥ lives: the concrete form of TauCeti.quiverRepEquivalenceFunctorObjShrinkIso, identifying the chosen preimage with the direct sum itself rather than with a model of it.

Equations

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