String boundary squares in the finite module category

The explicit string-module boundary complexes are first proved exact in the ambient functor category. This file bundles their maps in the category of finite-dimensional linear modules and reflects exactness along the faithful inclusion. Thus the chosen middle term is a literal binary biproduct in the finite module category, as required by the almost-split argument.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.finiteRightModuleHom {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} [Fintype Q] {C D : Word R} (hmono : IsMonomial R) (f : C.rightModule hmono ⟶ D.rightModule hmono) : C.finiteRightModule hmono ⟶ D.finiteRightModule hmono

Bundle a morphism between raw string modules in the finite-dimensional linear-module category.

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.finiteRightModuleHom_hom_hom {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} [Fintype Q] {C D : Word R} (hmono : IsMonomial R) (f : C.rightModule hmono ⟶ D.rightModule hmono) : (finiteRightModuleHom hmono f).hom.hom = f

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.finiteRightModule_binaryBiproductShortComplex_exact {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} [Fintype Q] {X A B Y : Word R} (hmono : IsMonomial R) (fA : X.rightModule hmono ⟶ A.rightModule hmono) (fB : X.rightModule hmono ⟶ B.rightModule hmono) (gA : A.rightModule hmono ⟶ Y.rightModule hmono) (gB : B.rightModule hmono ⟶ Y.rightModule hmono) (hzero : CategoryTheory.CategoryStruct.comp fA gA + CategoryTheory.CategoryStruct.comp fB gB = 0) (hexact : (CategoryTheory.binaryBiproductShortComplex fA fB gA gB hzero).Exact) : (CategoryTheory.binaryBiproductShortComplex (finiteRightModuleHom hmono fA) (finiteRightModuleHom hmono fB) (finiteRightModuleHom hmono gA) (finiteRightModuleHom hmono gB) ⋯).Exact

Exactness of a binary-biproduct complex of raw string modules lifts to the corresponding complex in the finite-dimensional module category.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.PositiveBoundarySquare.finiteShortComplex {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} [Fintype Q] {C : Word R} (square : C.PositiveBoundarySquare) (hmono : IsMonomial R) : CategoryTheory.ShortComplex (CoveringHom.FiniteDimensionalModuleCategory k)

The positive boundary complex bundled in the finite-dimensional module category.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.PositiveBoundarySquare.finiteShortComplex_exact {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} [Fintype Q] {C : Word R} (square : C.PositiveBoundarySquare) (hmono : IsMonomial R) : (square.finiteShortComplex hmono).Exact

The finite-dimensional positive boundary complex is exact.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.MixedBoundarySquare.finiteShortComplex {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} [Fintype Q] {D : Word R} (square : D.MixedBoundarySquare) (hmono : IsMonomial R) : CategoryTheory.ShortComplex (CoveringHom.FiniteDimensionalModuleCategory k)

The mixed cohook-hook boundary complex bundled in the finite-dimensional module category.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.MixedBoundarySquare.finiteShortComplex_exact {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} [Fintype Q] {D : Word R} (square : D.MixedBoundarySquare) (hmono : IsMonomial R) : (square.finiteShortComplex hmono).Exact

The finite-dimensional mixed boundary complex is exact.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.NegativeBoundarySquare.finiteShortComplex {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} [Fintype Q] {D : Word R} (square : D.NegativeBoundarySquare) (hmono : IsMonomial R) : CategoryTheory.ShortComplex (CoveringHom.FiniteDimensionalModuleCategory k)

The double-cohook boundary complex bundled in the finite-dimensional module category.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.NegativeBoundarySquare.finiteShortComplex_exact {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} [Fintype Q] {D : Word R} (square : D.NegativeBoundarySquare) (hmono : IsMonomial R) : (square.finiteShortComplex hmono).Exact

The finite-dimensional double-cohook boundary complex is exact.