The norm of a reduced composition algebra is hyperbolic (GPR 22.9(iv))

At an elementary idempotent c, the Peirce decomposition writes an element as

a₁ c + x₁₂ + x₂₁ + a₂ (conj c)

and GPR Exc. 19.35(3) gives its norm as a₁a₂ + n(x₁₂, x₂₁). When the norm is regular, the polar pairing identifies C₁₂ with C₂₁*. Consequently the whole norm is the hyperbolic form QuadraticForm.dualProd k (k × C₂₁) of k ⊕ C₂₁. This file packages that coordinate calculation as an isometry equivalence and completes clause (iv) of GPR 22.9.

Main definitions

• ConicAlgebra.IsElementaryIdempotent.peirceHyperbolicEquiv : the Peirce-coordinate linear equivalence from the hyperbolic module on k ⊕ C₂₁ to the algebra.
• ConicAlgebra.IsElementaryIdempotent.peirceHyperbolicIsometryEquiv : the same map as an isometry of quadratic forms.

Main results

• ConicAlgebra.IsElementaryIdempotent.norm_peirceHyperbolicEquiv : the coordinate map carries the norm to the hyperbolic form.

References

• [GPR] Garibaldi, Petersson, Racine, Albert Algebras over Commutative Rings, Exc. 19.35, 22.9.

@[reducible, inline]

abbrev ConicAlgebra.IsElementaryIdempotent.HyperbolicModule {k : Type u} {A : Type v} [CommRing k] [NonAssocRing A] [Module k A] [SMulCommClass k A A] [IsScalarTower k A A] (c : A) : Submodule k A

The lower-left Peirce component used as one half of the hyperbolic presentation.

Equations

• ConicAlgebra.IsElementaryIdempotent.HyperbolicModule c = IsAlternative.peirceComponent c true false

noncomputable def ConicAlgebra.IsElementaryIdempotent.peirceHyperbolicTo {k : Type u} {A : Type v} [CommRing k] [NonAssocRing A] [Module k A] [SMulCommClass k A A] [IsScalarTower k A A] [IsAlternative A] {C : ConicAlgebra k A} {c : A} (hc : C.IsElementaryIdempotent c) (hmul : C.IsMultiplicative) (hreg : C.norm.IsGPRRegular) : Module.Dual k (k × ↥(HyperbolicModule c)) × k × ↥(HyperbolicModule c) →ₗ[k] A

The Peirce-coordinate map from the hyperbolic module on k ⊕ C₂₁ to the algebra. The first hyperbolic coordinate is a functional on k ⊕ C₂₁; dualProdEquiv separates it into its scalar and C₂₁* parts, and off-diagonal duality turns the latter into the C₁₂ coordinate.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem ConicAlgebra.IsElementaryIdempotent.peirceHyperbolicTo_apply {k : Type u} {A : Type v} [CommRing k] [NonAssocRing A] [Module k A] [SMulCommClass k A A] [IsScalarTower k A A] [IsAlternative A] {C : ConicAlgebra k A} {c : A} (hc : C.IsElementaryIdempotent c) (hmul : C.IsMultiplicative) (hreg : C.norm.IsGPRRegular) (x : Module.Dual k (k × ↥(HyperbolicModule c)) × k × ↥(HyperbolicModule c)) : (hc.peirceHyperbolicTo hmul hreg) x = peirceElement c x.2.1 ((dualProdEquiv k ↥(HyperbolicModule c)).symm x.1).1 ((hc.offDiagonalDuality hmul hreg).symm (-((dualProdEquiv k ↥(HyperbolicModule c)).symm x.1).2)) x.2.2

theorem ConicAlgebra.IsElementaryIdempotent.bijective_peirceHyperbolicTo {k : Type u} {A : Type v} [CommRing k] [NonAssocRing A] [Module k A] [SMulCommClass k A A] [IsScalarTower k A A] [IsAlternative A] {C : ConicAlgebra k A} {c : A} (hc : C.IsElementaryIdempotent c) (hmul : C.IsMultiplicative) (hreg : C.norm.IsGPRRegular) : Function.Bijective ⇑(hc.peirceHyperbolicTo hmul hreg)

The Peirce-coordinate map from the hyperbolic module is bijective.

noncomputable def ConicAlgebra.IsElementaryIdempotent.peirceHyperbolicEquiv {k : Type u} {A : Type v} [CommRing k] [NonAssocRing A] [Module k A] [SMulCommClass k A A] [IsScalarTower k A A] [IsAlternative A] {C : ConicAlgebra k A} {c : A} (hc : C.IsElementaryIdempotent c) (hmul : C.IsMultiplicative) (hreg : C.norm.IsGPRRegular) : (Module.Dual k (k × ↥(HyperbolicModule c)) × k × ↥(HyperbolicModule c)) ≃ₗ[k] A

The Peirce-coordinate linear equivalence from the hyperbolic module on k ⊕ C₂₁ to A.

Equations

• hc.peirceHyperbolicEquiv hmul hreg = LinearEquiv.ofBijective (hc.peirceHyperbolicTo hmul hreg) ⋯

@[simp]

theorem ConicAlgebra.IsElementaryIdempotent.peirceHyperbolicEquiv_apply {k : Type u} {A : Type v} [CommRing k] [NonAssocRing A] [Module k A] [SMulCommClass k A A] [IsScalarTower k A A] [IsAlternative A] {C : ConicAlgebra k A} {c : A} (hc : C.IsElementaryIdempotent c) (hmul : C.IsMultiplicative) (hreg : C.norm.IsGPRRegular) (x : Module.Dual k (k × ↥(HyperbolicModule c)) × k × ↥(HyperbolicModule c)) : (hc.peirceHyperbolicEquiv hmul hreg) x = (hc.peirceHyperbolicTo hmul hreg) x

theorem ConicAlgebra.IsElementaryIdempotent.norm_peirceHyperbolicEquiv {k : Type u} {A : Type v} [CommRing k] [NonAssocRing A] [Module k A] [SMulCommClass k A A] [IsScalarTower k A A] [IsAlternative A] {C : ConicAlgebra k A} {c : A} (hc : C.IsElementaryIdempotent c) (hmul : C.IsMultiplicative) (hreg : C.norm.IsGPRRegular) (x : Module.Dual k (k × ↥(HyperbolicModule c)) × k × ↥(HyperbolicModule c)) : C.norm ((hc.peirceHyperbolicEquiv hmul hreg) x) = (QuadraticForm.dualProd k (k × ↥(HyperbolicModule c))) x

GPR 22.9(iv): the Peirce-coordinate equivalence identifies the norm with the hyperbolic form QuadraticForm.dualProd k (k × C₂₁).

noncomputable def ConicAlgebra.IsElementaryIdempotent.peirceHyperbolicIsometryEquiv {k : Type u} {A : Type v} [CommRing k] [NonAssocRing A] [Module k A] [SMulCommClass k A A] [IsScalarTower k A A] [IsAlternative A] {C : ConicAlgebra k A} {c : A} (hc : C.IsElementaryIdempotent c) (hmul : C.IsMultiplicative) (hreg : C.norm.IsGPRRegular) : QuadraticMap.IsometryEquiv (QuadraticForm.dualProd k (k × ↥(HyperbolicModule c))) C.norm

The norm of a reduced regular multiplicative conic algebra is hyperbolic, GPR 22.9(iv). The displayed isometry uses the hyperbolic form QuadraticForm.dualProd k (k × C₂₁).

Equations

• hc.peirceHyperbolicIsometryEquiv hmul hreg = { toLinearEquiv := hc.peirceHyperbolicEquiv hmul hreg, map_app' := ⋯ }