Evaluating the contravariant defect

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

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

attached to the second map B → C of the module complex.

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteContravariantFunctorInclusion {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : FiniteIndecomposableSkeleton k A) : CategoryTheory.Functor S.FiniteContravariantFunctor (CategoryTheory.Functor S.IndecCategoryᵒᵖ (ModuleCat k))

Forget the finite-dimensional and linear-property wrappers.

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteContravariantFunctorEvaluation {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : FiniteIndecomposableSkeleton k A) (X : S.IndecCategoryᵒᵖ) : CategoryTheory.Functor S.FiniteContravariantFunctor (ModuleCat k)

Evaluation of a finite contravariant functor at a chosen indecomposable.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.instPreservesColimitFiniteContravariantFunctorLinearModuleCategoryOppositeIndecCategoryWalkingParallelPairParallelPairOfNatHomFiniteContravariantModuleInclusion {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : FiniteIndecomposableSkeleton k A) {M N : S.FiniteContravariantFunctor} (f : M ⟶ N) : CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f 0) (MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteContravariantModuleInclusion✝ S)

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.instPreservesLimitFiniteContravariantFunctorLinearModuleCategoryOppositeIndecCategoryWalkingParallelPairParallelPairOfNatHomFiniteContravariantModuleInclusion {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : FiniteIndecomposableSkeleton k A) {M N : S.FiniteContravariantFunctor} (f : M ⟶ N) : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair f 0) (MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteContravariantModuleInclusion✝ S)

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.instPreservesColimitLinearModuleCategoryOppositeIndecCategoryFunctorModuleCatWalkingParallelPairParallelPairOfNatHomContravariantLinearModuleInclusion {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.contravariantLinearModuleInclusion✝ S)

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.instPreservesLimitLinearModuleCategoryOppositeIndecCategoryFunctorModuleCatWalkingParallelPairParallelPairOfNatHomContravariantLinearModuleInclusion {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.contravariantLinearModuleInclusion✝ S)

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.instPreservesFiniteLimitsFullSubcategoryLinearModuleCategoryOppositeIndecCategoryIsFiniteDimensionalModuleFiniteContravariantModuleInclusion {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : FiniteIndecomposableSkeleton k A) : CategoryTheory.Limits.PreservesFiniteLimits (MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteContravariantModuleInclusion✝ S)

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.instPreservesFiniteLimitsFullSubcategoryFunctorOppositeIndecCategoryModuleCatIsLinearModuleContravariantLinearModuleInclusion {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : FiniteIndecomposableSkeleton k A) : CategoryTheory.Limits.PreservesFiniteLimits (MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.contravariantLinearModuleInclusion✝ S)

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.instPreservesFiniteLimitsFullSubcategoryLinearModuleCategoryOppositeIndecCategoryIsFiniteDimensionalModuleFunctorModuleCatCompFiniteContravariantModuleInclusionContravariantLinearModuleInclusion {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : FiniteIndecomposableSkeleton k A) : CategoryTheory.Limits.PreservesFiniteLimits ((MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteContravariantModuleInclusion✝ S).comp (MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.contravariantLinearModuleInclusion✝ S))

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.instPreservesFiniteColimitsFullSubcategoryLinearModuleCategoryOppositeIndecCategoryIsFiniteDimensionalModuleFiniteContravariantModuleInclusion {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : FiniteIndecomposableSkeleton k A) : CategoryTheory.Limits.PreservesFiniteColimits (MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteContravariantModuleInclusion✝ S)

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.instPreservesFiniteColimitsFullSubcategoryFunctorOppositeIndecCategoryModuleCatIsLinearModuleContravariantLinearModuleInclusion {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : FiniteIndecomposableSkeleton k A) : CategoryTheory.Limits.PreservesFiniteColimits (MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.contravariantLinearModuleInclusion✝ S)

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.instPreservesFiniteColimitsFullSubcategoryLinearModuleCategoryOppositeIndecCategoryIsFiniteDimensionalModuleFunctorModuleCatCompFiniteContravariantModuleInclusionContravariantLinearModuleInclusion {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : FiniteIndecomposableSkeleton k A) : CategoryTheory.Limits.PreservesFiniteColimits ((MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteContravariantModuleInclusion✝ S).comp (MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.contravariantLinearModuleInclusion✝ S))

instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteContravariantFunctorInclusion_preservesFiniteColimits {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : FiniteIndecomposableSkeleton k A) : CategoryTheory.Limits.PreservesFiniteColimits S.finiteContravariantFunctorInclusion

instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteContravariantFunctorInclusion_preservesFiniteLimits {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : FiniteIndecomposableSkeleton k A) : CategoryTheory.Limits.PreservesFiniteLimits S.finiteContravariantFunctorInclusion

instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteContravariantFunctorEvaluation_preservesFiniteLimits {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : FiniteIndecomposableSkeleton k A) (X : S.IndecCategoryᵒᵖ) : CategoryTheory.Limits.PreservesFiniteLimits (S.finiteContravariantFunctorEvaluation X)

instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteContravariantFunctorEvaluation_preservesFiniteColimits {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : FiniteIndecomposableSkeleton k A) (X : S.IndecCategoryᵒᵖ) : CategoryTheory.Limits.PreservesFiniteColimits (S.finiteContravariantFunctorEvaluation X)

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.instPreservesFiniteColimitsFiniteContravariantFunctorModuleCatFiniteContravariantFunctorEvaluation {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : FiniteIndecomposableSkeleton k A) (X : S.IndecCategoryᵒᵖ) : CategoryTheory.Limits.PreservesFiniteColimits (S.finiteContravariantFunctorEvaluation X)

@[reducible, inline]

abbrev MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteContravariantPresentationRange {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : FiniteIndecomposableSkeleton k A) (K : CategoryTheory.ShortComplex FG) (X : S.IndecCategory) : Submodule k ((S.fgObj X).obj ⟶ K.X₃.obj)

The ambient module-theoretic presentation coboundaries obtained by postcomposing with the second map of K.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteContravariantFunctorEvaluation_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.finiteContravariantFunctorEvaluation (Opposite.op X)).map (S.finiteRestrictedContravariantRepresentableMap K.g))).range = S.finiteContravariantPresentationRange K X

Evaluating the contravariant representable map gives the ordinary postcomposition map in the module category.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteContravariantDefectEvaluationIsoPresentationQuotient {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.finiteContravariantDefect K).obj.obj.obj (Opposite.op X) ≅ ModuleCat.of k (((S.fgObj X).obj ⟶ K.X₃.obj) ⧸ S.finiteContravariantPresentationRange K X)

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

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteContravariantDefectEvaluationLinearEquivPresentationQuotient {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.finiteContravariantDefect K).obj.obj.obj (Opposite.op X)) ≃ₗ[k] ((S.fgObj X).obj ⟶ K.X₃.obj) ⧸ S.finiteContravariantPresentationRange K X

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