Restricted linear Yoneda modules

For a linear functor J : P ⥤ C, restriction of the contravariant representable C(-, X) to P is a covariant linear module on Pᵒᵖ. Bundling these restricted representables functorially in X is the formal core of the Bongartz--Gabriel recovery functor

C ⟶ mod(P), X ↦ C(-, X)|_P.

This file only constructs the functor and its finite-dimensional restriction. Full faithfulness and essential surjectivity are the substantive Auslander- category assertions and are deliberately not assumed here.

@[instance_reducible]

noncomputable def MagnitudeConjecture.CoveringHom.instFintypeOpposite_magnitudeConjecture {P : Type w} [Fintype P] : Fintype Pᵒᵖ

def MagnitudeConjecture.CoveringHom.restrictedLinearYoneda {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {P : Type w} [CategoryTheory.Category.{v, w} P] (J : CategoryTheory.Functor P C) (X : C) : CategoryTheory.Functor Pᵒᵖ (ModuleCat k)

The contravariant representable C(-, X), restricted along J, as a module on Pᵒᵖ.

instance MagnitudeConjecture.CoveringHom.restrictedLinearYoneda_additive {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {P : Type w} [CategoryTheory.Category.{v, w} P] [CategoryTheory.Preadditive P] (J : CategoryTheory.Functor P C) [J.Additive] (X : C) : (restrictedLinearYoneda J X).Additive

instance MagnitudeConjecture.CoveringHom.restrictedLinearYoneda_linear {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {P : Type w} [CategoryTheory.Category.{v, w} P] [CategoryTheory.Preadditive P] [CategoryTheory.Linear k P] (J : CategoryTheory.Functor P C) [CategoryTheory.Functor.Linear k J] (X : C) : CategoryTheory.Functor.Linear k (restrictedLinearYoneda J X)

def MagnitudeConjecture.CoveringHom.restrictedLinearYonedaLinearModule {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {P : Type w} [CategoryTheory.Category.{v, w} P] [CategoryTheory.Preadditive P] [CategoryTheory.Linear k P] (J : CategoryTheory.Functor P C) [J.Additive] [CategoryTheory.Functor.Linear k J] (X : C) : LinearModuleCategory k

Bundled additive linear-module form of a restricted representable.

def MagnitudeConjecture.CoveringHom.restrictedLinearYonedaLinearModuleMap {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {P : Type w} [CategoryTheory.Category.{v, w} P] [CategoryTheory.Preadditive P] [CategoryTheory.Linear k P] (J : CategoryTheory.Functor P C) [J.Additive] [CategoryTheory.Functor.Linear k J] {X Y : C} (f : X ⟶ Y) : restrictedLinearYonedaLinearModule J X ⟶ restrictedLinearYonedaLinearModule J Y

A map of representing objects induces the corresponding map of restricted representables.

@[simp]

theorem MagnitudeConjecture.CoveringHom.restrictedLinearYonedaLinearModuleMap_id {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {P : Type w} [CategoryTheory.Category.{v, w} P] [CategoryTheory.Preadditive P] [CategoryTheory.Linear k P] (J : CategoryTheory.Functor P C) [J.Additive] [CategoryTheory.Functor.Linear k J] (X : C) : restrictedLinearYonedaLinearModuleMap J (CategoryTheory.CategoryStruct.id X) = CategoryTheory.CategoryStruct.id (restrictedLinearYonedaLinearModule J X)

@[simp]

theorem MagnitudeConjecture.CoveringHom.restrictedLinearYonedaLinearModuleMap_comp {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {P : Type w} [CategoryTheory.Category.{v, w} P] [CategoryTheory.Preadditive P] [CategoryTheory.Linear k P] (J : CategoryTheory.Functor P C) [J.Additive] [CategoryTheory.Functor.Linear k J] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) : restrictedLinearYonedaLinearModuleMap J (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (restrictedLinearYonedaLinearModuleMap J f) (restrictedLinearYonedaLinearModuleMap J g)

def MagnitudeConjecture.CoveringHom.restrictedLinearYonedaFunctor {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {P : Type w} [CategoryTheory.Category.{v, w} P] [CategoryTheory.Preadditive P] [CategoryTheory.Linear k P] (J : CategoryTheory.Functor P C) [J.Additive] [CategoryTheory.Functor.Linear k J] : CategoryTheory.Functor C (LinearModuleCategory k)

The restricted Yoneda realization, before imposing any finiteness condition on its values.

instance MagnitudeConjecture.CoveringHom.restrictedLinearYonedaFunctor_additive {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {P : Type w} [CategoryTheory.Category.{v, w} P] [CategoryTheory.Preadditive P] [CategoryTheory.Linear k P] (J : CategoryTheory.Functor P C) [J.Additive] [CategoryTheory.Functor.Linear k J] : (restrictedLinearYonedaFunctor J).Additive

instance MagnitudeConjecture.CoveringHom.restrictedLinearYonedaFunctor_linear {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {P : Type w} [CategoryTheory.Category.{v, w} P] [CategoryTheory.Preadditive P] [CategoryTheory.Linear k P] (J : CategoryTheory.Functor P C) [J.Additive] [CategoryTheory.Functor.Linear k J] : CategoryTheory.Functor.Linear k (restrictedLinearYonedaFunctor J)

theorem MagnitudeConjecture.CoveringHom.restrictedLinearYonedaFunctor_faithful_of_sourceDetection {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {P : Type w} [CategoryTheory.Category.{v, w} P] [CategoryTheory.Preadditive P] [CategoryTheory.Linear k P] (J : CategoryTheory.Functor P C) [J.Additive] [CategoryTheory.Functor.Linear k J] (hdetect : ∀ {X Y : C} (f : X ⟶ Y), f ≠ 0 → ∃ (Z : P) (g : J.obj Z ⟶ X), CategoryTheory.CategoryStruct.comp g f ≠ 0) : (restrictedLinearYonedaFunctor J).Faithful

Restricted Yoneda is faithful as soon as the selected source objects detect every nonzero ambient morphism by precomposition.

@[simp]

theorem MagnitudeConjecture.CoveringHom.restrictedLinearYoneda_obj_obj {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {P : Type w} [CategoryTheory.Category.{v, w} P] [CategoryTheory.Preadditive P] [CategoryTheory.Linear k P] (J : CategoryTheory.Functor P C) [J.Additive] [CategoryTheory.Functor.Linear k J] (X : C) (Y : Pᵒᵖ) : (restrictedLinearYonedaLinearModule J X).obj.obj Y = ModuleCat.of k (J.obj (Opposite.unop Y) ⟶ X)

@[simp]

theorem MagnitudeConjecture.CoveringHom.restrictedLinearYoneda_map_app_apply {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {P : Type w} [CategoryTheory.Category.{v, w} P] [CategoryTheory.Preadditive P] [CategoryTheory.Linear k P] (J : CategoryTheory.Functor P C) [J.Additive] [CategoryTheory.Functor.Linear k J] {X Y : C} (f : X ⟶ Y) (W : Pᵒᵖ) (h : J.obj (Opposite.unop W) ⟶ X) : (CategoryTheory.ConcreteCategory.hom ((restrictedLinearYonedaLinearModuleMap J f).hom.app W)) h = CategoryTheory.CategoryStruct.comp h f

theorem MagnitudeConjecture.CoveringHom.restrictedLinearYoneda_isFiniteDimensional_of_finite_support {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {P : Type w} [CategoryTheory.Category.{v, w} P] [CategoryTheory.Preadditive P] [CategoryTheory.Linear k P] (J : CategoryTheory.Functor P C) [J.Additive] [CategoryTheory.Functor.Linear k J] (X : C) (hfinite : ∀ (Y : P), FiniteDimensional k (J.obj Y ⟶ X)) : {Y : Pᵒᵖ | Nontrivial (J.obj (Opposite.unop Y) ⟶ X)}.Finite → IsFiniteDimensionalModule k (restrictedLinearYonedaLinearModule J X)

Pointwise finite-dimensional ambient Hom spaces and finite incoming support make a restricted representable a finite-dimensional module.

theorem MagnitudeConjecture.CoveringHom.restrictedLinearYoneda_isFiniteDimensional {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {P : Type w} [CategoryTheory.Category.{v, w} P] [CategoryTheory.Preadditive P] [CategoryTheory.Linear k P] (J : CategoryTheory.Functor P C) [J.Additive] [CategoryTheory.Functor.Linear k J] [Fintype P] (X : C) (hfinite : ∀ (Y : P), FiniteDimensional k (J.obj Y ⟶ X)) : IsFiniteDimensionalModule k (restrictedLinearYonedaLinearModule J X)

On a finite source subcategory, finite-dimensional ambient Hom spaces make a restricted representable a finite-dimensional module.

def MagnitudeConjecture.CoveringHom.finiteSupportRestrictedLinearYonedaFunctor {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {P : Type w} [CategoryTheory.Category.{v, w} P] [CategoryTheory.Preadditive P] [CategoryTheory.Linear k P] (J : CategoryTheory.Functor P C) [J.Additive] [CategoryTheory.Functor.Linear k J] (hproperty : ∀ (X : C), IsFiniteDimensionalModule k (restrictedLinearYonedaLinearModule J X)) : CategoryTheory.Functor C (FiniteDimensionalModuleCategory k)

Restricted Yoneda with a finite-dimensional target, using finite incoming support rather than finiteness of the entire source category.

instance MagnitudeConjecture.CoveringHom.finiteSupportRestrictedLinearYonedaFunctor_additive {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {P : Type w} [CategoryTheory.Category.{v, w} P] [CategoryTheory.Preadditive P] [CategoryTheory.Linear k P] (J : CategoryTheory.Functor P C) [J.Additive] [CategoryTheory.Functor.Linear k J] (hproperty : ∀ (X : C), IsFiniteDimensionalModule k (restrictedLinearYonedaLinearModule J X)) : (finiteSupportRestrictedLinearYonedaFunctor J hproperty).Additive

instance MagnitudeConjecture.CoveringHom.finiteSupportRestrictedLinearYonedaFunctor_linear {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {P : Type w} [CategoryTheory.Category.{v, w} P] [CategoryTheory.Preadditive P] [CategoryTheory.Linear k P] (J : CategoryTheory.Functor P C) [J.Additive] [CategoryTheory.Functor.Linear k J] (hproperty : ∀ (X : C), IsFiniteDimensionalModule k (restrictedLinearYonedaLinearModule J X)) : CategoryTheory.Functor.Linear k (finiteSupportRestrictedLinearYonedaFunctor J hproperty)

theorem MagnitudeConjecture.CoveringHom.finiteSupportRestrictedLinearYonedaFunctor_faithful_of_sourceDetection {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {P : Type w} [CategoryTheory.Category.{v, w} P] [CategoryTheory.Preadditive P] [CategoryTheory.Linear k P] (J : CategoryTheory.Functor P C) [J.Additive] [CategoryTheory.Functor.Linear k J] (hproperty : ∀ (X : C), IsFiniteDimensionalModule k (restrictedLinearYonedaLinearModule J X)) (hdetect : ∀ {X Y : C} (f : X ⟶ Y), f ≠ 0 → ∃ (Z : P) (g : J.obj Z ⟶ X), CategoryTheory.CategoryStruct.comp g f ≠ 0) : (finiteSupportRestrictedLinearYonedaFunctor J hproperty).Faithful

The finite-support target restriction preserves the source-detection criterion for faithfulness.

def MagnitudeConjecture.CoveringHom.finiteRestrictedLinearYonedaFunctor {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {P : Type w} [CategoryTheory.Category.{v, w} P] [CategoryTheory.Preadditive P] [CategoryTheory.Linear k P] (J : CategoryTheory.Functor P C) [J.Additive] [CategoryTheory.Functor.Linear k J] [Fintype P] (hfinite : ∀ (X : C) (Y : P), FiniteDimensional k (J.obj Y ⟶ X)) : CategoryTheory.Functor C (FiniteDimensionalModuleCategory k)

The finite-dimensional restricted Yoneda realization.

instance MagnitudeConjecture.CoveringHom.finiteRestrictedLinearYonedaFunctor_additive {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {P : Type w} [CategoryTheory.Category.{v, w} P] [CategoryTheory.Preadditive P] [CategoryTheory.Linear k P] (J : CategoryTheory.Functor P C) [J.Additive] [CategoryTheory.Functor.Linear k J] [Fintype P] (hfinite : ∀ (X : C) (Y : P), FiniteDimensional k (J.obj Y ⟶ X)) : (finiteRestrictedLinearYonedaFunctor J hfinite).Additive

instance MagnitudeConjecture.CoveringHom.finiteRestrictedLinearYonedaFunctor_linear {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {P : Type w} [CategoryTheory.Category.{v, w} P] [CategoryTheory.Preadditive P] [CategoryTheory.Linear k P] (J : CategoryTheory.Functor P C) [J.Additive] [CategoryTheory.Functor.Linear k J] [Fintype P] (hfinite : ∀ (X : C) (Y : P), FiniteDimensional k (J.obj Y ⟶ X)) : CategoryTheory.Functor.Linear k (finiteRestrictedLinearYonedaFunctor J hfinite)

theorem MagnitudeConjecture.CoveringHom.finiteRestrictedLinearYonedaFunctor_faithful_of_sourceDetection {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {P : Type w} [CategoryTheory.Category.{v, w} P] [CategoryTheory.Preadditive P] [CategoryTheory.Linear k P] (J : CategoryTheory.Functor P C) [J.Additive] [CategoryTheory.Functor.Linear k J] [Fintype P] (hfinite : ∀ (X : C) (Y : P), FiniteDimensional k (J.obj Y ⟶ X)) (hdetect : ∀ {X Y : C} (f : X ⟶ Y), f ≠ 0 → ∃ (Z : P) (g : J.obj Z ⟶ X), CategoryTheory.CategoryStruct.comp g f ≠ 0) : (finiteRestrictedLinearYonedaFunctor J hfinite).Faithful

The finite-dimensional target restriction preserves the preceding source-detection criterion for faithfulness.