Magnitude conjecture

MagnitudeConjecture.Algebra.RightModuleOrdinaryQuiverLiftedPresentation

A universe-local ordinary-quiver presentation #

The ordinary quiver is naturally indexed by a small finite type, whereas the public bound-quiver presentation bundle places its coefficient field, algebra, and vertex type in one universe. We therefore transport the exact ordinary kernel attached to any ordinary-arrow representative system to ULift of the projective labels. Path reindexing preserves length, so admissibility and the quotient realization are unchanged.

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

Realize the lifted ordinary quiver by first forgetting the universe lift.

Instances For
    source
    instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.ordinaryLiftedRealization_additive {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (D : OrdinaryArrowRepresentatives) :
    (S.ordinaryLiftedRealization D).Additive
    source
    instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.ordinaryLiftedRealization_linear {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (D : OrdinaryArrowRepresentatives) :
    CategoryTheory.Functor.Linear k (S.ordinaryLiftedRealization D)
    source
    structure MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.LiftedProjectiveLabel {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : FiniteIndecomposableSkeleton k A) :
    Type u

    A wrapper separating the lifted projective objects from the quiver vertex type, so their distinct categorical and quiver structures never compete in typeclass inference.

    Instances For
      source
      theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.LiftedProjectiveLabel.ext_iff {k A : Type u} {inst✝ : Field k} {inst✝¹ : Ring A} {inst✝² : Algebra k A} {S : FiniteIndecomposableSkeleton k A} {x y : S.LiftedProjectiveLabel} :
      x = y ↔ x.vertex = y.vertex
      source
      theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.LiftedProjectiveLabel.ext {k A : Type u} {inst✝ : Field k} {inst✝¹ : Ring A} {inst✝² : Algebra k A} {S : FiniteIndecomposableSkeleton k A} {x y : S.LiftedProjectiveLabel} (vertex : x.vertex = y.vertex) :
      x = y
      source
      @[instance_reducible]
      noncomputable instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.liftedProjectiveLabelFintype {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : FiniteIndecomposableSkeleton k A) :
      Fintype S.LiftedProjectiveLabel
      source
      @[reducible, inline]
      abbrev MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.LiftedProjectiveCategory {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : FiniteIndecomposableSkeleton k A) :
      Type u

      The selected-projective category reindexed by wrapped lifted labels.

      Instances For
        source
        @[instance_reducible]
        noncomputable instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.liftedProjectiveCategoryCategory {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : FiniteIndecomposableSkeleton k A) :
        CategoryTheory.Category.{u, u} S.LiftedProjectiveCategory
        source
        @[instance_reducible]
        noncomputable instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.liftedProjectiveCategoryPreadditive {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : FiniteIndecomposableSkeleton k A) :
        CategoryTheory.Preadditive S.LiftedProjectiveCategory
        source
        @[instance_reducible]
        noncomputable instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.liftedProjectiveCategoryLinear {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : FiniteIndecomposableSkeleton k A) :
        CategoryTheory.Linear k S.LiftedProjectiveCategory
        source
        @[instance_reducible]
        noncomputable instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.liftedProjectiveCategoryFintype {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : FiniteIndecomposableSkeleton k A) :
        Fintype S.LiftedProjectiveCategory
        source
        noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.ordinaryLiftedProjectiveRealization {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (D : OrdinaryArrowRepresentatives) :
        CategoryTheory.Functor (LinearPathCategory.Category k S.OrdinaryLiftedVertex) S.LiftedProjectiveCategory

        Realize the lifted ordinary quiver in the universe-local copy of the selected-projective category.

        Instances For
          source
          instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.ordinaryLiftedProjectiveRealization_additive {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (D : OrdinaryArrowRepresentatives) :
          (S.ordinaryLiftedProjectiveRealization D).Additive
          source
          instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.ordinaryLiftedProjectiveRealization_linear {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (D : OrdinaryArrowRepresentatives) :
          CategoryTheory.Functor.Linear k (S.ordinaryLiftedProjectiveRealization D)
          source
          @[simp]
          theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.ordinaryLiftedProjectiveRealization_map_hom {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (D : OrdinaryArrowRepresentatives) {X Y : LinearPathCategory.Category k S.OrdinaryLiftedVertex} (f : X ⟶ Y) :
          ((S.ordinaryLiftedProjectiveRealization D).map f).hom = (S.ordinaryLiftedRealization D).map f
          source
          def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.ordinaryLiftedRelations {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (D : OrdinaryArrowRepresentatives) :
          BoundQuiver.RelationFamily k S.OrdinaryLiftedVertex

          The full kernel of the lifted ordinary-quiver realization.

          Instances For
            source
            @[simp]
            theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.mem_ordinaryLiftedRelations_iff {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (D : OrdinaryArrowRepresentatives) {X Y : LinearPathCategory.Category k S.OrdinaryLiftedVertex} (f : X ⟶ Y) :
            f ∈ S.ordinaryLiftedRelations D X Y ↔ (S.ordinaryLiftedRealization D).map f = 0
            source
            theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.ordinaryLiftedRelations_generatedHomSubmodule_eq_ker {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (D : OrdinaryArrowRepresentatives) (X Y : LinearPathCategory.Category k S.OrdinaryLiftedVertex) :
            QuotientSubmoduleEquidistribution.CategoricalIdeal.HomIdeal.generatedHomSubmodule k (S.ordinaryLiftedRelations D) X Y = (CategoryTheory.Functor.mapLinearMap k (S.ordinaryLiftedRealization D)).ker

            The relation family is already a two-sided linear kernel.

            source
            @[simp]
            theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.ordinaryLiftedPathEquiv_length {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.ordinaryLiftedPathEquiv x y) p).length = p.length

            Forgetting the universe lift preserves path length.

            source
            @[simp]
            theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.ordinaryLiftedFunctorPathEquiv_length {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.ordinaryLiftedFunctorPathEquiv X Y) p).length = p.length

            The endpoint-exact path equivalence used by the free-category functor also preserves length.

            source
            theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.homPathLinearEquiv_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) (f : X ⟶ Y) :
            (LinearPathCategory.homPathLinearEquiv (S.ordinaryLiftedToOrdinary.obj X) (S.ordinaryLiftedToOrdinary.obj Y)) ((S.ordinaryLiftedHomLinearEquiv X Y) f) = Finsupp.equivMapDomain (S.ordinaryLiftedFunctorPathEquiv X Y) ((LinearPathCategory.homPathLinearEquiv X Y) f)

            The path-coordinate map of the Hom equivalence is literal domain reindexing.

            source
            theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.ordinaryLiftedRelations_generatedHomSubmodule_le_lengthTail_two {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (D : OrdinaryArrowRepresentatives) (X Y : LinearPathCategory.Category k S.OrdinaryLiftedVertex) :
            QuotientSubmoduleEquidistribution.CategoricalIdeal.HomIdeal.generatedHomSubmodule k (S.ordinaryLiftedRelations D) X Y ≤ LinearPathCategory.lengthTail X Y 2

            The lifted kernel has no path terms below length two.

            source
            theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.ordinaryLiftedRelations_long_paths_mem {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (D : OrdinaryArrowRepresentatives) :
            ∃ (N : ℕ), 2 ≤ N ∧ ∀ {x y : S.OrdinaryLiftedVertex} (p : Quiver.Path x y), N ≤ p.length → LinearPathCategory.pathHom p ∈ QuotientSubmoduleEquidistribution.CategoricalIdeal.HomIdeal.generatedHomSubmodule k (S.ordinaryLiftedRelations D) (LinearPathCategory.obj k S.OrdinaryLiftedVertex y) (LinearPathCategory.obj k S.OrdinaryLiftedVertex x)

            The same radical-nilpotence cutoff kills every sufficiently long lifted ordinary path.

            source
            theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.ordinaryLiftedRelations_isAdmissible {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (D : OrdinaryArrowRepresentatives) :
            BoundQuiver.IsAdmissible (S.ordinaryLiftedRelations D)

            The lifted full kernel is an admissible relation ideal.

            source
            theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.liftedProjectiveCategory_finiteRepresentables {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] (S : FiniteIndecomposableSkeleton k A) (X : S.LiftedProjectiveCategory) :
            CoveringHom.IsFiniteDimensionalModule k (CoveringHom.linearCoyonedaLinearModule X)

            Covariant representables of the lifted selected-projective category are pointwise finite-dimensional and finitely supported.

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

            The chosen basic algebra, formed from one lifted copy of every selected indecomposable projective.

            Instances For
              source
              instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.basicAlgebra_finiteDimensional {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] (S : FiniteIndecomposableSkeleton k A) :
              FiniteDimensional k S.basicAlgebra
              source
              theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.ordinaryLiftedRelationIdeal_isKilledBy {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (D : OrdinaryArrowRepresentatives) :
              (LinearPathCategory.HomogeneousQuotient.relationIdeal (S.ordinaryLiftedRelations D)).IsKilledBy (S.ordinaryLiftedProjectiveRealization D)

              The lifted realization kills the ideal generated by its full kernel.

              source
              noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.ordinaryLiftedQuiverQuotientRealization {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (D : OrdinaryArrowRepresentatives) :
              CategoryTheory.Functor (BoundQuiver.Category (S.ordinaryLiftedRelations D)) S.LiftedProjectiveCategory

              Realization of the lifted ordinary bound-quiver category.

              Instances For
                source
                @[simp]
                theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.ordinaryLiftedQuiverQuotientRealization_map_arrowMap_hom {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (D : OrdinaryArrowRepresentatives) {x y : S.OrdinaryLiftedVertex} (a : x ⟶ y) :
                ((S.ordinaryLiftedQuiverQuotientRealization D).map (BoundQuiver.arrowMap (S.ordinaryLiftedRelations D) a)).hom = D.hom a

                Under the quotient realization, a displayed lifted arrow is the selected ordinary-arrow representative with the same underlying endpoints.

                source
                instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.ordinaryLiftedQuiverQuotientRealization_additive {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (D : OrdinaryArrowRepresentatives) :
                (S.ordinaryLiftedQuiverQuotientRealization D).Additive
                source
                instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.ordinaryLiftedQuiverQuotientRealization_linear {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (D : OrdinaryArrowRepresentatives) :
                CategoryTheory.Functor.Linear k (S.ordinaryLiftedQuiverQuotientRealization D)
                source
                instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.ordinaryLiftedQuiverQuotientRealization_faithful {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (D : OrdinaryArrowRepresentatives) :
                (S.ordinaryLiftedQuiverQuotientRealization D).Faithful
                source
                theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.ordinaryLiftedQuiverQuotientRealization_obj_bijective {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (D : OrdinaryArrowRepresentatives) :
                Function.Bijective (S.ordinaryLiftedQuiverQuotientRealization D).obj

                The lifted quotient still has exactly one object for each selected indecomposable projective.

                source
                instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.ordinaryLiftedQuiverQuotientRealization_essSurj {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (D : OrdinaryArrowRepresentatives) :
                (S.ordinaryLiftedQuiverQuotientRealization D).EssSurj
                source
                instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.ordinaryLiftedRealization_full {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [IsAlgClosed k] (D : OrdinaryArrowRepresentatives) :
                (S.ordinaryLiftedRealization D).Full
                source
                instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.ordinaryLiftedProjectiveRealization_full {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [IsAlgClosed k] (D : OrdinaryArrowRepresentatives) :
                (S.ordinaryLiftedProjectiveRealization D).Full
                source
                instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.ordinaryLiftedQuiverQuotientRealization_full {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [IsAlgClosed k] (D : OrdinaryArrowRepresentatives) :
                (S.ordinaryLiftedQuiverQuotientRealization D).Full
                source
                noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.ordinaryLiftedQuiverQuotientEquivalence {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [IsAlgClosed k] (D : OrdinaryArrowRepresentatives) :
                BoundQuiver.Category (S.ordinaryLiftedRelations D) ≌ S.LiftedProjectiveCategory

                The lifted ordinary bound-quiver category is linearly equivalent to the selected-projective category.

                Instances For
                  source
                  instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.ordinaryLiftedQuiverQuotientEquivalence_functor_additive {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [IsAlgClosed k] (D : OrdinaryArrowRepresentatives) :
                  (S.ordinaryLiftedQuiverQuotientEquivalence D).functor.Additive
                  source
                  instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.ordinaryLiftedQuiverQuotientEquivalence_functor_linear {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [IsAlgClosed k] (D : OrdinaryArrowRepresentatives) :
                  CategoryTheory.Functor.Linear k (S.ordinaryLiftedQuiverQuotientEquivalence D).functor
                  source
                  noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.ordinaryLiftedPresentation {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [IsAlgClosed k] (D : OrdinaryArrowRepresentatives) :
                  BoundQuiver.Presentation k S.basicAlgebra S.OrdinaryLiftedVertex

                  The chosen basic algebra has a literal universe-local bound-quiver presentation by the lifted ordinary quiver and its exact kernel.

                  Instances For