Documentation

TauCeti.RepresentationTheory.Quiver.PathAlgebra.Rescale

Rescaling the arrows of a path algebra #

A labelling of the arrows of a quiver by scalars multiplies out along a path to the weight of that path, and rescaling every basis path by its weight is an algebra endomorphism of the path algebra: weights are multiplicative under concatenation and trivial on the vertex idempotents, which is exactly what the universal property TauCeti.PathAlgebra.liftAlgHom asks for. Two rescalings compose by multiplying labellings, and the constant labelling 1 rescales by the identity, so a labelling by units rescales by an algebra automorphism, inverted by the labelling by inverses.

These rescalings are the gauge transformations of a quiver with relations: each fixes every vertex idempotent and multiplies each arrow by its label, so it carries a relation to the correspondingly rescaled relation.

Implementation notes #

A labelling of the arrows is spelled out as the dependent function type ∀ ⦃a b⦄, (a ⟶ b) → k rather than through Mathlib's Quiver.Labelling, which is a non-reducible definition of the same type: rewriting with a lemma whose labelling argument is a metavariable of that type fails, since the metavariable cannot be applied to an arrow before the definition is unfolded.

Main definitions #

Main results #

References #

This is infrastructure for the gauge-change clause of Layer 4 of TauCetiRoadmap/ZigzagPreprojective/README.md, which asks for the algebra isomorphisms rescaling the arrows of a doubled quiver by signs, and for their generalization to an arbitrary antisymmetric scalar labelling.

Properties of path weights #

source
@[simp]
theorem Quiver.Path.weight_toPath {k : Type w} {Q : Type u} [Monoid k] [Quiver Q] (c : ⦃a b : Q⦄ → (a ⟶ b) → k) {a b : Q} (e : a ⟶ b) :
weight (fun {x x_1 : Q} (f : x ⟶ x_1) => c f) e.toPath = c e
source
theorem Quiver.Path.weight_congr {k : Type w} {Q : Type u} [Monoid k] [Quiver Q] (c d : ⦃a b : Q⦄ → (a ⟶ b) → k) (h : ∀ ⦃a b : Q⦄ (e : a ⟶ b), c e = d e) {a b : Q} (p : Path a b) :
weight (fun {x x_1 : Q} (e : x ⟶ x_1) => c e) p = weight (fun {x x_1 : Q} (e : x ⟶ x_1) => d e) p

Pointwise equal labellings give equal weights.

source
@[simp]
theorem Quiver.Path.weight_one {k : Type w} {Q : Type u} [Monoid k] [Quiver Q] {a b : Q} (p : Path a b) :
weight (fun {x x_1 : Q} (x_2 : x ⟶ x_1) => 1) p = 1

Every path has weight one under the constant labelling by one.

source
theorem Quiver.Path.weight_mul {k : Type w} {Q : Type u} [CommMonoid k] [Quiver Q] (c d : ⦃a b : Q⦄ → (a ⟶ b) → k) {a b : Q} (p : Path a b) :
weight (fun {x x_1 : Q} (e : x ⟶ x_1) => c e * d e) p = weight (fun {x x_1 : Q} (e : x ⟶ x_1) => c e) p * weight (fun {x x_1 : Q} (e : x ⟶ x_1) => d e) p

The weight under a pointwise product of labellings is the product of the weights.

The rescaling endomorphism #

source
noncomputable def TauCeti.PathAlgebra.rescale {k : Type w} {Q : Type u} [CommSemiring k] [Quiver Q] [Finite Q] (c : ⦃a b : Q⦄ → (a ⟶ b) → k) :
pathAlgebra k Q →ₐ[k] pathAlgebra k Q

