Documentation

LeanPool.CompositionAlgebrasOverRings.Conic.CayleyDicksonAssociative

Commutativity and associativity of the double (GPR 18.14(a),(b)) #

Cay(B, μ) is associative if and only if B is commutative and associative with involutive conjugation (GPR 18.14(b)), and commutative if and only if B is commutative with trivial conjugation (GPR 18.14(a)). This file proves the directions that build algebras, and packages them as Ring, CommRing and Algebra structures on the double so that the Cayley–Dickson tower can be iterated.

Associativity of Cay(B, μ) supplies the associative input needed for a further application of ConicAlgebra.isMultiplicative_cay or ConicAlgebra.isAlternative_cay. To prove that a double is associative, mul_assoc_cay asks its input to be commutative. The base ring starts this process, but it is not the only possible commutative input: in characteristic two, iterated doubles with trivial conjugation can remain commutative (GPR 18.17(b)).

For iteration, ConicAlgebra.isMultiplicative_cay (the associative special case of GPR Exc. 18.18) and ConicAlgebra.isAlternative_cay (GPR 18.14(c)) both require their input B to be associative, which for a double Cay(B₀, μ₀) is what this file supplies.

The computation #

Write x = (a, b), y = (c, d), z = (e, f). Both components of (xy)z and of x(yz) expand into four terms each, and they match term by term using only

The conjugates conj a, conj c, conj e, … are never expanded via conj z = t(z)·1 - z; they behave as atoms throughout. This is unlike Conic/CayleyDicksonAlternative.lean, where eliminating the conjugation first is what makes the cancellations linear — here commutativity does that job instead, and ring closes both components.

Main results #

Implementation notes #

Cay.ring and Cay.algebra are defs, not instances: associativity of the double depends on hypotheses on B (CommRing, and involutivity of the conjugation) that instance search cannot discharge, and a global instance would be unsound. Use them with letI at the point where the next rung of the tower is built. Cay.algebra is Algebra.ofModule, which needs exactly the SMulCommClass/IsScalarTower pair the double already carries.

⚠ The involutivity hypothesis does not follow from commutativity and associativity over an arbitrary base — see the trace-defect counterexample over ℤ/4 — but it does as soon as B is finitely generated projective, or the base is a field.

References #

source
theorem ConicAlgebra.mul_assoc_cay {k : Type u} {B : Type v} [CommRing k] [CommRing B] [Algebra k B] (C : ConicAlgebra k B) (μ : k) (hconj : C.ConjIsInvolution) (x y z : C.Cay μ) :
x * y * z = x * (y * z)

GPR 18.14(b), ⇐. If B is commutative associative and its conjugation is an involution, then Cay(B, μ) is associative, for every scalar μ.

source
@[instance_reducible]
def ConicAlgebra.Cay.ring {k : Type u} {B : Type v} [CommRing k] [CommRing B] [Algebra k B] (C : ConicAlgebra k B) (μ : k) (hconj : C.ConjIsInvolution) :
Ring (C.Cay μ)

The double of a commutative associative conic algebra with involutive conjugation, as a Ring. A def, not an instance: see the module docstring.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[instance_reducible]
    def ConicAlgebra.Cay.algebra {k : Type u} {B : Type v} [CommRing k] [CommRing B] [Algebra k B] (C : ConicAlgebra k B) (μ : k) (hconj : C.ConjIsInvolution) :
    Algebra k (C.Cay μ)

    The double as a k-algebra, given the Ring structure of ConicAlgebra.Cay.ring. Built by Algebra.ofModule from the SMulCommClass/IsScalarTower instances the double already has.

    Equations
    Instances For

      Failure of commutativity and associativity (GPR 18.14(a),(b), ⇒) #

      The contrapositives, in the explicit form the tower needs: a witness that B's conjugation is not the identity produces a witness that the double is not commutative, and a witness that B is not commutative produces a witness that the double is not associative. These are what show the Cayley–Dickson tower really does lose a property at each step rather than merely failing to preserve it.

      source
      theorem ConicAlgebra.exists_mul_ne_mul_cay {k' : Type u} {B' : Type v} [CommRing k'] [NonAssocRing B'] [Module k' B'] (C' : ConicAlgebra k' B') (μ' : k') {u : B'} (h : C'.conj u ≠ u) :
      ∃ (x : C'.Cay μ') (y : C'.Cay μ'), x * y ≠ y * x

      Cay(B, μ) is not commutative as soon as the conjugation of B moves some element: (u, 0)(0, 1) = (0, u) while (0, 1)(u, 0) = (0, conj u).

      source
      theorem ConicAlgebra.exists_mul_mul_ne_mul_mul_cay {k' : Type u} {B' : Type v} [CommRing k'] [NonAssocRing B'] [Module k' B'] (C' : ConicAlgebra k' B') (μ' : k') (hconj : C'.ConjIsInvolution) {a c : B'} (h : a * c ≠ c * a) :
      ∃ (x : C'.Cay μ') (y : C'.Cay μ') (z : C'.Cay μ'), x * y * z ≠ x * (y * z)

      Cay(B, μ) is not associative as soon as B is not commutative. With x = (0, 1), y = (conj a, 0) and z = (conj c, 0), the second components of (xy)z and x(yz) are ac and ca.

      Commutativity (GPR 18.14(a)) #

      source
      theorem ConicAlgebra.mul_comm_cay {k : Type u} {B : Type v} [CommRing k] [CommRing B] [Algebra k B] (C : ConicAlgebra k B) (μ : k) (hconj : ∀ (u : B), C.conj u = u) (x y : C.Cay μ) :
      x * y = y * x

      If the conjugation of a commutative B is the identity then Cay(B, μ) is commutative.

      Both products come out as (ac + μ db, da + bc); only commutativity of B is used, since with conj = id there is nothing left for the conjugation to do. The base ring satisfies the hypothesis (ConicAlgebra.baseRing_conj_apply). More generally, GPR 18.14(a) characterizes commutativity of Cay(B, μ) by commutativity of B with trivial conjugation.

      source
      theorem ConicAlgebra.conjIsInvolution_of_conj_eq_id {k : Type u} {B : Type v} [CommRing k] [CommRing B] [Algebra k B] (C : ConicAlgebra k B) (hconj : ∀ (u : B), C.conj u = u) :
      C.ConjIsInvolution

      With the conjugation of B the identity, the conjugation is automatically an involution: the condition conj (xy) = conj y * conj x reduces to xy = yx.

      source
      @[instance_reducible]
      def ConicAlgebra.Cay.commRing {k : Type u} {B : Type v} [CommRing k] [CommRing B] [Algebra k B] (C : ConicAlgebra k B) (μ : k) (hconj : ∀ (u : B), C.conj u = u) :
      CommRing (C.Cay μ)

      The double of a commutative conic algebra whose conjugation is the identity, as a CommRing. This is the instance that gets the Cayley–Dickson tower off the ground: it makes Cay(k, μ₁) commutative, which is what ConicAlgebra.mul_assoc_cay needs in order to make Cay(Cay(k, μ₁), μ₂) associative. A def, not an instance — see the module docstring.

      Equations
      Instances For