Restricting a conic structure to a subalgebra

A unital subalgebra B of a conic algebra (A, n) is again a conic algebra, with the restricted norm n|_B. Nothing has to be checked beyond the two axioms of GPR 16.1, both of which are inherited: n(1) = 1 because B contains the ambient unit, and the degree-two identity because it is an identity in A between elements of B.

Trace, conjugation and multiplicativity are likewise the ambient ones restricted, which is what makes the subalgebra usable as an input to the Cayley–Dickson construction.

Main definitions

• ConicAlgebra.restrict : the conic algebra B carved out of C : ConicAlgebra k A.

Main results

• ConicAlgebra.restrict_norm_apply, ConicAlgebra.restrict_trace_apply, ConicAlgebra.coe_restrict_conj : norm, trace and conjugation restrict.
• ConicAlgebra.IsMultiplicative.restrict : so does multiplicativity of the norm.

References

• [GPR] Garibaldi, Petersson, Racine, Albert Algebras over Commutative Rings, 16.1.

def ConicAlgebra.normRestrict {k : Type u} {A : Type v} [CommRing k] [NonAssocRing A] [Module k A] (C : ConicAlgebra k A) (B : NonAssocSubalgebra k A) : QuadraticForm k ↥B

The norm of C restricted to a unital subalgebra.

Equations

• C.normRestrict B = QuadraticMap.comp C.norm B.toSubmodule.subtype

@[simp]

theorem ConicAlgebra.normRestrict_apply {k : Type u} {A : Type v} [CommRing k] [NonAssocRing A] [Module k A] {C : ConicAlgebra k A} {B : NonAssocSubalgebra k A} (b : ↥B) : (C.normRestrict B) b = C.norm ↑b

def ConicAlgebra.restrict {k : Type u} {A : Type v} [CommRing k] [NonAssocRing A] [Module k A] (C : ConicAlgebra k A) (B : NonAssocSubalgebra k A) : ConicAlgebra k ↥B

A unital subalgebra of a conic algebra is a conic algebra, with the restricted norm.

Both axioms are inherited verbatim; in particular no regularity, projectivity or rank hypothesis is involved, and the subalgebra need not be associative.

Equations

• C.restrict B = { norm := C.normRestrict B, norm_one := ⋯, mul_self := ⋯ }

@[simp]

theorem ConicAlgebra.restrict_norm_apply {k : Type u} {A : Type v} [CommRing k] [NonAssocRing A] [Module k A] {C : ConicAlgebra k A} {B : NonAssocSubalgebra k A} (b : ↥B) : (C.restrict B).norm b = C.norm ↑b

@[simp]

theorem ConicAlgebra.restrict_trace_apply {k : Type u} {A : Type v} [CommRing k] [NonAssocRing A] [Module k A] {C : ConicAlgebra k A} {B : NonAssocSubalgebra k A} (b : ↥B) : (C.restrict B).trace b = C.trace ↑b

@[simp]

theorem ConicAlgebra.coe_restrict_conj {k : Type u} {A : Type v} [CommRing k] [NonAssocRing A] [Module k A] {C : ConicAlgebra k A} {B : NonAssocSubalgebra k A} (b : ↥B) : ↑((C.restrict B).conj b) = C.conj ↑b

theorem ConicAlgebra.IsMultiplicative.restrict {k : Type u} {A : Type v} [CommRing k] [NonAssocRing A] [Module k A] {C : ConicAlgebra k A} {B : NonAssocSubalgebra k A} (h : C.IsMultiplicative) : (C.restrict B).IsMultiplicative

Multiplicativity of the norm is inherited by every unital subalgebra.