Magnitude conjecture

MagnitudeConjecture.CategoryTheory.BiserialObject

Biserial objects #

This file packages the simple-top form of biseriality intrinsically in the subobject lattice of an abelian category. The formulation is designed to be transported through categorical equivalences, without retaining coordinates from a category algebra.

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

An object is biserial when its unique maximal subobject is the join of two chains whose intersection is zero or simple.

Instances For
    source
    theorem MagnitudeConjecture.IsBiserialObject.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
    source
    theorem MagnitudeConjecture.IsBiserialObject.congrOrderIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Abelian C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {X : C} [CategoryTheory.Abelian D] {Y : D} (hX : IsBiserialObject X) (e : CategoryTheory.Subobject X ≃o CategoryTheory.Subobject Y) :
    IsBiserialObject Y

    Intrinsic biseriality is invariant under an order isomorphism of subobject lattices.

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

    Intrinsic biseriality is invariant under isomorphism.

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

    An equivalence sends biserial objects to biserial objects.

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

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

    source
    theorem MagnitudeConjecture.IsBiserialObject.of_fullSubcategory_ambient {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Abelian C] (P : CategoryTheory.ObjectProperty C) [P.ContainsZero] [P.IsClosedUnderSubobjects] [CategoryTheory.Abelian P.FullSubcategory] {Z : P.FullSubcategory} (hZ : IsBiserialObject Z.obj) :
    IsBiserialObject Z

    Intrinsic biseriality in an ambient abelian category restricts to a full abelian subcategory closed under subobjects.

    source
    theorem MagnitudeConjecture.IsBiserialObject.to_fullSubcategory_ambient {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Abelian C] (P : CategoryTheory.ObjectProperty C) [P.ContainsZero] [P.IsClosedUnderSubobjects] [CategoryTheory.Abelian P.FullSubcategory] {Z : P.FullSubcategory} (hZ : IsBiserialObject Z) :
    IsBiserialObject Z.obj

    Intrinsic biseriality in a full abelian subcategory closed under subobjects also holds in the ambient category.

    source
    theorem MagnitudeConjecture.IsBiserialModule.toIsBiserialObject {R : Type uR} [Ring R] {M : Type uM} [AddCommGroup M] [Module R M] (hbis : IsBiserialModule R M) (htop : IsSimpleModule R (M ⧸ Module.jacobson R M)) :
    IsBiserialObject (ModuleCat.of R M)

    A biserial module with simple top is intrinsically biserial as an object of the module category.

    source
    theorem MagnitudeConjecture.IsBiserialModule.toFGModuleCatIsBiserialObject {R : Type uR} [Ring R] [IsNoetherianRing R] (N : FGModuleCat R) (hbis : IsBiserialModule R ↑N) (htop : IsSimpleModule R (↑N ⧸ Module.jacobson R ↑N)) :
    IsBiserialObject N

    A biserial finitely generated module with simple top is intrinsically biserial in the finitely generated module category.

    source
    theorem MagnitudeConjecture.IsBiserialObject.toIsBiserialModule {R : Type uR} [Ring R] {M : Type uM} [AddCommGroup M] [Module R M] (hbis : IsBiserialObject (ModuleCat.of R M)) :
    IsBiserialModule R M

    Intrinsic biseriality of a module-category object recovers the usual module-theoretic biserial decomposition.

    source
    theorem MagnitudeConjecture.IsBiserialObject.toIsBiserialModule_of_fg {R : Type uR} [Ring R] [IsNoetherianRing R] (N : FGModuleCat R) (hN : IsBiserialObject N) :
    IsBiserialModule R ↑N

    Intrinsic biseriality in the finitely generated module category recovers the usual biserial decomposition of the underlying module.