Module

OrthogonalIdempotentsDegree.lean

Nyll.SchemeTheory.RingTheory.OrthogonalIdempotentsDegree

1 declaration indexed from sourceView source ↗

Module documentation

A full-degree orthogonal family splits a finite algebra

Nonzero orthogonal idempotents are linearly independent. If their number is at least the dimension of the algebra, the explicit sum of scalar multiples is a bijective algebra map from a product of copies of the base field. No separability or reducedness hypothesis is required.

Imports4

Mathlib.Algebra.Algebra.Pi
Mathlib.LinearAlgebra.Dimension.Constructions
Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
Mathlib.RingTheory.Idempotents

Imported by2

def

splitAlgEquivOfCompleteOrthogonalIdempotents

L29 ↗

SchemeTheory.splitAlgEquivOfCompleteOrthogonalIdempotents

Documentation

A complete orthogonal family of nonzero idempotents whose cardinality is at least the algebra's degree gives an actual split algebra isomorphism.

Source context 3 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace SchemeTheory
universe u v w

Lean source · statement

def splitAlgEquivOfCompleteOrthogonalIdempotents
    {K : Type u} {A : Type v} {ι : Type w}
    [Field K] [CommRing A] [Algebra K A] [FiniteDimensional K A] [Fintype ι]
    (e : ι → A) (he : CompleteOrthogonalIdempotents e)
    (hne : ∀ i, e i ≠ 0) (hdegree : Module.finrank K A ≤ Fintype.card ι) :
    A ≃ₐ[K] (ι → K)

Module documentation

A full-degree orthogonal family splits a finite algebra

Declarations

splitAlgEquivOfCompleteOrthogonalIdempotents