Two-sided tau-data assembly for finite right-module categories

This file makes the modulewise mesh choices canonical on the selected indecomposable objects, identifies the nonzero mesh boundaries with the nonprojective and noninjective labels, and assembles the two-sided translation data required by the generic finite tau-category interface.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.canonicalRightMesh {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (X : FinitelyGeneratedCategory A) : CategoryTheory.ShortComplex (FinitelyGeneratedCategory A)

Use the literal selected-label right mesh whenever the supplied module is one of the selected indecomposables, and the componentwise construction otherwise.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.canonicalRightTermIso {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (X : FinitelyGeneratedCategory A) : (S.canonicalRightMesh X).X₃ ≅ X

The canonical right mesh has the supplied module as right endpoint.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.canonicalRightTau {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (X : FinitelyGeneratedCategory A) : QuotientSubmoduleEquidistribution.Iyama.RightTauSequence (S.canonicalRightMesh X)

Every canonical right mesh is a right tau-sequence.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.canonicalRightMesh_at_label {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x : Fin S.n) : S.canonicalRightMesh (S.fgObj x) = S.labelRightMesh x

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

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.canonicalLeftMesh {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (X : FinitelyGeneratedCategory A) : CategoryTheory.ShortComplex (FinitelyGeneratedCategory A)

Use the literal selected-label left mesh whenever the supplied module is one of the selected indecomposables, and the componentwise construction otherwise.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.canonicalLeftTermIso {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (X : FinitelyGeneratedCategory A) : (S.canonicalLeftMesh X).X₁ ≅ X

The canonical left mesh has the supplied module as left endpoint.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.canonicalLeftTau {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (X : FinitelyGeneratedCategory A) : QuotientSubmoduleEquidistribution.Iyama.LeftTauSequence (S.canonicalLeftMesh X)

Every canonical left mesh is a left tau-sequence.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.canonicalLeftMesh_at_label {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x : Fin S.n) : S.canonicalLeftMesh (S.fgObj x) = S.labelLeftMesh x

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

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.labelRightMesh_X₁_isZero_iff_projective {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x : Fin S.n) : CategoryTheory.Limits.IsZero (S.labelRightMesh x).X₁ ↔ CategoryTheory.Projective (S.fgObj x)

The first term of a selected right mesh is zero exactly at a projective label.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.labelLeftMesh_X₃_isZero_iff_injective {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x : Fin S.n) : CategoryTheory.Limits.IsZero (S.labelLeftMesh x).X₃ ↔ CategoryTheory.Injective (S.fgObj x)

The third term of a selected left mesh is zero exactly at an injective label.

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.canonicalRightNonzeroEquivNonprojective {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) : { x : Fin S.n // ¬CategoryTheory.Limits.IsZero (S.canonicalRightMesh (S.fgObj x)).X₁ } ≃ { x : Fin S.n // ¬CategoryTheory.Projective (S.fgObj x) }

Nonzero first terms of the canonical right meshes are exactly the nonprojective selected labels.

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.canonicalLeftNonzeroEquivNoninjective {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) : { x : Fin S.n // ¬CategoryTheory.Limits.IsZero (S.canonicalLeftMesh (S.fgObj x)).X₃ } ≃ { x : Fin S.n // ¬CategoryTheory.Injective (S.fgObj x) }

Nonzero third terms of the canonical left meshes are exactly the noninjective selected labels.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.canonicalTauPlusEquiv {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) : { x : Fin S.n // ¬CategoryTheory.Limits.IsZero (S.canonicalRightMesh (S.fgObj x)).X₁ } ≃ { x : Fin S.n // ¬CategoryTheory.Limits.IsZero (S.canonicalLeftMesh (S.fgObj x)).X₃ }

Translation on the nonzero boundaries of the canonical module meshes.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.eqToHom_comp_dependent_morphism {C : Type u} [CategoryTheory.Category.{u_2, u} C] {J : Type u_1} (X Y : J → C) (f : (j : J) → X j ⟶ Y j) {i j : J} (h : i = j) : CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (f j) = CategoryTheory.CategoryStruct.comp (f i) (CategoryTheory.eqToHom ⋯)

Transporting both endpoints of a dependent family of morphisms commutes with the family morphism.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.dependent_iso_hom_naturality {C : Type u} [CategoryTheory.Category.{u_2, u} C] {J : Type u_1} (X Y : J → C) (e : (j : J) → X j ≅ Y j) {i j : J} (h : i = j) : CategoryTheory.CategoryStruct.comp (e i).hom (CategoryTheory.eqToHom ⋯) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (e j).hom

A dependent family of isomorphisms commutes with equality transport.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.nonprojectiveRightMeshIso_labelLeftMesh {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.nonprojectiveRightMesh z ≅ S.labelLeftMesh ↑(S.rightTranslationEquiv z)

A nonprojective right mesh is the left mesh at its Auslander--Reiten translate.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.canonicalTauPlusEquiv_val {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (X : { x : Fin S.n // ¬CategoryTheory.Limits.IsZero (S.canonicalRightMesh (S.fgObj x)).X₁ }) : ↑(S.canonicalTauPlusEquiv X) = ↑(S.rightTranslationEquiv (S.canonicalRightNonzeroEquivNonprojective X))

The canonical translation has the same underlying label as the Auslander--Reiten translation after identifying its source boundary.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.canonicalRightLeftMeshIso {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (X : { x : Fin S.n // ¬CategoryTheory.Limits.IsZero (S.canonicalRightMesh (S.fgObj x)).X₁ }) : S.canonicalRightMesh (S.fgObj ↑X) ≅ S.canonicalLeftMesh (S.fgObj ↑(S.canonicalTauPlusEquiv X))

The canonical right mesh at a nonzero boundary agrees with the canonical left mesh at its translated boundary.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.tauInput {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) : TauInput S

The two-sided tau-category input constructed from a finite indecomposable skeleton of finitely generated right modules.

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

The finite tau-category carried by a finite indecomposable skeleton of finitely generated right modules.