theorem MagnitudeConjecture.CategoryTheory.preadditiveCoyonedaObj_faithful_of_regular_finiteAddClosure {R : Type u} [Ring R] (G : ModuleCat R) (hregular : finiteAddClosure G (ModuleCat.of R R)) : (CategoryTheory.preadditiveCoyonedaObj G).Faithful

If the regular module belongs to the finite additive closure of G, then the all-module restricted Yoneda functor represented by G is faithful.

theorem MagnitudeConjecture.CategoryTheory.preadditiveCoyonedaObj_full_of_regular_finiteAddClosure {R : Type u} [Ring R] (G : ModuleCat R) (hregular : finiteAddClosure G (ModuleCat.of R R)) : (CategoryTheory.preadditiveCoyonedaObj G).Full

If the regular module belongs to the finite additive closure of G, then the all-module restricted Yoneda functor represented by G is full.

noncomputable def MagnitudeConjecture.CategoryTheory.finsuppInclusion {R : Type u} [Ring R] (G : ModuleCat R) (ι : Type u) (i : ι) : G ⟶ ModuleCat.of R (ι →₀ ↑G)

The inclusion of one summand into an arbitrary direct sum of copies of a module, using the concrete Finsupp model.

noncomputable def MagnitudeConjecture.CategoryTheory.freeModuleRepresentableLinearMap {R : Type u} [Ring R] (G : ModuleCat R) (ι : Type u) : (ι →₀ (CategoryTheory.End G)ᵐᵒᵖ) →ₗ[(CategoryTheory.End G)ᵐᵒᵖ] G ⟶ ModuleCat.of R (ι →₀ ↑G)

The canonical map from a free module over (End G)ᵐᵒᵖ to the module represented by the corresponding direct sum of copies of G.

noncomputable def MagnitudeConjecture.CategoryTheory.freeModuleRepresentableMap {R : Type u} [Ring R] (G : ModuleCat R) (ι : Type u) : ModuleCat.of (CategoryTheory.End G)ᵐᵒᵖ (ι →₀ (CategoryTheory.End G)ᵐᵒᵖ) ⟶ (CategoryTheory.preadditiveCoyonedaObj G).obj (ModuleCat.of R (ι →₀ ↑G))

The categorical form of freeModuleRepresentableLinearMap.

noncomputable def MagnitudeConjecture.CategoryTheory.freeModuleRepresentableIso {R : Type u} [Ring R] (G : ModuleCat R) (ι : Type u) [Module.Finite R ↑G] : ModuleCat.of (CategoryTheory.End G)ᵐᵒᵖ (ι →₀ (CategoryTheory.End G)ᵐᵒᵖ) ≅ (CategoryTheory.preadditiveCoyonedaObj G).obj (ModuleCat.of R (ι →₀ ↑G))

If G is finitely generated, Hom(G, ι →₀ G) is the free (End G)ᵐᵒᵖ-module on ι, for an arbitrary index type ι.

theorem MagnitudeConjecture.CategoryTheory.preadditiveCoyonedaObj_essSurj_of_regular_finiteAddClosure {R : Type u} [Ring R] (G : ModuleCat R) [Module.Finite R ↑G] [CategoryTheory.Projective G] (hregular : finiteAddClosure G (ModuleCat.of R R)) : (CategoryTheory.preadditiveCoyonedaObj G).EssSurj

A finitely generated projective generator represents every module over its opposite endomorphism ring.

noncomputable def MagnitudeConjecture.CategoryTheory.moduleEquivalenceOfProgenerator {R : Type u} [Ring R] (G : ModuleCat R) [Module.Finite R ↑G] [CategoryTheory.Projective G] (hregular : finiteAddClosure G (ModuleCat.of R R)) : ModuleCat R ≌ ModuleCat (CategoryTheory.End G)ᵐᵒᵖ

The all-module equivalence represented by a finitely generated projective generator.

instance MagnitudeConjecture.CategoryTheory.preadditiveCoyonedaObj_linear {R : Type u} [Ring R] {k : Type v} [CommSemiring k] [Algebra k R] (G : ModuleCat R) : CategoryTheory.Functor.Linear k (CategoryTheory.preadditiveCoyonedaObj G)

The represented all-module functor respects the scalar action inherited from an algebra over a commutative semiring.

noncomputable def MagnitudeConjecture.CategoryTheory.moritaEquivalenceOfProgenerator {R : Type u} [Ring R] {k : Type v} [CommSemiring k] [Algebra k R] (G : ModuleCat R) [Module.Finite R ↑G] [CategoryTheory.Projective G] (hregular : finiteAddClosure G (ModuleCat.of R R)) : MoritaEquivalence k R (CategoryTheory.End G)ᵐᵒᵖ

The Morita equivalence supplied by a finitely generated projective generator, in Mathlib's all-module and linear convention.