Magnitude conjecture

MagnitudeConjecture.Algebra.RightModuleRepresentationFiniteSquareFree

Square-freeness of a representation-finite module category #

Riedtmann, Section 3.5, proves that over an algebraically closed field the irreducible quotient between two indecomposable modules of a representation-finite algebra has dimension at most one. The proof uses two facts already available here: irreducible maps are monic or epic, and an almost-split mesh containing two copies of one indecomposable forces strict dimension growth after translation.

Rather than construct an infinite alternating translation chain, we choose a multiple-arrow pair of maximal endpoint dimension. The Riedtmann step produces another multiple-arrow pair with strictly larger endpoint dimension, which is impossible because the selected indecomposable skeleton is finite.

source
noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.objectFinrank {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : FiniteIndecomposableSkeleton k A) (x : Fin S.n) :
ℕ

Coefficient-field dimension of one selected indecomposable module.

Instances For
    source
    def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.homRestrictScalars {k A : Type u} [Field k] [Ring A] [Algebra k A] {X Y : FinitelyGeneratedCategory A} (f : X ⟶ Y) :
    ↑X →ₗ[k] ↑Y

    Restrict a morphism of finitely generated right modules to a k-linear map on the same underlying function.

    Instances For
      source
      @[simp]
      theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.homRestrictScalars_apply {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {X Y : FinitelyGeneratedCategory A} (f : X ⟶ Y) (x : ↑X) :
      (homRestrictScalars f) x = (ModuleCat.Hom.hom f.hom) x
      source
      theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.objectFinrank_lt_of_irreducible_mono {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {x y : Fin S.n} (f : S.fgObj x ⟶ S.fgObj y) (hf : QuotientSubmoduleEquidistribution.IsIrreducibleMorphism f) [CategoryTheory.Mono f] :
      S.objectFinrank x < S.objectFinrank y

      A monic irreducible map between selected indecomposables strictly raises coefficient-field dimension.

      source
      theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.objectFinrank_lt_of_irreducible_epi {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {x y : Fin S.n} (f : S.fgObj x ⟶ S.fgObj y) (hf : QuotientSubmoduleEquidistribution.IsIrreducibleMorphism f) [CategoryTheory.Epi f] :
      S.objectFinrank y < S.objectFinrank x

      An epic irreducible map between selected indecomposables strictly lowers coefficient-field dimension.

      source
      noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormOccurrenceInclusion {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {x y : Fin S.n} (a : S.StandardFormArrow x y) :
      S.fgObj y ⟶ (S.finiteTauCategoryData.rightMesh (S.fgObj x)).X₂

      Inclusion of the occurrence represented by one standard-form arrow into the chosen right-mesh middle term.

      Instances For
        source
        noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormOccurrenceProjection {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {x y : Fin S.n} (a : S.StandardFormArrow x y) :
        (S.finiteTauCategoryData.rightMesh (S.fgObj x)).X₂ ⟶ S.fgObj y

        Projection from the chosen right-mesh middle term onto one represented standard-form occurrence.

        Instances For
          source
          @[simp]
          theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormOccurrenceInclusion_projection {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {x y : Fin S.n} (a : S.StandardFormArrow x y) :
          CategoryTheory.CategoryStruct.comp (S.standardFormOccurrenceInclusion a) (S.standardFormOccurrenceProjection a) = CategoryTheory.CategoryStruct.id (S.fgObj y)
          source
          @[simp]
          theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormOccurrenceInclusion_projection_assoc {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {x y : Fin S.n} (a : S.StandardFormArrow x y) {Z : FinitelyGeneratedCategory A} (h : S.fgObj y ⟶ Z) :
          CategoryTheory.CategoryStruct.comp (S.standardFormOccurrenceInclusion a) (CategoryTheory.CategoryStruct.comp (S.standardFormOccurrenceProjection a) h) = h
          source
          theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormArrowOccurrenceEquiv_fst_ne {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {x y : Fin S.n} {a b : S.StandardFormArrow x y} (hab : a ≠ b) :
          ↑((S.standardFormArrowOccurrenceEquiv x y) a) ≠ ↑((S.standardFormArrowOccurrenceEquiv x y) b)

          Distinct parallel standard-form arrows represent distinct middle-term indices.

          source
          @[simp]
          theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormOccurrenceInclusion_projection_ne {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {x y : Fin S.n} {a b : S.StandardFormArrow x y} (hab : a ≠ b) :
          CategoryTheory.CategoryStruct.comp (S.standardFormOccurrenceInclusion a) (S.standardFormOccurrenceProjection b) = 0
          source
          @[simp]
          theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormOccurrenceInclusion_projection_ne_assoc {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {x y : Fin S.n} {a b : S.StandardFormArrow x y} (hab : a ≠ b) {Z : FinitelyGeneratedCategory A} (h : S.fgObj y ⟶ Z) :
          CategoryTheory.CategoryStruct.comp (S.standardFormOccurrenceInclusion a) (CategoryTheory.CategoryStruct.comp (S.standardFormOccurrenceProjection b) h) = CategoryTheory.CategoryStruct.comp 0 h
          source
          @[simp]
          theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormOccurrenceProjection_apply_inclusion {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {x y : Fin S.n} (a : S.StandardFormArrow x y) (v : ↑(S.fgObj y)) :
          (ModuleCat.Hom.hom (S.standardFormOccurrenceProjection a).hom) ((ModuleCat.Hom.hom (S.standardFormOccurrenceInclusion a).hom) v) = v
          source
          @[simp]
          theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormOccurrenceProjection_apply_inclusion_ne {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {x y : Fin S.n} {a b : S.StandardFormArrow x y} (hab : a ≠ b) (v : ↑(S.fgObj y)) :
          (ModuleCat.Hom.hom (S.standardFormOccurrenceProjection b).hom) ((ModuleCat.Hom.hom (S.standardFormOccurrenceInclusion a).hom) v) = 0
          source
          noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.duplicateOccurrenceLinearMap {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {x y : Fin S.n} (a b : S.StandardFormArrow x y) :
          ↑(S.fgObj y) × ↑(S.fgObj y) →ₗ[k] ↑(S.finiteTauCategoryData.rightMesh (S.fgObj x)).X₂

          Two distinct occurrences of the same indecomposable define the explicit injective coefficient-field map from two copies into the mesh middle term.

          Instances For
            source
            theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.duplicateOccurrenceLinearMap_injective {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {x y : Fin S.n} {a b : S.StandardFormArrow x y} (hab : a ≠ b) :
            Function.Injective ⇑(S.duplicateOccurrenceLinearMap a b)

            The two-occurrence map is injective because the two displayed projections recover its two coordinates.

            source
            theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.two_mul_objectFinrank_le_rightMiddle {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x y : Fin S.n) (hxy : 2 ≤ FiniteTauMatrix.arrowMultiplicity S.finiteTauCategoryData.toFiniteRightTauCategoryData y x) :
            2 * S.objectFinrank y ≤ Module.finrank k ↑(S.finiteTauCategoryData.rightMesh (S.fgObj x)).X₂

            If an endpoint mesh contains at least two copies of y, twice the dimension of y is bounded by the dimension of the middle term.

            source
            theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.rightMesh_finrank_eq_translation_add_endpoint {k A : Type u} [Field k] [IsAlgClosed 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) }) :
            Module.finrank k ↑(S.finiteTauCategoryData.rightMesh (S.fgObj ↑z)).X₂ = S.objectFinrank ↑(S.rightTranslationEquiv z) + S.objectFinrank ↑z

            Coefficient-field dimensions are additive across the selected ambient Auslander--Reiten sequence.

            source
            theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.exists_multipleArrow_pair_of_multipleArrow {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x y : Fin S.n) (hxy : 2 ≤ FiniteTauMatrix.arrowMultiplicity S.finiteTauCategoryData.toFiniteRightTauCategoryData x y) :
            ∃ (x' : Fin S.n) (y' : Fin S.n), 2 ≤ FiniteTauMatrix.arrowMultiplicity S.finiteTauCategoryData.toFiniteRightTauCategoryData x' y' ∧ max (S.objectFinrank x) (S.objectFinrank y) < max (S.objectFinrank x') (S.objectFinrank y')

            A pair carrying at least two parallel irreducible maps produces another such pair with strictly larger maximal endpoint dimension. This is the dimension-growth step in Riedtmann's square-freeness argument.

            source
            theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.arrowMultiplicity_le_one {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x y : Fin S.n) :
            FiniteTauMatrix.arrowMultiplicity S.finiteTauCategoryData.toFiniteRightTauCategoryData x y ≤ 1

            Between two selected indecomposable modules of a representation-finite algebra over an algebraically closed field, the numerical irreducible-arrow multiplicity is at most one.

            source
            theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormArrow_subsingleton {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x y : Fin S.n) :
            Subsingleton (S.StandardFormArrow x y)

            The standard-form reversed AR quiver has at most one arrow between any ordered pair of vertices.