Underlying functions of the radical and branch inclusions

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.representedVertexRadicalInclusion_apply {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) (z : ↑(P.representedVertexRadicalFGObj y)) : (ModuleCat.Hom.hom (P.representedVertexRadicalInclusion y).hom) z = ↑z

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.arrowBranchRadicalInclusion_apply_coe {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) (z : ↑(P.incomingArrowRangeFGObj a)) : ↑((ModuleCat.Hom.hom (P.arrowBranchRadicalInclusion a).hom) z) = ↑z

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.arrowBranchRadicalInclusionLinearMap_apply_coe {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) (z : ↥(P.representedArrowLinearMap a.snd).range) : ↑((P.arrowBranchRadicalInclusionLinearMap a) z) = ↑z