The category algebra of an opposite category as a direct tuple #
@[instance_reducible]
def
MagnitudeConjecture.CoveringHom.categoryAlgebraOppositeTupleFintype
{C : Type}
[Fintype C]
:
Fintype Cᵒᵖ
Instances For
theorem
MagnitudeConjecture.CoveringHom.instAdditiveOppositeUnopUnop_magnitudeConjecture
{C : Type}
[CategoryTheory.Category.{v, 0} C]
[CategoryTheory.Preadditive C]
:
(CategoryTheory.unopUnop C).Additive
theorem
MagnitudeConjecture.CoveringHom.instLinearOppositeUnopUnop_magnitudeConjecture
{k : Type v}
[Field k]
{C : Type}
[CategoryTheory.Category.{v, 0} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Linear k C]
:
CategoryTheory.Functor.Linear k (CategoryTheory.unopUnop C)
noncomputable def
MagnitudeConjecture.CoveringHom.categoryAlgebraOppositeTupleEquiv
{k : Type v}
[Field k]
{C : Type}
[CategoryTheory.Category.{v, 0} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Linear k C]
[Fintype C]
{D : Type u}
[CategoryTheory.Category.{v, u} D]
[CategoryTheory.Preadditive D]
[CategoryTheory.Linear k D]
(F : CategoryTheory.Functor C D)
[F.Additive]
[CategoryTheory.Functor.Linear k F]
[F.Full]
[F.Faithful]
:
CategoryTheory.End categoryAlgebraTuple ≃ₐ[k] CategoryTheory.End { ι := C, fintype := inst✝, X := F.obj }
For a fully faithful linear realization, the algebra of the opposite category is the endomorphism algebra of the tuple of realized objects.