Families on the complement of an incoming arrow

@[reducible, inline]

abbrev MagnitudeConjecture.BoundQuiver.StringPresentation.OtherIncomingArrow {Q : Type u} [Quiver Q] {y : Q} (a : DisplayedIncomingArrow y) : Type u

Incoming displayed arrows other than a fixed marked arrow.

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.otherIncomingArrow_subsingleton {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) : Subsingleton (OtherIncomingArrow a)

At a special-biserial vertex, deleting one marked incoming arrow leaves at most one incoming arrow.

noncomputable def MagnitudeConjecture.BoundQuiver.StringPresentation.otherIncomingFamilyInsertion {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) : ((b : OtherIncomingArrow a) → ↑(P.incomingArrowRangeFGObj ↑b)) →ₗ[P.quotientCategoryAlgebraᵐᵒᵖ] (b : DisplayedIncomingArrow y) → ↑(P.incomingArrowRangeFGObj b)

Extend the incoming-arrow family by zero on the marked branch.

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.otherIncomingFamilyInsertion_apply_self {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) (g : (b : OtherIncomingArrow a) → ↑(P.incomingArrowRangeFGObj ↑b)) : (P.otherIncomingFamilyInsertion a) g a = 0

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.otherIncomingFamilyInsertion_apply_other {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) (g : (b : OtherIncomingArrow a) → ↑(P.incomingArrowRangeFGObj ↑b)) (b : OtherIncomingArrow a) : (P.otherIncomingFamilyInsertion a) g ↑b = g b