Magnitude conjecture

MagnitudeConjecture.Algebra.SpecialBiserialAlgebra

Special-biserial algebras up to Morita equivalence #

The frozen manuscript calls an algebra special biserial when its basic algebra admits a special-biserial bound-quiver presentation. This file records that convention literally: a witness consists of a Morita-equivalent algebra and the exact bound-quiver presentation from BoundQuiverPresentation. Such a bound-quiver algebra is itself the chosen basic representative, so basicness is not stored as a redundant field.

source
structure MagnitudeConjecture.BoundQuiver.SpecialBiserialMoritaModel (k A : Type u) [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] :
Type (u + 1)

A special-biserial bound-quiver representative of the Morita class of A.

Instances For
    source
    def MagnitudeConjecture.BoundQuiver.SpecialBiserialMoritaModel.precompMorita {k A B : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [Ring B] [Algebra k B] [FiniteDimensional k B] (M : SpecialBiserialMoritaModel k A) (e : MoritaEquivalence k B A) :
    SpecialBiserialMoritaModel k B

    Change the source algebra of a special-biserial Morita model.

    Instances For
      source
      def MagnitudeConjecture.BoundQuiver.IsSpecialBiserial (k A : Type u) [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] :
      Prop

      The manuscript's convention for an arbitrary finite-dimensional algebra: some basic representative of its Morita class has a special-biserial bound-quiver presentation.

      Instances For
        source
        theorem MagnitudeConjecture.BoundQuiver.isSpecialBiserial_of_presentation {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] (hpresentation : AdmitsSpecialBiserialPresentation k A) :
        IsSpecialBiserial k A

        An algebra carrying the literal presentation is special biserial in the manuscript's Morita-invariant sense.

        source
        theorem MagnitudeConjecture.BoundQuiver.isSpecialBiserial_iff_of_moritaEquivalence {k A B : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [Ring B] [Algebra k B] [FiniteDimensional k B] (e : MoritaEquivalence k A B) :
        IsSpecialBiserial k A ↔ IsSpecialBiserial k B

        Special biseriality depends only on the Morita class of the algebra.

        source
        theorem MagnitudeConjecture.BoundQuiver.isSpecialBiserial_iff_of_algEquiv {k A B : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [Ring B] [Algebra k B] [FiniteDimensional k B] (e : A ≃ₐ[k] B) :
        IsSpecialBiserial k A ↔ IsSpecialBiserial k B

        In particular, special biseriality is invariant under algebra equivalence.