Documentation

TauCeti.RepresentationTheory.Quiver.PathAlgebra.PathsInto

Paths ending at a vertex #

For a quiver R, pathsInto k n j is the span in its path algebra of paths of length n ending at j. This file describes the span through the path-length grading and the vertex idempotent, proves its multiplication and last-arrow decomposition, and counts its dimension. The last-arrow decomposition is unique: ∑_{b : i ⟶ j} b f_b determines each eᵢ f_b. These results apply to path algebras independently of any relations.

Main results #

source
@[reducible, inline]
abbrev TauCeti.PathAlgebra.PathInto (R : Type u) [Quiver R] (n : ℕ) (j : R) :
Type (max u v)

The paths of length n ending at j, recorded together with their source.

Equations
Instances For
    source
    @[reducible, inline]
    abbrev TauCeti.PathAlgebra.PathBetween (R : Type u) [Quiver R] (n : ℕ) (i j : R) :
    Type (max u v)

    The paths of length n from i to j.

    Equations
    Instances For
      source
      instance TauCeti.PathAlgebra.finite_pathInto {R : Type u} [Quiver R] [Finite R] [∀ (a b : R), Finite (a ⟶ b)] (n : ℕ) (j : R) :
      Finite (PathInto R n j)

      For a finite quiver, the paths of a fixed length into one vertex form a finite type.

      source
      instance TauCeti.PathAlgebra.finite_pathBetween {R : Type u} [Quiver R] [Finite R] [∀ (a b : R), Finite (a ⟶ b)] (n : ℕ) (i j : R) :
      Finite (PathBetween R n i j)

      For a finite quiver, the paths of a fixed length between two vertices form a finite type.

      source
      theorem TauCeti.PathAlgebra.card_arrow_mul_card_pathInto_eq {R : Type u} [Quiver R] [Fintype R] [(a b : R) → Fintype (a ⟶ b)] (n : ℕ) (j : R) :
      ∑ i : R, Fintype.card (i ⟶ j) * Nat.card (PathInto R n i) = Nat.card (PathInto R (n + 1) j)

      Every path of length n + 1 into j has a unique last arrow and a length-n prefix.

      source
      noncomputable def TauCeti.PathAlgebra.pathsInto {R : Type u} [Quiver R] (k : Type w) [CommSemiring k] (n : ℕ) (j : R) :
      Submodule k (pathAlgebra k R)

      The span of the paths of length n ending at j: the degree-n part of the left corner e_j kR (TauCeti.PathAlgebra.mem_pathsInto_iff).

      Equations
      Instances For
        source
        noncomputable def TauCeti.PathAlgebra.pathsBetween {R : Type u} [Quiver R] (k : Type w) [CommSemiring k] (n : ℕ) (i j : R) :
        Submodule k (pathAlgebra k R)

        The span of paths of length n from i to j. For a finite vertex type this is the degree-n part of the corner e_j kR e_i.

        Equations
        Instances For
          source
          theorem TauCeti.PathAlgebra.ofPath_mem_pathsInto {R : Type u} [Quiver R] {k : Type w} [CommSemiring k] {s j : R} (p : Quiver.Path s j) :
          ofPath ⟨s, ⟨j, p⟩⟩ ∈ pathsInto k p.length j

          A path ending at j lies in the span of the paths of its length into j.

          source
          theorem TauCeti.PathAlgebra.ofPath_mem_pathsInto_of_length {R : Type u} [Quiver R] {k : Type w} [CommSemiring k] {s j : R} {n : ℕ} (p : Quiver.Path s j) (hp : p.length = n) :
          ofPath ⟨s, ⟨j, p⟩⟩ ∈ pathsInto k n j

          A path of length n ending at j lies in the span of the paths of length n into j.

          source
          theorem TauCeti.PathAlgebra.pathsInto_le_grade {R : Type u} [Quiver R] {k : Type w} [CommSemiring k] (n : ℕ) (j : R) :
          pathsInto k n j ≤ grade k R n

          The paths of length n into j span a subspace of the degree-n part of the path algebra.

          source
          theorem TauCeti.PathAlgebra.vertexIdempotent_mul_of_mem_pathsInto {R : Type u} [Quiver R] {k : Type w} [CommSemiring k] {n : ℕ} {j : R} {x : pathAlgebra k R} (hx : x ∈ pathsInto k n j) :
          vertexIdempotent k j * x = x

          A vertex idempotent acts as the identity on paths ending at that vertex.

          source
          theorem TauCeti.PathAlgebra.vertexIdempotent_mul_mem_pathsInto {R : Type u} [Quiver R] {k : Type w} [CommSemiring k] {n : ℕ} (j : R) {x : pathAlgebra k R} (hx : x ∈ grade k R n) :
          vertexIdempotent k j * x ∈ pathsInto k n j

          Projecting a homogeneous element to the corner at j gives a path span into j.

          source
          @[simp]
          theorem TauCeti.PathAlgebra.mem_pathsInto_iff {R : Type u} [Quiver R] {k : Type w} [CommSemiring k] {n : ℕ} {j : R} {x : pathAlgebra k R} :
          x ∈ pathsInto k n j ↔ x ∈ grade k R n ∧ vertexIdempotent k j * x = x

          The span of the paths of length n into j is the degree-n part of the corner e_j kR.

          source
          @[simp]
          theorem TauCeti.PathAlgebra.mem_pathsBetween_iff {R : Type u} [Quiver R] {k : Type w} [CommSemiring k] {n : ℕ} {i j : R} {x : pathAlgebra k R} :
          x ∈ pathsBetween k n i j ↔ x ∈ grade k R n ∧ vertexIdempotent k j * x * vertexIdempotent k i = x

          The paths of length n from i to j span the degree-n part of the corner e_j kR e_i.

          source
          theorem TauCeti.PathAlgebra.pathsBetween_eq_cornerSubmodule_inf_grade {R : Type u} [Quiver R] {k : Type w} [CommSemiring k] [Finite R] (n : ℕ) (i j : R) :
          pathsBetween k n i j = cornerSubmodule k (vertexIdempotent k j) (vertexIdempotent k i) ⊓ grade k R n

          The paths of fixed length between two vertices form the corresponding graded corner.

          source
          theorem TauCeti.PathAlgebra.mul_mem_pathsInto {R : Type u} [Quiver R] {k : Type w} [CommSemiring k] {a c : ℕ} {i j : R} {x y : pathAlgebra k R} (hx : x ∈ pathsInto k a i) (hy : y ∈ pathsInto k c j) :
          x * y ∈ pathsInto k (c + a) i

          The product of an element of pathsInto k a i and one of pathsInto k c j lies in pathsInto k (c + a) i: the paths of the right factor are followed by those of the left one.

          source
          theorem TauCeti.PathAlgebra.exists_eq_sum_ofArrow_mul {R : Type u} [Quiver R] {k : Type w} [CommSemiring k] [Fintype R] [(a b : R) → Fintype (a ⟶ b)] {n : ℕ} {j : R} {x : pathAlgebra k R} (hx : x ∈ pathsInto k (n + 1) j) :
          ∃ (z : (i : R) → (i ⟶ j) → pathAlgebra k R), (∀ (i : R) (b : i ⟶ j), z i b ∈ pathsInto k n i) ∧ x = ∑ i : R, ∑ b : i ⟶ j, ofArrow b * z i b

          Last-arrow decomposition. An element of the span of the paths of length n + 1 into j is a sum, over the arrows b : i ⟶ j, of b times an element of the span of the paths of length n into i.

          source
          theorem TauCeti.PathAlgebra.sum_ofArrow_mul_eq_zero_iff {R : Type u} [Quiver R] {k : Type w} [CommSemiring k] [Fintype R] [(a b : R) → Fintype (a ⟶ b)] {j : R} {f : (i : R) → (i ⟶ j) → pathAlgebra k R} :
          ∑ i : R, ∑ b : i ⟶ j, ofArrow b * f i b = 0 ↔ ∀ (i : R) (b : i ⟶ j), vertexIdempotent k i * f i b = 0

          Uniqueness of the last-arrow decomposition. A sum ∑_{b : i ⟶ j} b f_b vanishes exactly when each f_b is killed by the vertex idempotent at the source of b: the paths q followed by distinct arrows b into j are distinct basis paths. Only the part eᵢ f_b of f_b on paths ending at i contributes to b f_b.

          source
          instance TauCeti.PathAlgebra.finiteDimensional_pathsInto {R : Type u} [Quiver R] (k : Type w) [Field k] [Finite R] [∀ (a b : R), Finite (a ⟶ b)] (n : ℕ) (j : R) :
          FiniteDimensional k ↥(pathsInto k n j)
          source
          theorem TauCeti.PathAlgebra.finrank_pathsInto {R : Type u} [Quiver R] (k : Type w) [Field k] [Finite R] [∀ (a b : R), Finite (a ⟶ b)] (n : ℕ) (j : R) :
          Module.finrank k ↥(pathsInto k n j) = Nat.card { p : (s : R) × Quiver.Path s j // p.snd.length = n }

          The dimension of the span of the paths of length n into j is the number of such paths: distinct paths are linearly independent in the path algebra.

          source
          instance TauCeti.PathAlgebra.finiteDimensional_pathsBetween {R : Type u} [Quiver R] (k : Type w) [Field k] (n : ℕ) (i j : R) [Finite (PathBetween R n i j)] :
          FiniteDimensional k ↥(pathsBetween k n i j)
          source
          theorem TauCeti.PathAlgebra.finrank_pathsBetween {R : Type u} [Quiver R] (k : Type w) [Field k] (n : ℕ) (i j : R) [Finite (PathBetween R n i j)] :
          Module.finrank k ↥(pathsBetween k n i j) = Nat.card (PathBetween R n i j)

          The dimension of the length-n corner from i to j is the number of length-n paths from i to j.