Hook and cohook maps as graph components

The canonical hook and cohook maps are carried by the single coefficient component pairing every old word position with its inherited position in the extended word. This file identifies those maps with literal vectors in the compiled graph-component basis. It is the coefficient-level input for the remaining irreducible-factorization argument.

def MagnitudeConjecture.BoundQuiver.StringWord.Word.pairedMorphismCoefficientPosition {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (W C D : Word R) (inputPosition : {x : Q} → W.PositionAt x → C.PositionAt x) (outputPosition : {x : Q} → W.PositionAt x → D.PositionAt x) {x : Q} (i : W.PositionAt x) : C.MorphismCoefficientPosition D

A coefficient position obtained by mapping the same position of an indexing word into a source word and a target word.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.pairedMorphismCoefficientPosition_eqvGen_source {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (W C D : Word R) (inputPosition : {x : Q} → W.PositionAt x → C.PositionAt x) (outputPosition : {x : Q} → W.PositionAt x → D.PositionAt x) (hinput : ∀ {x y : Q} (a : x ⟶ y) (i : W.PositionAt x) (j : W.PositionAt y), W.ArrowStep a i j → C.ArrowStep a (inputPosition i) (inputPosition j)) (houtput : ∀ {x y : Q} (a : x ⟶ y) (i : W.PositionAt x) (j : W.PositionAt y), W.ArrowStep a i j → D.ArrowStep a (outputPosition i) (outputPosition j)) {x : Q} (i : W.PositionAt x) : Relation.EqvGen (C.MorphismCoefficientStep D) (W.pairedMorphismCoefficientPosition C D (fun {x : Q} => inputPosition) (fun {x : Q} => outputPosition) i) (W.pairedMorphismCoefficientPosition C D (fun {x : Q} => inputPosition) (fun {x : Q} => outputPosition) W.sourcePosition)

Position maps preserving displayed-arrow steps carry the whole indexing word into one coefficient component.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.isBoundaryFreeMorphismCoefficientComponent_of_eqvGen {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C D : Word R) {root root' : C.MorphismCoefficientPosition D} (hfree : C.IsBoundaryFreeMorphismCoefficientComponent D root) (hroot : Relation.EqvGen (C.MorphismCoefficientStep D) root root') : C.IsBoundaryFreeMorphismCoefficientComponent D root'

Boundary-freeness is independent of the chosen root inside one coefficient component.

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

The boundary-free component class containing a specified root.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.boundaryFreeMorphismCoefficientComponentOf_representative_eqvGen {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C D : Word R) (root : C.MorphismCoefficientPosition D) (hfree : C.IsBoundaryFreeMorphismCoefficientComponent D root) : Relation.EqvGen (C.MorphismCoefficientStep D) (↑(C.boundaryFreeMorphismCoefficientComponentOf D root hfree)).representative root

The chosen representative of the component class of root lies in the same generated coefficient component as root.

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

A coefficient component meets every position of its source word.

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

A coefficient component meets every position of its target word.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.eq_boundaryFreeMorphismCoefficientComponentMap_of_root {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) (root : C.MorphismCoefficientPosition D) (hroot : C.morphismCoefficientAt D hC hD f root = 1) (hsupport : ∀ (p : C.MorphismCoefficientPosition D), C.morphismCoefficientAt D hC hD f p ≠ 0 → Relation.EqvGen (C.MorphismCoefficientStep D) root p) : f = C.boundaryFreeMorphismCoefficientComponentMap D hC hD (C.boundaryFreeMorphismCoefficientComponentOf D root ⋯)

A morphism with root coefficient one and no support outside the root component is exactly the corresponding graph-component basis map.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.RightExtension.inclusionMorphismCoefficientPosition {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (extension : C.RightExtension D) {x : Q} (i : C.PositionAt x) : C.MorphismCoefficientPosition D

The coefficient position pairing an old position with its image in a right extension, in the inclusion direction.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.RightExtension.projectionMorphismCoefficientPosition {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (extension : C.RightExtension D) {x : Q} (i : C.PositionAt x) : D.MorphismCoefficientPosition C

The same inherited-position pair in the projection direction.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.RightExtension.inclusionMorphismCoefficientPosition_eqvGen_source {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (extension : C.RightExtension D) {x : Q} (i : C.PositionAt x) : Relation.EqvGen (C.MorphismCoefficientStep D) (extension.inclusionMorphismCoefficientPosition i) (extension.inclusionMorphismCoefficientPosition C.sourcePosition)

All inherited pairs in the inclusion direction lie in the component of the inherited source position.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.RightExtension.projectionMorphismCoefficientPosition_eqvGen_source {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (extension : C.RightExtension D) {x : Q} (i : C.PositionAt x) : Relation.EqvGen (D.MorphismCoefficientStep C) (extension.projectionMorphismCoefficientPosition i) (extension.projectionMorphismCoefficientPosition C.sourcePosition)

All inherited pairs in the projection direction lie in the component of the inherited source position.

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.NegativeBoundaryExtension.rightModuleInclusion_morphismCoefficientAt_source {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (extension : C.NegativeBoundaryExtension D) (hmono : IsMonomial R) : C.morphismCoefficientAt D hmono hmono (extension.rightModuleInclusion hmono) (extension.toRightExtension.inclusionMorphismCoefficientPosition C.sourcePosition) = 1

The right-boundary inclusion has coefficient one at the inherited source position.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.NegativeBoundaryExtension.rightModuleInclusion_coefficient_eqvGen_source {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (extension : C.NegativeBoundaryExtension D) (hmono : IsMonomial R) (p : C.MorphismCoefficientPosition D) (hp : C.morphismCoefficientAt D hmono hmono (extension.rightModuleInclusion hmono) p ≠ 0) : Relation.EqvGen (C.MorphismCoefficientStep D) (extension.toRightExtension.inclusionMorphismCoefficientPosition C.sourcePosition) p

Every nonzero coefficient of a right-boundary inclusion belongs to its inherited-position component.

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

The graph-basis component carrying a right-boundary inclusion.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.NegativeBoundaryExtension.rightModuleInclusion_eq_componentMap {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (extension : C.NegativeBoundaryExtension D) (hmono : IsMonomial R) : extension.rightModuleInclusion hmono = C.boundaryFreeMorphismCoefficientComponentMap D hmono hmono (extension.rightModuleInclusionComponent hmono)

A right-boundary inclusion is exactly its inherited-position graph-basis map.

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.PositiveBoundaryExtension.rightModuleProjection_morphismCoefficientAt_source {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (extension : C.PositiveBoundaryExtension D) (hmono : IsMonomial R) : D.morphismCoefficientAt C hmono hmono (extension.rightModuleProjection hmono) (extension.toRightExtension.projectionMorphismCoefficientPosition C.sourcePosition) = 1

The right-boundary projection has coefficient one at the inherited source position.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.PositiveBoundaryExtension.rightModuleProjection_coefficient_eqvGen_source {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (extension : C.PositiveBoundaryExtension D) (hmono : IsMonomial R) (p : D.MorphismCoefficientPosition C) (hp : D.morphismCoefficientAt C hmono hmono (extension.rightModuleProjection hmono) p ≠ 0) : Relation.EqvGen (D.MorphismCoefficientStep C) (extension.toRightExtension.projectionMorphismCoefficientPosition C.sourcePosition) p

Every nonzero coefficient of a right-boundary projection belongs to its inherited-position component.

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

The graph-basis component carrying a right-boundary projection.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.PositiveBoundaryExtension.rightModuleProjection_eq_componentMap {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (extension : C.PositiveBoundaryExtension D) (hmono : IsMonomial R) : extension.rightModuleProjection hmono = D.boundaryFreeMorphismCoefficientComponentMap C hmono hmono (extension.rightModuleProjectionComponent hmono)

A right-boundary projection is exactly its inherited-position graph-basis map.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.NegativeBoundaryExtension.rightModuleInclusionComponent_position_support {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (extension : C.NegativeBoundaryExtension D) (hmono : IsMonomial R) {x : Q} (i : C.PositionAt x) : Relation.EqvGen (C.MorphismCoefficientStep D) (↑(extension.rightModuleInclusionComponent hmono)).representative ⟨x, (i, extension.toRightExtension.position i)⟩

Every inherited pair belongs to the component of a right-boundary inclusion.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.NegativeBoundaryExtension.rightModuleInclusionComponent_hasFullInputSupport {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (extension : C.NegativeBoundaryExtension D) (hmono : IsMonomial R) : (extension.rightModuleInclusionComponent hmono).HasFullInputSupport

The component of a right-boundary inclusion has full support on its source word.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.PositiveBoundaryExtension.rightModuleProjectionComponent_position_support {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (extension : C.PositiveBoundaryExtension D) (hmono : IsMonomial R) {x : Q} (i : C.PositionAt x) : Relation.EqvGen (D.MorphismCoefficientStep C) (↑(extension.rightModuleProjectionComponent hmono)).representative ⟨x, (extension.toRightExtension.position i, i)⟩

Every inherited pair belongs to the component of a right-boundary projection.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.PositiveBoundaryExtension.rightModuleProjectionComponent_hasFullOutputSupport {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (extension : C.PositiveBoundaryExtension D) (hmono : IsMonomial R) : (extension.rightModuleProjectionComponent hmono).HasFullOutputSupport

The component of a right-boundary projection has full support on its target word.

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

The graph-basis component carrying a right hook projection.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.HookExtension.moduleMap_eq_componentMap {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (hook : C.HookExtension D) (hmono : IsMonomial R) : hook.moduleMap hmono = D.boundaryFreeMorphismCoefficientComponentMap C hmono hmono (hook.moduleMapComponent hmono)

A right hook projection is one graph-basis vector.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.HookExtension.moduleMapComponent_hasFullOutputSupport {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (hook : C.HookExtension D) (hmono : IsMonomial R) : (hook.moduleMapComponent hmono).HasFullOutputSupport

A right hook component covers every position of its target word.

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

The graph-basis component carrying a right cohook inclusion.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.CohookExtension.moduleMap_eq_componentMap {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (cohook : C.CohookExtension D) (hmono : IsMonomial R) : cohook.moduleMap hmono = C.boundaryFreeMorphismCoefficientComponentMap D hmono hmono (cohook.moduleMapComponent hmono)

A right cohook inclusion is one graph-basis vector.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.CohookExtension.moduleMapComponent_hasFullInputSupport {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (cohook : C.CohookExtension D) (hmono : IsMonomial R) : (cohook.moduleMapComponent hmono).HasFullInputSupport

A right cohook component covers every position of its source word.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.LeftPositiveBoundaryExtension.arrowStep_position {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C : Word R} (extension : C.LeftPositiveBoundaryExtension) {x y : Q} (a : x ⟶ y) (i : C.PositionAt x) (j : C.PositionAt y) (hij : C.ArrowStep a i j) : extension.result.ArrowStep a (extension.position i) (extension.position j)

A positive left-boundary extension preserves every displayed-arrow step between inherited positions.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.LeftNegativeBoundaryExtension.arrowStep_position {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C : Word R} (extension : C.LeftNegativeBoundaryExtension) {x y : Q} (a : x ⟶ y) (i : C.PositionAt x) (j : C.PositionAt y) (hij : C.ArrowStep a i j) : extension.result.ArrowStep a (extension.position i) (extension.position j)

A negative left-boundary extension preserves every displayed-arrow step between inherited positions.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.LeftPositiveBoundaryExtension.projectionMorphismCoefficientPosition {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C : Word R} (extension : C.LeftPositiveBoundaryExtension) {x : Q} (i : C.PositionAt x) : extension.result.MorphismCoefficientPosition C

An inherited-position coefficient pair for a positive left-boundary projection.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.LeftNegativeBoundaryExtension.inclusionMorphismCoefficientPosition {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C : Word R} (extension : C.LeftNegativeBoundaryExtension) {x : Q} (i : C.PositionAt x) : C.MorphismCoefficientPosition extension.result

An inherited-position coefficient pair for a negative left-boundary inclusion.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.LeftPositiveBoundaryExtension.projectionMorphismCoefficientPosition_eqvGen_source {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C : Word R} (extension : C.LeftPositiveBoundaryExtension) {x : Q} (i : C.PositionAt x) : Relation.EqvGen (extension.result.MorphismCoefficientStep C) (extension.projectionMorphismCoefficientPosition i) (extension.projectionMorphismCoefficientPosition C.sourcePosition)

All inherited pairs of a positive left-boundary projection lie in the component of the original source position.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.LeftNegativeBoundaryExtension.inclusionMorphismCoefficientPosition_eqvGen_source {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C : Word R} (extension : C.LeftNegativeBoundaryExtension) {x : Q} (i : C.PositionAt x) : Relation.EqvGen (C.MorphismCoefficientStep extension.result) (extension.inclusionMorphismCoefficientPosition i) (extension.inclusionMorphismCoefficientPosition C.sourcePosition)

All inherited pairs of a negative left-boundary inclusion lie in the component of the original source position.

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.LeftPositiveBoundaryExtension.moduleMap_morphismCoefficientAt_source {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C : Word R} (extension : C.LeftPositiveBoundaryExtension) (hmono : IsMonomial R) : extension.result.morphismCoefficientAt C hmono hmono (extension.moduleMap hmono) (extension.projectionMorphismCoefficientPosition C.sourcePosition) = 1

The positive left-boundary projection has coefficient one at the inherited source position.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.LeftPositiveBoundaryExtension.moduleMap_coefficient_eqvGen_source {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C : Word R} (extension : C.LeftPositiveBoundaryExtension) (hmono : IsMonomial R) (p : extension.result.MorphismCoefficientPosition C) (hp : extension.result.morphismCoefficientAt C hmono hmono (extension.moduleMap hmono) p ≠ 0) : Relation.EqvGen (extension.result.MorphismCoefficientStep C) (extension.projectionMorphismCoefficientPosition C.sourcePosition) p

Every nonzero coefficient of a positive left-boundary projection belongs to its inherited-position component.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.LeftPositiveBoundaryExtension.moduleMapComponent {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C : Word R} (extension : C.LeftPositiveBoundaryExtension) (hmono : IsMonomial R) : extension.result.BoundaryFreeMorphismCoefficientComponent C

The graph-basis component carrying a positive left-boundary projection.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.LeftPositiveBoundaryExtension.moduleMap_eq_componentMap {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C : Word R} (extension : C.LeftPositiveBoundaryExtension) (hmono : IsMonomial R) : extension.moduleMap hmono = extension.result.boundaryFreeMorphismCoefficientComponentMap C hmono hmono (extension.moduleMapComponent hmono)

A positive left-boundary projection is exactly its inherited-position graph-basis map.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.LeftPositiveBoundaryExtension.moduleMapComponent_position_support {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C : Word R} (extension : C.LeftPositiveBoundaryExtension) (hmono : IsMonomial R) {x : Q} (i : C.PositionAt x) : Relation.EqvGen (extension.result.MorphismCoefficientStep C) (↑(extension.moduleMapComponent hmono)).representative ⟨x, (extension.position i, i)⟩

Every inherited pair belongs to the component of a positive left-boundary projection.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.LeftPositiveBoundaryExtension.moduleMapComponent_hasFullOutputSupport {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C : Word R} (extension : C.LeftPositiveBoundaryExtension) (hmono : IsMonomial R) : (extension.moduleMapComponent hmono).HasFullOutputSupport

A positive left-boundary projection component has full support on its target word.

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.LeftNegativeBoundaryExtension.moduleMap_morphismCoefficientAt_source {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C : Word R} (extension : C.LeftNegativeBoundaryExtension) (hmono : IsMonomial R) : C.morphismCoefficientAt extension.result hmono hmono (extension.moduleMap hmono) (extension.inclusionMorphismCoefficientPosition C.sourcePosition) = 1

The negative left-boundary inclusion has coefficient one at the inherited source position.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.LeftNegativeBoundaryExtension.moduleMap_coefficient_eqvGen_source {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C : Word R} (extension : C.LeftNegativeBoundaryExtension) (hmono : IsMonomial R) (p : C.MorphismCoefficientPosition extension.result) (hp : C.morphismCoefficientAt extension.result hmono hmono (extension.moduleMap hmono) p ≠ 0) : Relation.EqvGen (C.MorphismCoefficientStep extension.result) (extension.inclusionMorphismCoefficientPosition C.sourcePosition) p

Every nonzero coefficient of a negative left-boundary inclusion belongs to its inherited-position component.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.LeftNegativeBoundaryExtension.moduleMapComponent {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C : Word R} (extension : C.LeftNegativeBoundaryExtension) (hmono : IsMonomial R) : C.BoundaryFreeMorphismCoefficientComponent extension.result

The graph-basis component carrying a negative left-boundary inclusion.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.LeftNegativeBoundaryExtension.moduleMap_eq_componentMap {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C : Word R} (extension : C.LeftNegativeBoundaryExtension) (hmono : IsMonomial R) : extension.moduleMap hmono = C.boundaryFreeMorphismCoefficientComponentMap extension.result hmono hmono (extension.moduleMapComponent hmono)

A negative left-boundary inclusion is exactly its inherited-position graph-basis map.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.LeftNegativeBoundaryExtension.moduleMapComponent_position_support {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C : Word R} (extension : C.LeftNegativeBoundaryExtension) (hmono : IsMonomial R) {x : Q} (i : C.PositionAt x) : Relation.EqvGen (C.MorphismCoefficientStep extension.result) (↑(extension.moduleMapComponent hmono)).representative ⟨x, (i, extension.position i)⟩

Every inherited pair belongs to the component of a negative left-boundary inclusion.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.LeftNegativeBoundaryExtension.moduleMapComponent_hasFullInputSupport {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C : Word R} (extension : C.LeftNegativeBoundaryExtension) (hmono : IsMonomial R) : (extension.moduleMapComponent hmono).HasFullInputSupport

A negative left-boundary inclusion component has full support on its source word.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.LeftHookExtension.moduleMapComponent {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C : Word R} (hook : C.LeftHookExtension) (hmono : IsMonomial R) : hook.result.BoundaryFreeMorphismCoefficientComponent C

The graph-basis component carrying a left hook projection.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.LeftHookExtension.moduleMap_eq_componentMap {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C : Word R} (hook : C.LeftHookExtension) (hmono : IsMonomial R) : hook.moduleMap hmono = hook.result.boundaryFreeMorphismCoefficientComponentMap C hmono hmono (hook.moduleMapComponent hmono)

A left hook projection is one graph-basis vector.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.LeftHookExtension.moduleMapComponent_hasFullOutputSupport {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C : Word R} (hook : C.LeftHookExtension) (hmono : IsMonomial R) : (hook.moduleMapComponent hmono).HasFullOutputSupport

A left hook component covers every position of its target word.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.LeftHookExtension.moduleMap_ne_rightHook_moduleMap {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C : Word R} (left : C.LeftHookExtension) (right : C.HookExtension left.result) (hmono : IsMonomial R) : left.moduleMap hmono ≠ right.moduleMap hmono

A left hook and a right hook from the same extended word to the same base word give different module maps. At the initial position of the common extended word, the right projection is the identity while the left projection kills the basis vector.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.LeftHookExtension.moduleMapComponent_ne_rightHook_moduleMapComponent {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C : Word R} (left : C.LeftHookExtension) (right : C.HookExtension left.result) (hmono : IsMonomial R) : left.moduleMapComponent hmono ≠ right.moduleMapComponent hmono

The graph components of a left hook and a right hook with the same literal source word are distinct.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.LeftHookExtension.morphismCoefficientAt_moduleMap_rightHookComponent_eq_zero {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C : Word R} (left : C.LeftHookExtension) (right : C.HookExtension left.result) (hmono : IsMonomial R) : left.result.morphismCoefficientAt C hmono hmono (left.moduleMap hmono) (↑(right.moduleMapComponent hmono)).representative = 0

A left-hook projection has coefficient zero on the different component carrying the right-hook projection from the same extended word.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.LeftCohookExtension.moduleMapComponent {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C : Word R} (cohook : C.LeftCohookExtension) (hmono : IsMonomial R) : C.BoundaryFreeMorphismCoefficientComponent cohook.result

The graph-basis component carrying a left cohook inclusion.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.LeftCohookExtension.moduleMap_eq_componentMap {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C : Word R} (cohook : C.LeftCohookExtension) (hmono : IsMonomial R) : cohook.moduleMap hmono = C.boundaryFreeMorphismCoefficientComponentMap cohook.result hmono hmono (cohook.moduleMapComponent hmono)

A left cohook inclusion is one graph-basis vector.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.LeftCohookExtension.moduleMapComponent_hasFullInputSupport {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C : Word R} (cohook : C.LeftCohookExtension) (hmono : IsMonomial R) : (cohook.moduleMapComponent hmono).HasFullInputSupport

A left cohook component covers every position of its source word.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.LeftCohookExtension.moduleMap_ne_rightCohook_moduleMap {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C : Word R} (left : C.LeftCohookExtension) (right : C.CohookExtension left.result) (hmono : IsMonomial R) : left.moduleMap hmono ≠ right.moduleMap hmono

A left cohook and a right cohook from the same base word to the same literal extended word give different module maps. Their images of the initial basis vector occupy different positions.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.LeftCohookExtension.moduleMapComponent_ne_rightCohook_moduleMapComponent {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C : Word R} (left : C.LeftCohookExtension) (right : C.CohookExtension left.result) (hmono : IsMonomial R) : left.moduleMapComponent hmono ≠ right.moduleMapComponent hmono

The graph components of literal left and right cohook inclusions are distinct.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.LeftCohookExtension.morphismCoefficientAt_moduleMap_rightCohookComponent_eq_zero {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C : Word R} (left : C.LeftCohookExtension) (right : C.CohookExtension left.result) (hmono : IsMonomial R) : C.morphismCoefficientAt left.result hmono hmono (left.moduleMap hmono) (↑(right.moduleMapComponent hmono)).representative = 0

A left-cohook inclusion has coefficient zero on the different component carrying the right-cohook inclusion into the same literal result word.