Magnitude conjecture

MagnitudeConjecture.Algebra.RightModuleCovariantRepresentable

Covariant representables on the finite module skeleton #

This file packages the ordinary functor Hom(X, -) restricted to the finite skeleton of indecomposable right modules. Stable and costable quotients are built in separate leaf files.

source
def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.restrictedCovariantRepresentable {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : FiniteIndecomposableSkeleton k A) (X : FinitelyGeneratedCategory A) :
CategoryTheory.Functor S.IndecCategory (ModuleCat k)

The ordinary covariant representable Hom(X, -) restricted to the finite indecomposable skeleton.

Instances For
    source
    instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.restrictedCovariantRepresentable_additive {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : FiniteIndecomposableSkeleton k A) (X : FinitelyGeneratedCategory A) :
    (S.restrictedCovariantRepresentable X).Additive
    source
    instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.restrictedCovariantRepresentable_linear {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : FiniteIndecomposableSkeleton k A) (X : FinitelyGeneratedCategory A) :
    CategoryTheory.Functor.Linear k (S.restrictedCovariantRepresentable X)
    source
    def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.restrictedCovariantRepresentableLinearModule {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : FiniteIndecomposableSkeleton k A) (X : FinitelyGeneratedCategory A) :
    CoveringHom.LinearModuleCategory k

    The ordinary restricted covariant representable as a linear module.

    Instances For
      source
      theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.restrictedCovariantRepresentable_isFiniteDimensional {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (X : FinitelyGeneratedCategory A) :
      CoveringHom.IsFiniteDimensionalModule k (S.restrictedCovariantRepresentableLinearModule X)

      The ordinary restricted covariant representable is finite-dimensional on the finite indecomposable skeleton.

      source
      def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteRestrictedCovariantRepresentable {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (X : FinitelyGeneratedCategory A) :
      CoveringHom.FiniteDimensionalModuleCategory k

      The ordinary restricted covariant representable in the finite functor category.

      Instances For
        source
        def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.indecCovariantRepresentableFinite {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : FiniteIndecomposableSkeleton k A) (i : S.IndecCategory) :
        CoveringHom.IsFiniteDimensionalModule k (CoveringHom.linearCoyonedaLinearModule i)

        The covariant representable of a chosen skeleton object is finite-dimensional.

        Instances For
          source
          def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.restrictedFgObjHomLinearEquiv {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : FiniteIndecomposableSkeleton k A) (i Y : S.IndecCategory) :
          ((S.fgObj i).obj ⟶ S.inclusion.obj Y) ≃ₗ[k] i ⟶ Y

          Ambient morphisms out of a chosen skeleton object are the intrinsic morphisms of the induced skeleton.

          Instances For
            source
            def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.restrictedCovariantRepresentableFgObjRawIso {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : FiniteIndecomposableSkeleton k A) (i : S.IndecCategory) :
            S.restrictedCovariantRepresentable (S.fgObj i) ≅ (CategoryTheory.linearCoyoneda k S.IndecCategory).obj (Opposite.op i)

            Restricted ambient covariant Yoneda at a chosen indecomposable agrees naturally with intrinsic covariant Yoneda on the finite skeleton.

            Instances For
              source
              noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.restrictedCovariantRepresentableFgObjLinearIso {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : FiniteIndecomposableSkeleton k A) (i : S.IndecCategory) :
              S.restrictedCovariantRepresentableLinearModule (S.fgObj i) ≅ CoveringHom.linearCoyonedaLinearModule i

              Linear-module form of restricted covariant Yoneda on a chosen indecomposable.

              Instances For
                source
                noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteRestrictedCovariantRepresentableFgObjIso {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (i : S.IndecCategory) :
                S.finiteRestrictedCovariantRepresentable (S.fgObj i) ≅ CoveringHom.finiteDimensionalLinearCoyoneda i ⋯

                Finite-module form of restricted covariant Yoneda on a chosen indecomposable.

                Instances For
                  source
                  instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteRestrictedCovariantRepresentableFgObj_projective {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (i : S.IndecCategory) :
                  CategoryTheory.Projective (S.finiteRestrictedCovariantRepresentable (S.fgObj i))
                  source
                  def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteRestrictedCovariantRepresentableMap {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {X Y : FinitelyGeneratedCategory A} (f : X ⟶ Y) :
                  S.finiteRestrictedCovariantRepresentable Y ⟶ S.finiteRestrictedCovariantRepresentable X

                  Precomposition gives the expected variance-reversing map between restricted covariant representables.

                  Instances For
                    source
                    @[simp]
                    theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteRestrictedCovariantRepresentableMap_app_apply {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {X Y : FinitelyGeneratedCategory A} (f : X ⟶ Y) (Z : S.IndecCategory) (g : Y.obj ⟶ S.inclusion.obj Z) :
                    (CategoryTheory.ConcreteCategory.hom ((S.finiteRestrictedCovariantRepresentableMap f).hom.hom.app Z)) g = CategoryTheory.CategoryStruct.comp f.hom g
                    source
                    theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteRestrictedCovariantRepresentableMap_fgObj_eq {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (i j : S.IndecCategory) (a : S.finiteRestrictedCovariantRepresentable (S.fgObj i) ⟶ S.finiteRestrictedCovariantRepresentable (S.fgObj j)) :
                    have f := CategoryTheory.ObjectProperty.homMk (id ((CategoryTheory.ConcreteCategory.hom (a.hom.hom.app i)) (CategoryTheory.CategoryStruct.id (S.inclusion.obj i)))); S.finiteRestrictedCovariantRepresentableMap f = a

                    Restricted covariant Yoneda is full on chosen indecomposables. The variance reversal recovers a module map by evaluating at the identity.

                    source
                    @[simp]
                    theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteRestrictedCovariantRepresentableMap_comp {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {X Y Z : FinitelyGeneratedCategory A} (f : X ⟶ Y) (g : Y ⟶ Z) :
                    S.finiteRestrictedCovariantRepresentableMap (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (S.finiteRestrictedCovariantRepresentableMap g) (S.finiteRestrictedCovariantRepresentableMap f)
                    source
                    @[simp]
                    theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteRestrictedCovariantRepresentableMap_id {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (X : FinitelyGeneratedCategory A) :
                    S.finiteRestrictedCovariantRepresentableMap (CategoryTheory.CategoryStruct.id X) = CategoryTheory.CategoryStruct.id (S.finiteRestrictedCovariantRepresentable X)
                    source
                    @[simp]
                    theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteRestrictedCovariantRepresentableMap_add {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {X Y : FinitelyGeneratedCategory A} (f g : X ⟶ Y) :
                    S.finiteRestrictedCovariantRepresentableMap (f + g) = S.finiteRestrictedCovariantRepresentableMap f + S.finiteRestrictedCovariantRepresentableMap g
                    source
                    @[simp]
                    theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteRestrictedCovariantRepresentableMap_zero {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (X Y : FinitelyGeneratedCategory A) :
                    S.finiteRestrictedCovariantRepresentableMap 0 = 0