Path algebras are functorial in the quiver

A prefunctor φ : Q ⥤q R pushes a path of Q to a path of R, hence a basis element of kQ to a basis element of kR. This file extends that assignment to an algebra homomorphism TauCeti.PathAlgebra.mapAlgHom, and shows that it is an isomorphism when φ is one.

A uniform condition sufficient for this construction is that φ be bijective on vertices. The unit of kQ is the sum of all the vertex idempotents, so surjectivity ensures that their images sum to the unit of kR. Injectivity ensures that two paths which do not meet still do not meet after mapping, so their product remains zero. Thus mapAlgHom assumes vertex bijectivity, which the intended source of prefunctors — an isomorphism of the underlying graph or quiver — supplies. Nothing is asked of φ on arrows: a prefunctor which is not injective on arrows still gives an algebra homomorphism, just not an injective one.

Main definitions

• Prefunctor.mapTotalPath: the indexed path obtained by pushing an indexed path along a prefunctor.
• TauCeti.PathAlgebra.mapAlgHom: the algebra homomorphism kQ →ₐ[k] kR induced by a prefunctor bijective on vertices.
• TauCeti.PathAlgebra.mapAlgEquiv: the algebra isomorphism induced by a pair of mutually inverse prefunctors.

Main results

• TauCeti.PathAlgebra.mapAlgHom_ofPath, TauCeti.PathAlgebra.mapAlgHom_vertexIdempotent and TauCeti.PathAlgebra.mapAlgHom_ofArrow: the homomorphism on paths, vertex idempotents and arrows.
• TauCeti.PathAlgebra.mapAlgHom_id and TauCeti.PathAlgebra.mapAlgHom_comp: functoriality.
• TauCeti.PathAlgebra.mapAlgHom_mem_gradeBy: a map is graded for the pulled-back arrow weight.
• TauCeti.PathAlgebra.mapAlgEquiv_id, TauCeti.PathAlgebra.mapAlgEquiv_comp and TauCeti.PathAlgebra.mapAlgEquiv_symm: the same laws for the induced isomorphism, together with the congruence lemma TauCeti.PathAlgebra.mapAlgEquiv_congr.

References

This is the "functoriality under graph/quiver isomorphism" clause of Layer 0 of TauCetiRoadmap/ZigzagPreprojective/README.md, at the level of the ambient path algebra; the relation quotients are carried along it in TauCeti/RepresentationTheory/Quiver/Zigzag/Isomorphism.lean.

