Magnitude conjecture

MagnitudeConjecture.Algebra.RightModuleRestrictedCoyonedaHom

Full faithfulness of restricted covariant Yoneda #

This packages the finite-density Yoneda results as the linear equivalence

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

when X is a chosen indecomposable and B is any finitely generated module.

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

Restricted covariant Yoneda is faithful on all finitely generated modules.

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

The map on Hom spaces induced by restricted covariant Yoneda.

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

    Restricted covariant Yoneda is a linear equivalence from maps out of a chosen indecomposable to maps between the corresponding representables.

    Instances For
      source
      @[simp]
      theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteRestrictedCovariantRepresentableHomLinearEquiv_apply {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (B : FinitelyGeneratedCategory A) (X : S.IndecCategory) (f : S.fgObj X ⟶ B) :
      (S.finiteRestrictedCovariantRepresentableHomLinearEquiv B X) f = S.finiteRestrictedCovariantRepresentableMap f
      source
      def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.covariantFgHomLinearEquiv {k A : Type u} [Field k] [Ring A] [Algebra k A] (B C : FinitelyGeneratedCategory A) :
      (B.obj ⟶ C.obj) ≃ₗ[k] B ⟶ C

      Ambient and finitely generated Hom spaces agree linearly.

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

        Ambient form of the restricted covariant-Yoneda Hom equivalence.

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