Magnitude conjecture

MagnitudeConjecture.Algebra.BiserialLeftIdealOpposite

Left ideals as right ideals over the opposite algebra #

Restriction of scalars along A ≃ (Aᵐᵒᵖ)ᵐᵒᵖ identifies the principal right ideal generated by op e with the literal principal left ideal Ae. This identification transports intrinsic biseriality between the two objects.

source
def MagnitudeConjecture.RightModule.oppositeRightIdealLeftIdealLinearEquiv {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖᵐᵒᵖ] (e : A) :
↑(MagnitudeConjecture.RightModule.oppositeRightIdealLeftEquivalence✝.functor.obj (rightIdealFGObj (MulOpposite.op e))) ≃ₗ[A] ↑(leftIdealFGObj e)
Instances For
    source
    noncomputable def MagnitudeConjecture.RightModule.oppositeRightIdealLeftIdealIso {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖᵐᵒᵖ] (e : A) :
    MagnitudeConjecture.RightModule.oppositeRightIdealLeftEquivalence✝.functor.obj (rightIdealFGObj (MulOpposite.op e)) ≅ leftIdealFGObj e
    Instances For
      source
      theorem MagnitudeConjecture.RightModule.leftIdeal_isUniserial_of_oppositeRightIdeal {A : Type u} [Ring A] (e : A) (h : IsUniserialModule Aᵐᵒᵖᵐᵒᵖ ↥(rightIdeal (MulOpposite.op e))) :
      IsUniserialModule A ↥(leftIdeal e)

      Uniseriality of the principal right ideal generated by op e over the opposite algebra transports to uniseriality of the literal left ideal Ae. The scalar conversion is the canonical double-opposite identification.

      source
      theorem MagnitudeConjecture.RightModule.leftIdealFGObj_isBiserialObject_iff_oppositeRightIdeal {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing A] [IsNoetherianRing Aᵐᵒᵖᵐᵒᵖ] (e : A) :
      IsBiserialObject (leftIdealFGObj e) ↔ IsBiserialObject (rightIdealFGObj (MulOpposite.op e))