Transport of represented modules along a fully faithful linear functor

noncomputable def MagnitudeConjecture.CategoryTheory.representedEndEquiv {k : Type t} [Field k] {C : Type u} {D : Type v} [CategoryTheory.Category.{w, u} C] [CategoryTheory.Category.{z, v} D] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [CategoryTheory.Linear k C] [CategoryTheory.Linear k D] (F : CategoryTheory.Functor C D) [F.Additive] [CategoryTheory.Functor.Linear k F] [F.Full] [F.Faithful] {P : C} {Q : D} (e : F.obj P ≅ Q) : CategoryTheory.End P ≃ₐ[k] CategoryTheory.End Q

The algebra comparison induced by realization and a chosen generator isomorphism.

noncomputable def MagnitudeConjecture.CategoryTheory.representedHomEquiv {k : Type t} [Field k] {C : Type u} {D : Type v} [CategoryTheory.Category.{w, u} C] [CategoryTheory.Category.{z, v} D] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [CategoryTheory.Linear k C] [CategoryTheory.Linear k D] (F : CategoryTheory.Functor C D) [F.Additive] [CategoryTheory.Functor.Linear k F] [F.Full] [F.Faithful] {P : C} {Q : D} (e : F.obj P ≅ Q) (X : C) : (P ⟶ X) ≃ₗ[k] Q ⟶ F.obj X

Hom from the generator is unchanged by fully faithful realization.

theorem MagnitudeConjecture.CategoryTheory.representedHomEquiv_precomp {k : Type t} [Field k] {C : Type u} {D : Type v} [CategoryTheory.Category.{w, u} C] [CategoryTheory.Category.{z, v} D] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [CategoryTheory.Linear k C] [CategoryTheory.Linear k D] (F : CategoryTheory.Functor C D) [F.Additive] [CategoryTheory.Functor.Linear k F] [F.Full] [F.Faithful] {P : C} {Q : D} (e : F.obj P ≅ Q) (X : C) (a : CategoryTheory.End P) (f : P ⟶ X) : (representedHomEquiv F e X) (CategoryTheory.CategoryStruct.comp a.asHom f) = CategoryTheory.CategoryStruct.comp ((representedEndEquiv F e) a).asHom ((representedHomEquiv F e X) f)

This comparison preserves the right endomorphism-algebra action.

theorem MagnitudeConjecture.CategoryTheory.representedHomEquiv_postcomp {k : Type t} [Field k] {C : Type u} {D : Type v} [CategoryTheory.Category.{w, u} C] [CategoryTheory.Category.{z, v} D] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [CategoryTheory.Linear k C] [CategoryTheory.Linear k D] (F : CategoryTheory.Functor C D) [F.Additive] [CategoryTheory.Functor.Linear k F] [F.Full] [F.Faithful] {P : C} {Q : D} (e : F.obj P ≅ Q) {X Y : C} (f : P ⟶ X) (g : X ⟶ Y) : (representedHomEquiv F e Y) (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp ((representedHomEquiv F e X) f) (F.map g)

The comparison is natural in the target.

noncomputable def MagnitudeConjecture.CategoryTheory.representedModuleEquiv {k : Type t} [Field k] {C : Type u} {D : Type v} [CategoryTheory.Category.{w, u} C] [CategoryTheory.Category.{z, v} D] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [CategoryTheory.Linear k C] [CategoryTheory.Linear k D] (F : CategoryTheory.Functor C D) [F.Additive] [CategoryTheory.Functor.Linear k F] [F.Full] [F.Faithful] {P : C} {Q : D} (e : F.obj P ≅ Q) (X : C) : (P ⟶ X) ≃ₗ[(CategoryTheory.End P)ᵐᵒᵖ] Q ⟶ F.obj X

After restriction along the opposite algebra comparison, the Hom comparison is an isomorphism of actual right modules.

noncomputable def MagnitudeConjecture.CategoryTheory.representedModuleEquivOverTarget {k : Type t} [Field k] {C : Type u} {D : Type v} [CategoryTheory.Category.{w, u} C] [CategoryTheory.Category.{z, v} D] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [CategoryTheory.Linear k C] [CategoryTheory.Linear k D] (F : CategoryTheory.Functor C D) [F.Additive] [CategoryTheory.Functor.Linear k F] [F.Full] [F.Faithful] {P : C} {Q : D} (e : F.obj P ≅ Q) (X : C) : (P ⟶ X) ≃ₗ[(CategoryTheory.End Q)ᵐᵒᵖ] Q ⟶ F.obj X

The same comparison over the realized generator algebra, restricting the source action along the inverse algebra equivalence.