The projective generator of a finite linear category

For a finite-object locally bounded linear category, the biproduct of all covariant representables is a finite projective generator of its finite- dimensional module category. The represented functor to modules over its endomorphism algebra is therefore full and faithful. This is the first half of the finite-category-algebra bridge used in the manuscript's local directed deletion theorem.

@[reducible, inline]

noncomputable abbrev MagnitudeConjecture.CoveringHom.finiteCategoryProjectiveGenerator {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] [Fintype C] (hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)) : FiniteDimensionalModuleCategory k

The biproduct of all covariant representables of a finite linear category.

noncomputable def MagnitudeConjecture.CoveringHom.finiteCategoryProjectiveGenerator.representableRetract {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] [Fintype C] (hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)) (X : C) : CategoryTheory.Retract (MagnitudeConjecture.CoveringHom.finiteCategoryProjectiveGenerator.representable✝ hP X) (finiteCategoryProjectiveGenerator hP)

Each representable is a retract of the finite projective generator.

noncomputable def MagnitudeConjecture.CoveringHom.finiteCategoryProjectiveGenerator.finiteRepresentableSumPresentation {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] [Fintype C] (hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)) {n : ℕ} (X : Fin n → C) : CategoryTheory.FiniteAddPresentation (finiteCategoryProjectiveGenerator hP) (⨁ fun (i : Fin n) => MagnitudeConjecture.CoveringHom.finiteCategoryProjectiveGenerator.representable✝ hP (X i))

A finite sum of representables belongs to the additive closure of the finite projective generator.

instance MagnitudeConjecture.CoveringHom.finiteCategoryProjectiveGenerator.projective {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] [Fintype C] (hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)) : CategoryTheory.Projective (finiteCategoryProjectiveGenerator hP)

The finite projective generator is projective.

noncomputable def MagnitudeConjecture.CoveringHom.finiteCategoryProjectiveGenerator.toFiniteAddGeneratorPresentation {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] [Fintype C] (hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)) {M : FiniteDimensionalModuleCategory k} (P : TwoStepFiniteRepresentablePresentation hP M) : CategoryTheory.FiniteAddGeneratorPresentation (finiteCategoryProjectiveGenerator hP) M

A two-step finite-representable presentation is also a presentation by the single finite projective generator.

theorem MagnitudeConjecture.CoveringHom.finiteCategoryProjectiveGenerator.finiteAddGeneratorPresentation_nonempty {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] [Fintype C] (hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)) (M : FiniteDimensionalModuleCategory k) : Nonempty (CategoryTheory.FiniteAddGeneratorPresentation (finiteCategoryProjectiveGenerator hP) M)

Every finite-dimensional module has a two-term presentation by the finite projective generator.

instance MagnitudeConjecture.CoveringHom.finiteCategoryProjectiveGenerator.representedFaithful {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] [Fintype C] (hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)) : (CategoryTheory.preadditiveCoyonedaObj (finiteCategoryProjectiveGenerator hP)).Faithful

The represented functor of the finite projective generator is faithful.

instance MagnitudeConjecture.CoveringHom.finiteCategoryProjectiveGenerator.representedFull {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] [Fintype C] (hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)) : (CategoryTheory.preadditiveCoyonedaObj (finiteCategoryProjectiveGenerator hP)).Full

The represented functor of the finite projective generator is full.

@[reducible, inline]

abbrev MagnitudeConjecture.CoveringHom.finiteCategoryProjectiveGenerator.algebra {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] [Fintype C] (hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)) : Type (max u v)

The finite category algebra in the right-module convention.

theorem MagnitudeConjecture.CoveringHom.finiteCategoryProjectiveGenerator.algebra_finiteDimensional {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] [Fintype C] (hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)) : FiniteDimensional k (algebra hP)

The finite category algebra is finite-dimensional over the coefficient field.

noncomputable def MagnitudeConjecture.CoveringHom.finiteCategoryProjectiveGenerator.representedFGFunctor {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] [Fintype C] (hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)) : CategoryTheory.Functor (FiniteDimensionalModuleCategory k) (FGModuleCat (algebra hP)ᵐᵒᵖ)

Hom(G,-) restricted to finitely generated right modules over the finite category algebra.

instance MagnitudeConjecture.CoveringHom.finiteCategoryProjectiveGenerator.representedFGFunctor_additive {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] [Fintype C] (hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)) : (representedFGFunctor hP).Additive

The target restriction of the represented functor remains additive.

instance MagnitudeConjecture.CoveringHom.finiteCategoryProjectiveGenerator.representedFGFunctor_linear {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] [Fintype C] (hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)) : CategoryTheory.Functor.Linear k (representedFGFunctor hP)

The target-restricted represented functor respects the coefficient-field linear structures.

instance MagnitudeConjecture.CoveringHom.finiteCategoryProjectiveGenerator.representedFGFunctor_faithful {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] [Fintype C] (hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)) : (representedFGFunctor hP).Faithful

The target-restricted represented functor remains faithful.

instance MagnitudeConjecture.CoveringHom.finiteCategoryProjectiveGenerator.representedFGFunctor_full {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] [Fintype C] (hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)) : (representedFGFunctor hP).Full

The target-restricted represented functor remains full.

@[reducible, inline]

noncomputable abbrev MagnitudeConjecture.CoveringHom.finiteCategoryProjectiveGenerator.generatorPower {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] [Fintype C] (hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)) (n : ℕ) : FiniteDimensionalModuleCategory k

A finite power of the projective generator.

noncomputable def MagnitudeConjecture.CoveringHom.finiteCategoryProjectiveGenerator.representedGeneratorPowerIso {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] [Fintype C] (hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)) (n : ℕ) : (CategoryTheory.preadditiveCoyonedaObj (finiteCategoryProjectiveGenerator hP)).obj (generatorPower hP n) ≅ ModuleCat.of (algebra hP)ᵐᵒᵖ (Fin n → (algebra hP)ᵐᵒᵖ)

The represented module of a finite generator power is the corresponding finite free module over the opposite endomorphism algebra.

theorem MagnitudeConjecture.CoveringHom.finiteCategoryProjectiveGenerator.representedFGFunctor_essSurj {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] [Fintype C] (hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)) : (representedFGFunctor hP).EssSurj

Every finitely generated right module over the finite category algebra is represented.

noncomputable def MagnitudeConjecture.CoveringHom.finiteCategoryProjectiveGenerator.moduleEquivalence {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] [Fintype C] (hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)) : FiniteDimensionalModuleCategory k ≌ FGModuleCat (algebra hP)ᵐᵒᵖ

Finite-dimensional modules over a finite linear category are equivalent to finitely generated right modules over its finite category algebra.