Dual-corepresentable coordinates on injective modules

Finite dual corepresentables are fully faithful coordinates once their values are finite-dimensional. Consequently they are indecomposable over objects with local endomorphism rings, and every indecomposable injective finite module is one of them.

@[simp]

theorem MagnitudeConjecture.CoveringHom.finiteDualLinearYonedaHomEquiv_functor_map_apply {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (hI : ∀ (X : C), IsFiniteDimensionalModule k (dualLinearYonedaLinearModule X)) {X Y : Cᵒᵖ} (f : X ⟶ Y) (phi : ↑(((finiteDimensionalDualLinearYonedaFunctor hI).obj X).obj.obj.obj (Opposite.unop Y))) : ((finiteDualLinearYonedaHomEquiv ((finiteDimensionalDualLinearYonedaFunctor hI).obj X) (Opposite.unop Y) ⋯) ((finiteDimensionalDualLinearYonedaFunctor hI).map f)) phi = (have this := phi; this) f.unop

The dual co-Yoneda coordinate of a map induced by a representing morphism is ordinary evaluation at that morphism.

instance MagnitudeConjecture.CoveringHom.finiteDimensionalDualLinearYonedaFunctor_faithful {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (hI : ∀ (X : C), IsFiniteDimensionalModule k (dualLinearYonedaLinearModule X)) : (finiteDimensionalDualLinearYonedaFunctor hI).Faithful

Finite dual corepresentables faithfully remember the representing morphism.

instance MagnitudeConjecture.CoveringHom.finiteDimensionalDualLinearYonedaFunctor_full {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (hI : ∀ (X : C), IsFiniteDimensionalModule k (dualLinearYonedaLinearModule X)) : (finiteDimensionalDualLinearYonedaFunctor hI).Full

Finite-dimensionality makes the double-dual coordinate construction surjective, hence finite dual corepresentables are full.

theorem MagnitudeConjecture.CoveringHom.finiteDimensionalDualLinearYoneda_end_isLocalRing {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (hI : ∀ (X : C), IsFiniteDimensionalModule k (dualLinearYonedaLinearModule X)) (hlocal : ∀ (X : C), IsLocalRing (CategoryTheory.End X)) (X : C) : IsLocalRing (CategoryTheory.End ((finiteDimensionalDualLinearYonedaFunctor hI).obj (Opposite.op X)))

A finite dual corepresentable has local endomorphism ring whenever its representing object does.

theorem MagnitudeConjecture.CoveringHom.finiteDimensionalDualLinearYoneda_indecomposable {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (hI : ∀ (X : C), IsFiniteDimensionalModule k (dualLinearYonedaLinearModule X)) (hlocal : ∀ (X : C), IsLocalRing (CategoryTheory.End X)) (X : C) : CategoryTheory.Indecomposable ((finiteDimensionalDualLinearYonedaFunctor hI).obj (Opposite.op X))

A finite dual corepresentable represented by an object with local endomorphism ring is indecomposable.

theorem MagnitudeConjecture.CoveringHom.indecomposable_injective_iso_finiteDimensionalDualLinearYoneda {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (hI : ∀ (X : C), IsFiniteDimensionalModule k (dualLinearYonedaLinearModule X)) (hlocal : ∀ (X : C), IsLocalRing (CategoryTheory.End X)) (M : FiniteDimensionalModuleCategory k) [CategoryTheory.Injective M] (hMind : CategoryTheory.Indecomposable M) : ∃ (X : C), Nonempty ((finiteDimensionalDualLinearYonedaFunctor hI).obj (Opposite.op X) ≅ M)

Every indecomposable injective finite module is a finite dual corepresentable.

structure MagnitudeConjecture.CoveringHom.FiniteDualCorepresentableCoordinates {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (hI : ∀ (X : C), IsFiniteDimensionalModule k (dualLinearYonedaLinearModule X)) (M : FiniteDimensionalModuleCategory k) : Type (max u v)

Literal finite dual-corepresentable coordinates on a finite injective module.

• n : ℕ
• X : Fin self.n → C
• isoSource : (⨁ fun (i : Fin self.n) => (finiteDimensionalDualLinearYonedaFunctor hI).obj (Opposite.op (self.X i))) ≅ M

theorem MagnitudeConjecture.CoveringHom.finiteDualCorepresentableCoordinates_nonempty_of_injective {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (hI : ∀ (X : C), IsFiniteDimensionalModule k (dualLinearYonedaLinearModule X)) (hlocal : ∀ (X : C), IsLocalRing (CategoryTheory.End X)) (M : FiniteDimensionalModuleCategory k) [CategoryTheory.Injective M] : Nonempty (FiniteDualCorepresentableCoordinates hI M)

Every finite injective module has finite coordinates by dual corepresentables when the representing objects have local endomorphism rings.

theorem MagnitudeConjecture.CoveringHom.finiteDimensionalModule_projective_of_injective_of_indec_projective {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (M : FiniteDimensionalModuleCategory k) [CategoryTheory.Injective M] (hprojective : ∀ (N : FiniteDimensionalModuleCategory k), CategoryTheory.Indecomposable N → CategoryTheory.Injective N → ∀ (i : N ⟶ M) (r : M ⟶ N), CategoryTheory.CategoryStruct.comp i r = CategoryTheory.CategoryStruct.id N → CategoryTheory.Projective N) : CategoryTheory.Projective M

An injective finite module is projective as soon as each of its indecomposable injective summands is projective. This packages the finite Krull--Schmidt reduction used in Auslander-category recovery.