The arrow rescaling attached to a labelling c of the arrows of Q by scalars: the algebra endomorphism of the path algebra multiplying each basis path by its weight. Equivalently it fixes every vertex idempotent and multiplies each arrow by its label.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem TauCeti.PathAlgebra.rescale_ofPath {k : Type w} {Q : Type u} [CommSemiring k] [Quiver Q] [Finite Q] (c : ⦃a b : Q⦄ → (a ⟶ b) → k) (x : Quiver.TotalPath Q) :
    (rescale c) (ofPath x) = Quiver.Path.weight (fun {x x_1 : Q} (f : x ⟶ x_1) => c f) x.snd.snd • ofPath x

    Rescaling a basis path multiplies it by the path's weight.

    source
    @[simp]
    theorem TauCeti.PathAlgebra.rescale_vertexIdempotent {k : Type w} {Q : Type u} [CommSemiring k] [Quiver Q] [Finite Q] (c : ⦃a b : Q⦄ → (a ⟶ b) → k) (v : Q) :
    (rescale c) (vertexIdempotent k v) = vertexIdempotent k v

    Every vertex idempotent is fixed by arrow rescaling.

    source
    theorem TauCeti.PathAlgebra.rescale_ofArrow {k : Type w} {Q : Type u} [CommSemiring k] [Quiver Q] [Finite Q] (c : ⦃a b : Q⦄ → (a ⟶ b) → k) {a b : Q} (e : a ⟶ b) :
    (rescale c) (ofArrow e) = c e • ofArrow e

    Rescaling an arrow multiplies it by its label.

    source
    @[simp]
    theorem TauCeti.PathAlgebra.rescale_one {k : Type w} {Q : Type u} [CommSemiring k] [Quiver Q] [Finite Q] :
    (rescale fun (x x_1 : Q) (x_2 : x ⟶ x_1) => 1) = AlgHom.id k (pathAlgebra k Q)

    Rescaling by the constant labelling one is the identity.

    source
    @[simp]
    theorem TauCeti.PathAlgebra.rescale_comp_rescale {k : Type w} {Q : Type u} [CommSemiring k] [Quiver Q] [Finite Q] (c d : ⦃a b : Q⦄ → (a ⟶ b) → k) :
    (rescale c).comp (rescale d) = rescale fun (x x_1 : Q) (e : x ⟶ x_1) => c e * d e

    Rescalings compose by multiplying labellings.

    source
    theorem TauCeti.PathAlgebra.rescale_congr {k : Type w} {Q : Type u} [CommSemiring k] [Quiver Q] [Finite Q] (c d : ⦃a b : Q⦄ → (a ⟶ b) → k) (h : ∀ ⦃a b : Q⦄ (e : a ⟶ b), c e = d e) :
    rescale c = rescale d

    Pointwise equal labellings give equal rescalings.

    source
    theorem TauCeti.PathAlgebra.rescale_rescale_of_mul_eq_one {k : Type w} {Q : Type u} [CommSemiring k] [Quiver Q] [Finite Q] (c d : ⦃a b : Q⦄ → (a ⟶ b) → k) (h : ∀ ⦃a b : Q⦄ (e : a ⟶ b), c e * d e = 1) (x : pathAlgebra k Q) :
    (rescale c) ((rescale d) x) = x

    Two rescalings whose labellings have pointwise product one undo one another. The order of the product in the hypothesis matches the order of composition.

    source
    theorem TauCeti.PathAlgebra.rescale_mem_gradeBy {k : Type w} {Q : Type u} [CommSemiring k] [Quiver Q] [Finite Q] (c : ⦃a b : Q⦄ → (a ⟶ b) → k) {M : Type u_1} [AddMonoid M] (wt : {a b : Q} → (a ⟶ b) → M) {m : M} {x : pathAlgebra k Q} (hx : x ∈ gradeBy k (fun {a b : Q} => wt) m) :
    (rescale c) x ∈ gradeBy k (fun {a b : Q} => wt) m

    Arrow rescaling is graded for every arrow weight: it multiplies each basis path by a scalar, so it preserves the span of the paths of any given weight.

    source
    theorem TauCeti.PathAlgebra.rescale_mem_grade {k : Type w} {Q : Type u} [CommSemiring k] [Quiver Q] [Finite Q] (c : ⦃a b : Q⦄ → (a ⟶ b) → k) {n : ℕ} {x : pathAlgebra k Q} (hx : x ∈ grade k Q n) :
    (rescale c) x ∈ grade k Q n

    Arrow rescaling preserves the path-length grading.