The proper-component subspace of a string endomorphism ring

The graph-component basis splits into the diagonal identity component and the remaining proper self-overlap components. This file packages the span of the proper components and identifies it with the kernel of the diagonal basis coordinate. Closure under multiplication and nilpotence remain separate combinatorial obligations.

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

Boundary-free self-components other than the diagonal component.

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

@[instance_reducible]

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

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.properBoundaryFreeMorphismCoefficientComponentMap {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) (hmono : IsMonomial R) (component : C.ProperBoundaryFreeMorphismCoefficientComponent) : C.rightModule hmono ⟶ C.rightModule hmono

The endomorphism carried by one proper self-component.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.diagonalMorphismCoefficientLinearMap {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) (hmono : IsMonomial R) : (C.rightModule hmono ⟶ C.rightModule hmono) →ₗ[k] k

The scalar coordinate in the diagonal graph-component direction.

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.diagonalMorphismCoefficientLinearMap_apply {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) (hmono : IsMonomial R) (f : C.rightModule hmono ⟶ C.rightModule hmono) : (C.diagonalMorphismCoefficientLinearMap hmono) f = C.morphismCoefficientAt C hmono hmono f C.diagonalMorphismCoefficientComponent.representative

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.diagonalMorphismCoefficientLinearMap_id {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) (hmono : IsMonomial R) : (C.diagonalMorphismCoefficientLinearMap hmono) (CategoryTheory.CategoryStruct.id (C.rightModule hmono)) = 1

The diagonal coordinate sends the identity to one.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.diagonalMorphismCoefficientLinearMap_properComponentMap {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) (hmono : IsMonomial R) (component : C.ProperBoundaryFreeMorphismCoefficientComponent) : (C.diagonalMorphismCoefficientLinearMap hmono) (C.properBoundaryFreeMorphismCoefficientComponentMap hmono component) = 0

Every proper component map lies in the kernel of the diagonal coordinate.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.properMorphismCoefficientComponentSubspace {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) (hmono : IsMonomial R) : Submodule k (C.rightModule hmono ⟶ C.rightModule hmono)

The candidate radical: the span of all proper self-component maps.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.properMorphismCoefficientComponentSubspace_le_ker {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) (hmono : IsMonomial R) : C.properMorphismCoefficientComponentSubspace hmono ≤ (C.diagonalMorphismCoefficientLinearMap hmono).ker

The proper-component span is contained in the kernel of the diagonal coordinate.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.mem_properMorphismCoefficientComponentSubspace_of_diagonal_eq_zero {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) (hmono : IsMonomial R) (f : C.rightModule hmono ⟶ C.rightModule hmono) (hf : (C.diagonalMorphismCoefficientLinearMap hmono) f = 0) : f ∈ C.properMorphismCoefficientComponentSubspace hmono

A zero diagonal graph coordinate is a linear combination of proper self-component maps.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.properMorphismCoefficientComponentSubspace_eq_ker {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) (hmono : IsMonomial R) : C.properMorphismCoefficientComponentSubspace hmono = (C.diagonalMorphismCoefficientLinearMap hmono).ker

The proper-component span is exactly the kernel of the diagonal basis coordinate.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.exists_eq_smul_id_add_mem_properComponentSubspace {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) (hmono : IsMonomial R) (f : C.rightModule hmono ⟶ C.rightModule hmono) : ∃ r ∈ C.properMorphismCoefficientComponentSubspace hmono, f = (C.diagonalMorphismCoefficientLinearMap hmono) f • CategoryTheory.CategoryStruct.id (C.rightModule hmono) + r

Every string endomorphism is its diagonal scalar times the identity plus a member of the proper-component subspace.