Irreducible hook and cohook maps in the finite module category

This file isolates the exact finite-string-sum input needed to turn the raw string-sum factorization theorems into categorical irreducibility. A finite-dimensional module is a finite string sum when its underlying raw functor is isomorphic to a finite biproduct of literal string modules. If every finite-dimensional module has this form, all four canonical hook and cohook maps are irreducible in the finite-dimensional module category.

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

The right-hook map bundled in the finite-dimensional linear-module category.

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

The right-cohook map bundled in the finite-dimensional linear-module category.

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

The left-hook map bundled in the finite-dimensional linear-module category.

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

The left-cohook map bundled in the finite-dimensional linear-module category.

@[simp]

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

@[simp]

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

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.LeftHookExtension.finiteModuleMap_hom_hom {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} [Fintype Q] {C : Word R} (hook : C.LeftHookExtension) (hmono : IsMonomial R) : (hook.finiteModuleMap hmono).hom.hom = hook.moduleMap hmono

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.LeftCohookExtension.finiteModuleMap_hom_hom {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} [Fintype Q] {C : Word R} (cohook : C.LeftCohookExtension) (hmono : IsMonomial R) : (cohook.finiteModuleMap hmono).hom.hom = cohook.moduleMap hmono

def MagnitudeConjecture.BoundQuiver.StringWord.Word.CohookExtension.transportResult {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D D' : Word R} (cohook : C.CohookExtension D) (h : D = D') : C.CohookExtension D'

Transport the result word of a right cohook along a literal equality.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.CohookExtension.finiteModuleMap_transportResult {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} [Fintype Q] {C D D' : Word R} (cohook : C.CohookExtension D) (h : D = D') (hmono : IsMonomial R) : (cohook.transportResult h).finiteModuleMap hmono = CategoryTheory.CategoryStruct.comp (cohook.finiteModuleMap hmono) (CategoryTheory.eqToIso ⋯).hom

Transporting a cohook result agrees with postcomposition by the induced equality isomorphism of finite string modules.

def MagnitudeConjecture.BoundQuiver.StringWord.Word.CohookExtension.transportSource {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C C' D : Word R} (cohook : C.CohookExtension D) (h : C = C') : C'.CohookExtension D

Transport the source word of a right cohook along a literal equality.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.CohookExtension.finiteModuleMap_transportSource {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} [Fintype Q] {C C' D : Word R} (cohook : C.CohookExtension D) (h : C = C') (hmono : IsMonomial R) : (cohook.transportSource h).finiteModuleMap hmono = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToIso ⋯).inv (cohook.finiteModuleMap hmono)

Transporting a cohook source agrees with precomposition by the inverse of the induced equality isomorphism of finite string modules.

