Magnitude conjecture

MagnitudeConjecture.Algebra.CornerQuotient

Primitive idempotents under surjective ring maps #

This file isolates the small ring-theoretic fact needed for literal support quotients. The corner of a primitive idempotent is identified with the endomorphism ring of its indecomposable principal right ideal, hence is local. A surjective ring map is surjective on the corresponding corners, and a nonzero image of a primitive idempotent is therefore primitive.

source
def MagnitudeConjecture.idempotentCornerMap {R : Type u} {T : Type v} [Ring R] [Ring T] (f : R →+* T) {e : R} (he : IsIdempotentElem e) :
he.Corner →+* ⋯.Corner

A ring homomorphism restricts to the corresponding idempotent corners.

Instances For
    source
    theorem MagnitudeConjecture.idempotentCornerMap_surjective {R : Type u} {T : Type v} [Ring R] [Ring T] (f : R →+* T) (hf : Function.Surjective ⇑f) {e : R} (he : IsIdempotentElem e) :
    Function.Surjective ⇑(idempotentCornerMap f he)

    A surjective ring map is surjective on every corresponding corner.

    source
    def MagnitudeConjecture.RightModule.cornerEndRingEquiv {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {e : A} (he : IsIdempotentElem e) :
    he.Corner ≃+* Module.End Aᵐᵒᵖ ↥(rightIdeal e)

    Left multiplication identifies an idempotent corner with the endomorphism ring of its principal right ideal.

    Instances For
      source
      theorem MagnitudeConjecture.isLocalRing_of_surjective {R : Type u} {T : Type v} [Ring R] [Ring T] [IsLocalRing R] [Nontrivial T] (f : R →+* T) (hf : Function.Surjective ⇑f) :
      IsLocalRing T

      The noncommutative quotient of a local ring by a surjective ring map is local, provided the target is nontrivial.

      source
      theorem MagnitudeConjecture.RightModule.PrimitiveIdempotentData.corner_isLocalRing {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {e : A} (D : PrimitiveIdempotentData e) :
      IsLocalRing ⋯.Corner

      The corner of a primitive idempotent in a finite-dimensional algebra is local.

      source
      theorem MagnitudeConjecture.RightModule.PrimitiveIdempotentData.map_of_surjective {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {T : Type v} [Ring T] {e : A} (D : PrimitiveIdempotentData e) (f : A →+* T) (hf : Function.Surjective ⇑f) (hne : f e ≠ 0) :
      PrimitiveIdempotentData (f e)

      A nonzero image of a primitive idempotent under a surjective ring map is again primitive.