Composition of string coefficient-component maps

Composition is matrix multiplication in the position bases. This file records that formula at the coefficient level and specializes it to the component-indicator basis. It is the algebraic interface for the remaining proper-overlap nilpotence argument.

@[instance_reducible]

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.positionAtFintype {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) (x : Q) : Fintype (C.PositionAt x)

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.morphismCoefficient_comp {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C D E : Word R) (hC hD hE : IsMonomial R) (f : C.rightModule hC ⟶ D.rightModule hD) (g : D.rightModule hD ⟶ E.rightModule hE) {x : Q} (i : C.PositionAt x) (l : E.PositionAt x) : C.morphismCoefficient E hC hE (CategoryTheory.CategoryStruct.comp f g) i l = ∑ j : D.PositionAt x, C.morphismCoefficient D hC hD f i j * D.morphismCoefficient E hD hE g j l

Coefficients of a composite are obtained by summing over the intermediate word positions above the displayed vertex.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.morphismCoefficientAt_comp {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C D E : Word R) (hC hD hE : IsMonomial R) (f : C.rightModule hC ⟶ D.rightModule hD) (g : D.rightModule hD ⟶ E.rightModule hE) (p : C.MorphismCoefficientPosition E) : C.morphismCoefficientAt E hC hE (CategoryTheory.CategoryStruct.comp f g) p = ∑ j : D.PositionAt p.fst, C.morphismCoefficientAt D hC hD f ⟨p.fst, (p.snd.1, j)⟩ * D.morphismCoefficientAt E hD hE g ⟨p.fst, (j, p.snd.2)⟩

The position-indexed form of the coefficient composition formula.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.morphismCoefficientAt_boundaryFreeComponentMap_comp {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C D E : Word R) (hC hD hE : IsMonomial R) (first : C.BoundaryFreeMorphismCoefficientComponent D) (second : D.BoundaryFreeMorphismCoefficientComponent E) (p : C.MorphismCoefficientPosition E) : C.morphismCoefficientAt E hC hE (CategoryTheory.CategoryStruct.comp (C.boundaryFreeMorphismCoefficientComponentMap D hC hD first) (D.boundaryFreeMorphismCoefficientComponentMap E hD hE second)) p = ∑ j : D.PositionAt p.fst, C.coefficientComponentIndicator D (↑first).representative ⟨p.fst, (p.snd.1, j)⟩ * D.coefficientComponentIndicator E (↑second).representative ⟨p.fst, (j, p.snd.2)⟩

Composition of two graph-component basis maps is the convolution of their zero-one component indicators over intermediate word positions.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.boundaryFreeMorphismCoefficientComponentCompositionCoefficient {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C D E : Word R) (hC hD hE : IsMonomial R) (first : C.BoundaryFreeMorphismCoefficientComponent D) (second : D.BoundaryFreeMorphismCoefficientComponent E) (output : C.BoundaryFreeMorphismCoefficientComponent E) : k

The structure coefficient of the product of two graph-component basis maps in a third graph-component basis direction.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.boundaryFreeMorphismCoefficientComponentCompositionCoefficient_eq {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C D E : Word R) (hC hD hE : IsMonomial R) (first : C.BoundaryFreeMorphismCoefficientComponent D) (second : D.BoundaryFreeMorphismCoefficientComponent E) (output : C.BoundaryFreeMorphismCoefficientComponent E) : C.boundaryFreeMorphismCoefficientComponentCompositionCoefficient D E hC hD hE first second output = ∑ j : D.PositionAt (↑output).representative.fst, C.coefficientComponentIndicator D (↑first).representative ⟨(↑output).representative.fst, ((↑output).representative.snd.1, j)⟩ * D.coefficientComponentIndicator E (↑second).representative ⟨(↑output).representative.fst, (j, (↑output).representative.snd.2)⟩

A structure coefficient counts, in the coefficient field, intermediate positions simultaneously supported by the two component relations.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.boundaryFreeMorphismCoefficientComponentMap_comp_eq_sum {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C D E : Word R) (hC hD hE : IsMonomial R) (first : C.BoundaryFreeMorphismCoefficientComponent D) (second : D.BoundaryFreeMorphismCoefficientComponent E) : CategoryTheory.CategoryStruct.comp (C.boundaryFreeMorphismCoefficientComponentMap D hC hD first) (D.boundaryFreeMorphismCoefficientComponentMap E hD hE second) = ∑ output : C.BoundaryFreeMorphismCoefficientComponent E, C.boundaryFreeMorphismCoefficientComponentCompositionCoefficient D E hC hD hE first second output • C.boundaryFreeMorphismCoefficientComponentMap E hC hE output

The graph-component multiplication table reconstructs the composite of two basis maps.