Normalizing a recursively assembled mesh map

Ringel's standardness recursion first assembles a map from an Auslander--Reiten translate to the displayed middle term using arrows that were chosen at earlier vertices. Fullness at those earlier vertices gives factorizations in both directions between this assembled map and the actual left almost-split kernel inclusion. This file isolates the finite-length argument which upgrades the comparison endomorphism of the middle term to an automorphism. Twisting the right almost-split map by its inverse then makes the mesh relation hold literally.

theorem MagnitudeConjecture.RightModule.leftAlmostSplit_postcomp_iso {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X E E' : C} {f : X ⟶ E} (hf : QuotientSubmoduleEquidistribution.IsLeftAlmostSplit f) (e : E ≅ E') : QuotientSubmoduleEquidistribution.IsLeftAlmostSplit (CategoryTheory.CategoryStruct.comp f e.hom)

Postcomposition by an isomorphism preserves left almost-splitness.

theorem MagnitudeConjecture.RightModule.leftMinimal_postcomp_iso {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X E E' : C} {f : X ⟶ E} (hf : QuotientSubmoduleEquidistribution.IsLeftMinimal f) (e : E ≅ E') : QuotientSubmoduleEquidistribution.IsLeftMinimal (CategoryTheory.CategoryStruct.comp f e.hom)

Postcomposition by an isomorphism preserves left minimality.

