Representatives of ordinary-quiver arrows

The ordinary quiver remembers only a basis of each projective radical quotient rad / rad². A bound-quiver realization additionally chooses a radical representative of every basis vector. Skowroński--Waschbüsch's special-biserial construction changes these representatives, so the choice is made explicit here rather than identified with the ordinary quiver itself.

Any two choices differ in the internal projective radical square. More generally, their evaluations of a path of length n agree modulo the (n + 1)-st radical power. Thus changing representatives is unitriangular for the projective-radical filtration, although literal zero/nonzero two-arrow compositions need not be preserved.

structure MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.OrdinaryArrowRepresentatives {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} : Type u

A simultaneous choice of radical representatives for the fixed basis arrows of the ordinary projective quiver.

• representative {x y : S.ProjectiveLabel} : S.OrdinaryArrow x y → ↥(S.projectiveRadicalSubmodule x y)
• representative_mkQ {x y : S.ProjectiveLabel} (a : S.OrdinaryArrow x y) : Submodule.Quotient.mk (self.representative a) = S.ordinaryArrowClass a

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.OrdinaryArrowRepresentatives.hom {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (D : OrdinaryArrowRepresentatives) {x y : S.ProjectiveLabel} (a : S.OrdinaryArrow x y) : S.ordinaryProjectiveObj y ⟶ S.ordinaryProjectiveObj x

The selected-projective morphism represented by an ordinary arrow.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.OrdinaryArrowRepresentatives.hom_mem_radical {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (D : OrdinaryArrowRepresentatives) {x y : S.ProjectiveLabel} (a : S.OrdinaryArrow x y) : D.hom a ∈ S.projectiveNilpotentRadicalData.ideal.hom (S.ordinaryProjectiveObj y) (S.ordinaryProjectiveObj x)

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.OrdinaryArrowRepresentatives.hom_not_mem_radicalSquare {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (D : OrdinaryArrowRepresentatives) {x y : S.ProjectiveLabel} (a : S.OrdinaryArrow x y) : D.hom a ∉ S.projectiveRadicalSquareSubmodule x y

A representative of a displayed ordinary arrow does not lie in the internal projective radical square.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.OrdinaryArrowRepresentatives.codomainEndomorphism_mem_radical_of_comp_mem_radicalSquare {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (D : OrdinaryArrowRepresentatives) {x y : S.ProjectiveLabel} (a : S.OrdinaryArrow x y) (e : S.ordinaryProjectiveObj x ⟶ S.ordinaryProjectiveObj x) (hcomp : CategoryTheory.CategoryStruct.comp (D.hom a) e ∈ S.projectiveRadicalSquareSubmodule x y) : e ∈ S.projectiveNilpotentRadicalData.ideal.hom (S.ordinaryProjectiveObj x) (S.ordinaryProjectiveObj x)

If postcomposition carries an ordinary-arrow representative into the internal projective radical square, the endomorphism multiplier is radical. The local-ring argument is performed in the ambient right-module category; full faithfulness then reflects the resulting split mono for cancellation.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.OrdinaryArrowRepresentatives.domainEndomorphism_mem_radical_of_comp_mem_radicalSquare {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (D : OrdinaryArrowRepresentatives) {x y : S.ProjectiveLabel} (a : S.OrdinaryArrow x y) (e : S.ordinaryProjectiveObj y ⟶ S.ordinaryProjectiveObj y) (hcomp : CategoryTheory.CategoryStruct.comp e (D.hom a) ∈ S.projectiveRadicalSquareSubmodule x y) : e ∈ S.projectiveNilpotentRadicalData.ideal.hom (S.ordinaryProjectiveObj y) (S.ordinaryProjectiveObj y)

If precomposition carries an ordinary-arrow representative into the internal projective radical square, the endomorphism multiplier is radical. This is the split-epi dual of codomainEndomorphism_mem_radical_of_comp_mem_radicalSquare.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.OrdinaryArrowRepresentatives.perturb {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (D : OrdinaryArrowRepresentatives) (r : {x y : S.ProjectiveLabel} → S.OrdinaryArrow x y → ↥(S.projectiveRadicalSquareSubmodule x y)) : OrdinaryArrowRepresentatives

Perturb every arrow representative by an element of the internal projective radical square. This is exactly the freedom available when changing lifts of the fixed ordinary-arrow classes.

@[simp]

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.OrdinaryArrowRepresentatives.perturb_hom {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (D : OrdinaryArrowRepresentatives) (r : {x y : S.ProjectiveLabel} → S.OrdinaryArrow x y → ↥(S.projectiveRadicalSquareSubmodule x y)) {x y : S.ProjectiveLabel} (a : S.OrdinaryArrow x y) : (D.perturb fun {x y : S.ProjectiveLabel} => r).hom a = D.hom a + ↑(r a)

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.OrdinaryArrowRepresentatives.irrToHomModSquare {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x y : S.ProjectiveLabel) : S.projectiveIrreducibleHomSpace x y →ₗ[k] (S.ordinaryProjectiveObj y ⟶ S.ordinaryProjectiveObj x) ⧸ S.projectiveRadicalSquareSubmodule x y

Include the irreducible quotient into the full projective Hom-space modulo the internal projective radical square.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.OrdinaryArrowRepresentatives.irrToHomModSquare_injective {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x y : S.ProjectiveLabel) : Function.Injective ⇑(irrToHomModSquare S x y)

@[simp]

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.OrdinaryArrowRepresentatives.irrToHomModSquare_arrowClass {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (D : OrdinaryArrowRepresentatives) {x y : S.ProjectiveLabel} (a : S.OrdinaryArrow x y) : (irrToHomModSquare S x y) (S.ordinaryArrowClass a) = (S.projectiveRadicalSquareSubmodule x y).mkQ (D.hom a)

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.OrdinaryArrowRepresentatives.homModSquare_linearIndependent {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (D : OrdinaryArrowRepresentatives) (x y : S.ProjectiveLabel) : LinearIndependent k fun (a : S.OrdinaryArrow x y) => (S.projectiveRadicalSquareSubmodule x y).mkQ (D.hom a)

Any representatives of the displayed arrows remain linearly independent in the full projective Hom-space modulo its radical square.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.OrdinaryArrowRepresentatives.identityModSquare_not_mem_span_hom {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (D : OrdinaryArrowRepresentatives) (x : S.ProjectiveLabel) : (S.projectiveRadicalSquareSubmodule x x).mkQ (CategoryTheory.CategoryStruct.id (S.ordinaryProjectiveObj x)) ∉ Submodule.span k (Set.range fun (a : S.OrdinaryArrow x x) => (S.projectiveRadicalSquareSubmodule x x).mkQ (D.hom a))

The identity class is not spanned by loop-arrow representatives modulo the internal projective radical square.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.OrdinaryArrowRepresentatives.hom_sub_hom_mem_radicalSquare {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (D E : OrdinaryArrowRepresentatives) {x y : S.ProjectiveLabel} (a : S.OrdinaryArrow x y) : D.hom a - E.hom a ∈ S.projectiveRadicalSquareSubmodule x y

Two choices of representatives of the same displayed arrow differ by an element of the internal projective radical square.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.OrdinaryArrowRepresentatives.pathMap {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (D : OrdinaryArrowRepresentatives) {x y : S.ProjectiveLabel} (p : Quiver.Path x y) : S.ordinaryProjectiveObj y ⟶ S.ordinaryProjectiveObj x

Evaluation of a path using a specified representative system.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.OrdinaryArrowRepresentatives.pathMap_mem_radicalPow {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (D : OrdinaryArrowRepresentatives) {x y : S.ProjectiveLabel} (p : Quiver.Path x y) : D.pathMap p ∈ (S.projectiveNilpotentRadicalData.ideal.pow p.length).hom (S.ordinaryProjectiveObj y) (S.ordinaryProjectiveObj x)

A path of length n evaluated with any representative system belongs to the n-th internal projective-radical power.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.OrdinaryArrowRepresentatives.pathMap_sub_pathMap_mem_radicalPow_succ {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (D E : OrdinaryArrowRepresentatives) {x y : S.ProjectiveLabel} (p : Quiver.Path x y) : D.pathMap p - E.pathMap p ∈ (S.projectiveNilpotentRadicalData.ideal.pow (p.length + 1)).hom (S.ordinaryProjectiveObj y) (S.ordinaryProjectiveObj x)

Replacing every arrow representative changes the evaluation of a path of length n only in radical degree at least n + 1.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.OrdinaryArrowRepresentatives.realization {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (D : OrdinaryArrowRepresentatives) : CategoryTheory.Functor (LinearPathCategory.Category k S.ProjectiveLabel) S.ProjectiveCategory

The free linear path realization determined by a representative system.

instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.OrdinaryArrowRepresentatives.realization_additive {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (D : OrdinaryArrowRepresentatives) : D.realization.Additive

instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.OrdinaryArrowRepresentatives.realization_linear {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (D : OrdinaryArrowRepresentatives) : CategoryTheory.Functor.Linear k D.realization

@[simp]

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.OrdinaryArrowRepresentatives.realization_map_pathHom {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (D : OrdinaryArrowRepresentatives) {x y : S.ProjectiveLabel} (p : Quiver.Path x y) : D.realization.map (LinearPathCategory.pathHom p) = D.pathMap p

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.OrdinaryArrowRepresentatives.relations {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (D : OrdinaryArrowRepresentatives) : BoundQuiver.RelationFamily k S.ProjectiveLabel

The exact kernel relation family attached to a representative system.

@[simp]

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.OrdinaryArrowRepresentatives.mem_relations_iff {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (D : OrdinaryArrowRepresentatives) {X Y : LinearPathCategory.Category k S.ProjectiveLabel} (f : X ⟶ Y) : f ∈ D.relations X Y ↔ D.realization.map f = 0

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.OrdinaryArrowRepresentatives.relations_generatedHomSubmodule_eq_ker {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (D : OrdinaryArrowRepresentatives) (X Y : LinearPathCategory.Category k S.ProjectiveLabel) : QuotientSubmoduleEquidistribution.CategoricalIdeal.HomIdeal.generatedHomSubmodule k D.relations X Y = (CategoryTheory.Functor.mapLinearMap k D.realization).ker

The generated ideal of the kernel relation family is the pointwise linear kernel of the realization.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.OrdinaryArrowRepresentatives.exists_realization_pathHom_eq_zero {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (D : OrdinaryArrowRepresentatives) : ∃ (N : ℕ), 2 ≤ N ∧ ∀ {x y : S.ProjectiveLabel} (p : Quiver.Path x y), N ≤ p.length → D.realization.map (LinearPathCategory.pathHom p) = 0

Nilpotence kills all sufficiently long paths for every choice of arrow representatives.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.OrdinaryArrowRepresentatives.relations_long_paths_mem {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (D : OrdinaryArrowRepresentatives) : ∃ (N : ℕ), 2 ≤ N ∧ ∀ {x y : S.ProjectiveLabel} (p : Quiver.Path x y), N ≤ p.length → LinearPathCategory.pathHom p ∈ QuotientSubmoduleEquidistribution.CategoricalIdeal.HomIdeal.generatedHomSubmodule k D.relations (LinearPathCategory.obj k S.ProjectiveLabel y) (LinearPathCategory.obj k S.ProjectiveLabel x)

Every sufficiently long path belongs to the generated kernel ideal for every representative system.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.OrdinaryArrowRepresentatives.lowPathQuotient_linearIndependent {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (D : OrdinaryArrowRepresentatives) (x y : S.ProjectiveLabel) : LinearIndependent k fun (p : { p : Quiver.Path x y // p.length < 2 }) => (S.projectiveRadicalSquareSubmodule x y).mkQ (D.pathMap ↑p)

Short path evaluations remain linearly independent modulo the radical square for every representative system.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.OrdinaryArrowRepresentatives.pathMap_mem_radicalSquare {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (D : OrdinaryArrowRepresentatives) {x y : S.ProjectiveLabel} (p : Quiver.Path x y) (hp : 2 ≤ p.length) : D.pathMap p ∈ S.projectiveRadicalSquareSubmodule x y

Paths of length at least two evaluate into the internal projective radical square for every representative system.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.OrdinaryArrowRepresentatives.relations_generatedHomSubmodule_le_lengthTail_two {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (D : OrdinaryArrowRepresentatives) (X Y : LinearPathCategory.Category k S.ProjectiveLabel) : QuotientSubmoduleEquidistribution.CategoricalIdeal.HomIdeal.generatedHomSubmodule k D.relations X Y ≤ LinearPathCategory.lengthTail X Y 2

The kernel of any representative-system realization has no terms of path length below two.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.OrdinaryArrowRepresentatives.relations_isAdmissible {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (D : OrdinaryArrowRepresentatives) : BoundQuiver.IsAdmissible D.relations

Every choice of representatives of the fixed ordinary arrows has an admissible exact kernel.