Finite category algebras under object-bijective linear equivalence

A linear equivalence of finite categories need not preserve the chosen category algebra: an equivalent category may contain duplicate isomorphic objects, and the biproduct of all representables then changes. This file records the exact replacement. When the forward functor is literally bijective on objects, precomposition identifies corresponding representables, the two finite projective generators, and hence their endomorphism algebras.

noncomputable def MagnitudeConjecture.CategoryTheory.Functor.mapLinearEquivOfFullyFaithful {k : Type uK} [Field k] {C : Type uC} {D : Type uD} [CategoryTheory.Category.{vC, uC} C] [CategoryTheory.Category.{vD, uD} 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] (X Y : C) : (X ⟶ Y) ≃ₗ[k] F.obj X ⟶ F.obj Y

A fully faithful linear functor identifies Hom spaces linearly.

noncomputable def MagnitudeConjecture.CategoryTheory.Functor.endAlgEquivOfFullyFaithful {k : Type uK} [Field k] {C : Type uC} {D : Type uD} [CategoryTheory.Category.{vC, uC} C] [CategoryTheory.Category.{vD, uD} 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] (X : C) : CategoryTheory.End X ≃ₐ[k] CategoryTheory.End (F.obj X)

A fully faithful linear functor identifies endomorphism algebras.

noncomputable def MagnitudeConjecture.CategoryTheory.Iso.endAlgEquiv {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {X Y : C} (e : X ≅ Y) : CategoryTheory.End X ≃ₐ[k] CategoryTheory.End Y

Conjugation along an isomorphism is an equivalence of endomorphism algebras.

theorem MagnitudeConjecture.CoveringHom.linearCoyonedaFiniteOfFullyFaithful {k : Type v} [Field k] {C : Type uC} {D : Type uD} [CategoryTheory.Category.{v, uC} C] [CategoryTheory.Category.{v, uD} D] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [CategoryTheory.Linear k C] [CategoryTheory.Linear k D] [Fintype C] (F : CategoryTheory.Functor C D) [F.Additive] [CategoryTheory.Functor.Linear k F] [F.Full] [F.Faithful] (hD : ∀ (Y : D), IsFiniteDimensionalModule k (linearCoyonedaLinearModule Y)) (X : C) : IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)

Finite-dimensional representables pull back along a fully faithful linear functor whose source has finitely many objects.

theorem MagnitudeConjecture.CoveringHom.finiteDimensionalLinearCoyoneda_isBiserialObject_iff_of_equivalence {k : Type v} [Field k] {C : Type uC} {D : Type uD} [CategoryTheory.Category.{v, uC} C] [CategoryTheory.Category.{v, uD} D] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [CategoryTheory.Linear k C] [CategoryTheory.Linear k D] (hC : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)) (hD : ∀ (Y : D), IsFiniteDimensionalModule k (linearCoyonedaLinearModule Y)) (e : C ≌ D) [e.functor.Additive] [CategoryTheory.Functor.Linear k e.functor] (hobj : Function.Bijective e.functor.obj) (X : C) : IsBiserialObject ((finiteDimensionalLinearCoyonedaFunctor hD).obj (Opposite.op (e.functor.obj X))) ↔ IsBiserialObject ((finiteDimensionalLinearCoyonedaFunctor hC).obj (Opposite.op X))

A linear equivalence that is bijective on objects preserves intrinsic biseriality of the corresponding covariant representables.

noncomputable def MagnitudeConjecture.CoveringHom.finiteCategoryProjectiveGeneratorCongrIso {k : Type v} [Field k] {C : Type uC} {D : Type uD} [CategoryTheory.Category.{v, uC} C] [CategoryTheory.Category.{v, uD} D] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [CategoryTheory.Linear k C] [CategoryTheory.Linear k D] [Fintype C] [Fintype D] (hC : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)) (hD : ∀ (Y : D), IsFiniteDimensionalModule k (linearCoyonedaLinearModule Y)) (e : C ≌ D) [e.functor.Additive] [CategoryTheory.Functor.Linear k e.functor] (hobj : Function.Bijective e.functor.obj) : (MagnitudeConjecture.CoveringHom.moduleCongrEquivalence✝ e hobj).functor.obj (finiteCategoryProjectiveGenerator hD) ≅ finiteCategoryProjectiveGenerator hC

The object-bijective base equivalence identifies the two chosen finite projective generators.

noncomputable def MagnitudeConjecture.CoveringHom.finiteCategoryAlgebraMapEquiv {k : Type v} [Field k] {C : Type uC} {D : Type uD} [CategoryTheory.Category.{v, uC} C] [CategoryTheory.Category.{v, uD} D] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [CategoryTheory.Linear k C] [CategoryTheory.Linear k D] [Fintype D] (hD : ∀ (Y : D), IsFiniteDimensionalModule k (linearCoyonedaLinearModule Y)) (e : C ≌ D) [e.functor.Additive] [CategoryTheory.Functor.Linear k e.functor] (hobj : Function.Bijective e.functor.obj) : finiteCategoryProjectiveGenerator.algebra hD ≃ₐ[k] CategoryTheory.End ((MagnitudeConjecture.CoveringHom.moduleCongrEquivalence✝ e hobj).functor.obj (finiteCategoryProjectiveGenerator hD))

The fully faithful part of the finite category algebra equivalence, before conjugating the transported projective generator back to the chosen one.

noncomputable def MagnitudeConjecture.CoveringHom.finiteCategoryAlgebraConjEquiv {k : Type v} [Field k] {C : Type uC} {D : Type uD} [CategoryTheory.Category.{v, uC} C] [CategoryTheory.Category.{v, uD} D] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [CategoryTheory.Linear k C] [CategoryTheory.Linear k D] [Fintype C] [Fintype D] (hC : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)) (hD : ∀ (Y : D), IsFiniteDimensionalModule k (linearCoyonedaLinearModule Y)) (e : C ≌ D) [e.functor.Additive] [CategoryTheory.Functor.Linear k e.functor] (hobj : Function.Bijective e.functor.obj) : CategoryTheory.End ((MagnitudeConjecture.CoveringHom.moduleCongrEquivalence✝ e hobj).functor.obj (finiteCategoryProjectiveGenerator hD)) ≃ₐ[k] finiteCategoryProjectiveGenerator.algebra hC

Conjugation by the transported-generator isomorphism is the second part of the finite category algebra equivalence.

noncomputable def MagnitudeConjecture.CoveringHom.finiteCategoryAlgebraEquiv {k : Type v} [Field k] {C : Type uC} {D : Type uD} [CategoryTheory.Category.{v, uC} C] [CategoryTheory.Category.{v, uD} D] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [CategoryTheory.Linear k C] [CategoryTheory.Linear k D] [Fintype C] [Fintype D] (hC : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)) (hD : ∀ (Y : D), IsFiniteDimensionalModule k (linearCoyonedaLinearModule Y)) (e : C ≌ D) [e.functor.Additive] [CategoryTheory.Functor.Linear k e.functor] (hobj : Function.Bijective e.functor.obj) : finiteCategoryProjectiveGenerator.algebra hC ≃ₐ[k] finiteCategoryProjectiveGenerator.algebra hD

An object-bijective linear equivalence identifies the finite category algebras, not merely their Morita classes.