Documentation

LeanPool.CompositionAlgebrasOverRings.Composition.Reduced.Reducedness

Reduced composition algebras (GPR 22.6–22.7) #

GPR 22.6 defines a composition algebra to be reduced when it contains an absolutely primitive idempotent. GPR 22.7 supplies the characterization used throughout the structure theory: in rank greater than one, reducedness is equivalent to the existence of an elementary idempotent, while every rank-one composition algebra is reduced.

This file uses that equivalent characterization together with the rank decomposition of GPR Exc. 9.31. Thus a composition algebra is reduced when its rank 2, 4, and 8 components have elementary idempotents; the rank-one component needs no condition.

Main definitions #

Main results #

Implementation notes #

⚠ Equivalent characterization rather than absolute primitivity. Absolute primitivity in GPR 22.1 quantifies over all field extensions and decompositions into orthogonal idempotents. Nothing downstream uses that data: every application passes immediately through GPR 22.7 to elementary idempotents. Accordingly IsReduced records the rankwise elementary-idempotent condition equivalent to GPR 22.6, rather than introducing an unused absolute-primitivity API. The distinction at rank one is preserved explicitly: rank one is reduced but generally has no elementary idempotent.

Zero rank factors cause no exception. Their base rings are zero rings, where 0 is elementary because 0 = 1; retaining all three factors therefore matches the convention in GPR 21.19.

References #

source
def ConicAlgebra.IsReduced {k : Type u} {A : Type v} [CommRing k] [NonAssocRing A] [Module k A] [SMulCommClass k A A] [IsScalarTower k A A] [Module.Finite k A] [Module.Projective k A] (C : ConicAlgebra k A) :
Prop

Reducedness (GPR 22.6–22.7) through the rank decomposition. A conic algebra is reduced when it is a composition algebra and each of its rank 2, 4, and 8 components has an elementary idempotent. The rank-one component is automatically reduced and deliberately carries no elementary-idempotent condition.

Equations
Instances For
    source
    theorem ConicAlgebra.IsReduced.isComposition {k : Type u} {A : Type v} [CommRing k] [NonAssocRing A] [Module k A] [SMulCommClass k A A] [IsScalarTower k A A] [Module.Finite k A] [Module.Projective k A] {C : ConicAlgebra k A} (h : C.IsReduced) :
    C.IsComposition

    A reduced conic algebra is a composition algebra, by definition.

    source
    theorem ConicAlgebra.IsReduced.hasElementaryIdempotent_splitRankComponent_two {k : Type u} {A : Type v} [CommRing k] [NonAssocRing A] [Module k A] [SMulCommClass k A A] [IsScalarTower k A A] [Module.Finite k A] [Module.Projective k A] {C : ConicAlgebra k A} (h : C.IsReduced) :
    (C.splitRankComponent 2).HasElementaryIdempotent

    The rank-two component of a reduced composition algebra has an elementary idempotent.

    source
    theorem ConicAlgebra.IsReduced.hasElementaryIdempotent_splitRankComponent_four {k : Type u} {A : Type v} [CommRing k] [NonAssocRing A] [Module k A] [SMulCommClass k A A] [IsScalarTower k A A] [Module.Finite k A] [Module.Projective k A] {C : ConicAlgebra k A} (h : C.IsReduced) :
    (C.splitRankComponent 4).HasElementaryIdempotent

    The rank-four component of a reduced composition algebra has an elementary idempotent.

    source
    theorem ConicAlgebra.IsReduced.hasElementaryIdempotent_splitRankComponent_eight {k : Type u} {A : Type v} [CommRing k] [NonAssocRing A] [Module k A] [SMulCommClass k A A] [IsScalarTower k A A] [Module.Finite k A] [Module.Projective k A] {C : ConicAlgebra k A} (h : C.IsReduced) :
    (C.splitRankComponent 8).HasElementaryIdempotent

    The rank-eight component of a reduced composition algebra has an elementary idempotent.

    source
    theorem ConicAlgebra.IsSplit.isReduced {k : Type u} {A : Type v} [CommRing k] [NonAssocRing A] [Module k A] [SMulCommClass k A A] [IsScalarTower k A A] [Module.Finite k A] [Module.Projective k A] {C : ConicAlgebra k A} (h : C.IsSplit) :
    C.IsReduced

    GPR 22.16, split ⇒ reduced. Every split composition algebra over an arbitrary commutative ring is reduced.

    On each rank greater than one, the defining isomorphism with the standard split model transports its visible elementary idempotent back to the corresponding rank component. Rank one is reduced without an elementary-idempotent condition.