Spanning string morphisms by coefficient-component maps

The finite coefficient constraint graph partitions all possible matrix coefficients into equality components. This file chooses one representative per component and decomposes every actual string-module morphism as the sum of its component coefficient times the corresponding component-indicator map. Components meeting a zero boundary contribute zero automatically.

def MagnitudeConjecture.BoundQuiver.StringWord.Word.MorphismCoefficientComponent {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C D : Word R) : Type u

Equality components of the matched-step coefficient graph.

def MagnitudeConjecture.BoundQuiver.StringWord.Word.morphismCoefficientComponentOf {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C D : Word R) (p : C.MorphismCoefficientPosition D) : C.MorphismCoefficientComponent D

The component containing a coefficient position.

instance MagnitudeConjecture.BoundQuiver.StringWord.Word.morphismCoefficientComponent_finite {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C D : Word R) : Finite (C.MorphismCoefficientComponent D)

@[instance_reducible]

noncomputable instance MagnitudeConjecture.BoundQuiver.StringWord.Word.morphismCoefficientComponent_fintype {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C D : Word R) : Fintype (C.MorphismCoefficientComponent D)

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.MorphismCoefficientComponent.representative {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (component : C.MorphismCoefficientComponent D) : C.MorphismCoefficientPosition D

A chosen coefficient position in a component.

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.morphismCoefficientComponentOf_representative {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C D : Word R) (component : C.MorphismCoefficientComponent D) : C.morphismCoefficientComponentOf D component.representative = component

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.morphismCoefficientComponentOf_eq_iff {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C D : Word R) (p q : C.MorphismCoefficientPosition D) : C.morphismCoefficientComponentOf D p = C.morphismCoefficientComponentOf D q ↔ Relation.EqvGen (C.MorphismCoefficientStep D) p q

Equality of component classes is precisely generated matched-step equivalence.

def MagnitudeConjecture.BoundQuiver.StringWord.Word.BoundaryFreeMorphismCoefficientComponent {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C D : Word R) : Type u

The coefficient components which carry no unmatched zero boundary.

instance MagnitudeConjecture.BoundQuiver.StringWord.Word.boundaryFreeMorphismCoefficientComponent_finite {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C D : Word R) : Finite (C.BoundaryFreeMorphismCoefficientComponent D)

@[instance_reducible]

noncomputable instance MagnitudeConjecture.BoundQuiver.StringWord.Word.boundaryFreeMorphismCoefficientComponent_fintype {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C D : Word R) : Fintype (C.BoundaryFreeMorphismCoefficientComponent D)

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.representative_eqv_iff {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C D : Word R) (first second : C.MorphismCoefficientComponent D) : Relation.EqvGen (C.MorphismCoefficientStep D) first.representative second.representative ↔ first = second

Two chosen component representatives are matched-step equivalent exactly when their components are equal.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.boundaryFreeMorphismCoefficientComponentMap {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C D : Word R) (hC hD : IsMonomial R) (component : C.BoundaryFreeMorphismCoefficientComponent D) : C.rightModule hC ⟶ D.rightModule hD

The module map indexed by a boundary-free coefficient component.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.morphismCoefficientAt_boundaryFreeComponentMap {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C D : Word R) (hC hD : IsMonomial R) (component : C.BoundaryFreeMorphismCoefficientComponent D) (p : C.MorphismCoefficientPosition D) : C.morphismCoefficientAt D hC hD (C.boundaryFreeMorphismCoefficientComponentMap D hC hD component) p = C.coefficientComponentIndicator D (↑component).representative p

The coefficient matrix of a boundary-free component map is its component indicator.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.morphismCoefficientComponentSummand {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C D : Word R) (hC hD : IsMonomial R) (f : C.rightModule hC ⟶ D.rightModule hD) (component : C.MorphismCoefficientComponent D) : C.rightModule hC ⟶ D.rightModule hD

The contribution of one coefficient component to an actual morphism. Boundary components have zero coefficient and contribute the zero map; otherwise the chosen coefficient scales the component-indicator map.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.morphismCoefficientAt_componentSummand_eq {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C D : Word R) (hC hD : IsMonomial R) (f : C.rightModule hC ⟶ D.rightModule hD) (component : C.MorphismCoefficientComponent D) (p : C.MorphismCoefficientPosition D) (hp : C.morphismCoefficientComponentOf D p = component) : C.morphismCoefficientAt D hC hD (C.morphismCoefficientComponentSummand D hC hD f component) p = C.morphismCoefficientAt D hC hD f p

On its own component, a summand recovers the coefficient of the original morphism.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.morphismCoefficientAt_componentSummand_eq_zero {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C D : Word R) (hC hD : IsMonomial R) (f : C.rightModule hC ⟶ D.rightModule hD) (component : C.MorphismCoefficientComponent D) (p : C.MorphismCoefficientPosition D) (hp : C.morphismCoefficientComponentOf D p ≠ component) : C.morphismCoefficientAt D hC hD (C.morphismCoefficientComponentSummand D hC hD f component) p = 0

Away from its own component, a summand has zero coefficient.

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

Sum the contributions of all coefficient components of a morphism.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.morphismCoefficientAt_componentSum {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C D : Word R) (hC hD : IsMonomial R) (f : C.rightModule hC ⟶ D.rightModule hD) (p : C.MorphismCoefficientPosition D) : C.morphismCoefficientAt D hC hD (C.morphismCoefficientComponentSum D hC hD f) p = C.morphismCoefficientAt D hC hD f p

The component sum has the same coefficient matrix as the original morphism.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.morphismCoefficientComponentSum_eq {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C D : Word R) (hC hD : IsMonomial R) (f : C.rightModule hC ⟶ D.rightModule hD) : C.morphismCoefficientComponentSum D hC hD f = f

Every morphism between two string modules is the sum of its nonzero boundary-free coefficient-component maps.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.boundaryFreeMorphismCoefficientComponentMap_linearIndependent {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C D : Word R) (hC hD : IsMonomial R) : LinearIndependent k (C.boundaryFreeMorphismCoefficientComponentMap D hC hD)

Boundary-free component maps are linearly independent.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.mem_span_boundaryFreeMorphismCoefficientComponentMap {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C D : Word R) (hC hD : IsMonomial R) (f : C.rightModule hC ⟶ D.rightModule hD) : f ∈ Submodule.span k (Set.range (C.boundaryFreeMorphismCoefficientComponentMap D hC hD))

Every string-module morphism lies in the span of the boundary-free component maps.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.span_boundaryFreeMorphismCoefficientComponentMap {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C D : Word R) (hC hD : IsMonomial R) : Submodule.span k (Set.range (C.boundaryFreeMorphismCoefficientComponentMap D hC hD)) = ⊤

Boundary-free coefficient-component maps span the whole Hom-space.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.boundaryFreeMorphismCoefficientBasis {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C D : Word R) (hC hD : IsMonomial R) : Module.Basis (C.BoundaryFreeMorphismCoefficientComponent D) k (C.rightModule hC ⟶ D.rightModule hD)

The boundary-free equality components give a basis of the Hom-space between two string modules.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.boundaryFreeMorphismCoefficientBasis_repr_apply {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C D : Word R) (hC hD : IsMonomial R) (f : C.rightModule hC ⟶ D.rightModule hD) (component : C.BoundaryFreeMorphismCoefficientComponent D) : ((C.boundaryFreeMorphismCoefficientBasis D hC hD).repr f) component = C.morphismCoefficientAt D hC hD f (↑component).representative

The coordinate of a morphism in the graph-component basis is its matrix coefficient at the chosen representative of that component.