Peak-wedge projectivity under algebra-skeleton transport

The quotient-category algebra skeleton is classified by reverse coefficient duals of literal right-string modules. This file records the resulting projective/injective reversal explicitly: a projective literal string gives an injective object of the right-module algebra skeleton. In particular, the strict overlapping-cohook boundary is injective after transport.

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.peakWedgeTransportAlgebraFiniteDimensional {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.peakWedgeTransportAlgebraOppositeNoetherian {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ᵐᵒᵖ

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.algebraSkeletonObj_injective_iff_literalString_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) (S : P.ArrowPolarization) (T : RightModule.FiniteIndecomposableSkeleton k P.quotientCategoryAlgebra) (i : Fin T.n) : have L := (P.algebraSkeletonDetectorIndex S T i).endpointWord.word.finiteRightModule ⋯; CategoryTheory.Injective (T.fgObj i) ↔ CategoryTheory.Projective L

An algebra-skeleton object is injective exactly when its selected literal right-string representative is projective.

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.algebraSkeletonObj_injective_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) (S : P.ArrowPolarization) (T : RightModule.FiniteIndecomposableSkeleton k P.quotientCategoryAlgebra) (i : Fin T.n) {L D : StringWord.Word P.relations} (leftDeletion : (P.algebraSkeletonDetectorIndex S T i).endpointWord.word.LeftCohookDeletion D) (rightDeletion : (P.algebraSkeletonDetectorIndex S T i).endpointWord.word.CohookDeletion L) (hoverlap : StringWord.Word.length P.relations (P.algebraSkeletonDetectorIndex S T i).endpointWord.word < leftDeletion.steps + rightDeletion.steps) : CategoryTheory.Injective (T.fgObj i)

A strict overlap of the two maximal cohook deletions makes the corresponding quotient-algebra skeleton object injective.