Documentation

TauCeti.RepresentationTheory.Quiver.Representation.Projective.Simple.Resolution

The projective resolution of a vertex simple #

Let i be a vertex of a quiver Q with finitely many arrows out of it. A path out of i is either trivial or an arrow e : i ⟶ j followed by a path out of j, and this decomposition is unique. Consequently the kernel of the surjection Pᵢ ↠ Sᵢ, which is spanned by the paths of positive length, is the direct sum of the projectives Pⱼ over the arrows e : i ⟶ j, embedded by prefixing e. This gives the short exact sequence

0 ⟶ ⨁_{e : i ⟶ j} Pⱼ ⟶ Pᵢ ⟶ Sᵢ ⟶ 0

of representations, a projective resolution of Sᵢ of length at most one. No acyclicity is needed: cycles through i lie in the kernel of Pᵢ ↠ Sᵢ and are accounted for by the summands Pⱼ. For example, for the quiver 1 ⟶ 2 it is 0 ⟶ P₂ ⟶ P₁ ⟶ S₁ ⟶ 0, while S₂ = P₂ because no arrow leaves 2.

Every invariant additive on short exact sequences therefore satisfies [Sᵢ] = [Pᵢ] - ∑_{e : i ⟶ j} [Pⱼ]: this is how Euler characteristics computed on the projectives Pᵢ pass to the simples.

Main definitions #

Main results #

References #

source
noncomputable def TauCeti.indecProjRepArrowHom (k : Type u) {Q : Type v} [Field k] [Quiver Q] {i j : Q} (e : i ⟶ j) :
indecProjRep k Q j ⟶ indecProjRep k Q i

The morphism of an arrow: for e : i ⟶ j, the morphism Pⱼ ⟶ Pᵢ prefixing e to every path out of j. Under the universal property of Pⱼ it is the element e of (Pᵢ)ⱼ.