def MagnitudeConjecture.BoundQuiver.StringWord.Word.IsFiniteStringSum {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (hmono : IsMonomial R) (N : CoveringHom.FiniteDimensionalModuleCategory k) : Prop

A finite-dimensional module is a finite string sum when its underlying raw module is isomorphic to a finite biproduct of literal string modules.

def MagnitudeConjecture.BoundQuiver.StringWord.Word.EveryFiniteModuleIsFiniteStringSum {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (hmono : IsMonomial R) : Prop

The exact object-coverage statement needed below: every finite-dimensional module is a finite sum of literal string modules.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.HookExtension.isSplitMono_or_isSplitEpi_of_finiteModule_factorization {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} [Fintype Q] {C D : Word R} (hook : C.HookExtension D) (hmono : IsMonomial R) {N : CoveringHom.FiniteDimensionalModuleCategory k} (hN : IsFiniteStringSum hmono N) (f : D.finiteRightModule hmono ⟶ N) (g : N ⟶ C.finiteRightModule hmono) (hfactor : CategoryTheory.CategoryStruct.comp f g = hook.finiteModuleMap hmono) : CategoryTheory.IsSplitMono f ∨ CategoryTheory.IsSplitEpi g

The right-hook factorization clause in the finite-dimensional category, assuming only that this particular intermediate object is a finite string sum.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.CohookExtension.isSplitMono_or_isSplitEpi_of_finiteModule_factorization {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} [Fintype Q] {C D : Word R} (cohook : C.CohookExtension D) (hmono : IsMonomial R) {N : CoveringHom.FiniteDimensionalModuleCategory k} (hN : IsFiniteStringSum hmono N) (f : C.finiteRightModule hmono ⟶ N) (g : N ⟶ D.finiteRightModule hmono) (hfactor : CategoryTheory.CategoryStruct.comp f g = cohook.finiteModuleMap hmono) : CategoryTheory.IsSplitMono f ∨ CategoryTheory.IsSplitEpi g

The right-cohook factorization clause in the finite-dimensional category for one finite-string-sum intermediate object.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.HookExtension.isSplitMono_or_isSplitEpi_of_finiteModule_factorization_of_coefficient_ne_zero {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} [Fintype Q] {C D : Word R} (hook : C.HookExtension D) (hmono : IsMonomial R) {N : CoveringHom.FiniteDimensionalModuleCategory k} (hN : IsFiniteStringSum hmono N) (f : D.finiteRightModule hmono ⟶ N) (g : N ⟶ C.finiteRightModule hmono) (hcoefficient : D.morphismCoefficientAt C hmono hmono (CategoryTheory.CategoryStruct.comp f g).hom.hom (↑(hook.moduleMapComponent hmono)).representative ≠ 0) : CategoryTheory.IsSplitMono f ∨ CategoryTheory.IsSplitEpi g

The right-hook distinguished-coefficient criterion in the bundled finite-dimensional module category.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.CohookExtension.isSplitMono_or_isSplitEpi_of_finiteModule_factorization_of_coefficient_ne_zero {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} [Fintype Q] {C D : Word R} (cohook : C.CohookExtension D) (hmono : IsMonomial R) {N : CoveringHom.FiniteDimensionalModuleCategory k} (hN : IsFiniteStringSum hmono N) (f : C.finiteRightModule hmono ⟶ N) (g : N ⟶ D.finiteRightModule hmono) (hcoefficient : C.morphismCoefficientAt D hmono hmono (CategoryTheory.CategoryStruct.comp f g).hom.hom (↑(cohook.moduleMapComponent hmono)).representative ≠ 0) : CategoryTheory.IsSplitMono f ∨ CategoryTheory.IsSplitEpi g

The right-cohook distinguished-coefficient criterion in the bundled finite-dimensional module category.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.LeftHookExtension.isSplitMono_or_isSplitEpi_of_finiteModule_factorization {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} [Fintype Q] {C : Word R} (hook : C.LeftHookExtension) (hmono : IsMonomial R) {N : CoveringHom.FiniteDimensionalModuleCategory k} (hN : IsFiniteStringSum hmono N) (f : hook.result.finiteRightModule hmono ⟶ N) (g : N ⟶ C.finiteRightModule hmono) (hfactor : CategoryTheory.CategoryStruct.comp f g = hook.finiteModuleMap hmono) : CategoryTheory.IsSplitMono f ∨ CategoryTheory.IsSplitEpi g

The left-hook factorization clause in the finite-dimensional category for one finite-string-sum intermediate object.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.LeftCohookExtension.isSplitMono_or_isSplitEpi_of_finiteModule_factorization {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} [Fintype Q] {C : Word R} (cohook : C.LeftCohookExtension) (hmono : IsMonomial R) {N : CoveringHom.FiniteDimensionalModuleCategory k} (hN : IsFiniteStringSum hmono N) (f : C.finiteRightModule hmono ⟶ N) (g : N ⟶ cohook.result.finiteRightModule hmono) (hfactor : CategoryTheory.CategoryStruct.comp f g = cohook.finiteModuleMap hmono) : CategoryTheory.IsSplitMono f ∨ CategoryTheory.IsSplitEpi g

The left-cohook factorization clause in the finite-dimensional category for one finite-string-sum intermediate object.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.HookExtension.isIrreducibleMorphism_of_isRadicalMorphism_of_coefficient_ne_zero {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} [Fintype Q] {C D : Word R} (hook : C.HookExtension D) (hmono : IsMonomial R) (hcover : EveryFiniteModuleIsFiniteStringSum hmono) (t : D.finiteRightModule hmono ⟶ C.finiteRightModule hmono) (hradical : QuotientSubmoduleEquidistribution.CategoricalRadical.IsRadicalMorphism t) (hcoefficient : D.morphismCoefficientAt C hmono hmono t.hom.hom (↑(hook.moduleMapComponent hmono)).representative ≠ 0) : QuotientSubmoduleEquidistribution.IsIrreducibleMorphism t

A radical map with a nonzero coefficient on a distinguished right-hook component is irreducible, provided finite modules are finite string sums.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.CohookExtension.isIrreducibleMorphism_of_isRadicalMorphism_of_coefficient_ne_zero {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} [Fintype Q] {C D : Word R} (cohook : C.CohookExtension D) (hmono : IsMonomial R) (hcover : EveryFiniteModuleIsFiniteStringSum hmono) (t : C.finiteRightModule hmono ⟶ D.finiteRightModule hmono) (hradical : QuotientSubmoduleEquidistribution.CategoricalRadical.IsRadicalMorphism t) (hcoefficient : C.morphismCoefficientAt D hmono hmono t.hom.hom (↑(cohook.moduleMapComponent hmono)).representative ≠ 0) : QuotientSubmoduleEquidistribution.IsIrreducibleMorphism t

A radical map with a nonzero coefficient on a distinguished right-cohook component is irreducible, provided finite modules are finite string sums.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.HookExtension.finiteModuleMap_isIrreducible_of_finiteStringSum {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} [Fintype Q] {C D : Word R} (hook : C.HookExtension D) (hmono : IsMonomial R) (hcover : EveryFiniteModuleIsFiniteStringSum hmono) : QuotientSubmoduleEquidistribution.IsIrreducibleMorphism (hook.finiteModuleMap hmono)

Under finite-string-sum coverage, the right-hook projection is an irreducible morphism in the finite-dimensional module category.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.CohookExtension.finiteModuleMap_isIrreducible_of_finiteStringSum {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} [Fintype Q] {C D : Word R} (cohook : C.CohookExtension D) (hmono : IsMonomial R) (hcover : EveryFiniteModuleIsFiniteStringSum hmono) : QuotientSubmoduleEquidistribution.IsIrreducibleMorphism (cohook.finiteModuleMap hmono)

Under finite-string-sum coverage, the right-cohook inclusion is an irreducible morphism in the finite-dimensional module category.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.LeftHookExtension.finiteModuleMap_isIrreducible_of_finiteStringSum {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} [Fintype Q] {C : Word R} (hook : C.LeftHookExtension) (hmono : IsMonomial R) (hcover : EveryFiniteModuleIsFiniteStringSum hmono) : QuotientSubmoduleEquidistribution.IsIrreducibleMorphism (hook.finiteModuleMap hmono)

Under finite-string-sum coverage, the left-hook projection is an irreducible morphism in the finite-dimensional module category.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.LeftCohookExtension.finiteModuleMap_isIrreducible_of_finiteStringSum {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} [Fintype Q] {C : Word R} (cohook : C.LeftCohookExtension) (hmono : IsMonomial R) (hcover : EveryFiniteModuleIsFiniteStringSum hmono) : QuotientSubmoduleEquidistribution.IsIrreducibleMorphism (cohook.finiteModuleMap hmono)

Under finite-string-sum coverage, the left-cohook inclusion is an irreducible morphism in the finite-dimensional module category.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.HookExtension.finiteModuleMap_sub_smul_isIrreducible_of_coefficient_eq_zero {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} [Fintype Q] {C D : Word R} (hook : C.HookExtension D) (hmono : IsMonomial R) (hcover : EveryFiniteModuleIsFiniteStringSum hmono) (first : D.finiteRightModule hmono ⟶ C.finiteRightModule hmono) (hfirstRadical : QuotientSubmoduleEquidistribution.CategoricalRadical.IsRadicalMorphism first) (hfirstCoefficient : D.morphismCoefficientAt C hmono hmono first.hom.hom (↑(hook.moduleMapComponent hmono)).representative = 0) (c : k) : QuotientSubmoduleEquidistribution.IsIrreducibleMorphism (hook.finiteModuleMap hmono - c • first)

Subtracting a scalar multiple of a radical map whose distinguished right-hook coefficient vanishes leaves a nonzero distinguished coefficient, and hence remains irreducible.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.CohookExtension.finiteModuleMap_sub_smul_isIrreducible_of_coefficient_eq_zero {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} [Fintype Q] {C D : Word R} (cohook : C.CohookExtension D) (hmono : IsMonomial R) (hcover : EveryFiniteModuleIsFiniteStringSum hmono) (first : C.finiteRightModule hmono ⟶ D.finiteRightModule hmono) (hfirstRadical : QuotientSubmoduleEquidistribution.CategoricalRadical.IsRadicalMorphism first) (hfirstCoefficient : C.morphismCoefficientAt D hmono hmono first.hom.hom (↑(cohook.moduleMapComponent hmono)).representative = 0) (c : k) : QuotientSubmoduleEquidistribution.IsIrreducibleMorphism (cohook.finiteModuleMap hmono - c • first)

The dual coefficient criterion for a right-cohook inclusion.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.HookExtension.finiteModuleMap_sub_smul_isIrreducible_of_component_ne {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} [Fintype Q] {C D : Word R} (first second : C.HookExtension D) (hmono : IsMonomial R) (hcover : EveryFiniteModuleIsFiniteStringSum hmono) (hcomponents : ¬Relation.EqvGen (D.MorphismCoefficientStep C) (↑(first.moduleMapComponent hmono)).representative (↑(second.moduleMapComponent hmono)).representative) (c : k) : QuotientSubmoduleEquidistribution.IsIrreducibleMorphism (second.finiteModuleMap hmono - c • first.finiteModuleMap hmono)

If two right hooks between the same literal string modules have distinct graph components, every scalar row operation on their maps remains irreducible. This is the coefficient-basis form of the exceptional two-dimensional irreducible space.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.CohookExtension.finiteModuleMap_sub_smul_isIrreducible_of_component_ne {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} [Fintype Q] {C D : Word R} (first second : C.CohookExtension D) (hmono : IsMonomial R) (hcover : EveryFiniteModuleIsFiniteStringSum hmono) (hcomponents : ¬Relation.EqvGen (C.MorphismCoefficientStep D) (↑(first.moduleMapComponent hmono)).representative (↑(second.moduleMapComponent hmono)).representative) (c : k) : QuotientSubmoduleEquidistribution.IsIrreducibleMorphism (second.finiteModuleMap hmono - c • first.finiteModuleMap hmono)

If two right cohooks between the same literal string modules have distinct graph components, every scalar row operation on their maps remains irreducible.