Algebra isomorphisms and norm isometries

The first direction of the classification of composition algebras by their norm forms says that an algebra isomorphism is an isometry. The key input is that a conic norm on a finitely generated projective algebra is intrinsic: two conic structures on the same algebra have the same norm. This is the easy half of GPR 23.4(a).

For the converse direction, the first step normalizes an arbitrary norm similarity to a unital norm isometry (GPR 23.3). If its multiplier is μ and the image of 1 is x, left multiplication by conj x / μ has the inverse multiplier and sends x to 1. Such a normalized map preserves the whole conic calculus — trace, conjugation and squares — which is GPR 23.2.

Over a nontrivial LG ring, the converse is completed without a constant-rank hypothesis; that completion is the norm equivalence theorem GPR 23.5. The rank idempotents reduce it to the constant-rank cases. In rank one, unitForm canonically identifies the algebra with the base ring, even when its polar form is nonregular in characteristic two. In ranks two, four, and eight, the proof starts from the corresponding regular quadratic subalgebras of GPR 19.16(b), uses Witt cancellation (GN 6.5) to match successive doubling vectors, and iterates to regular full-rank subalgebras, which are the ambient algebras.

Main results

• ConicAlgebra.norm_eq_of_projective : two conic norms on the same finite projective algebra coincide.
• ConicAlgebra.isometryEquivOfLinearEquiv : GPR 23.4(a), a unital multiplicative linear equivalence of conic algebras is an isometry of their norms.
• ConicAlgebra.trace_map_of_linearEquiv, ConicAlgebra.conj_map_of_linearEquiv : such an equivalence also preserves trace and conjugation.
• ConicAlgebra.IsMultiplicative.exists_isometryEquiv_map_one_of_similarity : full GPR 23.3, normalizing a norm similarity to a unital norm isometry.
• ConicAlgebra.IsMultiplicative.exists_isometryEquiv_map_one : its isometry special case.
• ConicAlgebra.trace_map_of_isometryEquiv_map_one, .conj_map_of_isometryEquiv_map_one, .map_mul_self_of_isometryEquiv_map_one : GPR 23.2, a unital norm isometry preserves the conic calculus and squaring.
• ConicAlgebra.adjoinElementLinearEquivOfMapOne : a unital norm isometry restricts to an algebra isomorphism k[u] ≅ k[e u] (expressed as a multiplicative unital linear equivalence).
• ConicAlgebra.isRegularRankTwoComposition_map_of_isometryEquiv_map_one : the regular quadratic starting subalgebra transfers across a unital norm isometry.
• ConicAlgebra.cayAdjoinElementIsometryEquivOfMapOne : the matched quadratic subalgebras can be doubled with a common Cayley–Dickson scalar, preserving the norm and multiplication.
• ConicAlgebra.exists_doubledSubalgebras_isometryEquiv_of_isGPRRegular : one internal matched doubling step carries equivalent regular subalgebras to equivalent doubled image subalgebras.
• ConicAlgebra.IsComposition.exists_next_doubledSubalgebras_isometryEquiv : unit representation, complement cancellation and internal doubling combined into one complete induction step.
• ConicAlgebra.IsComposition.exists_next_isGPRRegular_rankAtStalk_two_mul : the self-feeding version of that step, recording regularity and doubled rank for both new image subalgebras.
• ConicAlgebra.exists_isometryEquiv_polarOrthogonal : cancellation for arbitrary corresponding regular subalgebras.
• ConicAlgebra.IsComposition.exists_isometryEquiv_map_one_map_mul : GPR 23.5, the norm equivalence theorem over a nontrivial LG ring, with no constant-rank hypothesis.
• ConicAlgebra.exists_isometryEquiv_polarOrthogonal_adjoinElement : Witt cancellation identifies the orthogonal complements of the corresponding quadratic subalgebras.
• ConicAlgebra.exists_polarOrthogonal_adjoinElement_eq_norm : corresponding complement vectors give the same Cayley–Dickson parameter.
• ConicAlgebra.isometryEquivOf_fullRank_subalgebras : a matched equivalence of regular full-rank subalgebras assembles to an ambient equivalence.
• ConicAlgebra.exists_isometryEquiv_map_one_map_mul_of_rankAtStalk_eq_one : the exceptional rank-one converse, proved directly through unitForm.
• ConicAlgebra.IsComposition.exists_isometryEquiv_map_one_map_mul_of_rankAtStalk : the constant-rank-at-least-two step.
• ConicAlgebra.IsComposition.exists_isometryEquiv_map_one_map_mul_of_rankAtStalk_eq : the constant-rank theorem used on each idempotent factor.

Implementation notes

Mathlib's AlgEquiv applies only to associative semirings, while composition algebras need not be associative. Accordingly the second theorem accepts a LinearEquiv together with the two laws that make it an isomorphism of unital non-associative algebras. This avoids introducing a local competitor to the NonUnitalAlgEquiv that mathlib itself records as a future TODO.

The uniqueness argument is elementary. Subtracting the two degree-two identities gives

(t_C(x) - t_D(x)) x = (n_C(x) - n_D(x)) 1.

Applying a functional taking 1 to 1 shows that the trace difference annihilates its own traceless argument. The projective self-annihilation lemma then makes the traces equal, and the same displayed identity makes the norms equal.

References

• [GPR] Garibaldi, Petersson, Racine, Albert Algebras over Commutative Rings, 16.7, 19.3, 19.16(b), 19.18, 23.2, 23.3, 23.4(a), 23.5.
• [GN] Gille, Neher, Group schemes over LG-rings and applications to cancellation theorems and Azumaya algebras, European Journal of Mathematics 11 (2025), article 42, 6.5.

noncomputable def ConicAlgebra.isometryEquivOfLinearEquivOfMapMulSelf {k : Type u} {A : Type v} [CommRing k] [NonAssocRing A] [Module k A] [Module.Finite k A] [Module.Projective k A] {B : Type w} [NonAssocRing B] [Module k B] (C : ConicAlgebra k A) (D : ConicAlgebra k B) (e : A ≃ₗ[k] B) (map_one : e 1 = 1) (map_mul_self : ∀ (x : A), e (x * x) = e x * e x) : QuadraticMap.IsometryEquiv C.norm D.norm

The engine of GPR 23.4(a). A unital linear equivalence between finitely generated projective conic algebras that preserves squares, e (x * x) = e x * e x, is an isometry of their norm forms: pulling the norm of B back along e gives a second conic norm on A, and the conic norm of a finitely generated projective algebra is unique (ConicAlgebra.norm_eq_of_projective, GPR 16.16). Isomorphisms (isometryEquivOfLinearEquiv) and anti-isomorphisms (isometryEquivOfLinearEquivOfMapMulRev) both preserve squares.

