Magnitude conjecture

MagnitudeConjecture.Algebra.RightModuleCoherentDefectEvaluation

Evaluating the covariant defect #

Evaluation is exact on the finite linear functor category. Consequently the value of the covariant defect at X is the ordinary quotient

Hom(A, X) / im(Hom(B, X) → Hom(A, X))

attached to the first map A → B of the module complex.

source
@[reducible, inline]
abbrev MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.FiniteCovariantFunctor {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : FiniteIndecomposableSkeleton k A) :
Type (u + 1)
Instances For
    source
    def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteCovariantFunctorInclusion {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : FiniteIndecomposableSkeleton k A) :
    CategoryTheory.Functor S.FiniteCovariantFunctor (CategoryTheory.Functor S.IndecCategory (ModuleCat k))

    Forget the finite-dimensional and linear-property wrappers.

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

      Evaluation of a finite covariant functor at a chosen indecomposable.

      Instances For
        source
        theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.instPreservesColimitFiniteCovariantFunctorLinearModuleCategoryIndecCategoryWalkingParallelPairParallelPairOfNatHomFiniteModuleInclusion {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : FiniteIndecomposableSkeleton k A) {M N : S.FiniteCovariantFunctor} (f : M ⟶ N) :
        CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f 0) (MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteModuleInclusion✝ S)
        source
        theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.instPreservesLimitFiniteCovariantFunctorLinearModuleCategoryIndecCategoryWalkingParallelPairParallelPairOfNatHomFiniteModuleInclusion {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : FiniteIndecomposableSkeleton k A) {M N : S.FiniteCovariantFunctor} (f : M ⟶ N) :
        CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair f 0) (MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteModuleInclusion✝ S)
        source
        theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.instPreservesColimitLinearModuleCategoryIndecCategoryFunctorModuleCatWalkingParallelPairParallelPairOfNatHomLinearModuleInclusion {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : FiniteIndecomposableSkeleton k A) {M N : CoveringHom.LinearModuleCategory k} (f : M ⟶ N) :
        CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f 0) (MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.linearModuleInclusion✝ S)
        source
        theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.instPreservesLimitLinearModuleCategoryIndecCategoryFunctorModuleCatWalkingParallelPairParallelPairOfNatHomLinearModuleInclusion {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : FiniteIndecomposableSkeleton k A) {M N : CoveringHom.LinearModuleCategory k} (f : M ⟶ N) :
        CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair f 0) (MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.linearModuleInclusion✝ S)
        source
        theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.instPreservesFiniteLimitsFullSubcategoryLinearModuleCategoryIndecCategoryIsFiniteDimensionalModuleFiniteModuleInclusion {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : FiniteIndecomposableSkeleton k A) :
        CategoryTheory.Limits.PreservesFiniteLimits (MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteModuleInclusion✝ S)
        source
        theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.instPreservesFiniteLimitsFullSubcategoryFunctorIndecCategoryModuleCatIsLinearModuleLinearModuleInclusion {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : FiniteIndecomposableSkeleton k A) :
        CategoryTheory.Limits.PreservesFiniteLimits (MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.linearModuleInclusion✝ S)
        source
        theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.instPreservesFiniteLimitsFullSubcategoryLinearModuleCategoryIndecCategoryIsFiniteDimensionalModuleFunctorModuleCatCompFiniteModuleInclusionLinearModuleInclusion {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : FiniteIndecomposableSkeleton k A) :
        CategoryTheory.Limits.PreservesFiniteLimits ((MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteModuleInclusion✝ S).comp (MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.linearModuleInclusion✝ S))
        source
        theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.instPreservesFiniteColimitsFullSubcategoryLinearModuleCategoryIndecCategoryIsFiniteDimensionalModuleFiniteModuleInclusion {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : FiniteIndecomposableSkeleton k A) :
        CategoryTheory.Limits.PreservesFiniteColimits (MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteModuleInclusion✝ S)
        source
        theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.instPreservesFiniteColimitsFullSubcategoryFunctorIndecCategoryModuleCatIsLinearModuleLinearModuleInclusion {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : FiniteIndecomposableSkeleton k A) :
        CategoryTheory.Limits.PreservesFiniteColimits (MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.linearModuleInclusion✝ S)
        source
        theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.instPreservesFiniteColimitsFullSubcategoryLinearModuleCategoryIndecCategoryIsFiniteDimensionalModuleFunctorModuleCatCompFiniteModuleInclusionLinearModuleInclusion {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : FiniteIndecomposableSkeleton k A) :
        CategoryTheory.Limits.PreservesFiniteColimits ((MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteModuleInclusion✝ S).comp (MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.linearModuleInclusion✝ S))
        source
        instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteCovariantFunctorInclusion_preservesFiniteColimits {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : FiniteIndecomposableSkeleton k A) :
        CategoryTheory.Limits.PreservesFiniteColimits S.finiteCovariantFunctorInclusion
        source
        instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteCovariantFunctorInclusion_preservesFiniteLimits {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : FiniteIndecomposableSkeleton k A) :
        CategoryTheory.Limits.PreservesFiniteLimits S.finiteCovariantFunctorInclusion
        source
        instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteCovariantFunctorEvaluation_preservesFiniteLimits {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : FiniteIndecomposableSkeleton k A) (X : S.IndecCategory) :
        CategoryTheory.Limits.PreservesFiniteLimits (S.finiteCovariantFunctorEvaluation X)
        source
        instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteCovariantFunctorEvaluation_preservesFiniteColimits {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : FiniteIndecomposableSkeleton k A) (X : S.IndecCategory) :
        CategoryTheory.Limits.PreservesFiniteColimits (S.finiteCovariantFunctorEvaluation X)
        source
        theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.instPreservesFiniteColimitsFiniteCovariantFunctorModuleCatFiniteCovariantFunctorEvaluation {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : FiniteIndecomposableSkeleton k A) (X : S.IndecCategory) :
        CategoryTheory.Limits.PreservesFiniteColimits (S.finiteCovariantFunctorEvaluation X)
        source
        @[reducible, inline]
        abbrev MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteCovariantPresentationRange {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : FiniteIndecomposableSkeleton k A) (K : CategoryTheory.ShortComplex FG) (X : S.IndecCategory) :
        Submodule k (K.X₁.obj ⟶ (S.fgObj X).obj)

        The ambient module-theoretic presentation coboundaries obtained by precomposing with the first map of K.

        Instances For
          source
          theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteCovariantFunctorEvaluation_map_range {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (K : CategoryTheory.ShortComplex FG) (X : S.IndecCategory) :
          (ModuleCat.Hom.hom ((S.finiteCovariantFunctorEvaluation X).map (S.finiteRestrictedCovariantRepresentableMap K.f))).range = S.finiteCovariantPresentationRange K X

          Evaluating the covariant representable map gives the ordinary precomposition map in the module category.

          source
          noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteCovariantDefectEvaluationIsoPresentationQuotient {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (K : CategoryTheory.ShortComplex FG) (X : S.IndecCategory) :
          (S.finiteCovariantDefect K).obj.obj.obj X ≅ ModuleCat.of k ((K.X₁.obj ⟶ (S.fgObj X).obj) ⧸ S.finiteCovariantPresentationRange K X)

          The value of the covariant defect is the module-presentation quotient.

          Instances For
            source
            noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteCovariantDefectEvaluationLinearEquivPresentationQuotient {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (K : CategoryTheory.ShortComplex FG) (X : S.IndecCategory) :
            ↑((S.finiteCovariantDefect K).obj.obj.obj X) ≃ₗ[k] (K.X₁.obj ⟶ (S.fgObj X).obj) ⧸ S.finiteCovariantPresentationRange K X

            Linear-equivalence form of the evaluated covariant-defect calculation.

            Instances For