def Prefunctor.mapTotalPath {Q : Type u} {R : Type u'} [Quiver Q] [Quiver R] (φ : Q ⥤q R) (x : TauCeti.Quiver.TotalPath Q) : TauCeti.Quiver.TotalPath R

The indexed path of R obtained by pushing an indexed path of Q along a prefunctor. This is the map on the path bases which TauCeti.PathAlgebra.mapAlgHom extends.

Equations

• φ.mapTotalPath x = ⟨φ.obj x.fst, ⟨φ.obj x.snd.fst, φ.mapPath x.snd.snd⟩⟩

@[simp]

theorem Prefunctor.mapTotalPath_mk {Q : Type u} {R : Type u'} [Quiver Q] [Quiver R] (φ : Q ⥤q R) {a b : Q} (p : Quiver.Path a b) : φ.mapTotalPath ⟨a, ⟨b, p⟩⟩ = ⟨φ.obj a, ⟨φ.obj b, φ.mapPath p⟩⟩

Pushing an indexed path along a prefunctor pushes its two endpoints and its path.

@[simp]

theorem Prefunctor.mapTotalPath_fst {Q : Type u} {R : Type u'} [Quiver Q] [Quiver R] (φ : Q ⥤q R) (x : TauCeti.Quiver.TotalPath Q) : (φ.mapTotalPath x).fst = φ.obj x.fst

The source of a pushed indexed path is the image of the source.

@[simp]

theorem Prefunctor.mapTotalPath_snd_fst {Q : Type u} {R : Type u'} [Quiver Q] [Quiver R] (φ : Q ⥤q R) (x : TauCeti.Quiver.TotalPath Q) : (φ.mapTotalPath x).snd.fst = φ.obj x.snd.fst

The target of a pushed indexed path is the image of the target.

@[simp]

theorem Prefunctor.length_mapTotalPath {Q : Type u} {R : Type u'} [Quiver Q] [Quiver R] (φ : Q ⥤q R) (x : TauCeti.Quiver.TotalPath Q) : (φ.mapTotalPath x).snd.snd.length = x.snd.snd.length

Pushing an indexed path along a prefunctor preserves its length.

@[simp]

theorem Prefunctor.mapTotalPath_id {Q : Type u} [Quiver Q] (x : TauCeti.Quiver.TotalPath Q) : (𝟭q Q).mapTotalPath x = x

The identity prefunctor leaves an indexed path unchanged.

@[simp]

theorem Prefunctor.mapTotalPath_comp_apply {Q : Type u} {R : Type u'} {S : Type u''} [Quiver Q] [Quiver R] [Quiver S] (φ : Q ⥤q R) (ψ : R ⥤q S) (x : TauCeti.Quiver.TotalPath Q) : (φ ⋙q ψ).mapTotalPath x = ψ.mapTotalPath (φ.mapTotalPath x)

Pushing along a composite of prefunctors is pushing along each in turn. The name follows Prefunctor.mapPath_comp_apply, Prefunctor.mapPath_comp being reserved for concatenation.

noncomputable def TauCeti.PathAlgebra.mapAlgHom {Q : Type u} {R : Type u'} [Quiver Q] [Quiver R] (k : Type w) [CommSemiring k] [Finite Q] [Finite R] (φ : Q ⥤q R) (hφ : Function.Bijective φ.obj) : pathAlgebra k Q →ₐ[k] pathAlgebra k R

The algebra homomorphism of path algebras induced by a prefunctor bijective on vertices: it sends the basis element of a path to the basis element of the image path.

Equations

• TauCeti.PathAlgebra.mapAlgHom k φ hφ = TauCeti.PathAlgebra.liftAlgHom k (fun (x : TauCeti.Quiver.TotalPath Q) => TauCeti.PathAlgebra.ofPath (φ.mapTotalPath x)) ⋯ ⋯ ⋯

@[simp]

theorem TauCeti.PathAlgebra.mapAlgHom_ofPath {Q : Type u} {R : Type u'} [Quiver Q] [Quiver R] (k : Type w) [CommSemiring k] [Finite Q] [Finite R] (φ : Q ⥤q R) (hφ : Function.Bijective φ.obj) (x : Quiver.TotalPath Q) : (mapAlgHom k φ hφ) (ofPath x) = ofPath (φ.mapTotalPath x)

The induced homomorphism sends the basis element of an indexed path to the basis element of the pushed-forward path.

@[simp]

theorem TauCeti.PathAlgebra.mapAlgHom_single {Q : Type u} {R : Type u'} [Quiver Q] [Quiver R] (k : Type w) [CommSemiring k] [Finite Q] [Finite R] (φ : Q ⥤q R) (hφ : Function.Bijective φ.obj) (x : Quiver.TotalPath Q) (c : k) : (mapAlgHom k φ hφ) (single x c) = single (φ.mapTotalPath x) c

The induced homomorphism sends a scalar multiple of a basis path to the same scalar multiple of the pushed-forward basis path.

@[simp]

theorem TauCeti.PathAlgebra.mapAlgHom_vertexIdempotent {Q : Type u} {R : Type u'} [Quiver Q] [Quiver R] (k : Type w) [CommSemiring k] [Finite Q] [Finite R] (φ : Q ⥤q R) (hφ : Function.Bijective φ.obj) (v : Q) : (mapAlgHom k φ hφ) (vertexIdempotent k v) = vertexIdempotent k (φ.obj v)

The induced homomorphism sends the idempotent of a vertex to the idempotent of the image vertex.

theorem TauCeti.PathAlgebra.mapAlgHom_ofArrow {Q : Type u} {R : Type u'} [Quiver Q] [Quiver R] (k : Type w) [CommSemiring k] [Finite Q] [Finite R] (φ : Q ⥤q R) (hφ : Function.Bijective φ.obj) {a b : Q} (e : a ⟶ b) : (mapAlgHom k φ hφ) (ofArrow e) = ofArrow (φ.map e)

Pushing an arrow along mapAlgHom carries it to the image arrow. Deliberately not a simp lemma, TauCeti.PathAlgebra.ofArrow_eq_ofPath already rewriting its left-hand side.

theorem TauCeti.PathAlgebra.mapAlgHom_mem_gradeBy {Q : Type u} {R : Type u'} [Quiver Q] [Quiver R] (k : Type w) [CommSemiring k] [Finite Q] [Finite R] {M : Type u_1} [AddCommMonoid M] (φ : Q ⥤q R) (hφ : Function.Bijective φ.obj) (wt : {a b : R} → (a ⟶ b) → M) {m : M} {x : pathAlgebra k Q} (hx : x ∈ gradeBy k (fun {a b : Q} (e : a ⟶ b) => wt (φ.map e)) m) : (mapAlgHom k φ hφ) x ∈ gradeBy k (fun {a b : R} => wt) m

A prefunctor-induced algebra map is graded for the pulled-back arrow weight. If an element is homogeneous for the weight obtained by pulling wt back along φ, then its image is homogeneous of the same weight.

theorem TauCeti.PathAlgebra.mapAlgHom_congr {Q : Type u} {R : Type u'} [Quiver Q] [Quiver R] (k : Type w) [CommSemiring k] [Finite Q] [Finite R] {φ φ' : Q ⥤q R} (h : φ = φ') (hφ : Function.Bijective φ.obj) (hφ' : Function.Bijective φ'.obj) : mapAlgHom k φ hφ = mapAlgHom k φ' hφ'

Equal prefunctors induce equal homomorphisms; the bijectivity hypotheses are propositions, so they need not be compared.

@[simp]

theorem TauCeti.PathAlgebra.mapAlgHom_id {Q : Type u} [Quiver Q] (k : Type w) [CommSemiring k] [Finite Q] : mapAlgHom k (𝟭q Q) ⋯ = AlgHom.id k (pathAlgebra k Q)

The identity prefunctor induces the identity.

theorem TauCeti.PathAlgebra.mapAlgHom_comp {Q : Type u} {R : Type u'} {S : Type u''} [Quiver Q] [Quiver R] [Quiver S] (k : Type w) [CommSemiring k] [Finite Q] [Finite R] [Finite S] (φ : Q ⥤q R) (ψ : R ⥤q S) (hφ : Function.Bijective φ.obj) (hψ : Function.Bijective ψ.obj) : mapAlgHom k (φ ⋙q ψ) ⋯ = (mapAlgHom k ψ hψ).comp (mapAlgHom k φ hφ)

Composition of prefunctors induces composition. The bijectivity of the composite is that of the two factors.

noncomputable def TauCeti.PathAlgebra.mapAlgEquiv {Q : Type u} {R : Type u'} [Quiver Q] [Quiver R] (k : Type w) [CommSemiring k] [Finite Q] [Finite R] (φ : Q ⥤q R) (ψ : R ⥤q Q) (hφψ : φ ⋙q ψ = 𝟭q Q) (hψφ : ψ ⋙q φ = 𝟭q R) : pathAlgebra k Q ≃ₐ[k] pathAlgebra k R

The algebra isomorphism of path algebras induced by an isomorphism of quivers, presented as a pair of mutually inverse prefunctors.

Equations

• TauCeti.PathAlgebra.mapAlgEquiv k φ ψ hφψ hψφ = AlgEquiv.ofAlgHom (TauCeti.PathAlgebra.mapAlgHom k φ ⋯) (TauCeti.PathAlgebra.mapAlgHom k ψ ⋯) ⋯ ⋯

@[simp]

theorem TauCeti.PathAlgebra.mapAlgEquiv_apply {Q : Type u} {R : Type u'} [Quiver Q] [Quiver R] (k : Type w) [CommSemiring k] [Finite Q] [Finite R] (φ : Q ⥤q R) (ψ : R ⥤q Q) (hφψ : φ ⋙q ψ = 𝟭q Q) (hψφ : ψ ⋙q φ = 𝟭q R) (x : pathAlgebra k Q) : (mapAlgEquiv k φ ψ hφψ hψφ) x = (mapAlgHom k φ ⋯) x

The induced isomorphism acts as the homomorphism induced by the forward prefunctor.

theorem TauCeti.PathAlgebra.mapAlgEquiv_symm_apply {Q : Type u} {R : Type u'} [Quiver Q] [Quiver R] (k : Type w) [CommSemiring k] [Finite Q] [Finite R] (φ : Q ⥤q R) (ψ : R ⥤q Q) (hφψ : φ ⋙q ψ = 𝟭q Q) (hψφ : ψ ⋙q φ = 𝟭q R) (y : pathAlgebra k R) : (mapAlgEquiv k φ ψ hφψ hψφ).symm y = (mapAlgHom k ψ ⋯) y

The inverse of the induced isomorphism acts as the homomorphism induced by the inverse prefunctor. Deliberately not a simp lemma: TauCeti.PathAlgebra.mapAlgEquiv_symm followed by TauCeti.PathAlgebra.mapAlgEquiv_apply already rewrites its left-hand side, and simpNF rejects the pair.

theorem TauCeti.PathAlgebra.mapAlgEquiv_congr {Q : Type u} {R : Type u'} [Quiver Q] [Quiver R] (k : Type w) [CommSemiring k] [Finite Q] [Finite R] {φ φ' : Q ⥤q R} {ψ ψ' : R ⥤q Q} (hφ : φ = φ') (hψ : ψ = ψ') (hφψ : φ ⋙q ψ = 𝟭q Q) (hψφ : ψ ⋙q φ = 𝟭q R) (hφψ' : φ' ⋙q ψ' = 𝟭q Q) (hψφ' : ψ' ⋙q φ' = 𝟭q R) : mapAlgEquiv k φ ψ hφψ hψφ = mapAlgEquiv k φ' ψ' hφψ' hψφ'

Equal pairs of prefunctors induce equal isomorphisms; the coherence hypotheses are propositions, so they need not be compared.

@[simp]

theorem TauCeti.PathAlgebra.mapAlgEquiv_id {Q : Type u} [Quiver Q] (k : Type w) [CommSemiring k] [Finite Q] : mapAlgEquiv k (𝟭q Q) (𝟭q Q) ⋯ ⋯ = AlgEquiv.refl

The identity prefunctor induces the identity isomorphism.

@[simp]

theorem TauCeti.PathAlgebra.mapAlgEquiv_symm {Q : Type u} {R : Type u'} [Quiver Q] [Quiver R] (k : Type w) [CommSemiring k] [Finite Q] [Finite R] (φ : Q ⥤q R) (ψ : R ⥤q Q) (hφψ : φ ⋙q ψ = 𝟭q Q) (hψφ : ψ ⋙q φ = 𝟭q R) : (mapAlgEquiv k φ ψ hφψ hψφ).symm = mapAlgEquiv k ψ φ hψφ hφψ

The inverse isomorphism is the one induced by the reversed pair.

theorem TauCeti.PathAlgebra.mapAlgEquiv_comp {Q : Type u} {R : Type u'} {S : Type u''} [Quiver Q] [Quiver R] [Quiver S] (k : Type w) [CommSemiring k] [Finite Q] [Finite R] [Finite S] (φ : Q ⥤q R) (ψ : R ⥤q Q) (φ' : R ⥤q S) (ψ' : S ⥤q R) (hφψ : φ ⋙q ψ = 𝟭q Q) (hψφ : ψ ⋙q φ = 𝟭q R) (hφψ' : φ' ⋙q ψ' = 𝟭q R) (hψφ' : ψ' ⋙q φ' = 𝟭q S) : mapAlgEquiv k (φ ⋙q φ') (ψ' ⋙q ψ) ⋯ ⋯ = (mapAlgEquiv k φ ψ hφψ hψφ).trans (mapAlgEquiv k φ' ψ' hφψ' hψφ')

Composition of prefunctors induces composition of the isomorphisms. The two inverse laws of the composite pair are those of the two factor pairs, by Prefunctor.comp_comp_comp_eq_id.