Magnitude conjecture

MagnitudeConjecture.Algebra.RightModuleRestrictedYonedaHom

Full faithfulness of restricted Yoneda on a finite module skeleton #

For a finitely generated module B and a chosen indecomposable X, this file packages the already proved fullness and faithfulness statements as the linear equivalence

Hom(B, X) ≃ Nat(Hom(-, B), Hom(-, X)).

This is the Yoneda comparison needed to turn Auslander's presentation quotient in the functor category into the ordinary module presentation quotient.

source
def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.fgHomLinearEquiv {k A : Type u} [Field k] [Ring A] [Algebra k A] (B C : FinitelyGeneratedCategory A) :
(B.obj ⟶ C.obj) ≃ₗ[k] B ⟶ C

Forgetting and rebundling finite generation does not change a Hom space.

Instances For
    source
    def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteRestrictedContravariantRepresentableHomLinear {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (B C : FinitelyGeneratedCategory A) :
    (B ⟶ C) →ₗ[k] S.finiteRestrictedContravariantRepresentable B ⟶ S.finiteRestrictedContravariantRepresentable C

    The map on Hom spaces induced by restricted contravariant Yoneda.

    Instances For
      source
      noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteRestrictedContravariantRepresentableHomLinearEquiv {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (B : FinitelyGeneratedCategory A) (X : S.IndecCategory) :
      (B ⟶ S.fgObj X) ≃ₗ[k] S.finiteRestrictedContravariantRepresentable B ⟶ S.finiteRestrictedContravariantRepresentable (S.fgObj X)

      Restricted contravariant Yoneda is a linear equivalence on maps from an arbitrary finitely generated module to a chosen indecomposable.

      Instances For
        source
        noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.ambientFiniteRestrictedContravariantRepresentableHomLinearEquiv {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (B : FinitelyGeneratedCategory A) (X : S.IndecCategory) :
        (B.obj ⟶ (S.fgObj X).obj) ≃ₗ[k] S.finiteRestrictedContravariantRepresentable B ⟶ S.finiteRestrictedContravariantRepresentable (S.fgObj X)

        Ambient module maps to a chosen indecomposable are likewise identified with maps between the corresponding restricted representables.

        Instances For
          source
          @[simp]
          theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.ambientFiniteRestrictedContravariantRepresentableHomLinearEquiv_apply {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (B : FinitelyGeneratedCategory A) (X : S.IndecCategory) (f : B.obj ⟶ (S.fgObj X).obj) :
          (S.ambientFiniteRestrictedContravariantRepresentableHomLinearEquiv B X) f = S.finiteRestrictedContravariantRepresentableMap (CategoryTheory.ObjectProperty.homMk f)
          source
          @[simp]
          theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteRestrictedContravariantRepresentableHomLinearEquiv_apply {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (B : FinitelyGeneratedCategory A) (X : S.IndecCategory) (f : B ⟶ S.fgObj X) :
          (S.finiteRestrictedContravariantRepresentableHomLinearEquiv B X) f = S.finiteRestrictedContravariantRepresentableMap f