The residue scalar of a finite-dimensional local algebra

Let E be a finite-dimensional local algebra over an algebraically closed field k. Every element of E has a scalar in its spectrum. Locality makes that scalar unique, and the resulting function E → k is linear, surjective, and has precisely the nonunits as its kernel.

This formulation applies to noncommutative endomorphism algebras; commutativity of E is not assumed.

def MagnitudeConjecture.LocalAlgebraResidue.IsResidueScalar (k : Type u_3) {E : Type u_4} [Field k] [Ring E] [Algebra k E] (a : E) (c : k) : Prop

A scalar whose subtraction from an algebra element is a nonunit.

theorem MagnitudeConjecture.LocalAlgebraResidue.exists_isResidueScalar (k : Type u_3) {E : Type u_4} [Field k] [Ring E] [Algebra k E] [IsAlgClosed k] [FiniteDimensional k E] [IsLocalRing E] (a : E) : ∃ (c : k), IsResidueScalar k a c

Every element has a residue scalar, by nonemptiness of its spectrum.

theorem MagnitudeConjecture.LocalAlgebraResidue.isResidueScalar_unique {k : Type u_1} {E : Type u_2} [Field k] [Ring E] [Algebra k E] [IsLocalRing E] {a : E} {c d : k} (hc : IsResidueScalar k a c) (hd : IsResidueScalar k a d) : c = d

Locality makes the residue scalar unique.

noncomputable def MagnitudeConjecture.LocalAlgebraResidue.residueScalar (k : Type u_3) {E : Type u_4} [Field k] [Ring E] [Algebra k E] [IsAlgClosed k] [FiniteDimensional k E] [IsLocalRing E] (a : E) : k

The unique residue scalar of an element of a finite-dimensional local algebra over an algebraically closed field.

theorem MagnitudeConjecture.LocalAlgebraResidue.residueScalar_spec {k : Type u_1} {E : Type u_2} [Field k] [Ring E] [Algebra k E] [IsAlgClosed k] [FiniteDimensional k E] [IsLocalRing E] (a : E) : IsResidueScalar k a (residueScalar k a)

theorem MagnitudeConjecture.LocalAlgebraResidue.residueScalar_eq_of_isResidueScalar {k : Type u_1} {E : Type u_2} [Field k] [Ring E] [Algebra k E] [IsAlgClosed k] [FiniteDimensional k E] [IsLocalRing E] {a : E} {c : k} (hc : IsResidueScalar k a c) : residueScalar k a = c

@[simp]

theorem MagnitudeConjecture.LocalAlgebraResidue.residueScalar_zero {k : Type u_1} {E : Type u_2} [Field k] [Ring E] [Algebra k E] [IsAlgClosed k] [FiniteDimensional k E] [IsLocalRing E] : residueScalar k 0 = 0

theorem MagnitudeConjecture.LocalAlgebraResidue.residueScalar_add {k : Type u_1} {E : Type u_2} [Field k] [Ring E] [Algebra k E] [IsAlgClosed k] [FiniteDimensional k E] [IsLocalRing E] (a b : E) : residueScalar k (a + b) = residueScalar k a + residueScalar k b

theorem MagnitudeConjecture.LocalAlgebraResidue.residueScalar_smul {k : Type u_1} {E : Type u_2} [Field k] [Ring E] [Algebra k E] [IsAlgClosed k] [FiniteDimensional k E] [IsLocalRing E] (c : k) (a : E) : residueScalar k (c • a) = c * residueScalar k a

noncomputable def MagnitudeConjecture.LocalAlgebraResidue.residueLinearMap (k : Type u_3) (E : Type u_4) [Field k] [Ring E] [Algebra k E] [IsAlgClosed k] [FiniteDimensional k E] [IsLocalRing E] : E →ₗ[k] k

The residue scalar as a linear map.

@[simp]

theorem MagnitudeConjecture.LocalAlgebraResidue.residueLinearMap_apply {k : Type u_1} {E : Type u_2} [Field k] [Ring E] [Algebra k E] [IsAlgClosed k] [FiniteDimensional k E] [IsLocalRing E] (a : E) : (residueLinearMap k E) a = residueScalar k a

@[simp]

theorem MagnitudeConjecture.LocalAlgebraResidue.residueScalar_algebraMap {k : Type u_1} {E : Type u_2} [Field k] [Ring E] [Algebra k E] [IsAlgClosed k] [FiniteDimensional k E] [IsLocalRing E] (c : k) : residueScalar k ((algebraMap k E) c) = c

theorem MagnitudeConjecture.LocalAlgebraResidue.residueScalar_mul {k : Type u_1} {E : Type u_2} [Field k] [Ring E] [Algebra k E] [IsAlgClosed k] [FiniteDimensional k E] [IsLocalRing E] (a b : E) : residueScalar k (a * b) = residueScalar k a * residueScalar k b

The residue scalar is multiplicative. Finite-dimensionality is used here to make the possibly noncommutative algebra Dedekind-finite, so a product can be a unit only when both its factors are units.

noncomputable def MagnitudeConjecture.LocalAlgebraResidue.residueAlgHom (k : Type u_3) (E : Type u_4) [Field k] [Ring E] [Algebra k E] [IsAlgClosed k] [FiniteDimensional k E] [IsLocalRing E] : E →ₐ[k] k

The residue scalar as a homomorphism of k-algebras.

@[simp]

theorem MagnitudeConjecture.LocalAlgebraResidue.residueAlgHom_apply {k : Type u_1} {E : Type u_2} [Field k] [Ring E] [Algebra k E] [IsAlgClosed k] [FiniteDimensional k E] [IsLocalRing E] (a : E) : (residueAlgHom k E) a = residueScalar k a

theorem MagnitudeConjecture.LocalAlgebraResidue.algHom_eq_residueAlgHom {k : Type u_1} {E : Type u_2} [Field k] [Ring E] [Algebra k E] [IsAlgClosed k] [FiniteDimensional k E] [IsLocalRing E] (φ : E →ₐ[k] k) : φ = residueAlgHom k E

The residue map is the unique k-algebra homomorphism from the local algebra to its algebraically closed coefficient field.

theorem MagnitudeConjecture.LocalAlgebraResidue.residueLinearMap_surjective {k : Type u_1} {E : Type u_2} [Field k] [Ring E] [Algebra k E] [IsAlgClosed k] [FiniteDimensional k E] [IsLocalRing E] : Function.Surjective ⇑(residueLinearMap k E)

The residue map is onto the ground field.

theorem MagnitudeConjecture.LocalAlgebraResidue.mem_ker_residueLinearMap_iff {k : Type u_1} {E : Type u_2} [Field k] [Ring E] [Algebra k E] [IsAlgClosed k] [FiniteDimensional k E] [IsLocalRing E] (a : E) : a ∈ (residueLinearMap k E).ker ↔ ¬IsUnit a

Its kernel is exactly the set of nonunits of the local algebra.