Instances For
    source
    @[simp]
    theorem TauCeti.indecProjRepArrowHom_app_basis (k : Type u) {Q : Type v} [Field k] [Quiver Q] {i j b : Q} (e : i ⟶ j) (q : Quiver.Path j b) :
    (CategoryTheory.ConcreteCategory.hom ((indecProjRepArrowHom k e).app ((CategoryTheory.Paths.of Q).obj b))) ((indecProjRepBasis k j b) q) = (indecProjRepBasis k i b) (e.toPath.comp q)

    The morphism of an arrow e sends the basis vector of a path q to that of e followed by q.

    source
    theorem TauCeti.indecProjRepBasis_repr_indecProjRepArrowHom_app (k : Type u) {Q : Type v} [Field k] [Quiver Q] {i j b : Q} (e : i ⟶ j) (x : ↑((indecProjRep k Q j).obj ((CategoryTheory.Paths.of Q).obj b))) :
    (indecProjRepBasis k i b).repr ((CategoryTheory.ConcreteCategory.hom ((indecProjRepArrowHom k e).app ((CategoryTheory.Paths.of Q).obj b))) x) = Finsupp.mapDomain (fun (q : Quiver.Path j b) => e.toPath.comp q) ((indecProjRepBasis k j b).repr x)

    The morphism of an arrow in the path bases: it moves the coordinates along the injection q ↦ e.toPath.comp q of paths.

    source
    @[simp]
    theorem TauCeti.indecProjRepBasis_repr_indecProjRepArrowHom_app_comp (k : Type u) {Q : Type v} [Field k] [Quiver Q] {i j b : Q} (e : i ⟶ j) (x : ↑((indecProjRep k Q j).obj ((CategoryTheory.Paths.of Q).obj b))) (q : Quiver.Path j b) :
    ((indecProjRepBasis k i b).repr ((CategoryTheory.ConcreteCategory.hom ((indecProjRepArrowHom k e).app ((CategoryTheory.Paths.of Q).obj b))) x)) (e.toPath.comp q) = ((indecProjRepBasis k j b).repr x) q

    The coordinate of the image of x under the morphism of e, at e followed by q, is the coordinate of x at q.

    source
    @[simp]
    theorem TauCeti.indecProjRepBasis_repr_indecProjRepArrowHom_app_comp_of_ne (k : Type u) {Q : Type v} [Field k] [Quiver Q] {i j j' b : Q} (e : i ⟶ j) (e' : i ⟶ j') (h : ⟨j, e⟩ ≠ ⟨j', e'⟩) (x : ↑((indecProjRep k Q j).obj ((CategoryTheory.Paths.of Q).obj b))) (q : Quiver.Path j' b) :
    ((indecProjRepBasis k i b).repr ((CategoryTheory.ConcreteCategory.hom ((indecProjRepArrowHom k e).app ((CategoryTheory.Paths.of Q).obj b))) x)) (e'.toPath.comp q) = 0

    The image of the morphism of an arrow e has no coordinate at a path starting with a different arrow e'.

    source
    noncomputable def TauCeti.arrowSumToIndecProjRep (k : Type u) {Q : Type v} [Field k] [Quiver Q] (i : Q) [Finite ((j : Q) × (i ⟶ j))] :
    (⨁ fun (a : (j : Q) × (i ⟶ j)) => indecProjRep k Q a.fst) ⟶ indecProjRep k Q i

    The kernel of Pᵢ ↠ Sᵢ as a direct sum: the morphism ⨁_{e : i ⟶ j} Pⱼ ⟶ Pᵢ whose component at e is the morphism TauCeti.indecProjRepArrowHom prefixing e.

    Instances For
      source
      @[simp]
      theorem TauCeti.ι_arrowSumToIndecProjRep (k : Type u) {Q : Type v} [Field k] [Quiver Q] (i : Q) [Finite ((j : Q) × (i ⟶ j))] (a : (j : Q) × (i ⟶ j)) :
      CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.ι (fun (a : (j : Q) × (i ⟶ j)) => indecProjRep k Q a.fst) a) (arrowSumToIndecProjRep k i) = indecProjRepArrowHom k a.snd

      The component of ⨁_{e : i ⟶ j} Pⱼ ⟶ Pᵢ at an arrow is the morphism of that arrow.

      source
      @[simp]
      theorem TauCeti.ι_arrowSumToIndecProjRep_assoc (k : Type u) {Q : Type v} [Field k] [Quiver Q] (i : Q) [Finite ((j : Q) × (i ⟶ j))] (a : (j : Q) × (i ⟶ j)) {Z : QuiverRep k Q} (h : indecProjRep k Q i ⟶ Z) :
      CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.ι (fun (a : (j : Q) × (i ⟶ j)) => indecProjRep k Q a.fst) a) (CategoryTheory.CategoryStruct.comp (arrowSumToIndecProjRep k i) h) = CategoryTheory.CategoryStruct.comp (indecProjRepArrowHom k a.snd) h

      The component of ⨁_{e : i ⟶ j} Pⱼ ⟶ Pᵢ at an arrow is the morphism of that arrow.

      source
      instance TauCeti.mono_arrowSumToIndecProjRep (k : Type u) {Q : Type v} [Field k] [Quiver Q] (i : Q) [Finite ((j : Q) × (i ⟶ j))] :
      CategoryTheory.Mono (arrowSumToIndecProjRep k i)

      ⨁_{e : i ⟶ j} Pⱼ ⟶ Pᵢ is a monomorphism.

      source
      @[simp]
      theorem TauCeti.arrowSumToIndecProjRep_comp_indecProjRepToSimpleRep (k : Type (max v w)) {Q : Type v} [Field k] [Quiver Q] (i : Q) [Finite ((j : Q) × (i ⟶ j))] :
      CategoryTheory.CategoryStruct.comp (arrowSumToIndecProjRep k i) (indecProjRepToSimpleRep k i) = 0

      The composite ⨁_{e : i ⟶ j} Pⱼ ⟶ Pᵢ ⟶ Sᵢ vanishes: a path beginning with an arrow has positive length.

      source
      @[simp]
      theorem TauCeti.arrowSumToIndecProjRep_comp_indecProjRepToSimpleRep_assoc (k : Type (max v w)) {Q : Type v} [Field k] [Quiver Q] (i : Q) [Finite ((j : Q) × (i ⟶ j))] {Z : QuiverRep k Q} (h : simpleRep k Q i ⟶ Z) :
      CategoryTheory.CategoryStruct.comp (arrowSumToIndecProjRep k i) (CategoryTheory.CategoryStruct.comp (indecProjRepToSimpleRep k i) h) = CategoryTheory.CategoryStruct.comp 0 h

      The composite ⨁_{e : i ⟶ j} Pⱼ ⟶ Pᵢ ⟶ Sᵢ vanishes: a path beginning with an arrow has positive length.

      source
      theorem TauCeti.shortExact_arrowSumToIndecProjRep (k : Type (max v w)) {Q : Type v} [Field k] [Quiver Q] (i : Q) [Finite ((j : Q) × (i ⟶ j))] :
      { X₁ := ⨁ fun (a : (j : Q) × (i ⟶ j)) => indecProjRep k Q a.fst, X₂ := indecProjRep k Q i, X₃ := simpleRep k Q i, f := arrowSumToIndecProjRep k i, g := indecProjRepToSimpleRep k i, zero := ⋯ }.ShortExact

      The projective resolution of a vertex simple: for a vertex i with finitely many arrows out of it, the sequence 0 ⟶ ⨁_{e : i ⟶ j} Pⱼ ⟶ Pᵢ ⟶ Sᵢ ⟶ 0 is short exact. Both nonzero terms before Sᵢ are projective, so Sᵢ has projective dimension at most one.