Magnitude conjecture

MagnitudeConjecture.CategoryTheory.FiniteCategoryAlgebraOpposite

Opposite algebras of finite linear categories #

The finite category algebra built from covariant representables of C is canonically isomorphic to the opposite of the corresponding algebra for Cᵒᵖ. The equivalence transposes the representable-summand matrix and sends each canonical projector to the opposite of the matching projector.

source
@[instance_reducible]
noncomputable def MagnitudeConjecture.CoveringHom.finiteCategoryAlgebraOppositeFintype {C : Type} [Fintype C] :
Fintype Cᵒᵖ
Instances For
    source
    noncomputable def MagnitudeConjecture.CoveringHom.finiteCategoryProjectiveGenerator.categoryAlgebraOppositeEquiv {k : Type u} [Field k] {C : Type} [CategoryTheory.Category.{u, 0} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] [Fintype C] (hC : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)) (hOp : ∀ (X : Cᵒᵖ), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)) :
    algebra hC ≃ₐ[k] (algebra hOp)ᵐᵒᵖ
    Instances For
      source
      theorem MagnitudeConjecture.CoveringHom.finiteCategoryProjectiveGenerator.categoryAlgebraOppositeEquiv_canonicalProjector {k : Type u} [Field k] {C : Type} [CategoryTheory.Category.{u, 0} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] [Fintype C] (hC : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)) (hOp : ∀ (X : Cᵒᵖ), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)) (X : C) :
      (categoryAlgebraOppositeEquiv hC hOp) (canonicalProjector hC X) = MulOpposite.op (canonicalProjector hOp (Opposite.op X))