Magnitude conjecture

MagnitudeConjecture.Algebra.RightModuleCoherentDefectFreyd

Freyd realizations of the two coherent-defect presentations #

The restricted contravariant and covariant Yoneda embeddings are fully faithful and have projective values. Their right-Freyd cokernel realizations are therefore fully faithful. This packages the projective-resolution lifting and homotopy-independence used in the morphism part of Auslander's coherent duality.

source
theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteRestrictedContravariantRepresentableFunctor_full {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) :
S.finiteRestrictedContravariantRepresentableFunctor.Full

Restricted contravariant Yoneda is full on all finitely generated modules.

source
theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteRestrictedContravariantRepresentableFunctor_faithful {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) :
S.finiteRestrictedContravariantRepresentableFunctor.Faithful

Restricted contravariant Yoneda is faithful on all finitely generated modules.

source
theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteRestrictedContravariantRepresentableFunctor_epi_covers {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (Y : CoveringHom.FiniteDimensionalModuleCategory k) :
∃ (X : FinitelyGeneratedCategory A) (p : S.finiteRestrictedContravariantRepresentableFunctor.obj X ⟶ Y), CategoryTheory.Epi p

Every finite contravariant functor is an epimorphic image of a restricted representable of a finitely generated module.

source
noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.contravariantDefectFreydRealization {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) :
CategoryTheory.Functor (CategoryTheory.Preadditive.RightFreyd (FinitelyGeneratedCategory A)) (CoveringHom.FiniteDimensionalModuleCategory k)

The right-Freyd realization of contravariant representable presentations.

Instances For
    source
    instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.contravariantDefectFreydRealization_essSurj {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) :
    S.contravariantDefectFreydRealization.EssSurj
    source
    instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.contravariantDefectFreydRealization_full {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) :
    S.contravariantDefectFreydRealization.Full
    source
    instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.contravariantDefectFreydRealization_faithful {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) :
    S.contravariantDefectFreydRealization.Faithful
    source
    instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.contravariantDefectFreydRealization_isEquivalence {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) :
    S.contravariantDefectFreydRealization.IsEquivalence
    source
    noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.contravariantDefectFreydEquivalence {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) :
    CategoryTheory.Preadditive.RightFreyd (FinitelyGeneratedCategory A) ≌ CoveringHom.FiniteDimensionalModuleCategory k

    Every finite contravariant functor has a restricted-representable presentation, and right homotopy is exactly equality on its cokernel.

    Instances For
      source
      noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.covariantDefectFreydRealization {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) :
      CategoryTheory.Functor (CategoryTheory.Preadditive.RightFreyd (FinitelyGeneratedCategory A)ᵒᵖ) (CoveringHom.FiniteDimensionalModuleCategory k)

      The right-Freyd realization of covariant representable presentations. The representing module variable is opposite because Hom(X,−) is contravariant in X.

      Instances For
        source
        instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.covariantDefectFreydRealization_full {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) :
        S.covariantDefectFreydRealization.Full
        source
        instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.covariantDefectFreydRealization_faithful {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) :
        S.covariantDefectFreydRealization.Faithful
        source
        theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteRestrictedCovariantRepresentableFunctor_epi_covers {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (Y : CoveringHom.FiniteDimensionalModuleCategory k) :
        ∃ (X : (FinitelyGeneratedCategory A)ᵒᵖ) (p : S.finiteRestrictedCovariantRepresentableFunctor.obj X ⟶ Y), CategoryTheory.Epi p

        Every finite covariant functor is an epimorphic image of a restricted covariant representable of an object of the opposite module category.

        source
        instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.covariantDefectFreydRealization_essSurj {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) :
        S.covariantDefectFreydRealization.EssSurj
        source
        instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.covariantDefectFreydRealization_isEquivalence {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) :
        S.covariantDefectFreydRealization.IsEquivalence
        source
        noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.covariantDefectFreydEquivalence {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) :
        CategoryTheory.Preadditive.RightFreyd (FinitelyGeneratedCategory A)ᵒᵖ ≌ CoveringHom.FiniteDimensionalModuleCategory k

        Every finite covariant functor has a restricted-corepresentable presentation, modulo right homotopy.

        Instances For
          source
          noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.contravariantEpiFreydRealizationRaw {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) :
          CategoryTheory.Functor MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.ModuleEpiFreyd✝ (CoveringHom.FiniteDimensionalModuleCategory k)

          The contravariant Freyd realization restricted to epimorphic presentations.

          Instances For
            source
            theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.contravariantEpiFreydRealizationRaw_isDefect {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (X : MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.ModuleEpiFreyd✝) :
            S.IsFiniteContravariantDefect (S.contravariantEpiFreydRealizationRaw.obj X)
            source
            noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.contravariantEpiFreydRealization {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) :
            CategoryTheory.Functor MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.ModuleEpiFreyd✝ S.FiniteContravariantDefectCategory

            Epimorphic Freyd presentations realized as exact contravariant defects.

            Instances For
              source
              instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.contravariantEpiFreydRealization_full {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) :
              S.contravariantEpiFreydRealization.Full
              source
              instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.contravariantEpiFreydRealization_faithful {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) :
              S.contravariantEpiFreydRealization.Faithful
              source
              instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.contravariantEpiFreydRealization_essSurj {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) :
              S.contravariantEpiFreydRealization.EssSurj
              source
              instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.contravariantEpiFreydRealization_isEquivalence {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) :
              S.contravariantEpiFreydRealization.IsEquivalence
              source
              noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.contravariantEpiFreydEquivalence {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) :
              MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.ModuleEpiFreyd✝ ≌ S.FiniteContravariantDefectCategory

              Exact contravariant defects are the cokernel realizations of epimorphic presentations.

              Instances For
                source
                noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.covariantEpiFreydRealizationRaw {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) :
                CategoryTheory.Functor MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.OppositeModuleEpiFreyd✝ (CoveringHom.FiniteDimensionalModuleCategory k)

                The covariant Freyd realization restricted to epimorphic presentations in the opposite module category.

                Instances For
                  source
                  theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.covariantEpiFreydRealizationRaw_isDefect {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (X : MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.OppositeModuleEpiFreyd✝) :
                  S.IsFiniteCovariantDefect (S.covariantEpiFreydRealizationRaw.obj X)
                  source
                  noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.covariantEpiFreydRealization {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) :
                  CategoryTheory.Functor MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.OppositeModuleEpiFreyd✝ S.FiniteCovariantDefectCategory

                  Epimorphic opposite-Freyd presentations realized as exact covariant defects.

                  Instances For
                    source
                    instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.covariantEpiFreydRealization_full {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) :
                    S.covariantEpiFreydRealization.Full
                    source
                    instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.covariantEpiFreydRealization_faithful {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) :
                    S.covariantEpiFreydRealization.Faithful
                    source
                    instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.covariantEpiFreydRealization_essSurj {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) :
                    S.covariantEpiFreydRealization.EssSurj
                    source
                    instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.covariantEpiFreydRealization_isEquivalence {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) :
                    S.covariantEpiFreydRealization.IsEquivalence
                    source
                    noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.covariantEpiFreydEquivalence {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) :
                    MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.OppositeModuleEpiFreyd✝ ≌ S.FiniteCovariantDefectCategory

                    Exact covariant defects are the cokernel realizations of epimorphic presentations in the opposite module category.

                    Instances For
                      source
                      noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.coherentDefectEquivalence {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) :
                      S.FiniteContravariantDefectCategoryᵒᵖ ≌ S.FiniteCovariantDefectCategory

                      Auslander's anti-equivalence on the exact-defect subcategories, realized by projective presentations and kernel reversal.

                      Instances For