Magnitude conjecture

MagnitudeConjecture.CategoryTheory.UniserialObject

Uniserial objects #

The covering part of the magnitude proof uses modules over finite and locally bounded linear categories. This file packages uniseriality intrinsically as totality of the categorical subobject order, independently of any chosen category algebra.

source
def MagnitudeConjecture.IsUniserialObject {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) :
Prop

An object is uniserial when any two of its subobjects are comparable.

Instances For
    source
    theorem MagnitudeConjecture.IsUniserialObject.total_of_orderIso {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (e : α ≃o β) (h : Std.Total fun (x1 x2 : α) => x1 ≤ x2) :
    Std.Total fun (x1 x2 : β) => x1 ≤ x2

    Totality of an order is invariant under an order isomorphism.

    source
    theorem MagnitudeConjecture.IsUniserialObject.congrOrderIso {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] {X : C} {Y : D} (hX : IsUniserialObject X) (e : CategoryTheory.Subobject X ≃o CategoryTheory.Subobject Y) :
    IsUniserialObject Y

    Uniseriality is invariant under an order isomorphism of subobject lattices.

    source
    theorem MagnitudeConjecture.IsUniserialObject.subobject_iff_total_Iic {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} (R : CategoryTheory.Subobject X) :
    IsUniserialObject (CategoryTheory.Subobject.underlying.obj R) ↔ Std.Total fun (x1 x2 : ↑(Set.Iic R)) => x1 ≤ x2

    The underlying object of a subobject is uniserial exactly when the subobjects below it form a chain.

    source
    theorem MagnitudeConjecture.IsUniserialObject.congr {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (hX : IsUniserialObject X) (e : X ≅ Y) :
    IsUniserialObject Y

    Uniseriality is invariant under isomorphism.

    source
    theorem MagnitudeConjecture.IsUniserialObject.map_equivalence {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] {X : C} (hX : IsUniserialObject X) (E : C ≌ D) :
    IsUniserialObject (E.functor.obj X)

    An equivalence sends uniserial objects to uniserial objects.

    source
    theorem MagnitudeConjecture.IsUniserialObject.of_map_equivalence {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] {X : C} (E : C ≌ D) (hEX : IsUniserialObject (E.functor.obj X)) :
    IsUniserialObject X

    Uniseriality of the image under an equivalence reflects to the source.

    source
    theorem MagnitudeConjecture.IsUniserialObject.op {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} [CategoryTheory.Abelian C] (hX : IsUniserialObject X) :
    IsUniserialObject (Opposite.op X)

    Passing to the opposite category preserves uniseriality. The subobject-order correspondence reverses order, which does not affect totality.

    source
    theorem MagnitudeConjecture.IsUniserialObject.subobject {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} (hX : IsUniserialObject X) (R : CategoryTheory.Subobject X) :
    IsUniserialObject (CategoryTheory.Subobject.underlying.obj R)

    The object underlying a subobject of a uniserial object is uniserial.

    source
    def MagnitudeConjecture.IsUniserialObject.IsRadicalSubobject {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} (R : CategoryTheory.Subobject X) :
    Prop

    A subobject is radical when it contains every proper subobject of its ambient object.

    Instances For
      source
      theorem MagnitudeConjecture.IsUniserialObject.of_radicalSubobject {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} (R : CategoryTheory.Subobject X) (hR : IsRadicalSubobject R) (hRU : IsUniserialObject (CategoryTheory.Subobject.underlying.obj R)) :
      IsUniserialObject X

      An object whose radical subobject is uniserial is itself uniserial.

      source
      theorem MagnitudeConjecture.IsUniserialObject.of_isZero {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} (hX : CategoryTheory.Limits.IsZero X) :
      IsUniserialObject X

      Every zero object is uniserial.

      source
      theorem MagnitudeConjecture.IsUniserialModule.iff_moduleCat {R : Type uR} [Ring R] {M : Type uM} [AddCommGroup M] [Module R M] :
      IsUniserialModule R M ↔ IsUniserialObject (ModuleCat.of R M)

      The module-theoretic and categorical definitions of uniseriality agree.

      source
      theorem MagnitudeConjecture.IsUniserialModule.toFGModuleCatIsUniserialObject {R : Type uR} [Ring R] [IsNoetherianRing R] (N : FGModuleCat R) (hN : IsUniserialModule R ↑N) :
      IsUniserialObject N

      A finitely generated uniserial module is intrinsically uniserial in the finitely generated module category.