Magnitude conjecture

MagnitudeConjecture.Algebra.RightModuleCoherentDefectEquivalence

The exact-defect anti-equivalence on a fixed short exact presentation #

This file identifies the abstract Freyd-category anti-equivalence with the two defects attached to the same short exact module sequence. It is the object-level bridge needed to transport uniseriality in Auslander--Reiten Proposition 1.3.

source
noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.contravariantDefectObject {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] (S : FiniteIndecomposableSkeleton k A) (K : CategoryTheory.ShortComplex (FinitelyGeneratedCategory A)) (hK : K.ShortExact) :
S.FiniteContravariantDefectCategory

The contravariant defect as an object of the exact-defect subcategory.

Instances For
    source
    noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.covariantDefectObject {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (K : CategoryTheory.ShortComplex (FinitelyGeneratedCategory A)) (hK : K.ShortExact) :
    S.FiniteCovariantDefectCategory

    The covariant defect as an object of the exact-defect subcategory.

    Instances For
      source
      def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.contravariantEpiPresentation {A : Type u} [Ring A] [IsNoetherianRing Aᵐᵒᵖ] (K : CategoryTheory.ShortComplex (FinitelyGeneratedCategory A)) (hK : K.ShortExact) :
      MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.ModuleEpiFreyd✝

      The epimorphic Freyd presentation B ⟶ C of a short exact sequence.

      Instances For
        source
        def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.covariantEpiPresentation {A : Type u} [Ring A] [IsNoetherianRing Aᵐᵒᵖ] (K : CategoryTheory.ShortComplex (FinitelyGeneratedCategory A)) (hK : K.ShortExact) :
        MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.OppositeModuleEpiFreyd✝

        The epimorphic opposite-Freyd presentation Bᵒᵖ ⟶ Aᵒᵖ.

        Instances For
          source
          noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.contravariantEpiPresentationRealizationIso {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) :
          S.contravariantEpiFreydRealization.obj (contravariantEpiPresentation K hK) ≅ S.contravariantDefectObject K hK

          The contravariant Freyd realization of the displayed epimorphism is the displayed contravariant defect.

          Instances For
            source
            noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.covariantEpiPresentationRealizationIso {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) :
            S.covariantEpiFreydRealization.obj (covariantEpiPresentation K hK) ≅ S.covariantDefectObject K hK

            The opposite-Freyd realization of the displayed monomorphism is the displayed covariant defect.

            Instances For
              source
              noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.kernelOpContravariantPresentationIso {A : Type u} [Ring A] [IsNoetherianRing Aᵐᵒᵖ] (K : CategoryTheory.ShortComplex (FinitelyGeneratedCategory A)) (hK : K.ShortExact) :
              CategoryTheory.Preadditive.RightFreyd.kernelOp.obj (Opposite.op (contravariantEpiPresentation K hK)) ≅ covariantEpiPresentation K hK

              Kernel reversal sends the epimorphic presentation B ⟶ C to the opposite presentation Bᵒᵖ ⟶ Aᵒᵖ, up to the canonical kernel isomorphism supplied by exactness.

              Instances For
                source
                noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.contravariantRealizationInverseIsoPresentation {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) :
                S.contravariantEpiFreydEquivalence.inverse.obj (S.contravariantDefectObject K hK) ≅ contravariantEpiPresentation K hK

                The chosen inverse of contravariant Freyd realization is canonically isomorphic to the displayed presentation.

                Instances For
                  source
                  noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.coherentDefectEquivalenceObjIso {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) :
                  S.coherentDefectEquivalence.functor.obj (Opposite.op (S.contravariantDefectObject K hK)) ≅ S.covariantDefectObject K hK

                  The exact-defect anti-equivalence sends the contravariant defect of a short exact sequence to its covariant defect.

                  Instances For