Magnitude conjecture

MagnitudeConjecture.CategoryTheory.LocallyBoundedOpposite

Locally bounded opposite categories #

The locally bounded package used by the covering argument is self-dual. This file records the variance change explicitly, including finite object support and the opposite endomorphism ring.

source
def MagnitudeConjecture.CoveringHom.oppositeEndRingEquiv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (X : C) :
(CategoryTheory.End X)ᵐᵒᵖ ≃+* CategoryTheory.End (Opposite.op X)

Endomorphisms in the opposite category form the opposite endomorphism ring.

Instances For
    source
    theorem MagnitudeConjecture.CoveringHom.isLocalRing_mulOpposite {R : Type v} [Ring R] [IsLocalRing R] :
    IsLocalRing Rᵐᵒᵖ

    A noncommutative local ring remains local after reversing multiplication.

    source
    theorem MagnitudeConjecture.CoveringHom.IsLocallyBounded.op {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (H : IsLocallyBounded) :
    IsLocallyBounded

    Locally boundedness is preserved by passage to the opposite category. The covariant-representable support on the opposite is controlled by the dual-corepresentable support on the original category, and conversely.