Module

FiniteSplitIdempotentSurjectivity.lean

Nyll.SchemeTheory.FiniteEtale.Algebra.FiniteSplitIdempotentSurjectivity

1 declaration indexed from sourceView source ↗

Module documentation

Surjectivity onto a split algebra from lifts of idempotents

The coordinate idempotents of a finite split algebra form a basis. If their preimages and the scalar coefficient preimages exist, every element has an explicitly constructed preimage. For proper H⁰, the idempotents are lifted by the actual proper-section lifting theorem.

Imports2

Mathlib.RingTheory.TotallySplit
Mathlib.LinearAlgebra.Pi

Imported by2

theorem

surjective_of_isFiniteSplit_of_idempotents_mem_range

L27 ↗

Algebra.surjective_of_isFiniteSplit_of_idempotents_mem_range

Documentation

Surjectivity onto a finite split algebra follows from lifting each idempotent and lifting scalar coefficients.

Source context 3 commands

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

noncomputable section
namespace Algebra
universe u v w z

Lean source · statement

theorem surjective_of_isFiniteSplit_of_idempotents_mem_range
    {R : Type u} {K : Type v} {A : Type w} {B : Type z}
    [CommRing R] [CommRing K] [CommRing A] [CommRing B]
    [Algebra R K] [Algebra R A] [Algebra R B] [Algebra K B]
    [IsScalarTower R K B] [IsFiniteSplit K B]
    (f : A →ₐ[R] B) (hK : Function.Surjective (algebraMap R K))
    (hIdempotents : ∀ e : B, IsIdempotentElem e → e ∈ f.range) :
    Function.Surjective f

Module documentation

Surjectivity onto a split algebra from lifts of idempotents

Declarations

surjective_of_isFiniteSplit_of_idempotents_mem_range