Two-sided tau-data assembly for literal finite-module factor categories

The right and left factor meshes are made canonical on surviving selected indecomposables. The remaining declarations identify their nonzero boundaries by restricting the ambient Auslander--Reiten translation and map the ambient mesh isomorphisms through the literal quotient.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.canonicalFactorRightMesh {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (K : Set (Fin S.n)) (X : S.FactorCategory K) : CategoryTheory.ShortComplex (S.FactorCategory K)

Use the literal surviving-label right mesh on a selected factor object and the componentwise construction otherwise.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.canonicalFactorRightTermIso {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (K : Set (Fin S.n)) (X : S.FactorCategory K) : (S.canonicalFactorRightMesh K X).X₃ ≅ X

The canonical factor right mesh ends at the supplied object.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.canonicalFactorRightTau {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (K : Set (Fin S.n)) (X : S.FactorCategory K) : QuotientSubmoduleEquidistribution.Iyama.RightTauSequence (S.canonicalFactorRightMesh K X)

Every canonical factor right mesh is a right tau-sequence.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.canonicalFactorRightMesh_at_label {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (K : Set (Fin S.n)) (x : S.SurvivingLabel K) : S.canonicalFactorRightMesh K (S.factorObject K x) = S.factorLabelRightMesh K x

On a surviving selected object, the canonical factor right mesh is its literal label mesh.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.canonicalFactorLeftMesh {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (K : Set (Fin S.n)) (X : S.FactorCategory K) : CategoryTheory.ShortComplex (S.FactorCategory K)

Use the literal surviving-label left mesh on a selected factor object and the componentwise construction otherwise.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.canonicalFactorLeftTermIso {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (K : Set (Fin S.n)) (X : S.FactorCategory K) : (S.canonicalFactorLeftMesh K X).X₁ ≅ X

The canonical factor left mesh starts at the supplied object.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.canonicalFactorLeftTau {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (K : Set (Fin S.n)) (X : S.FactorCategory K) : QuotientSubmoduleEquidistribution.Iyama.LeftTauSequence (S.canonicalFactorLeftMesh K X)

Every canonical factor left mesh is a left tau-sequence.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.canonicalFactorLeftMesh_at_label {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (K : Set (Fin S.n)) (x : S.SurvivingLabel K) : S.canonicalFactorLeftMesh K (S.factorObject K x) = S.factorLabelLeftMesh K x

On a surviving selected object, the canonical factor left mesh is its literal label mesh.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorRawRightLeftMeshIso {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (K : Set (Fin S.n)) (z : { z : Fin S.n // ¬CategoryTheory.Projective (S.fgObj z) }) : S.factorRawRightMesh K ↑z ≅ S.factorRawLeftMesh K ↑(S.rightTranslationEquiv z)

Mapping the ambient right/left mesh identification through the literal quotient identifies the corresponding raw factor meshes.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorRightBoundary_raw_condition {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (K : Set (Fin S.n)) (X : { x : S.SurvivingLabel K // ¬CategoryTheory.Limits.IsZero (S.canonicalFactorRightMesh K (S.factorObject K x)).X₁ }) : ¬CategoryTheory.Limits.IsZero (S.factorRawRightMesh K ↑↑X).X₁ ∧ (S.factorRawRightMesh K ↑↑X).f ≠ 0

A nonzero canonical factor-right boundary is precisely in the raw branch of the labelwise minimalization.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorLeftBoundary_raw_condition {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (K : Set (Fin S.n)) (Y : { y : S.SurvivingLabel K // ¬CategoryTheory.Limits.IsZero (S.canonicalFactorLeftMesh K (S.factorObject K y)).X₃ }) : ¬CategoryTheory.Limits.IsZero (S.factorRawLeftMesh K ↑↑Y).X₃ ∧ (S.factorRawLeftMesh K ↑↑Y).g ≠ 0

A nonzero canonical factor-left boundary is precisely in the raw branch of the labelwise minimalization.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorRawRightMesh_g_ne_zero {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (K : Set (Fin S.n)) (x : S.SurvivingLabel K) (hsource : ¬CategoryTheory.Limits.IsZero (S.factorRawRightMesh K ↑x).X₁) (hf : (S.factorRawRightMesh K ↑x).f ≠ 0) : (S.factorRawRightMesh K ↑x).g ≠ 0

In a surviving raw right mesh, a nonzero first map forces the second map to remain nonzero.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorRawLeftMesh_f_ne_zero {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (K : Set (Fin S.n)) (y : S.SurvivingLabel K) (htarget : ¬CategoryTheory.Limits.IsZero (S.factorRawLeftMesh K ↑y).X₃) (hg : (S.factorRawLeftMesh K ↑y).g ≠ 0) : (S.factorRawLeftMesh K ↑y).f ≠ 0

In a surviving raw left mesh, a nonzero second map forces the first map to remain nonzero.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorRightBoundaryToLeft {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (K : Set (Fin S.n)) (X : { x : S.SurvivingLabel K // ¬CategoryTheory.Limits.IsZero (S.canonicalFactorRightMesh K (S.factorObject K x)).X₁ }) : { y : S.SurvivingLabel K // ¬CategoryTheory.Limits.IsZero (S.canonicalFactorLeftMesh K (S.factorObject K y)).X₃ }

Restrict ambient positive translation to a nonzero factor-right boundary.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorLeftBoundaryToRight {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (K : Set (Fin S.n)) (Y : { y : S.SurvivingLabel K // ¬CategoryTheory.Limits.IsZero (S.canonicalFactorLeftMesh K (S.factorObject K y)).X₃ }) : { x : S.SurvivingLabel K // ¬CategoryTheory.Limits.IsZero (S.canonicalFactorRightMesh K (S.factorObject K x)).X₁ }

Restrict ambient negative translation to a nonzero factor-left boundary.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorRightBoundaryToLeft_val {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (K : Set (Fin S.n)) (X : { x : S.SurvivingLabel K // ¬CategoryTheory.Limits.IsZero (S.canonicalFactorRightMesh K (S.factorObject K x)).X₁ }) : ∃ (z : { z : Fin S.n // ¬CategoryTheory.Projective (S.fgObj z) }), ↑z = ↑↑X ∧ ↑↑(S.factorRightBoundaryToLeft K X) = ↑(S.rightTranslationEquiv z)

The underlying label of restricted positive factor translation is the ambient positive translation label.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorLeftBoundaryToRight_val {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (K : Set (Fin S.n)) (Y : { y : S.SurvivingLabel K // ¬CategoryTheory.Limits.IsZero (S.canonicalFactorLeftMesh K (S.factorObject K y)).X₃ }) : ∃ (y : { y : Fin S.n // ¬CategoryTheory.Injective (S.fgObj y) }), ↑y = ↑↑Y ∧ ↑↑(S.factorLeftBoundaryToRight K Y) = ↑(S.rightTranslationEquiv.symm y)

The underlying label of restricted negative factor translation is the ambient negative translation label.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorTauPlusEquiv {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (K : Set (Fin S.n)) : { x : S.SurvivingLabel K // ¬CategoryTheory.Limits.IsZero (S.canonicalFactorRightMesh K (S.factorObject K x)).X₁ } ≃ { y : S.SurvivingLabel K // ¬CategoryTheory.Limits.IsZero (S.canonicalFactorLeftMesh K (S.factorObject K y)).X₃ }

Positive and negative translation restrict to mutually inverse equivalences on the nonzero boundaries of the canonical factor meshes.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorRightLeftMeshIso {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (K : Set (Fin S.n)) (X : { x : S.SurvivingLabel K // ¬CategoryTheory.Limits.IsZero (S.canonicalFactorRightMesh K (S.factorObject K x)).X₁ }) : S.canonicalFactorRightMesh K (S.factorObject K ↑X) ≅ S.canonicalFactorLeftMesh K (S.factorObject K ↑((S.factorTauPlusEquiv K) X))

The canonical factor right mesh at a nonzero boundary agrees with the canonical factor left mesh at its restricted translate.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorFiniteTauCategoryData {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (K : Set (Fin S.n)) : QuotientSubmoduleEquidistribution.Iyama.FiniteTauCategoryData (S.FactorCategory K) (S.SurvivingLabel K)

Every literal quotient by selected labels carries compatible two-sided finite tau-category data on its surviving skeleton.