Extracting graph components from string-map factorizations

A nonzero coefficient of a composite selects an intermediate position where both factor coefficients are nonzero. The two coefficient components through that position have product coefficient exactly one: partial-bijection uniqueness leaves no second intermediate position and hence no characteristic-dependent cancellation. Full input or output support of a selected output component then transfers to the corresponding factor component.

@[instance_reducible]

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.factorizationPositionAtFintype {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.exists_intermediate_of_comp_coefficient_ne_zero {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) (hne : C.morphismCoefficientAt E hC hE (CategoryTheory.CategoryStruct.comp f g) p ≠ 0) : ∃ (j : D.PositionAt p.fst), C.morphismCoefficientAt D hC hD f ⟨p.fst, (p.snd.1, j)⟩ ≠ 0 ∧ D.morphismCoefficientAt E hD hE g ⟨p.fst, (j, p.snd.2)⟩ ≠ 0

A nonzero coefficient of an arbitrary composite has an intermediate position at which both factor coefficients are nonzero.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.morphismCoefficientAt_componentMaps_comp_eq_one_of_intermediate {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) {x : Q} (i : C.PositionAt x) (j : D.PositionAt x) (l : E.PositionAt x) (hfirst : Relation.EqvGen (C.MorphismCoefficientStep D) (↑first).representative ⟨x, (i, j)⟩) (hsecond : Relation.EqvGen (D.MorphismCoefficientStep E) (↑second).representative ⟨x, (j, l)⟩) : C.morphismCoefficientAt E hC hE (CategoryTheory.CategoryStruct.comp (C.boundaryFreeMorphismCoefficientComponentMap D hC hD first) (D.boundaryFreeMorphismCoefficientComponentMap E hD hE second)) ⟨x, (i, l)⟩ = 1

Component basis maps whose supports meet at one intermediate position have composite coefficient one at the induced outside pair.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.exists_intermediate_of_componentMaps_comp_coefficient_ne_zero {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) (hne : C.morphismCoefficientAt E hC hE (CategoryTheory.CategoryStruct.comp (C.boundaryFreeMorphismCoefficientComponentMap D hC hD first) (D.boundaryFreeMorphismCoefficientComponentMap E hD hE second)) p ≠ 0) : ∃ (j : D.PositionAt p.fst), Relation.EqvGen (C.MorphismCoefficientStep D) (↑first).representative ⟨p.fst, (p.snd.1, j)⟩ ∧ Relation.EqvGen (D.MorphismCoefficientStep E) (↑second).representative ⟨p.fst, (j, p.snd.2)⟩

A nonzero coefficient of a product of two graph-component basis maps has an intermediate position supported by both components.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.exists_component_pair_of_comp_coefficient_ne_zero {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) (hne : C.morphismCoefficientAt E hC hE (CategoryTheory.CategoryStruct.comp f g) p ≠ 0) : ∃ (first : C.BoundaryFreeMorphismCoefficientComponent D) (second : D.BoundaryFreeMorphismCoefficientComponent E), C.morphismCoefficientAt D hC hD f (↑first).representative ≠ 0 ∧ D.morphismCoefficientAt E hD hE g (↑second).representative ≠ 0 ∧ C.morphismCoefficientAt E hC hE (CategoryTheory.CategoryStruct.comp (C.boundaryFreeMorphismCoefficientComponentMap D hC hD first) (D.boundaryFreeMorphismCoefficientComponentMap E hD hE second)) p = 1

From a nonzero coefficient of an arbitrary composite, select one component from each factor whose basis-map product has coefficient exactly one at the same outside position.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.BoundaryFreeMorphismCoefficientComponent.HasFullInputSupport.first_of_comp {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C D E : Word R) (hC hD hE : IsMonomial R) (output : C.BoundaryFreeMorphismCoefficientComponent E) (houtput : output.HasFullInputSupport) (first : C.BoundaryFreeMorphismCoefficientComponent D) (second : D.BoundaryFreeMorphismCoefficientComponent E) (hne : C.morphismCoefficientAt E hC hE (CategoryTheory.CategoryStruct.comp (C.boundaryFreeMorphismCoefficientComponentMap D hC hD first) (D.boundaryFreeMorphismCoefficientComponentMap E hD hE second)) (↑output).representative ≠ 0) : first.HasFullInputSupport

Full source support of an output component transfers to the first factor component whenever their product is nonzero on the output component.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.BoundaryFreeMorphismCoefficientComponent.HasFullOutputSupport.second_of_comp {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C D E : Word R) (hC hD hE : IsMonomial R) (output : C.BoundaryFreeMorphismCoefficientComponent E) (houtput : output.HasFullOutputSupport) (first : C.BoundaryFreeMorphismCoefficientComponent D) (second : D.BoundaryFreeMorphismCoefficientComponent E) (hne : C.morphismCoefficientAt E hC hE (CategoryTheory.CategoryStruct.comp (C.boundaryFreeMorphismCoefficientComponentMap D hC hD first) (D.boundaryFreeMorphismCoefficientComponentMap E hD hE second)) (↑output).representative ≠ 0) : second.HasFullOutputSupport

Full target support of an output component transfers to the second factor component whenever their product is nonzero on the output component.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.exists_component_pair_of_factorization_eq_componentMap {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C D E : Word R) (hC hD hE : IsMonomial R) (output : C.BoundaryFreeMorphismCoefficientComponent E) (f : C.rightModule hC ⟶ D.rightModule hD) (g : D.rightModule hD ⟶ E.rightModule hE) (hfactor : CategoryTheory.CategoryStruct.comp f g = C.boundaryFreeMorphismCoefficientComponentMap E hC hE output) : ∃ (first : C.BoundaryFreeMorphismCoefficientComponent D) (second : D.BoundaryFreeMorphismCoefficientComponent E), C.morphismCoefficientAt D hC hD f (↑first).representative ≠ 0 ∧ D.morphismCoefficientAt E hD hE g (↑second).representative ≠ 0 ∧ C.morphismCoefficientAt E hC hE (CategoryTheory.CategoryStruct.comp (C.boundaryFreeMorphismCoefficientComponentMap D hC hD first) (D.boundaryFreeMorphismCoefficientComponentMap E hD hE second)) (↑output).representative = 1 ∧ (output.HasFullInputSupport → first.HasFullInputSupport) ∧ (output.HasFullOutputSupport → second.HasFullOutputSupport)

A factorization of one graph-basis map selects a pair of factor components with coefficient one on the output component. Any full support of the output transfers to the corresponding selected factor.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.HookExtension.exists_component_pair_of_moduleMap_factorization {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D M : Word R} (hook : C.HookExtension D) (hmono : IsMonomial R) (f : D.rightModule hmono ⟶ M.rightModule hmono) (g : M.rightModule hmono ⟶ C.rightModule hmono) (hfactor : CategoryTheory.CategoryStruct.comp f g = hook.moduleMap hmono) : ∃ (first : D.BoundaryFreeMorphismCoefficientComponent M) (second : M.BoundaryFreeMorphismCoefficientComponent C), D.morphismCoefficientAt M hmono hmono f (↑first).representative ≠ 0 ∧ M.morphismCoefficientAt C hmono hmono g (↑second).representative ≠ 0 ∧ D.morphismCoefficientAt C hmono hmono (CategoryTheory.CategoryStruct.comp (D.boundaryFreeMorphismCoefficientComponentMap M hmono hmono first) (M.boundaryFreeMorphismCoefficientComponentMap C hmono hmono second)) (↑(hook.moduleMapComponent hmono)).representative = 1 ∧ second.HasFullOutputSupport

A factorization of a right hook projection through a literal string module selects a second factor component with full target support.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.CohookExtension.exists_component_pair_of_moduleMap_factorization {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D M : Word R} (cohook : C.CohookExtension D) (hmono : IsMonomial R) (f : C.rightModule hmono ⟶ M.rightModule hmono) (g : M.rightModule hmono ⟶ D.rightModule hmono) (hfactor : CategoryTheory.CategoryStruct.comp f g = cohook.moduleMap hmono) : ∃ (first : C.BoundaryFreeMorphismCoefficientComponent M) (second : M.BoundaryFreeMorphismCoefficientComponent D), C.morphismCoefficientAt M hmono hmono f (↑first).representative ≠ 0 ∧ M.morphismCoefficientAt D hmono hmono g (↑second).representative ≠ 0 ∧ C.morphismCoefficientAt D hmono hmono (CategoryTheory.CategoryStruct.comp (C.boundaryFreeMorphismCoefficientComponentMap M hmono hmono first) (M.boundaryFreeMorphismCoefficientComponentMap D hmono hmono second)) (↑(cohook.moduleMapComponent hmono)).representative = 1 ∧ first.HasFullInputSupport

A factorization of a right cohook inclusion through a literal string module selects a first factor component with full source support.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.LeftHookExtension.exists_component_pair_of_moduleMap_factorization {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C M : Word R} (hook : C.LeftHookExtension) (hmono : IsMonomial R) (f : hook.result.rightModule hmono ⟶ M.rightModule hmono) (g : M.rightModule hmono ⟶ C.rightModule hmono) (hfactor : CategoryTheory.CategoryStruct.comp f g = hook.moduleMap hmono) : ∃ (first : hook.result.BoundaryFreeMorphismCoefficientComponent M) (second : M.BoundaryFreeMorphismCoefficientComponent C), hook.result.morphismCoefficientAt M hmono hmono f (↑first).representative ≠ 0 ∧ M.morphismCoefficientAt C hmono hmono g (↑second).representative ≠ 0 ∧ hook.result.morphismCoefficientAt C hmono hmono (CategoryTheory.CategoryStruct.comp (hook.result.boundaryFreeMorphismCoefficientComponentMap M hmono hmono first) (M.boundaryFreeMorphismCoefficientComponentMap C hmono hmono second)) (↑(hook.moduleMapComponent hmono)).representative = 1 ∧ second.HasFullOutputSupport

A factorization of a left hook projection through a literal string module selects a second factor component with full target support.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.LeftCohookExtension.exists_component_pair_of_moduleMap_factorization {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C M : Word R} (cohook : C.LeftCohookExtension) (hmono : IsMonomial R) (f : C.rightModule hmono ⟶ M.rightModule hmono) (g : M.rightModule hmono ⟶ cohook.result.rightModule hmono) (hfactor : CategoryTheory.CategoryStruct.comp f g = cohook.moduleMap hmono) : ∃ (first : C.BoundaryFreeMorphismCoefficientComponent M) (second : M.BoundaryFreeMorphismCoefficientComponent cohook.result), C.morphismCoefficientAt M hmono hmono f (↑first).representative ≠ 0 ∧ M.morphismCoefficientAt cohook.result hmono hmono g (↑second).representative ≠ 0 ∧ C.morphismCoefficientAt cohook.result hmono hmono (CategoryTheory.CategoryStruct.comp (C.boundaryFreeMorphismCoefficientComponentMap M hmono hmono first) (M.boundaryFreeMorphismCoefficientComponentMap cohook.result hmono hmono second)) (↑(cohook.moduleMapComponent hmono)).representative = 1 ∧ first.HasFullInputSupport

A factorization of a left cohook inclusion through a literal string module selects a first factor component with full source support.