Magnitude conjecture

MagnitudeConjecture.Algebra.RightModuleStandardFormUniversalRealization

Realization of the normalized standard-form universal cover #

The two-sided Bongartz--Gabriel normalization assigns an irreducible module morphism to every reversed universal-cover arrow and makes every realized mesh composite literally zero. Here that assignment is extended to the free linear path category and descended through the ordinary mesh ideal.

source
@[instance_reducible]
def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversalRealizationQuiverInstance {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) :
Quiver (Fin S.n)
Instances For
    source
    @[instance_reducible]
    noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversalRealizationArrowFintype {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) :
    Fintype (x ⟶ y)
    Instances For
      source
      @[instance_reducible]
      noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversalRealizationBaseStarFintype {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x : Fin S.n) :
      Fintype (Quiver.Star x)
      Instances For
        source
        @[instance_reducible]
        noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversalRealizationStarFintype {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x₀ : Fin S.n) (W : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀) :
        Fintype (Quiver.Star W)
        Instances For
          source
          theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversalNormalized_lift_map_meshRelation {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x₀ : Fin S.n) (W : { W : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀ // W ∉ MeshCategory.RightMeshData.UniversalCover.projectiveSet S.standardFormRightMeshData x₀ }) :
          (LinearPathCategory.lift (S.standardFormUniversalObj x₀) fun {i j : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀} => S.standardFormUniversalNormalizedArrowMap x₀).map ((MeshCategory.RightMeshData.UniversalCover.rightMeshData S.standardFormRightMeshData x₀).meshRelation W) = CategoryTheory.CategoryStruct.comp (S.standardFormUniversalRealizedSource x₀ (fun {W Z : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀} => S.standardFormUniversalNormalizedArrowMap x₀) W) (S.standardFormUniversalRealizedSink x₀ (fun {W Z : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀} => S.standardFormUniversalNormalizedArrowMap x₀) ↑W)

          The free linear path realization sends a lifted mesh relation to the composite of its reassembled normalized source and sink.

          source
          theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversalNormalized_lift_map_meshRelation_zero {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x₀ : Fin S.n) (W : { W : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀ // W ∉ MeshCategory.RightMeshData.UniversalCover.projectiveSet S.standardFormRightMeshData x₀ }) :
          (LinearPathCategory.lift (S.standardFormUniversalObj x₀) fun {i j : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀} => S.standardFormUniversalNormalizedArrowMap x₀).map ((MeshCategory.RightMeshData.UniversalCover.rightMeshData S.standardFormRightMeshData x₀).meshRelation W) = 0

          The normalized free realization kills every lifted mesh relation.

          source
          noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversalRealization {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x₀ : Fin S.n) :
          MeshCategory.Realization (MeshCategory.RightMeshData.UniversalCover.rightMeshData S.standardFormRightMeshData x₀) (S.standardFormUniversalObj x₀)

          The normalized arrow assignment as a realization of the ordinary mesh category of the standard-form universal cover.

          Instances For
            source
            @[reducible, inline]
            noncomputable abbrev MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversalMeshFunctor {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x₀ : Fin S.n) :
            CategoryTheory.Functor (MeshCategory.RawCategory (MeshCategory.RightMeshData.UniversalCover.rightMeshData S.standardFormRightMeshData x₀)) (FGModuleCat Aᵐᵒᵖ)

            The induced linear functor from the raw universal-cover mesh category to finitely generated right modules.

            Instances For
              source
              @[simp]
              theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversalRealization_freeFunctor_map_arrow {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x₀ : Fin S.n) {Y Z : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀} (a : Y ⟶ Z) :
              (S.standardFormUniversalRealization x₀).freeFunctor.map (LinearPathCategory.pathHom a.toPath) = S.standardFormUniversalNormalizedArrowMap x₀ a

              The free realization sends a one-arrow path to its chosen normalized irreducible representative.

              source
              @[simp]
              theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversalMeshFunctor_map_arrow {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x₀ : Fin S.n) {Y Z : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀} (a : Y ⟶ Z) :
              (S.standardFormUniversalMeshFunctor x₀).map ((MeshCategory.quotientFunctor (MeshCategory.RightMeshData.UniversalCover.rightMeshData S.standardFormRightMeshData x₀)).map (LinearPathCategory.pathHom a.toPath)) = S.standardFormUniversalNormalizedArrowMap x₀ a

              The descended mesh functor has the same value on each represented universal-cover arrow.

              source
              theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversalMeshFunctor_map_arrow_isIrreducible {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x₀ : Fin S.n) {Y Z : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀} (a : Y ⟶ Z) :
              QuotientSubmoduleEquidistribution.IsIrreducibleMorphism ((S.standardFormUniversalMeshFunctor x₀).map ((MeshCategory.quotientFunctor (MeshCategory.RightMeshData.UniversalCover.rightMeshData S.standardFormRightMeshData x₀)).map (LinearPathCategory.pathHom a.toPath)))

              In particular, every represented mesh-category arrow is sent to an irreducible module morphism.

              source
              theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversalNormalizedRealizedSink_isRightAlmostSplit {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x₀ : Fin S.n) (W : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀) :
              QuotientSubmoduleEquidistribution.IsRightAlmostSplit (S.standardFormUniversalRealizedSink x₀ (fun {W Z : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀} => S.standardFormUniversalNormalizedArrowMap x₀) W)

              At every lifted vertex, including projective boundary vertices, the normalized incoming components reassemble to a right almost-split sink.

              source
              theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversalNormalizedRealizedSink_isRightMinimal {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x₀ : Fin S.n) (W : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀) :
              QuotientSubmoduleEquidistribution.IsRightMinimal (S.standardFormUniversalRealizedSink x₀ (fun {W Z : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀} => S.standardFormUniversalNormalizedArrowMap x₀) W)

              The normalized incoming sink is also right minimal at every lifted vertex. This is the second half of the local Auslander--Reiten datum used when comparing its kernel with the normalized mesh source.

              source
              theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversalNormalizedRealizedSource_isLeftAlmostSplit {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x₀ : Fin S.n) (W : { W : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀ // W ∉ MeshCategory.RightMeshData.UniversalCover.projectiveSet S.standardFormRightMeshData x₀ }) :
              QuotientSubmoduleEquidistribution.IsLeftAlmostSplit (S.standardFormUniversalRealizedSource x₀ (fun {W Z : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀} => S.standardFormUniversalNormalizedArrowMap x₀) W)

              At a nonprojective lifted vertex, the normalized mesh source remains left almost split.

              source
              theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversalNormalizedRealizedSource_isLeftMinimal {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x₀ : Fin S.n) (W : { W : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀ // W ∉ MeshCategory.RightMeshData.UniversalCover.projectiveSet S.standardFormRightMeshData x₀ }) :
              QuotientSubmoduleEquidistribution.IsLeftMinimal (S.standardFormUniversalRealizedSource x₀ (fun {W Z : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀} => S.standardFormUniversalNormalizedArrowMap x₀) W)

              At a nonprojective lifted vertex, the normalized mesh source remains left minimal.

              source
              def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.FGIndecCategory {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : FiniteIndecomposableSkeleton k A) :
              Type

              The full category on the chosen finite skeleton, bundled inside the literal finitely generated module category. This is a definition rather than an abbreviation so that its induced category structure remains distinct from the quiver structure on the same finite label type.

              Instances For
                source
                @[instance_reducible]
                noncomputable instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.fgIndecCategoryCategory {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : FiniteIndecomposableSkeleton k A) :
                CategoryTheory.Category.{u, 0} S.FGIndecCategory
                source
                @[instance_reducible]
                noncomputable instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.fgIndecCategoryPreadditive {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : FiniteIndecomposableSkeleton k A) :
                CategoryTheory.Preadditive S.FGIndecCategory
                source
                @[instance_reducible]
                noncomputable instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.fgIndecCategoryLinear {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : FiniteIndecomposableSkeleton k A) :
                CategoryTheory.Linear k S.FGIndecCategory
                source
                noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversalIndecMeshFunctor {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x₀ : Fin S.n) :
                CategoryTheory.Functor (MeshCategory.RawCategory (MeshCategory.RightMeshData.UniversalCover.rightMeshData S.standardFormRightMeshData x₀)) S.FGIndecCategory

                The same universal mesh realization, with its codomain corestricted to the finite skeletal category of indecomposable finitely generated modules. This is the precise codomain in Riedtmann's covering theorem.

                Instances For
                  source
                  instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversalIndecMeshFunctor_additive {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x₀ : Fin S.n) :
                  (S.standardFormUniversalIndecMeshFunctor x₀).Additive
                  source
                  instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversalIndecMeshFunctor_linear {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x₀ : Fin S.n) :
                  CategoryTheory.Functor.Linear k (S.standardFormUniversalIndecMeshFunctor x₀)
                  source
                  @[simp]
                  theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversalIndecMeshFunctor_map_arrow {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x₀ : Fin S.n) {Y Z : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀} (a : Y ⟶ Z) :
                  ((S.standardFormUniversalIndecMeshFunctor x₀).map ((MeshCategory.quotientFunctor (MeshCategory.RightMeshData.UniversalCover.rightMeshData S.standardFormRightMeshData x₀)).map (LinearPathCategory.pathHom a.toPath))).hom = S.standardFormUniversalNormalizedArrowMap x₀ a

                  Corestriction does not alter the represented normalized arrow map.