Magnitude conjecture

MagnitudeConjecture.Algebra.RightModuleCoherentDefectSerre

Exact defects form Serre subcategories #

The coherent-duality equivalence is defined on exact defects. To compare uniseriality there with uniseriality in the ambient finite-functor category, we identify the exact defects by their vanishing on projective or injective modules. This file begins with the two direct vanishing implications.

source
def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.ContravariantVanishesOnProjectives {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : FiniteIndecomposableSkeleton k A) :
CategoryTheory.ObjectProperty (CoveringHom.FiniteDimensionalModuleCategory k)

Finite contravariant functors vanishing on the chosen projective indecomposables.

Instances For
    source
    def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.CovariantVanishesOnInjectives {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : FiniteIndecomposableSkeleton k A) :
    CategoryTheory.ObjectProperty S.FiniteCovariantFunctor

    Finite covariant functors vanishing on the chosen injective indecomposables.

    Instances For
      source
      instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.contravariantVanishes_closedUnderSubobjects {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : FiniteIndecomposableSkeleton k A) :
      S.ContravariantVanishesOnProjectives.IsClosedUnderSubobjects
      source
      instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.contravariantVanishes_closedUnderQuotients {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : FiniteIndecomposableSkeleton k A) :
      S.ContravariantVanishesOnProjectives.IsClosedUnderQuotients
      source
      instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.covariantVanishes_closedUnderSubobjects {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : FiniteIndecomposableSkeleton k A) :
      S.CovariantVanishesOnInjectives.IsClosedUnderSubobjects
      source
      instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.covariantVanishes_closedUnderQuotients {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : FiniteIndecomposableSkeleton k A) :
      S.CovariantVanishesOnInjectives.IsClosedUnderQuotients
      source
      theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteContravariantDefect_isZero_at_projective {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (K : CategoryTheory.ShortComplex (FinitelyGeneratedCategory A)) (hK : K.ShortExact) (i : S.IndecCategory) (hi : CategoryTheory.Projective (S.fgObj i)) :
      CategoryTheory.Limits.IsZero ((S.finiteContravariantDefect K).obj.obj.obj (Opposite.op i))

      A contravariant exact defect vanishes at every projective chosen indecomposable.

      source
      theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteCovariantDefect_isZero_at_injective {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (K : CategoryTheory.ShortComplex (FinitelyGeneratedCategory A)) (hK : K.ShortExact) (i : S.IndecCategory) (hi : CategoryTheory.Injective (S.fgObj i)) :
      CategoryTheory.Limits.IsZero ((S.finiteCovariantDefect K).obj.obj.obj i)

      A covariant exact defect vanishes at every injective chosen indecomposable.

      source
      theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.isFiniteContravariantDefect_le_vanishesOnProjectives {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) :
      S.IsFiniteContravariantDefect ≤ S.ContravariantVanishesOnProjectives

      Exact contravariant defects satisfy projective vanishing.

      source
      theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.isFiniteCovariantDefect_le_vanishesOnInjectives {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) :
      S.IsFiniteCovariantDefect ≤ S.CovariantVanishesOnInjectives

      Exact covariant defects satisfy injective vanishing.

      source
      theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.epi_of_contravariantCokernel_vanishesOnProjectives {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {X Y : FinitelyGeneratedCategory A} (f : X ⟶ Y) (hzero : S.ContravariantVanishesOnProjectives (CategoryTheory.Limits.cokernel (S.finiteRestrictedContravariantRepresentableMap f))) :
      CategoryTheory.Epi f

      If the cokernel of a restricted contravariant representable map vanishes on projective indecomposables, then the presenting module map is an epimorphism.

      source
      theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.mono_of_covariantCokernel_vanishesOnInjectives {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {X Y : FinitelyGeneratedCategory A} (f : X ⟶ Y) (hzero : S.CovariantVanishesOnInjectives (CategoryTheory.Limits.cokernel (S.finiteRestrictedCovariantRepresentableMap f))) :
      CategoryTheory.Mono f

      If the cokernel of a restricted covariant representable map vanishes on injective indecomposables, then the presenting module map is a monomorphism.

      source
      theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.vanishesOnProjectives_le_isFiniteContravariantDefect {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) :
      S.ContravariantVanishesOnProjectives ≤ S.IsFiniteContravariantDefect

      Projective vanishing is sufficient for a finite contravariant functor to admit an exact representable presentation.

      source
      theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.vanishesOnInjectives_le_isFiniteCovariantDefect {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) :
      S.CovariantVanishesOnInjectives ≤ S.IsFiniteCovariantDefect

      Injective vanishing is sufficient for a finite covariant functor to admit an exact representable presentation.

      source
      theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.isFiniteContravariantDefect_iff_vanishesOnProjectives {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (F : CoveringHom.FiniteDimensionalModuleCategory k) :
      S.IsFiniteContravariantDefect F ↔ S.ContravariantVanishesOnProjectives F

      Exact contravariant defects are precisely the finite functors vanishing on projective indecomposables.

      source
      theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.isFiniteCovariantDefect_iff_vanishesOnInjectives {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (F : S.FiniteCovariantFunctor) :
      S.IsFiniteCovariantDefect F ↔ S.CovariantVanishesOnInjectives F

      Exact covariant defects are precisely the finite functors vanishing on injective indecomposables.

      source
      instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.contravariantVanishes_containsZero {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : FiniteIndecomposableSkeleton k A) :
      S.ContravariantVanishesOnProjectives.ContainsZero
      source
      instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.covariantVanishes_containsZero {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : FiniteIndecomposableSkeleton k A) :
      S.CovariantVanishesOnInjectives.ContainsZero
      source
      instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.contravariantVanishes_closedUnderExtensions {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : FiniteIndecomposableSkeleton k A) :
      S.ContravariantVanishesOnProjectives.IsClosedUnderExtensions
      source
      instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.covariantVanishes_closedUnderExtensions {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : FiniteIndecomposableSkeleton k A) :
      S.CovariantVanishesOnInjectives.IsClosedUnderExtensions
      source
      instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.contravariantVanishes_closedUnderFiniteProducts {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : FiniteIndecomposableSkeleton k A) :
      S.ContravariantVanishesOnProjectives.IsClosedUnderFiniteProducts
      source
      instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.covariantVanishes_closedUnderFiniteProducts {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : FiniteIndecomposableSkeleton k A) :
      S.CovariantVanishesOnInjectives.IsClosedUnderFiniteProducts
      source
      instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteContravariantDefect_containsZero {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) :
      S.IsFiniteContravariantDefect.ContainsZero
      source
      instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteCovariantDefect_containsZero {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) :
      S.IsFiniteCovariantDefect.ContainsZero
      source
      instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteContravariantDefect_closedUnderSubobjects {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) :
      S.IsFiniteContravariantDefect.IsClosedUnderSubobjects
      source
      instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteContravariantDefect_closedUnderQuotients {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) :
      S.IsFiniteContravariantDefect.IsClosedUnderQuotients
      source
      instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteCovariantDefect_closedUnderSubobjects {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) :
      S.IsFiniteCovariantDefect.IsClosedUnderSubobjects
      source
      instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteCovariantDefect_closedUnderQuotients {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) :
      S.IsFiniteCovariantDefect.IsClosedUnderQuotients
      source
      instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteContravariantDefect_closedUnderExtensions {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) :
      S.IsFiniteContravariantDefect.IsClosedUnderExtensions
      source
      instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteCovariantDefect_closedUnderExtensions {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) :
      S.IsFiniteCovariantDefect.IsClosedUnderExtensions
      source
      instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteContravariantDefect_closedUnderFiniteProducts {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) :
      S.IsFiniteContravariantDefect.IsClosedUnderFiniteProducts
      source
      instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteCovariantDefect_closedUnderFiniteProducts {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) :
      S.IsFiniteCovariantDefect.IsClosedUnderFiniteProducts
      source
      instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteContravariantDefect_isSerreClass {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) :
      S.IsFiniteContravariantDefect.IsSerreClass
      source
      instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteCovariantDefect_isSerreClass {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) :
      S.IsFiniteCovariantDefect.IsSerreClass
      source
      theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteContravariantDefect_isUniserial_iff_subcategory {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (F : CoveringHom.FiniteDimensionalModuleCategory k) (hF : S.IsFiniteContravariantDefect F) :
      IsUniserialObject F ↔ IsUniserialObject { obj := F, property := hF }

      Passing to the exact contravariant-defect subcategory does not change whether an exact defect is uniserial.

      source
      theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteCovariantDefect_isUniserial_iff_subcategory {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (F : S.FiniteCovariantFunctor) (hF : S.IsFiniteCovariantDefect F) :
      IsUniserialObject F ↔ IsUniserialObject { obj := F, property := hF }

      Passing to the exact covariant-defect subcategory does not change whether an exact defect is uniserial.

      source
      theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteContravariantDefect_isUniserial_iff_finiteCovariantDefect {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (K : CategoryTheory.ShortComplex (FinitelyGeneratedCategory A)) (hK : K.ShortExact) :
      IsUniserialObject (S.finiteContravariantDefect K) ↔ IsUniserialObject (S.finiteCovariantDefect K)

      Auslander's coherent anti-equivalence preserves uniseriality for the two defects attached to the same short exact module presentation.