theorem MagnitudeConjecture.RightModule.rightAlmostSplit_precomp_iso {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {E' E Z : C} {f : E ⟶ Z} (hf : QuotientSubmoduleEquidistribution.IsRightAlmostSplit f) (e : E' ≅ E) : QuotientSubmoduleEquidistribution.IsRightAlmostSplit (CategoryTheory.CategoryStruct.comp e.hom f)

Precomposition by an isomorphism preserves right almost-splitness.

theorem MagnitudeConjecture.RightModule.isIso_of_mono_finiteLength_endomorphism {R : Type u} [Ring R] [IsNoetherianRing R] {X : FGModuleCat R} (hX : IsFiniteLength R ↑X) (f : X ⟶ X) [CategoryTheory.Mono f] : CategoryTheory.IsIso f

A monic endomorphism of a finite-length finitely generated module is an isomorphism.

theorem MagnitudeConjecture.RightModule.exists_middleIso_of_leftAlmostSplit_mutual_factorization {R : Type u} [Ring R] [IsNoetherianRing R] {K E : FGModuleCat R} (i q : K ⟶ E) (hE : IsFiniteLength R ↑E) (hi : QuotientSubmoduleEquidistribution.IsLeftAlmostSplit i) (himin : QuotientSubmoduleEquidistribution.IsLeftMinimal i) (hq : ¬CategoryTheory.IsSplitMono q) (hqi : ∃ (r : E ⟶ E), CategoryTheory.CategoryStruct.comp q r = i) : ∃ (e : E ≅ E), CategoryTheory.CategoryStruct.comp i e.hom = q

If a nonsplit map and a minimal left almost-split map with the same source factor through one another, their middle terms differ by an automorphism. Finite length is used only to turn the resulting split-monic endomorphism into an isomorphism.

theorem MagnitudeConjecture.RightModule.exists_middleIso_normalizing_leftAlmostSplit {R : Type u} [Ring R] [IsNoetherianRing R] {K E Z : FGModuleCat R} (i q : K ⟶ E) (g : E ⟶ Z) (hE : IsFiniteLength R ↑E) (hi : QuotientSubmoduleEquidistribution.IsLeftAlmostSplit i) (himin : QuotientSubmoduleEquidistribution.IsLeftMinimal i) (hq : ¬CategoryTheory.IsSplitMono q) (hqi : ∃ (r : E ⟶ E), CategoryTheory.CategoryStruct.comp q r = i) (hzero : CategoryTheory.CategoryStruct.comp i g = 0) : ∃ (e : E ≅ E), CategoryTheory.CategoryStruct.comp i e.hom = q ∧ CategoryTheory.CategoryStruct.comp q (CategoryTheory.CategoryStruct.comp e.inv g) = 0

Normalize a comparison map and transport a zero composite across the resulting automorphism. This is the literal mesh-relation step used at a nonprojective vertex of the standardness recursion.

@[instance_reducible]

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.instQuiverFinN {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) : Quiver (Fin S.n)

@[instance_reducible]

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.instFintypeHomFinN {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (i j : Fin S.n) : Fintype (i ⟶ j)

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.rightMeshSourceIndexEquiv {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [IsAlgClosed k] (H : S.HasAcyclicNonzeroNonisomorphisms) (z : { z : Fin S.n // ¬CategoryTheory.Projective (S.fgObj z) }) : (S.meshRightAlmostSplitAt ↑z).index.obj ≃ (y : Fin S.n) × S.MeshArrow y (S.rightTranslationLabel z)

The displayed middle summands at a nonprojective vertex, reindexed by all reversed quiver arrows out of its AR translate.

@[simp]

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.rightMeshSourceIndexEquiv_fst {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [IsAlgClosed k] (H : S.HasAcyclicNonzeroNonisomorphisms) (z : { z : Fin S.n // ¬CategoryTheory.Projective (S.fgObj z) }) (t : (S.meshRightAlmostSplitAt ↑z).index.obj) : ((S.rightMeshSourceIndexEquiv H z) t).fst = (S.meshRightAlmostSplitAt ↑z).label t

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.rightMeshSourceMap {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [IsAlgClosed k] (H : S.HasAcyclicNonzeroNonisomorphisms) (arrowMap : {i j : Fin S.n} → S.MeshArrow i j → (S.almostSplitSkeleton.obj j ⟶ S.almostSplitSkeleton.obj i)) (z : { z : Fin S.n // ¬CategoryTheory.Projective (S.fgObj z) }) : S.almostSplitSkeleton.obj (S.rightTranslationLabel z) ⟶ (S.meshRightAlmostSplitAt ↑z).middle

Assemble the already chosen arrows out of tau z into the displayed middle term at z, using the mesh-arrow pairing.

@[simp]

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.rightMeshSourceMap_decomposition_π {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [IsAlgClosed k] (H : S.HasAcyclicNonzeroNonisomorphisms) (arrowMap : {i j : Fin S.n} → S.MeshArrow i j → (S.almostSplitSkeleton.obj j ⟶ S.almostSplitSkeleton.obj i)) (z : { z : Fin S.n // ¬CategoryTheory.Projective (S.fgObj z) }) (t : (S.meshRightAlmostSplitAt ↑z).index.obj) : CategoryTheory.CategoryStruct.comp (S.rightMeshSourceMap H (fun {i j : Fin S.n} => arrowMap) z) (CategoryTheory.CategoryStruct.comp (S.meshRightAlmostSplitAt ↑z).decomposition.hom (CategoryTheory.Limits.biproduct.π (fun (j : (S.meshRightAlmostSplitAt ↑z).index.obj) => S.almostSplitSkeleton.obj ((S.meshRightAlmostSplitAt ↑z).label j)) t)) = CategoryTheory.CategoryStruct.comp (arrowMap ((S.rightMeshSourceIndexEquiv H z) t).snd) (CategoryTheory.eqToHom ⋯)

@[simp]

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.rightMeshSourceMap_decomposition_π_assoc {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [IsAlgClosed k] (H : S.HasAcyclicNonzeroNonisomorphisms) (arrowMap : {i j : Fin S.n} → S.MeshArrow i j → (S.almostSplitSkeleton.obj j ⟶ S.almostSplitSkeleton.obj i)) (z : { z : Fin S.n // ¬CategoryTheory.Projective (S.fgObj z) }) (t : (S.meshRightAlmostSplitAt ↑z).index.obj) {Z : FGModuleCat Aᵐᵒᵖ} (h : S.almostSplitSkeleton.obj ((S.meshRightAlmostSplitAt ↑z).label t) ⟶ Z) : CategoryTheory.CategoryStruct.comp (S.rightMeshSourceMap H (fun {i j : Fin S.n} => arrowMap) z) (CategoryTheory.CategoryStruct.comp (S.meshRightAlmostSplitAt ↑z).decomposition.hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.π (fun (j : (S.meshRightAlmostSplitAt ↑z).index.obj) => S.almostSplitSkeleton.obj ((S.meshRightAlmostSplitAt ↑z).label j)) t) h)) = CategoryTheory.CategoryStruct.comp (arrowMap ((S.rightMeshSourceIndexEquiv H z) t).snd) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) h)

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.hom_meshRightMiddle_to_rightTranslation_eq_zero {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [IsAlgClosed k] (H : S.HasAcyclicNonzeroNonisomorphisms) (z : { z : Fin S.n // ¬CategoryTheory.Projective (S.fgObj z) }) (f : (S.meshRightAlmostSplitAt ↑z).middle ⟶ S.fgObj (S.rightTranslationLabel z)) : f = 0

The displayed middle at z has no nonzero map back to tau z. This version uses the uniform mesh middle, before simplifying it to the chosen nonprojective almost-split middle.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.rightMeshSourceMap_not_isSplitMono {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [IsAlgClosed k] (H : S.HasAcyclicNonzeroNonisomorphisms) (arrowMap : {i j : Fin S.n} → S.MeshArrow i j → (S.almostSplitSkeleton.obj j ⟶ S.almostSplitSkeleton.obj i)) (z : { z : Fin S.n // ¬CategoryTheory.Projective (S.fgObj z) }) : ¬CategoryTheory.IsSplitMono (S.rightMeshSourceMap H (fun {i j : Fin S.n} => arrowMap) z)

In particular, the recursively assembled source map at a nonprojective mesh is never split monic.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.exists_rightMeshSourceMap_factor {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [IsAlgClosed k] (H : S.HasAcyclicNonzeroNonisomorphisms) (arrowMap : {i j : Fin S.n} → S.MeshArrow i j → (S.almostSplitSkeleton.obj j ⟶ S.almostSplitSkeleton.obj i)) (z : { z : Fin S.n // ¬CategoryTheory.Projective (S.fgObj z) }) (i : S.almostSplitSkeleton.obj (S.rightTranslationLabel z) ⟶ (S.meshRightAlmostSplitAt ↑z).middle) (hfull : ∀ y < ↑z, ∀ (f : S.almostSplitSkeleton.obj (S.rightTranslationLabel z) ⟶ S.almostSplitSkeleton.obj y), ∃ (p : LinearPathCategory.obj k (Fin S.n) (S.rightTranslationLabel z) ⟶ LinearPathCategory.obj k (Fin S.n) y), (LinearPathCategory.lift S.almostSplitSkeleton.obj fun {i j : Fin S.n} => arrowMap).map p = f) : ∃ (r : (S.meshRightAlmostSplitAt ↑z).middle ⟶ (S.meshRightAlmostSplitAt ↑z).middle), CategoryTheory.CategoryStruct.comp (S.rightMeshSourceMap H (fun {i j : Fin S.n} => arrowMap) z) r = i

Fullness at the strict predecessors of z makes every map from tau z to the displayed middle factor through the assembled source map. This is Ringel's first-arrow matrix argument, with the total outgoing-arrow family reindexed by the displayed middle occurrences.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.minimalToMeshRightMiddleIso {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (z : { z : Fin S.n // ¬CategoryTheory.Projective (S.fgObj z) }) : (S.minimalRightAlmostSplitAt ↑z).middle ≅ (S.meshRightAlmostSplitAt ↑z).middle

The canonical identification from the chosen nonprojective right-almost-split middle to the uniform displayed mesh middle.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.meshRightKernelMap {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (z : { z : Fin S.n // ¬CategoryTheory.Projective (S.fgObj z) }) : S.fgObj (S.rightTranslationLabel z) ⟶ (S.meshRightAlmostSplitAt ↑z).middle

The actual kernel inclusion, transported to the uniform displayed mesh middle used at both projective and nonprojective vertices.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.meshRightSinkMap {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (z : { z : Fin S.n // ¬CategoryTheory.Projective (S.fgObj z) }) : (S.meshRightAlmostSplitAt ↑z).middle ⟶ S.fgObj ↑z

The chosen nonprojective right almost-split sink, transported out of the uniform displayed mesh middle.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.meshRightSinkMap_rightAlmostSplit {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (z : { z : Fin S.n // ¬CategoryTheory.Projective (S.fgObj z) }) : QuotientSubmoduleEquidistribution.IsRightAlmostSplit (S.meshRightSinkMap z)

The transported displayed sink remains right almost split.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.meshRightKernelMap_leftAlmostSplit {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (z : { z : Fin S.n // ¬CategoryTheory.Projective (S.fgObj z) }) : QuotientSubmoduleEquidistribution.IsLeftAlmostSplit (S.meshRightKernelMap z)

The transported kernel inclusion remains left almost split.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.meshRightKernelMap_leftMinimal {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (z : { z : Fin S.n // ¬CategoryTheory.Projective (S.fgObj z) }) : QuotientSubmoduleEquidistribution.IsLeftMinimal (S.meshRightKernelMap z)

The transported kernel inclusion remains left minimal.

@[simp]

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.meshRightKernelMap_comp_map {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (z : { z : Fin S.n // ¬CategoryTheory.Projective (S.fgObj z) }) : CategoryTheory.CategoryStruct.comp (S.meshRightKernelMap z) (S.meshRightSinkMap z) = 0

The transported kernel inclusion followed by the displayed sink map is zero.

@[simp]

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.meshRightKernelMap_comp_map_assoc {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (z : { z : Fin S.n // ¬CategoryTheory.Projective (S.fgObj z) }) {Z : FinitelyGeneratedCategory A} (h : S.fgObj ↑z ⟶ Z) : CategoryTheory.CategoryStruct.comp (S.meshRightKernelMap z) (CategoryTheory.CategoryStruct.comp (S.meshRightSinkMap z) h) = CategoryTheory.CategoryStruct.comp 0 h

The transported kernel inclusion followed by the displayed sink map is zero.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.exists_comp_meshRightKernelMap_eq_of_comp_meshRightSinkMap_eq_zero {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (z : { z : Fin S.n // ¬CategoryTheory.Projective (S.fgObj z) }) {X : FGModuleCat Aᵐᵒᵖ} (q : X ⟶ (S.meshRightAlmostSplitAt ↑z).middle) (hq : CategoryTheory.CategoryStruct.comp q (S.meshRightSinkMap z) = 0) : ∃ (t : X ⟶ S.fgObj (S.rightTranslationLabel z)), CategoryTheory.CategoryStruct.comp t (S.meshRightKernelMap z) = q

The transported AR kernel has the literal kernel factorization property against the transported displayed sink.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.exists_comp_rightMeshSourceMap_eq_of_normalization {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [IsAlgClosed k] (H : S.HasAcyclicNonzeroNonisomorphisms) (arrowMap : {i j : Fin S.n} → S.MeshArrow i j → (S.almostSplitSkeleton.obj j ⟶ S.almostSplitSkeleton.obj i)) (z : { z : Fin S.n // ¬CategoryTheory.Projective (S.fgObj z) }) (e : (S.meshRightAlmostSplitAt ↑z).middle ≅ (S.meshRightAlmostSplitAt ↑z).middle) (he : CategoryTheory.CategoryStruct.comp (S.meshRightKernelMap z) e.hom = S.rightMeshSourceMap H (fun {i j : Fin S.n} => arrowMap) z) {X : FGModuleCat Aᵐᵒᵖ} (q : X ⟶ (S.meshRightAlmostSplitAt ↑z).middle) (hq : CategoryTheory.CategoryStruct.comp q (CategoryTheory.CategoryStruct.comp e.inv (S.meshRightSinkMap z)) = 0) : ∃ (t : X ⟶ S.fgObj (S.rightTranslationLabel z)), CategoryTheory.CategoryStruct.comp t (S.rightMeshSourceMap H (fun {i j : Fin S.n} => arrowMap) z) = q

Once an automorphism identifies the actual AR kernel with an assembled source map, the latter is the literal kernel of the correspondingly twisted sink.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.exists_rightMesh_normalization {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [IsAlgClosed k] (H : S.HasAcyclicNonzeroNonisomorphisms) (arrowMap : {i j : Fin S.n} → S.MeshArrow i j → (S.almostSplitSkeleton.obj j ⟶ S.almostSplitSkeleton.obj i)) (z : { z : Fin S.n // ¬CategoryTheory.Projective (S.fgObj z) }) (hfull : ∀ y < ↑z, ∀ (f : S.almostSplitSkeleton.obj (S.rightTranslationLabel z) ⟶ S.almostSplitSkeleton.obj y), ∃ (p : LinearPathCategory.obj k (Fin S.n) (S.rightTranslationLabel z) ⟶ LinearPathCategory.obj k (Fin S.n) y), (LinearPathCategory.lift S.almostSplitSkeleton.obj fun {i j : Fin S.n} => arrowMap).map p = f) : ∃ (e : (S.meshRightAlmostSplitAt ↑z).middle ≅ (S.meshRightAlmostSplitAt ↑z).middle), CategoryTheory.CategoryStruct.comp (S.meshRightKernelMap z) e.hom = S.rightMeshSourceMap H (fun {i j : Fin S.n} => arrowMap) z ∧ CategoryTheory.CategoryStruct.comp (S.rightMeshSourceMap H (fun {i j : Fin S.n} => arrowMap) z) (CategoryTheory.CategoryStruct.comp e.inv (S.meshRightSinkMap z)) = 0

Ringel's normalization step at a nonprojective vertex. Fullness below z compares the recursively assembled source map with the actual AR kernel inclusion. A finite-length automorphism of the displayed middle then makes the mesh relation literal after twisting the displayed sink map.