Retraction of an arrow-branch inclusion

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.arrowBranchProjectionAlgebraFiniteDimensional {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : StringPresentation k A Q) : FiniteDimensional k P.quotientCategoryAlgebra

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.arrowBranchProjectionAlgebraOppositeIsNoetherian {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : StringPresentation k A Q) : IsNoetherianRing P.quotientCategoryAlgebraᵐᵒᵖ

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.arrowBranchRadicalInclusion_projection {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : StringPresentation k A Q) {y : Q} (a : DisplayedIncomingArrow y) : P.arrowBranchRadicalProjectionLinearMap a ∘ₗ P.arrowBranchRadicalInclusionLinearMap a = LinearMap.id