Corners of path-algebra images #
Under a surjective algebra homomorphism, a submodule containing the images of every path
from a to b contains the corner cut out by the images of their vertex idempotents.
This turns reductions of individual paths into spanning statements for corners of relation
quotients. No finiteness assumption on the quiver or its paths is needed.
The argument is extracted from the type-A corner construction in
TauCeti.RepresentationTheory.Quiver.Preprojective.ADE.TypeA.NormalForm.
theorem
TauCeti.PathAlgebra.cornerSubmodule_le_of_ofPath_mem
{k : Type u}
[CommSemiring k]
{Q : Type v}
[Quiver Q]
{A : Type z}
[Semiring A]
[Algebra k A]
(φ : pathAlgebra k Q →ₙₐ[k] A)
(hφ : Function.Surjective ⇑φ)
(a b : Q)
(M : Submodule k A)
(hp : ∀ (p : Quiver.Path a b), φ (ofPath ⟨a, ⟨b, p⟩⟩) ∈ M)
:
A submodule containing all path images from a to b contains the corresponding corner
of any surjective image of the path algebra.