Magnitude conjecture

MagnitudeConjecture.Algebra.RightModuleOrdinaryQuiverUniverseLift

Universe lifting the ordinary quiver #

The bound-quiver presentation bundle is universe-local. The ordinary quiver has a naturally small vertex type, so this file lifts its vertices into the coefficient-field universe without changing arrows, paths, or the free linear path category. The resulting reindexing functor is a linear equivalence.

source
@[reducible, inline]
abbrev MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.OrdinaryLiftedVertex {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : FiniteIndecomposableSkeleton k A) :
Type u

The ordinary-quiver vertex set lifted to the algebra universe.

Instances For
    source
    @[instance_reducible]
    instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.ordinaryLiftedQuiver {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) :
    Quiver S.OrdinaryLiftedVertex

    Universe lifting changes only vertices, not the corresponding arrow spaces.

    source
    @[instance_reducible]
    noncomputable instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.ordinaryLiftedVertexFintype {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : FiniteIndecomposableSkeleton k A) :
    Fintype S.OrdinaryLiftedVertex
    source
    @[instance_reducible]
    noncomputable instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.ordinaryLiftedArrowFintype {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x y : S.OrdinaryLiftedVertex) :
    Fintype (x ⟶ y)
    source
    def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.ordinaryQuiverDownPrefunctor {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) :
    S.OrdinaryLiftedVertex ⥤q S.ProjectiveLabel

    Forget the universe lift on the ordinary quiver.

    Instances For
      source
      def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.ordinaryQuiverUpPrefunctor {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) :
      S.ProjectiveLabel ⥤q S.OrdinaryLiftedVertex

      Lift the vertices of the small ordinary quiver.

      Instances For
        source
        @[simp]
        theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.ordinaryQuiverUpDown_mapPath {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {x y : S.ProjectiveLabel} (p : Quiver.Path x y) :
        S.ordinaryQuiverDownPrefunctor.mapPath (S.ordinaryQuiverUpPrefunctor.mapPath p) = p
        source
        @[simp]
        theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.ordinaryQuiverDownUp_mapPath {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {x y : S.OrdinaryLiftedVertex} (p : Quiver.Path x y) :
        S.ordinaryQuiverUpPrefunctor.mapPath (S.ordinaryQuiverDownPrefunctor.mapPath p) = p
        source
        def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.ordinaryLiftedPathEquiv {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x y : S.OrdinaryLiftedVertex) :
        Quiver.Path x y ≃ Quiver.Path x.down y.down

        The quiver isomorphism gives a bijection between paths with the corresponding endpoints.

        Instances For
          source
          noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.ordinaryLiftedToOrdinary {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) :
          CategoryTheory.Functor (LinearPathCategory.Category k S.OrdinaryLiftedVertex) (LinearPathCategory.Category k S.ProjectiveLabel)

          Reindex the free linear category from lifted ordinary vertices back to the original small vertex set.

          Instances For
            source
            instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.ordinaryLiftedToOrdinary_additive {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) :
            S.ordinaryLiftedToOrdinary.Additive
            source
            instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.ordinaryLiftedToOrdinary_linear {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) :
            CategoryTheory.Functor.Linear k S.ordinaryLiftedToOrdinary
            source
            def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.ordinaryLiftedFunctorPathEquiv {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (X Y : LinearPathCategory.Category k S.OrdinaryLiftedVertex) :
            Quiver.Path (LinearPathCategory.vertex Y) (LinearPathCategory.vertex X) ≃ Quiver.Path (LinearPathCategory.vertex (S.ordinaryLiftedToOrdinary.obj Y)) (LinearPathCategory.vertex (S.ordinaryLiftedToOrdinary.obj X))

            Path reindexing with endpoints stated as the actual images of the free-category functor.

            Instances For
              source
              @[simp]
              theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.ordinaryLiftedToOrdinary_map_pathHom {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {x y : S.OrdinaryLiftedVertex} (p : Quiver.Path x y) :
              S.ordinaryLiftedToOrdinary.map (LinearPathCategory.pathHom p) = LinearPathCategory.pathHom ((S.ordinaryLiftedPathEquiv x y) p)
              source
              noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.ordinaryLiftedHomLinearEquiv {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (X Y : LinearPathCategory.Category k S.OrdinaryLiftedVertex) :
              (X ⟶ Y) ≃ₗ[k] S.ordinaryLiftedToOrdinary.obj X ⟶ S.ordinaryLiftedToOrdinary.obj Y

              Reindexing lifted paths gives a linear equivalence on each actual Hom space of the reindexing functor.

              Instances For
                source
                @[simp]
                theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.ordinaryLiftedHomLinearEquiv_pathHom {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {X Y : LinearPathCategory.Category k S.OrdinaryLiftedVertex} (p : Quiver.Path (LinearPathCategory.vertex Y) (LinearPathCategory.vertex X)) :
                (S.ordinaryLiftedHomLinearEquiv X Y) (LinearPathCategory.pathHom p) = LinearPathCategory.pathHom ((S.ordinaryLiftedFunctorPathEquiv X Y) p)
                source
                theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.ordinaryLiftedToOrdinary_map_eq_homLinearEquiv {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (X Y : LinearPathCategory.Category k S.OrdinaryLiftedVertex) :
                CategoryTheory.Functor.mapLinearMap k S.ordinaryLiftedToOrdinary = ↑(S.ordinaryLiftedHomLinearEquiv X Y)

                The Hom map of the lifted-vertex reindexing is the explicit path-basis linear equivalence.

                source
                instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.ordinaryLiftedToOrdinary_full {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) :
                S.ordinaryLiftedToOrdinary.Full
                source
                instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.ordinaryLiftedToOrdinary_faithful {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) :
                S.ordinaryLiftedToOrdinary.Faithful
                source
                theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.ordinaryLiftedToOrdinary_obj_bijective {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) :
                Function.Bijective S.ordinaryLiftedToOrdinary.obj

                The lifted-vertex reindexing is bijective on objects.

                source
                instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.ordinaryLiftedToOrdinary_essSurj {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) :
                S.ordinaryLiftedToOrdinary.EssSurj
                source
                noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.ordinaryLiftedPathCategoryEquivalence {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) :
                LinearPathCategory.Category k S.OrdinaryLiftedVertex ≌ LinearPathCategory.Category k S.ProjectiveLabel

                Universe lifting the ordinary vertices does not change the free linear path category.

                Instances For