Magnitude conjecture

MagnitudeConjecture.Algebra.IndecomposableLocalEnd

Local endomorphism rings of finite-dimensional indecomposable modules #

Fitting decomposition shows that every endomorphism of a finite-dimensional indecomposable module is either invertible or nilpotent. Consequently its endomorphism ring is local. The result is then transported through the fully faithful inclusion of finitely generated modules into all modules.

The Fitting argument and the two small transport lemmas are adapted from CartanDeterminant.RepresentationTheory.IndecomposableLocalEnd and CartanDeterminant.CategoryTheory.LinearEndTransport at homological-conjectures commit eade4e75.

The file also records a ring-level form: a finite-dimensional algebra with no nontrivial idempotents is local. This follows by applying Fitting's lemma to its right regular module.

source
noncomputable def MagnitudeConjecture.CategoryTheory.Functor.endRingEquivOfFullyFaithful {C : Type u₁} [CategoryTheory.Category.{v, u₁} C] [CategoryTheory.Preadditive C] {D : Type u₂} [CategoryTheory.Category.{v, u₂} D] [CategoryTheory.Preadditive D] (F : CategoryTheory.Functor C D) [F.Additive] [F.Full] [F.Faithful] (X : C) :
CategoryTheory.End X ≃+* CategoryTheory.End (F.obj X)

A fully faithful additive functor identifies the endomorphism rings of an object and its image.

Instances For
    source
    @[simp]
    theorem MagnitudeConjecture.CategoryTheory.Functor.endRingEquivOfFullyFaithful_apply {C : Type u₁} [CategoryTheory.Category.{v, u₁} C] [CategoryTheory.Preadditive C] {D : Type u₂} [CategoryTheory.Category.{v, u₂} D] [CategoryTheory.Preadditive D] (F : CategoryTheory.Functor C D) [F.Additive] [F.Full] [F.Faithful] (X : C) (f : CategoryTheory.End X) :
    (endRingEquivOfFullyFaithful F X) f = F.map f
    source
    noncomputable def MagnitudeConjecture.rightRegularEndEquiv (R : Type v) [Ring R] :
    R ≃+* Module.End Rᵐᵒᵖ R

    Left multiplication identifies a ring with the endomorphism ring of its right regular module.

    Instances For
      source
      theorem MagnitudeConjecture.finiteDimensional_isLocalRing_of_idempotents {k : Type u} [Field k] (R : Type v) [Ring R] [Algebra k R] [Nontrivial R] [FiniteDimensional k R] (hidem : ∀ (e : R), IsIdempotentElem e → e = 0 ∨ e = 1) :
      IsLocalRing R

      A finite-dimensional algebra whose only idempotents are zero and one is local. Fitting is applied to the right regular module, whose endomorphism ring is the original ring through left multiplication.

      source
      theorem MagnitudeConjecture.isUnit_or_isNilpotent_of_finite_indecomposable {k : Type u} [Field k] {A : Type v} [Ring A] [Algebra k A] [Module.Finite k A] (M : ModuleCat A) [Module.Finite k ↑M] (hM : CategoryTheory.Indecomposable M) (f : CategoryTheory.End M) :
      IsUnit f ∨ IsNilpotent f

      A finite-dimensional indecomposable module has the Fitting alternative: each endomorphism is invertible or nilpotent.

      source
      theorem MagnitudeConjecture.moduleCat_end_isLocalRing {k : Type u} [Field k] {A : Type v} [Ring A] [Algebra k A] [Module.Finite k A] (M : ModuleCat A) [Module.Finite k ↑M] (hM : CategoryTheory.Indecomposable M) :
      IsLocalRing (CategoryTheory.End M)

      The categorical endomorphism ring of a finite-dimensional indecomposable module is local.

      source
      theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.fgObj_end_isLocalRing {k : Type u} [Field k] {A : Type v} [Ring A] [Algebra k A] [FiniteDimensional k A] (S : FiniteIndecomposableSkeleton k A) (i : Fin S.n) :
      IsLocalRing (CategoryTheory.End (S.fgObj i))

      The chosen skeleton object's endomorphism ring remains local after it is bundled in the literal category of finitely generated right modules.