Peak-wedge string modules are representable

For a two-sided maximal peak wedge, evaluation at the common peak position identifies the covariant representable on the opposite bound-quiver category with the literal right-string module. The variance is explicit: a displayed path from the peak becomes a morphism out of the opposite peak object.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.PeakWedge.peakRepresentable {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) {C : Word P.relations} (W : C.PeakWedge) : CoveringHom.FiniteDimensionalModuleCategory k

The finite representable at the common peak, in the literal category of right modules on the opposite bound quiver.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.PeakWedge.peakRepresentableHom {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) {C : Word P.relations} (W : C.PeakWedge) : peakRepresentable P W ⟶ C.finiteRightModule ⋯

Evaluation at the peak position gives the canonical map from the peak representable to the string module.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.PeakWedge.peakRepresentableBasis {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) {C : Word P.relations} (W : C.PeakWedge) (y : Q) : Module.Basis (SurvivingPath P.relations W.peak y) k ↑((peakRepresentable P W).obj.obj.obj (Opposite.op (obj P.relations y)))

The surviving-path basis of one component of the peak representable.

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.PeakWedge.peakRepresentableBasis_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) {C : Word P.relations} (W : C.PeakWedge) (y : Q) (p : SurvivingPath P.relations W.peak y) : (peakRepresentableBasis P W y) p = (pathMap P.relations ↑p).op

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.PeakWedge.peakRepresentableHom_app_basis {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) {C : Word P.relations} (W : C.PeakWedge) (hleft : 0 < W.leftArm.length) (hright : 0 < W.rightArm.length) (y : Q) (p : SurvivingPath P.relations W.peak y) : (ModuleCat.Hom.hom ((peakRepresentableHom P W).hom.hom.app (Opposite.op (obj P.relations y)))) ((peakRepresentableBasis P W y) p) = Finsupp.single (survivingPathTargetPosition P.toSpecialBiserialPresentation W hleft hright y p) 1

On surviving-path basis vectors, peak evaluation is the corresponding position-basis vector.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.PeakWedge.peakRepresentableComponentLinearEquiv {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) {C : Word P.relations} (W : C.PeakWedge) (hleft : 0 < W.leftArm.length) (hright : 0 < W.rightArm.length) (y : Q) : ↑((peakRepresentable P W).obj.obj.obj (Opposite.op (obj P.relations y))) ≃ₗ[k] C.Space y

The componentwise linear equivalence induced by the surviving-path and word-position bases.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.PeakWedge.peakRepresentableHom_app_eq {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) {C : Word P.relations} (W : C.PeakWedge) (hleft : 0 < W.leftArm.length) (hright : 0 < W.rightArm.length) (y : Q) : ModuleCat.Hom.hom ((peakRepresentableHom P W).hom.hom.app (Opposite.op (obj P.relations y))) = ↑(peakRepresentableComponentLinearEquiv P W hleft hright y)

Each component of peak evaluation is the basis equivalence above.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.PeakWedge.peakRepresentableHom_isIso {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) {C : Word P.relations} (W : C.PeakWedge) (hleft : 0 < W.leftArm.length) (hright : 0 < W.rightArm.length) : CategoryTheory.IsIso (peakRepresentableHom P W)

Peak evaluation is an isomorphism of finite-dimensional modules on the opposite bound-quiver category.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.PeakWedge.peakRepresentableIso {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) {C : Word P.relations} (W : C.PeakWedge) (hleft : 0 < W.leftArm.length) (hright : 0 < W.rightArm.length) : peakRepresentable P W ≅ C.finiteRightModule ⋯

The literal right-string module of a two-sided maximal peak wedge is the finite representable at its common peak.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.PeakWedge.finiteRightModule_projective {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) {C : Word P.relations} (W : C.PeakWedge) (hleft : 0 < W.leftArm.length) (hright : 0 < W.rightArm.length) : CategoryTheory.Projective (C.finiteRightModule ⋯)

A two-sided maximal peak-wedge right-string module is projective.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.finiteRightModule_projective_of_overlappingCohookDeletions {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) {C L D : Word P.relations} (leftDeletion : C.LeftCohookDeletion D) (rightDeletion : C.CohookDeletion L) (hoverlap : length P.relations C < leftDeletion.steps + rightDeletion.steps) : CategoryTheory.Projective (C.finiteRightModule ⋯)

The literal right-string module at the exceptional overlapping-cohook boundary is projective.