Equations

• C.isometryEquivOfLinearEquivOfMapMulSelf D e map_one map_mul_self = { toLinearEquiv := e, map_app' := ⋯ }

noncomputable def ConicAlgebra.isometryEquivOfLinearEquiv {k : Type u} {A : Type v} [CommRing k] [NonAssocRing A] [Module k A] [Module.Finite k A] [Module.Projective k A] {B : Type w} [NonAssocRing B] [Module k B] (C : ConicAlgebra k A) (D : ConicAlgebra k B) (e : A ≃ₗ[k] B) (map_one : e 1 = 1) (map_mul : ∀ (x y : A), e (x * y) = e x * e y) : QuadraticMap.IsometryEquiv C.norm D.norm

GPR 23.4(a), isomorphisms. A unital multiplicative linear equivalence between conic algebras is an isometry of their norm forms. In particular, every isomorphism of composition algebras preserves the norm; the converse, in rank two, is Composition/NormEquivalence.lean.

⚠ Mathlib's AlgEquiv requires associative multiplication, so the non-associative algebra isomorphism is deliberately expressed as a LinearEquiv plus map_one and map_mul.

Equations

• C.isometryEquivOfLinearEquiv D e map_one map_mul = C.isometryEquivOfLinearEquivOfMapMulSelf D e map_one ⋯

noncomputable def ConicAlgebra.isometryEquivOfLinearEquivOfMapMulRev {k : Type u} {A : Type v} [CommRing k] [NonAssocRing A] [Module k A] [Module.Finite k A] [Module.Projective k A] {B : Type w} [NonAssocRing B] [Module k B] (C : ConicAlgebra k A) (D : ConicAlgebra k B) (e : A ≃ₗ[k] B) (map_one : e 1 = 1) (map_mul_rev : ∀ (x y : A), e (x * y) = e y * e x) : QuadraticMap.IsometryEquiv C.norm D.norm

GPR 23.4(a), anti-isomorphisms. A unital linear equivalence reversing multiplication, e (x * y) = e y * e x, between conic algebras is an isometry of their norm forms. For example the conjugation of a quaternion algebra is one.

Equations

• C.isometryEquivOfLinearEquivOfMapMulRev D e map_one map_mul_rev = C.isometryEquivOfLinearEquivOfMapMulSelf D e map_one ⋯

theorem ConicAlgebra.norm_map_of_linearEquiv {k : Type u} {A : Type v} [CommRing k] [NonAssocRing A] [Module k A] [Module.Finite k A] [Module.Projective k A] {B : Type w} [NonAssocRing B] [Module k B] (C : ConicAlgebra k A) (D : ConicAlgebra k B) (e : A ≃ₗ[k] B) (map_one : e 1 = 1) (map_mul : ∀ (x y : A), e (x * y) = e x * e y) (x : A) : D.norm (e x) = C.norm x

A unital multiplicative linear equivalence preserves the conic norm.

theorem ConicAlgebra.norm_map_of_linearEquiv_of_map_mul_rev {k : Type u} {A : Type v} [CommRing k] [NonAssocRing A] [Module k A] [Module.Finite k A] [Module.Projective k A] {B : Type w} [NonAssocRing B] [Module k B] (C : ConicAlgebra k A) (D : ConicAlgebra k B) (e : A ≃ₗ[k] B) (map_one : e 1 = 1) (map_mul_rev : ∀ (x y : A), e (x * y) = e y * e x) (x : A) : D.norm (e x) = C.norm x

A unital linear equivalence reversing multiplication preserves the conic norm (GPR 23.4(a) for anti-isomorphisms).

theorem ConicAlgebra.trace_map_of_linearEquiv {k : Type u} {A : Type v} [CommRing k] [NonAssocRing A] [Module k A] [Module.Finite k A] [Module.Projective k A] {B : Type w} [NonAssocRing B] [Module k B] (C : ConicAlgebra k A) (D : ConicAlgebra k B) (e : A ≃ₗ[k] B) (map_one : e 1 = 1) (map_mul : ∀ (x y : A), e (x * y) = e x * e y) (x : A) : D.trace (e x) = C.trace x

A unital multiplicative linear equivalence preserves the trace derived from the conic norm.

theorem ConicAlgebra.conj_map_of_linearEquiv {k : Type u} {A : Type v} [CommRing k] [NonAssocRing A] [Module k A] [Module.Finite k A] [Module.Projective k A] {B : Type w} [NonAssocRing B] [Module k B] (C : ConicAlgebra k A) (D : ConicAlgebra k B) (e : A ≃ₗ[k] B) (map_one : e 1 = 1) (map_mul : ∀ (x y : A), e (x * y) = e x * e y) (x : A) : D.conj (e x) = e (C.conj x)

A unital multiplicative linear equivalence preserves the standard conjugation.

noncomputable def ConicAlgebra.isometryEquivOfAlgEquiv {k : Type u} [CommRing k] {A' : Type v} {B' : Type w} [Ring A'] [Ring B'] [Algebra k A'] [Algebra k B'] [Module.Finite k A'] [Module.Projective k A'] (C : ConicAlgebra k A') (D : ConicAlgebra k B') (e : A' ≃ₐ[k] B') : QuadraticMap.IsometryEquiv C.norm D.norm

For associative conic algebras, the easy direction is available through mathlib's standard AlgEquiv API.

Equations

• C.isometryEquivOfAlgEquiv D e = C.isometryEquivOfLinearEquiv D ↑e ⋯ ⋯

def ConicAlgebra.leftMulConjLinearEquiv {k : Type u} [CommRing k] {B : Type w} [NonAssocRing B] [Module k B] [SMulCommClass k B B] [IsScalarTower k B B] {D : ConicAlgebra k B} [IsAlternative B] (x : B) (hx : D.norm x = 1) : B ≃ₗ[k] B

Left multiplication by conj x is a linear equivalence when n(x) = 1; its inverse is left multiplication by x.

Equations

• ConicAlgebra.leftMulConjLinearEquiv x hx = { toFun := fun (z : B) => D.conj x * z, map_add' := ⋯, map_smul' := ⋯, invFun := fun (z : B) => x * z, left_inv := ⋯, right_inv := ⋯ }

def ConicAlgebra.leftMulConjUnitLinearEquiv {k : Type u} [CommRing k] {B : Type w} [NonAssocRing B] [Module k B] [SMulCommClass k B B] [IsScalarTower k B B] {D : ConicAlgebra k B} [IsAlternative B] (x : B) (μ : kˣ) (hx : D.norm x = ↑μ) : B ≃ₗ[k] B

Left multiplication by conj x, followed by division by n(x), is a linear equivalence when n(x) is a unit. Its inverse is left multiplication by x.

Equations

• ConicAlgebra.leftMulConjUnitLinearEquiv x μ hx = { toFun := fun (z : B) => ↑μ⁻¹ • (D.conj x * z), map_add' := ⋯, map_smul' := ⋯, invFun := fun (z : B) => x * z, left_inv := ⋯, right_inv := ⋯ }

noncomputable def ConicAlgebra.IsMultiplicative.leftMulConjIsometryEquiv {k : Type u} [CommRing k] {B : Type w} [NonAssocRing B] [Module k B] [SMulCommClass k B B] [IsScalarTower k B B] {D : ConicAlgebra k B} [IsAlternative B] (h : D.IsMultiplicative) (x : B) (hx : D.norm x = 1) : QuadraticMap.IsometryEquiv D.norm D.norm

For a norm-one element x in an alternative multiplicative conic algebra, left multiplication by conj x is a self-isometry of the norm and carries x to 1.

Equations

• h.leftMulConjIsometryEquiv x hx = { toLinearEquiv := ConicAlgebra.leftMulConjLinearEquiv x hx, map_app' := ⋯ }

@[simp]

theorem ConicAlgebra.IsMultiplicative.leftMulConjIsometryEquiv_apply_self {k : Type u} [CommRing k] {B : Type w} [NonAssocRing B] [Module k B] [SMulCommClass k B B] [IsScalarTower k B B] {D : ConicAlgebra k B} [IsAlternative B] (h : D.IsMultiplicative) (x : B) (hx : D.norm x = 1) : (h.leftMulConjIsometryEquiv x hx) x = 1

theorem ConicAlgebra.IsMultiplicative.exists_isometryEquiv_map_one_of_similarity {k : Type u} {A : Type v} [CommRing k] [NonAssocRing A] [Module k A] {B : Type w} [NonAssocRing B] [Module k B] [SMulCommClass k B B] [IsScalarTower k B B] {D : ConicAlgebra k B} [IsAlternative B] (h : D.IsMultiplicative) (C : ConicAlgebra k A) (e : A ≃ₗ[k] B) (μ : kˣ) (he : ∀ (x : A), D.norm (e x) = ↑μ * C.norm x) : ∃ (e' : QuadraticMap.IsometryEquiv C.norm D.norm), e' 1 = 1

GPR 23.3, for norm similarities. A similarity from the norm of C to the norm of an alternative multiplicative conic algebra D can be normalized to a unital norm isometry.

Here a similarity is given by a linear equivalence e and its unit multiplier μ, with n_D(e x) = μ n_C(x). Postcomposition by μ⁻¹ L_{conj (e 1)} removes the multiplier and sends 1 to 1.

theorem ConicAlgebra.trace_map_of_isometryEquiv_map_one {k : Type u} {A : Type v} [CommRing k] [NonAssocRing A] [Module k A] {B : Type w} [NonAssocRing B] [Module k B] (C : ConicAlgebra k A) (D : ConicAlgebra k B) (e : QuadraticMap.IsometryEquiv C.norm D.norm) (h1 : e 1 = 1) (x : A) : D.trace (e x) = C.trace x

GPR 23.2. A unital norm isometry preserves the trace derived from the polar form.

theorem ConicAlgebra.conj_map_of_isometryEquiv_map_one {k : Type u} {A : Type v} [CommRing k] [NonAssocRing A] [Module k A] {B : Type w} [NonAssocRing B] [Module k B] (C : ConicAlgebra k A) (D : ConicAlgebra k B) (e : QuadraticMap.IsometryEquiv C.norm D.norm) (h1 : e 1 = 1) (x : A) : D.conj (e x) = e (C.conj x)

GPR 23.2. A unital norm isometry commutes with standard conjugation.

theorem ConicAlgebra.map_mul_self_of_isometryEquiv_map_one {k : Type u} {A : Type v} [CommRing k] [NonAssocRing A] [Module k A] {B : Type w} [NonAssocRing B] [Module k B] (C : ConicAlgebra k A) (D : ConicAlgebra k B) (e : QuadraticMap.IsometryEquiv C.norm D.norm) (h1 : e 1 = 1) (x : A) : e (x * x) = e x * e x

GPR 23.2. A unital norm isometry preserves squares. This is the multiplication that is already forced by the degree-two identity before the Cayley–Dickson induction recovers mixed products.

noncomputable def ConicAlgebra.adjoinElementLinearEquivOfMapOne {k : Type u} {A : Type v} [CommRing k] [NonAssocRing A] [Module k A] [SMulCommClass k A A] [IsScalarTower k A A] {B : Type w} [NonAssocRing B] [Module k B] [SMulCommClass k B B] [IsScalarTower k B B] (C : ConicAlgebra k A) (D : ConicAlgebra k B) (e : A ≃ₗ[k] B) (h1 : e 1 = 1) (u : A) : ↥(C.adjoinElement u) ≃ₗ[k] ↥(D.adjoinElement (e u))

A unital linear equivalence restricts to a linear equivalence k[u] ≃ₗ[k] k[e u] between the quadratic subalgebras generated by corresponding elements.

No discriminant or rank hypothesis is needed: both subalgebras are, by definition, the spans of 1 and the indicated element.

Equations

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

@[simp]

theorem ConicAlgebra.coe_adjoinElementLinearEquivOfMapOne_apply {k : Type u} {A : Type v} [CommRing k] [NonAssocRing A] [Module k A] [SMulCommClass k A A] [IsScalarTower k A A] {B : Type w} [NonAssocRing B] [Module k B] [SMulCommClass k B B] [IsScalarTower k B B] (C : ConicAlgebra k A) (D : ConicAlgebra k B) (e : A ≃ₗ[k] B) (h1 : e 1 = 1) (u : A) (x : ↥(C.adjoinElement u)) : ↑((C.adjoinElementLinearEquivOfMapOne D e h1 u) x) = e ↑x

theorem ConicAlgebra.adjoinElementLinearEquivOfIsometryEquiv_map_mul {k : Type u} {A : Type v} [CommRing k] [NonAssocRing A] [Module k A] [SMulCommClass k A A] [IsScalarTower k A A] {B : Type w} [NonAssocRing B] [Module k B] [SMulCommClass k B B] [IsScalarTower k B B] (C : ConicAlgebra k A) (D : ConicAlgebra k B) (e : QuadraticMap.IsometryEquiv C.norm D.norm) (h1 : e 1 = 1) (u : A) (x y : ↥(C.adjoinElement u)) : (C.adjoinElementLinearEquivOfMapOne D e.toLinearEquiv h1 u) (x * y) = (C.adjoinElementLinearEquivOfMapOne D e.toLinearEquiv h1 u) x * (C.adjoinElementLinearEquivOfMapOne D e.toLinearEquiv h1 u) y

The quadratic base case for Layer 9. A unital norm isometry restricts to a unital multiplicative linear equivalence k[u] ≅ k[e u].

Multiplication in these monogenic conic algebras is the coefficient formula of GPR 19.8; its only structure constants are t(u) and n(u), both preserved by a unital norm isometry.

@[simp]

theorem ConicAlgebra.adjoinElementLinearEquivOfMapOne_apply_one {k : Type u} {A : Type v} [CommRing k] [NonAssocRing A] [Module k A] [SMulCommClass k A A] [IsScalarTower k A A] {B : Type w} [NonAssocRing B] [Module k B] [SMulCommClass k B B] [IsScalarTower k B B] (C : ConicAlgebra k A) (D : ConicAlgebra k B) (e : A ≃ₗ[k] B) (h1 : e 1 = 1) (u : A) : (C.adjoinElementLinearEquivOfMapOne D e h1 u) 1 = 1

noncomputable def ConicAlgebra.adjoinElementIsometryEquivOfMapOne {k : Type u} {A : Type v} [CommRing k] [NonAssocRing A] [Module k A] [SMulCommClass k A A] [IsScalarTower k A A] {B : Type w} [NonAssocRing B] [Module k B] [SMulCommClass k B B] [IsScalarTower k B B] (C : ConicAlgebra k A) (D : ConicAlgebra k B) (e : QuadraticMap.IsometryEquiv C.norm D.norm) (h1 : e 1 = 1) (u : A) : QuadraticMap.IsometryEquiv (C.restrict (C.adjoinElement u)).norm (D.restrict (D.adjoinElement (e u))).norm

The quadratic base equivalence of Layer 9, including its norm-isometry structure.

Equations

• C.adjoinElementIsometryEquivOfMapOne D e h1 u = { toLinearEquiv := C.adjoinElementLinearEquivOfMapOne D e.toLinearEquiv h1 u, map_app' := ⋯ }

noncomputable def ConicAlgebra.cayAdjoinElementIsometryEquivOfMapOne {k : Type u} {A : Type v} [CommRing k] [NonAssocRing A] [Module k A] [SMulCommClass k A A] [IsScalarTower k A A] {B : Type w} [NonAssocRing B] [Module k B] [SMulCommClass k B B] [IsScalarTower k B B] (C : ConicAlgebra k A) (D : ConicAlgebra k B) (e : QuadraticMap.IsometryEquiv C.norm D.norm) (h1 : e 1 = 1) (u : A) (μ : k) : QuadraticMap.IsometryEquiv ((C.restrict (C.adjoinElement u)).cay μ).norm ((D.restrict (D.adjoinElement (e u))).cay μ).norm

The first Cayley–Dickson step in Layer 9. The corresponding quadratic subalgebras k[u] and k[e u] can be doubled by any common scalar μ; the componentwise equivalence is a unital, multiplicative norm isometry.

The complement isometry obtained from Witt cancellation supplies such a common scalar by carrying a chosen doubling vector to one with the same norm.

Equations

• C.cayAdjoinElementIsometryEquivOfMapOne D e h1 u μ = ConicAlgebra.cayIsometryEquiv (D.restrict (D.adjoinElement (e u))) (C.adjoinElementIsometryEquivOfMapOne D e h1 u)

theorem ConicAlgebra.cayAdjoinElementIsometryEquivOfMapOne_map_one {k : Type u} {A : Type v} [CommRing k] [NonAssocRing A] [Module k A] [SMulCommClass k A A] [IsScalarTower k A A] {B : Type w} [NonAssocRing B] [Module k B] [SMulCommClass k B B] [IsScalarTower k B B] (C : ConicAlgebra k A) (D : ConicAlgebra k B) (e : QuadraticMap.IsometryEquiv C.norm D.norm) (h1 : e 1 = 1) (u : A) (μ : k) : (C.cayAdjoinElementIsometryEquivOfMapOne D e h1 u μ) 1 = 1

The matched equivalence between the first doubles preserves the identity.

theorem ConicAlgebra.cayAdjoinElementIsometryEquivOfMapOne_map_mul {k : Type u} {A : Type v} [CommRing k] [NonAssocRing A] [Module k A] [SMulCommClass k A A] [IsScalarTower k A A] {B : Type w} [NonAssocRing B] [Module k B] [SMulCommClass k B B] [IsScalarTower k B B] (C : ConicAlgebra k A) (D : ConicAlgebra k B) (e : QuadraticMap.IsometryEquiv C.norm D.norm) (h1 : e 1 = 1) (u : A) (μ : k) (x y : (C.restrict (C.adjoinElement u)).Cay μ) : (C.cayAdjoinElementIsometryEquivOfMapOne D e h1 u μ) (x * y) = (C.cayAdjoinElementIsometryEquivOfMapOne D e h1 u μ) x * (C.cayAdjoinElementIsometryEquivOfMapOne D e h1 u μ) y

The matched equivalence between the first doubles preserves multiplication.

theorem ConicAlgebra.exists_doubledSubalgebras_isometryEquiv_and_equiv_cay {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] {B : Type w} [NonAssocRing B] [Module k B] [SMulCommClass k B B] [IsScalarTower k B B] [Module.Finite k B] [Module.Projective k B] [IsAlternative A] [IsAlternative B] (C : ConicAlgebra k A) (D : ConicAlgebra k B) (S : NonAssocSubalgebra k A) (T : NonAssocSubalgebra k B) (hCmul : C.IsMultiplicative) (hDmul : D.IsMultiplicative) (e : QuadraticMap.IsometryEquiv (C.restrict S).norm (D.restrict T).norm) (h1 : e 1 = 1) (hmul : ∀ (x y : ↥S), e (x * y) = e x * e y) {v : A} {v' : B} (hSv : ∀ s ∈ S, QuadraticMap.polar (⇑C.norm) s v = 0) (hTv' : ∀ t ∈ T, QuadraticMap.polar (⇑D.norm) t v' = 0) (hv : IsUnit (C.norm v)) (hnorm : D.norm v' = C.norm v) (hinjC : Function.Injective ⇑(C.cayToAlgebra S v)) (hinjD : Function.Injective ⇑(D.cayToAlgebra T v')) : ∃ (S' : NonAssocSubalgebra k A) (T' : NonAssocSubalgebra k B) (iC : (C.restrict S).Cay (-C.norm v) ≃ₗ[k] ↥S') (iD : (D.restrict T).Cay (-D.norm v') ≃ₗ[k] ↥T') (f : QuadraticMap.IsometryEquiv (C.restrict S').norm (D.restrict T').norm), (∀ (p : (C.restrict S).Cay (-C.norm v)), ↑(iC p) = (C.cayToAlgebra S v) p) ∧ (∀ (p : (D.restrict T).Cay (-D.norm v')), ↑(iD p) = (D.cayToAlgebra T v') p) ∧ f 1 = 1 ∧ ∀ (x y : ↥S'), f (x * y) = f x * f y

One internal matched-doubling step for Layer 9. Suppose S ⊆ A and T ⊆ B are already related by a unital multiplicative norm isometry. If v ⊥ S and v' ⊥ T have the same norm, then the internal doubles S + Sv and T + Tv' are again related by such an isometry, provided the two internal doubling maps are injective.

The resulting subalgebras are the images of cayToAlgebra. The equivalence is obtained by moving back to the external double, applying cayIsometryEquiv componentwise, and moving into the other image.

theorem ConicAlgebra.exists_doubledSubalgebras_isometryEquiv {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] {B : Type w} [NonAssocRing B] [Module k B] [SMulCommClass k B B] [IsScalarTower k B B] [Module.Finite k B] [Module.Projective k B] [IsAlternative A] [IsAlternative B] (C : ConicAlgebra k A) (D : ConicAlgebra k B) (S : NonAssocSubalgebra k A) (T : NonAssocSubalgebra k B) (hCmul : C.IsMultiplicative) (hDmul : D.IsMultiplicative) (e : QuadraticMap.IsometryEquiv (C.restrict S).norm (D.restrict T).norm) (h1 : e 1 = 1) (hmul : ∀ (x y : ↥S), e (x * y) = e x * e y) {v : A} {v' : B} (hSv : ∀ s ∈ S, QuadraticMap.polar (⇑C.norm) s v = 0) (hTv' : ∀ t ∈ T, QuadraticMap.polar (⇑D.norm) t v' = 0) (hv : IsUnit (C.norm v)) (hnorm : D.norm v' = C.norm v) (hinjC : Function.Injective ⇑(C.cayToAlgebra S v)) (hinjD : Function.Injective ⇑(D.cayToAlgebra T v')) : ∃ (S' : NonAssocSubalgebra k A) (T' : NonAssocSubalgebra k B) (f : QuadraticMap.IsometryEquiv (C.restrict S').norm (D.restrict T').norm), f 1 = 1 ∧ ∀ (x y : ↥S'), f (x * y) = f x * f y

The internal matched-doubling step, with the external-to-image equivalences hidden.

theorem ConicAlgebra.exists_doubledSubalgebras_isometryEquiv_of_isGPRRegular {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] {B : Type w} [NonAssocRing B] [Module k B] [SMulCommClass k B B] [IsScalarTower k B B] [Module.Finite k B] [Module.Projective k B] [IsAlternative A] [IsAlternative B] (C : ConicAlgebra k A) (D : ConicAlgebra k B) (S : NonAssocSubalgebra k A) (T : NonAssocSubalgebra k B) (hCmul : C.IsMultiplicative) (hDmul : D.IsMultiplicative) (hSreg : (C.restrict S).norm.IsGPRRegular) (hTreg : (D.restrict T).norm.IsGPRRegular) (e : QuadraticMap.IsometryEquiv (C.restrict S).norm (D.restrict T).norm) (h1 : e 1 = 1) (hmul : ∀ (x y : ↥S), e (x * y) = e x * e y) {v : A} {v' : B} (hSv : ∀ s ∈ S, QuadraticMap.polar (⇑C.norm) s v = 0) (hTv' : ∀ t ∈ T, QuadraticMap.polar (⇑D.norm) t v' = 0) (hv : IsUnit (C.norm v)) (hnorm : D.norm v' = C.norm v) : ∃ (S' : NonAssocSubalgebra k A) (T' : NonAssocSubalgebra k B) (f : QuadraticMap.IsometryEquiv (C.restrict S').norm (D.restrict T').norm), f 1 = 1 ∧ ∀ (x y : ↥S'), f (x * y) = f x * f y

The regular-base form of exists_doubledSubalgebras_isometryEquiv. Regularity makes both internal doubling maps injective, so it is the form used by the Layer 9 induction.

noncomputable def ConicAlgebra.unitFormLinearEquivOfRankAtStalkEqOne {k : Type u} {A : Type v} [CommRing k] [NonAssocRing A] [Module k A] [Module.Finite k A] [Module.Projective k A] (C : ConicAlgebra k A) [Nontrivial k] (hA : Module.rankAtStalk A = fun (x : PrimeSpectrum k) => 1) : A ≃ₗ[k] k

The canonical linear equivalence from a rank-one conic algebra to its base ring.

Equations

• C.unitFormLinearEquivOfRankAtStalkEqOne hA = { toLinearMap := C.unitForm, invFun := fun (a : k) => a • 1, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem ConicAlgebra.unitFormLinearEquivOfRankAtStalkEqOne_apply_one {k : Type u} {A : Type v} [CommRing k] [NonAssocRing A] [Module k A] [Module.Finite k A] [Module.Projective k A] (C : ConicAlgebra k A) [Nontrivial k] (hA : Module.rankAtStalk A = fun (x : PrimeSpectrum k) => 1) : (C.unitFormLinearEquivOfRankAtStalkEqOne hA) 1 = 1

theorem ConicAlgebra.linearEquiv_map_mul_of_rankAtStalk_eq_one {k : Type u} {A : Type v} [CommRing k] [NonAssocRing A] [Module k A] [IsScalarTower k A A] [Module.Finite k A] [Module.Projective k A] {B : Type w} [NonAssocRing B] [Module k B] [IsScalarTower k B B] [Nontrivial k] (C : ConicAlgebra k A) (e : A ≃ₗ[k] B) (he1 : e 1 = 1) (hA : Module.rankAtStalk A = fun (x : PrimeSpectrum k) => 1) (x y : A) : e (x * y) = e x * e y

Every unital linear equivalence between constant-rank-one conic algebras is multiplicative.

theorem ConicAlgebra.exists_isometryEquiv_map_one_map_mul_of_rankAtStalk_eq_one {k : Type u} {A : Type v} [CommRing k] [NonAssocRing A] [Module k A] [IsScalarTower k A A] [Module.Finite k A] [Module.Projective k A] {B : Type w} [NonAssocRing B] [Module k B] [IsScalarTower k B B] [Module.Finite k B] [Module.Projective k B] [Nontrivial k] (C : ConicAlgebra k A) (D : ConicAlgebra k B) (hA : Module.rankAtStalk A = fun (x : PrimeSpectrum k) => 1) (hB : Module.rankAtStalk B = fun (x : PrimeSpectrum k) => 1) : ∃ (e : QuadraticMap.IsometryEquiv C.norm D.norm), e 1 = 1 ∧ ∀ (x y : A), e (x * y) = e x * e y

The rank-one case of the converse direction in Layer 9. Any two constant-rank-one conic algebras over a nontrivial base are unital multiplicatively norm-isometric. Both are canonically identified with the base ring by unitForm; this avoids imposing regularity on the polar form, which can fail in characteristic two.

theorem ConicAlgebra.isometryEquivOf_fullRank_subalgebras {k : Type u} {A : Type v} [CommRing k] [NonAssocRing A] [Module k A] [Module.Finite k A] [Module.Projective k A] {B : Type w} [NonAssocRing B] [Module k B] [Module.Finite k B] [Module.Projective k B] (C : ConicAlgebra k A) (D : ConicAlgebra k B) (S : NonAssocSubalgebra k A) (T : NonAssocSubalgebra k B) (f : QuadraticMap.IsometryEquiv (C.restrict S).norm (D.restrict T).norm) (hf1 : f 1 = 1) (hfmul : ∀ (x y : ↥S), f (x * y) = f x * f y) (hSreg : (C.restrict S).norm.IsGPRRegular) (hTreg : (D.restrict T).norm.IsGPRRegular) {r : ℕ} (hA : Module.rankAtStalk A = fun (x : PrimeSpectrum k) => r) (hB : Module.rankAtStalk B = fun (x : PrimeSpectrum k) => r) (hS : Module.rankAtStalk ↥S.toSubmodule = fun (x : PrimeSpectrum k) => r) (hT : Module.rankAtStalk ↥T.toSubmodule = fun (x : PrimeSpectrum k) => r) : ∃ (e : QuadraticMap.IsometryEquiv C.norm D.norm), e 1 = 1 ∧ ∀ (x y : A), e (x * y) = e x * e y

Full-rank assembly for Layer 9. A unital multiplicative norm isometry between regular subalgebras of the same full rank extends to the ambient algebras, because each inclusion is then a linear equivalence.

The full-rank assertion is converted to surjectivity by ConicAlgebra.mem_of_isGPRRegular_of_rankAtStalk_eq; no choice of complements remains at this stage.

theorem ConicAlgebra.elementDiscriminant_map_of_isometryEquiv_map_one {k : Type u} {A : Type v} [CommRing k] [NonAssocRing A] [Module k A] {B : Type w} [NonAssocRing B] [Module k B] (C : ConicAlgebra k A) (D : ConicAlgebra k B) (e : QuadraticMap.IsometryEquiv C.norm D.norm) (h1 : e 1 = 1) (u : A) : D.elementDiscriminant (e u) = C.elementDiscriminant u

A unital norm isometry preserves the element discriminant t(u) ^ 2 - 4 * n(u).

theorem ConicAlgebra.isRegularRankTwoComposition_map_of_isometryEquiv_map_one {k : Type u} {A : Type v} [CommRing k] [NonAssocRing A] [Module k A] [SMulCommClass k A A] [IsScalarTower k A A] {B : Type w} [NonAssocRing B] [Module k B] [SMulCommClass k B B] [IsScalarTower k B B] (C : ConicAlgebra k A) (D : ConicAlgebra k B) (e : QuadraticMap.IsometryEquiv C.norm D.norm) (h1 : e 1 = 1) {u : A} (hu : C.IsRegularRankTwoComposition u) : D.IsRegularRankTwoComposition (e u)

A unital norm isometry carries the regular rank-two composition subalgebra generated by u to the one generated by e u. This is the base rung that the Layer 9 doubling induction uses.

theorem ConicAlgebra.exists_isometryEquiv_polarOrthogonal {k : Type u} {A : Type v} [CommRing k] [NonAssocRing A] [Module k A] [Module.Finite k A] [Module.Projective k A] {B : Type w} [NonAssocRing B] [Module k B] [Module.Finite k B] [Module.Projective k B] (hLG : IsLGRing k) (C : ConicAlgebra k A) (D : ConicAlgebra k B) (hD : D.IsComposition) (S : NonAssocSubalgebra k A) (T : NonAssocSubalgebra k B) (hSreg : (C.restrict S).norm.IsGPRRegular) (hTreg : (D.restrict T).norm.IsGPRRegular) (eST : QuadraticMap.IsometryEquiv (C.restrict S).norm (D.restrict T).norm) (e : QuadraticMap.IsometryEquiv C.norm D.norm) : Nonempty ((QuadraticMap.comp C.norm (C.norm.polarOrthogonal S.toSubmodule).subtype).IsometryEquiv (QuadraticMap.comp D.norm (D.norm.polarOrthogonal T.toSubmodule).subtype))

The general Witt-cancellation step for Layer 9. If an ambient norm isometry identifies the regular restricted norm forms on S ⊆ A and T ⊆ B, then their orthogonal complements are isometric over an LG ring.

This is the form needed after every matched doubling rung. The target ambient norm is assumed non-singular in the GPR sense through hD; no composition hypothesis on C is used.

theorem ConicAlgebra.IsComposition.exists_matched_isUnit_norm_orthogonal {k : Type u} {A : Type v} [CommRing k] [NonAssocRing A] [Module k A] [Module.Finite k A] [Module.Projective k A] {B : Type w} [NonAssocRing B] [Module k B] [Module.Finite k B] [Module.Projective k B] (hLG : IsLGRing k) (C : ConicAlgebra k A) (D : ConicAlgebra k B) (hC : C.IsComposition) (hD : D.IsComposition) (S : NonAssocSubalgebra k A) (T : NonAssocSubalgebra k B) (hSreg : (C.restrict S).norm.IsGPRRegular) (hTreg : (D.restrict T).norm.IsGPRRegular) (eST : QuadraticMap.IsometryEquiv (C.restrict S).norm (D.restrict T).norm) (e : QuadraticMap.IsometryEquiv C.norm D.norm) (hsupp : Module.HasFullSupport k ↥(C.norm.polarOrthogonal S.toSubmodule)) : ∃ (v : A) (v' : B), IsUnit (C.norm v) ∧ (∀ s ∈ S, QuadraticMap.polar (⇑C.norm) s v = 0) ∧ (∀ t ∈ T, QuadraticMap.polar (⇑D.norm) t v' = 0) ∧ D.norm v' = C.norm v

Selecting matched doubling vectors at an arbitrary Layer 9 rung. If the complement of S has full support, it represents a unit over the LG ring. The general cancellation isometry then carries that vector to the complement of T, preserving its norm exactly.

theorem ConicAlgebra.IsComposition.exists_next_doubledSubalgebras_isometryEquiv {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] {B : Type w} [NonAssocRing B] [Module k B] [SMulCommClass k B B] [IsScalarTower k B B] [Module.Finite k B] [Module.Projective k B] [IsAlternative A] [IsAlternative B] (hLG : IsLGRing k) (C : ConicAlgebra k A) (D : ConicAlgebra k B) (hC : C.IsComposition) (hD : D.IsComposition) (S : NonAssocSubalgebra k A) (T : NonAssocSubalgebra k B) (hSreg : (C.restrict S).norm.IsGPRRegular) (hTreg : (D.restrict T).norm.IsGPRRegular) (eST : QuadraticMap.IsometryEquiv (C.restrict S).norm (D.restrict T).norm) (h1 : eST 1 = 1) (hmul : ∀ (x y : ↥S), eST (x * y) = eST x * eST y) (e : QuadraticMap.IsometryEquiv C.norm D.norm) (hsupp : Module.HasFullSupport k ↥(C.norm.polarOrthogonal S.toSubmodule)) : ∃ (S' : NonAssocSubalgebra k A) (T' : NonAssocSubalgebra k B) (f : QuadraticMap.IsometryEquiv (C.restrict S').norm (D.restrict T').norm), f 1 = 1 ∧ ∀ (x y : ↥S'), f (x * y) = f x * f y

One complete induction step for Layer 9. Matched regular subalgebras with a proper source complement can be enlarged simultaneously: unit representation and Witt cancellation choose matched orthogonal vectors, and internal Cayley–Dickson doubling produces new image subalgebras related by a unital multiplicative norm isometry.

theorem ConicAlgebra.IsComposition.exists_next_isGPRRegular_rankAtStalk_two_mul {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] {B : Type w} [NonAssocRing B] [Module k B] [SMulCommClass k B B] [IsScalarTower k B B] [Module.Finite k B] [Module.Projective k B] [IsAlternative A] [IsAlternative B] (hLG : IsLGRing k) (C : ConicAlgebra k A) (D : ConicAlgebra k B) (hC : C.IsComposition) (hD : D.IsComposition) (S : NonAssocSubalgebra k A) (T : NonAssocSubalgebra k B) (hSreg : (C.restrict S).norm.IsGPRRegular) (hTreg : (D.restrict T).norm.IsGPRRegular) (eST : QuadraticMap.IsometryEquiv (C.restrict S).norm (D.restrict T).norm) (h1 : eST 1 = 1) (hmul : ∀ (x y : ↥S), eST (x * y) = eST x * eST y) (e : QuadraticMap.IsometryEquiv C.norm D.norm) {s : ℕ} (hSrank : Module.rankAtStalk ↥S.toSubmodule = fun (x : PrimeSpectrum k) => s) (hTrank : Module.rankAtStalk ↥T.toSubmodule = fun (x : PrimeSpectrum k) => s) (hsupp : Module.HasFullSupport k ↥(C.norm.polarOrthogonal S.toSubmodule)) : ∃ (S' : NonAssocSubalgebra k A) (T' : NonAssocSubalgebra k B) (f : QuadraticMap.IsometryEquiv (C.restrict S').norm (D.restrict T').norm), f 1 = 1 ∧ (∀ (x y : ↥S'), f (x * y) = f x * f y) ∧ (C.restrict S').norm.IsGPRRegular ∧ (D.restrict T').norm.IsGPRRegular ∧ (Module.rankAtStalk ↥S'.toSubmodule = fun (x : PrimeSpectrum k) => 2 * s) ∧ Module.rankAtStalk ↥T'.toSubmodule = fun (x : PrimeSpectrum k) => 2 * s

The self-feeding Layer 9 induction step. If the matched input subalgebras both have constant rank s, the enlarged subalgebras have regular restricted norms and constant rank 2s, in addition to carrying the new unital multiplicative norm isometry. Thus the output satisfies the hypotheses needed for the next doubling rung.

theorem ConicAlgebra.IsComposition.exists_fullRank_subalgebras_isometryEquiv {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] {B : Type w} [NonAssocRing B] [Module k B] [SMulCommClass k B B] [IsScalarTower k B B] [Nontrivial k] [Module.Finite k B] [Module.Projective k B] [IsAlternative A] [IsAlternative B] (hLG : IsLGRing k) (C : ConicAlgebra k A) (D : ConicAlgebra k B) (hC : C.IsComposition) (hD : D.IsComposition) (e : QuadraticMap.IsometryEquiv C.norm D.norm) (he1 : e 1 = 1) {r : ℕ} (hA : Module.rankAtStalk A = fun (x : PrimeSpectrum k) => r) (hB : Module.rankAtStalk B = fun (x : PrimeSpectrum k) => r) (hr : 2 ≤ r) : ∃ (S : NonAssocSubalgebra k A) (T : NonAssocSubalgebra k B) (f : QuadraticMap.IsometryEquiv (C.restrict S).norm (D.restrict T).norm), f 1 = 1 ∧ (∀ (x y : ↥S), f (x * y) = f x * f y) ∧ (C.restrict S).norm.IsGPRRegular ∧ (D.restrict T).norm.IsGPRRegular ∧ (Module.rankAtStalk ↥S.toSubmodule = fun (x : PrimeSpectrum k) => r) ∧ Module.rankAtStalk ↥T.toSubmodule = fun (x : PrimeSpectrum k) => r

Finite matched doubling from rank two to full rank. Starting from corresponding regular quadratic subalgebras, the self-feeding step is iterated until both image subalgebras have the full ambient rank.

theorem ConicAlgebra.IsComposition.exists_isometryEquiv_map_one_map_mul_of_rankAtStalk {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] {B : Type w} [NonAssocRing B] [Module k B] [SMulCommClass k B B] [IsScalarTower k B B] [Nontrivial k] [Module.Finite k B] [Module.Projective k B] (hLG : IsLGRing k) (C : ConicAlgebra k A) (D : ConicAlgebra k B) (hC : C.IsComposition) (hD : D.IsComposition) (e : QuadraticMap.IsometryEquiv C.norm D.norm) {r : ℕ} (hA : Module.rankAtStalk A = fun (x : PrimeSpectrum k) => r) (hr : 2 ≤ r) : ∃ (e' : QuadraticMap.IsometryEquiv C.norm D.norm), e' 1 = 1 ∧ ∀ (x y : A), e' (x * y) = e' x * e' y

GPR 23.5, the norm equivalence theorem, in constant rank at least two. Over a nontrivial LG ring, composition algebras of the same constant rank r ≥ 2 with isometric norm forms are isomorphic as unital non-associative algebras. The isomorphism is expressed, as elsewhere in this file, by a linear equivalence together with its unital and multiplicative laws.

The proof normalizes the norm isometry at 1, matches the regular quadratic starting subalgebras, iterates the matched Cayley–Dickson enlargement to full rank, and finally identifies the full-rank image subalgebras with the ambient algebras.

theorem ConicAlgebra.IsComposition.exists_isometryEquiv_map_one_map_mul_of_rankAtStalk_eq {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] {B : Type w} [NonAssocRing B] [Module k B] [SMulCommClass k B B] [IsScalarTower k B B] [Nontrivial k] [Module.Finite k B] [Module.Projective k B] (hLG : IsLGRing k) (C : ConicAlgebra k A) (D : ConicAlgebra k B) (hC : C.IsComposition) (hD : D.IsComposition) (e : QuadraticMap.IsometryEquiv C.norm D.norm) {r : ℕ} (hA : Module.rankAtStalk A = fun (x : PrimeSpectrum k) => r) : ∃ (e' : QuadraticMap.IsometryEquiv C.norm D.norm), e' 1 = 1 ∧ ∀ (x y : A), e' (x * y) = e' x * e' y

GPR 23.5, the norm equivalence theorem. Over a nontrivial LG ring, composition algebras of the same constant rank with isometric norm forms are isomorphic as unital non-associative algebras.

By GPR 19.18, the common rank is 1, 2, 4, or 8. Rank one is handled directly through the canonical unitForm coordinate, while the other three cases use the regular matched-doubling argument based on GPR 19.16(b) and Witt cancellation (GN 6.5).

theorem ConicAlgebra.IsComposition.exists_isometryEquiv_map_one_map_mul {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] {B : Type w} [NonAssocRing B] [Module k B] [SMulCommClass k B B] [IsScalarTower k B B] [Module.Finite k B] [Module.Projective k B] (hLG : IsLGRing k) (C : ConicAlgebra k A) (D : ConicAlgebra k B) (hC : C.IsComposition) (hD : D.IsComposition) (e : QuadraticMap.IsometryEquiv C.norm D.norm) : ∃ (e' : QuadraticMap.IsometryEquiv C.norm D.norm), e' 1 = 1 ∧ ∀ (x y : A), e' (x * y) = e' x * e' y

GPR 23.5, without a constant-rank hypothesis. Over a nontrivial LG ring, composition algebras with isometric norm forms are isomorphic as unital non-associative algebras.

The rank idempotents decompose both modules into the same constant-rank factors: a norm isometry is in particular a linear equivalence, so the two rank functions agree. The constant-rank norm equivalence theorem is applied on every idempotent factor, and the resulting isomorphisms are glued through the module decomposition of GPR Exc. 9.31.

theorem ConicAlgebra.exists_isometryEquiv_polarOrthogonal_adjoinElement {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] {B : Type w} [NonAssocRing B] [Module k B] [SMulCommClass k B B] [IsScalarTower k B B] [Module.Finite k B] [Module.Projective k B] (hLG : IsLGRing k) (C : ConicAlgebra k A) (D : ConicAlgebra k B) (hD : D.IsComposition) (e : QuadraticMap.IsometryEquiv C.norm D.norm) (h1 : e 1 = 1) {u : A} (hu : C.IsRegularRankTwoComposition u) : Nonempty ((QuadraticMap.comp C.norm (C.norm.polarOrthogonal (C.adjoinElement u).toSubmodule).subtype).IsometryEquiv (QuadraticMap.comp D.norm (D.norm.polarOrthogonal (D.adjoinElement (e u)).toSubmodule).subtype))

The Witt-cancellation step in GPR 23.5. Let a unital norm isometry carry u to e u, and suppose k[u] is a regular rank-two composition subalgebra. Then the orthogonal complements of k[u] and k[e u] are isometric over an LG ring.

The ambient forms split as the regular quadratic summand plus its orthogonal complement. The quadratic summands are isometric by adjoinElementLinearEquivOfMapOne; cancelling that common regular summand with GN 6.5 gives the result.

theorem ConicAlgebra.exists_polarOrthogonal_adjoinElement_eq_norm {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] {B : Type w} [NonAssocRing B] [Module k B] [SMulCommClass k B B] [IsScalarTower k B B] [Module.Finite k B] [Module.Projective k B] (hLG : IsLGRing k) (C : ConicAlgebra k A) (D : ConicAlgebra k B) (hD : D.IsComposition) (e : QuadraticMap.IsometryEquiv C.norm D.norm) (h1 : e 1 = 1) {u : A} (hu : C.IsRegularRankTwoComposition u) (v : ↥(C.norm.polarOrthogonal (C.adjoinElement u).toSubmodule)) : ∃ (v' : ↥(D.norm.polarOrthogonal (D.adjoinElement (e u)).toSubmodule)), D.norm ↑v' = C.norm ↑v

Matching the first doubling parameter in Layer 9. Under the hypotheses of the complement cancellation step, every vector in the complement of k[u] has a corresponding vector in the complement of k[e u] with exactly the same norm. In particular, unit-norm doubling vectors give the same Cayley–Dickson scalar on both sides.

theorem ConicAlgebra.IsMultiplicative.exists_isometryEquiv_map_one {k : Type u} {A : Type v} [CommRing k] [NonAssocRing A] [Module k A] {B : Type w} [NonAssocRing B] [Module k B] [SMulCommClass k B B] [IsScalarTower k B B] {D : ConicAlgebra k B} [IsAlternative B] (h : D.IsMultiplicative) (C : ConicAlgebra k A) (e : QuadraticMap.IsometryEquiv C.norm D.norm) : ∃ (e' : QuadraticMap.IsometryEquiv C.norm D.norm), e' 1 = 1

GPR 23.3, unital normalization of a norm isometry. If D is alternative and multiplicative, every isometry n_C ≅ n_D can be postcomposed with a self-isometry of n_D so that it sends 1 to 1. This is the first step of the norm equivalence theorem GPR 23.5.