Magnitude conjecture

MagnitudeConjecture.Algebra.RightModuleTranslation

Auslander--Reiten translation on the finite right-module skeleton #

The kernel of the chosen minimal right almost-split map defines translation from nonprojective to noninjective labels. Injectivity follows from uniqueness of minimal left almost-split maps. Surjectivity follows from the dual cokernel construction at every noninjective label and uniqueness of minimal right almost-split maps.

source
theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.chosenRight_kernel_ar_sequence {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 (CategoryTheory.Limits.kernel.ι (S.minimalRightAlmostSplitAt ↑z).map) ∧ QuotientSubmoduleEquidistribution.IsLeftMinimal (CategoryTheory.Limits.kernel.ι (S.minimalRightAlmostSplitAt ↑z).map) ∧ QuotientSubmoduleEquidistribution.Foundation.IsIndecomposableModule Aᵐᵒᵖ ↑(CategoryTheory.Limits.kernel (S.minimalRightAlmostSplitAt ↑z).map) ∧ ¬CategoryTheory.Injective (CategoryTheory.Limits.kernel (S.minimalRightAlmostSplitAt ↑z).map)

The chosen right almost-split map at a nonprojective label has an indecomposable noninjective kernel.

source
noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.rightTranslationLabel {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) }) :
Fin S.n

Skeleton label of the kernel of the chosen nonprojective right almost-split map.

Instances For
    source
    noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.rightTranslationKernelIso {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.Limits.kernel (S.minimalRightAlmostSplitAt ↑z).map ≅ S.fgObj (S.rightTranslationLabel z)

    The chosen kernel-to-skeleton isomorphism.

    Instances For
      source
      noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.rightTranslation {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 : Fin S.n // ¬CategoryTheory.Injective (S.fgObj x) }

      Auslander--Reiten translation from nonprojective to noninjective selected labels.

      Instances For
        source
        theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.rightTranslation_injective {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) :
        Function.Injective S.rightTranslation

        Equality of translation labels identifies the original nonprojective endpoints.

        source
        theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.rightTranslation_surjective {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) :
        Function.Surjective S.rightTranslation

        Every noninjective selected label is the translate of a nonprojective selected label.

        source
        noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.rightTranslationEquiv {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) :
        { z : Fin S.n // ¬CategoryTheory.Projective (S.fgObj z) } ≃ { x : Fin S.n // ¬CategoryTheory.Injective (S.fgObj x) }

        Auslander--Reiten translation is an equivalence between nonprojective and noninjective selected labels.

        Instances For