The two embeddings of ℂ in the quaternions are conjugate

Complex conjugation on the copy of ℂ inside the real quaternions is conjugation by j:

ofComplex (conj z) = j * ofComplex z * j⁻¹.

This is the second half of the "Skolem-Noether in the small" worked example of the semisimple algebras roadmap; the first half, that every ℝ-algebra automorphism of ℍ[ℝ] is inner, is an example in TauCeti/Algebra/CentralSimple/SkolemNoether.lean, read straight off TauCeti.exists_unit_conj_of_algEquiv.

The two halves are not the same theorem. TauCeti.skolemNoether conjugates two K-algebra maps B →ₐ[K] A when both A and B are central simple over K, and ℂ is not central over ℝ: its centre is all of ℂ, not the image of ℝ. Centrality of the source cannot simply be dropped either -- the negative control in that same file exhibits complex conjugation as an ℝ-algebra automorphism of ℂ that is not inner in ℂ. So the statement above is an instance of the noncentral Skolem-Noether theorem, which that roadmap defers, and it is proved here by hand.

The proof uses none of the central simple machinery. An ℝ-algebra map ℂ →ₐ[ℝ] A is the same thing as a square root of -1 in A (Mathlib's Complex.lift), so what has to be proved is that any two square roots of -1 in ℍ[ℝ] are conjugate. Given x * x = u * u = -1, the element w = 1 - u * x satisfies w * x = u * w, both sides being x + u; and w vanishes exactly when u * x = 1. Since x⁻¹ = -x, that excluded case is u = -x, and for x = i it is settled by j, which anticommutes with i. So every square root of -1 is conjugate to i, hence any two are conjugate to each other. Complex conjugation is exactly the excluded case, which is why j is the witness the roadmap names.

Main definitions

• TauCeti.Quaternion.jUnit: the quaternion j, as a unit of the division ring ℍ[ℝ].

Main statements

• TauCeti.Quaternion.conj_jUnit_ofComplex_I: conjugation by j negates i.
• TauCeti.Quaternion.exists_unit_conj_of_mul_self_eq_neg_one: any two square roots of -1 in ℍ[ℝ] are conjugate by a unit.
• TauCeti.Quaternion.exists_unit_conj_complexAlgHom: noncentral Skolem-Noether for ℂ ⊆ ℍ[ℝ] -- any two ℝ-algebra maps ℂ →ₐ[ℝ] ℍ[ℝ] are conjugate by a unit of ℍ[ℝ].
• TauCeti.Quaternion.ofComplex_conjAe: complex conjugation on ℂ ⊆ ℍ[ℝ] is conjugation by j, the roadmap's statement, with the explicit witness.

Implementation notes

Squares are written u * u = -1 rather than u ^ 2 = -1, matching the subtype {I' // I' * I' = -1} that Mathlib's Complex.lift is stated over, so that no sq/pow translation is needed where the universal property is used. That universal property is consumed rather than restated: the square relation is (Complex.lift.symm f).prop, and the coordinate formula for an ℝ-algebra map out of ℂ is Complex.lift.apply_symm_apply followed by Complex.liftAux_apply.

Two steps of the argument are stated as private lemmas because they are wanted only here, and in a generality -- any division ring for the conjugacy of the square roots of -1, any ℝ-algebra for the detection of a conjugacy on Complex.I -- that no statement of this file uses.

TauCeti.Quaternion.jUnit carries its inverse as data rather than being built with Units.mk0 from a nonvanishing proof: ↑jUnit⁻¹ is then a quaternion literal definitionally, which turns the one coordinate computation of the file into a rewrite rather than a division. The body is not exposed, so the two coercion lemmas below are proved (rfl) rather than rfl.

The two coordinate identities are stated with the type ascriptions written out, (⟨0, 0, 1, 0⟩ : ℍ[ℝ]) * …, and are consumed by exact/rw rather than being inlined into the proofs that need them. Quaternion R is a plain def for ℍ[R,-1,-1], so an ascribed anonymous constructor elaborates at the unfolded type and QuaternionAlgebra.mk_mul_mk applies to it, whereas the same literal reached through a declaration of type ℍ[ℝ] does not match that simp lemma at all and the product stays stuck. Neither TauCeti.Quaternion.coe_jUnit nor TauCeti.Quaternion.coe_inv_jUnit is a simp lemma for the same reason: rewriting with them puts a literal where nothing can act on it unless the goal is already in the ascribed form.

References

This is the ℂ ⊆ ℍ half of the "Skolem-Noether in the small" worked example of the semisimple algebras roadmap. See P. Gille, T. Szamuely, Central Simple Algebras and Galois Cohomology, CUP (2006), §2.7, and I. N. Herstein, Noncommutative Rings, MAA (1968), Ch. 4.

def TauCeti.Quaternion.jUnit : (Quaternion ℝ)ˣ

The quaternion j, as a unit of the division ring ℍ[ℝ]. Its inverse -j is supplied as data, so that ↑jUnit⁻¹ reduces to a quaternion literal without a division.

Equations

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

theorem TauCeti.Quaternion.coe_jUnit : ↑jUnit = { re := 0, imI := 0, imJ := 1, imK := 0 }

theorem TauCeti.Quaternion.coe_inv_jUnit : ↑jUnit⁻¹ = { re := 0, imI := 0, imJ := -1, imK := 0 }

theorem TauCeti.Quaternion.ofComplex_I : Quaternion.ofComplex Complex.I = { re := 0, imI := 1, imJ := 0, imK := 0 }

The coordinates of i: the image of Complex.I under the standard embedding.

theorem TauCeti.Quaternion.conj_jUnit_ofComplex_I : ↑jUnit * Quaternion.ofComplex Complex.I * ↑jUnit⁻¹ = -Quaternion.ofComplex Complex.I

Conjugation by j negates i. This is the one computation with quaternion coordinates that the file needs: j anticommutes with i.

theorem TauCeti.Quaternion.exists_unit_conj_ofComplex_I {u : Quaternion ℝ} (hu : u * u = -1) : ∃ (w : (Quaternion ℝ)ˣ), u = ↑w * Quaternion.ofComplex Complex.I * ↑w⁻¹

Every square root of -1 in ℍ[ℝ] is conjugate to i. In the generic case the conjugating unit is 1 - u * i; the one element that excludes is -i, which j conjugates i to.

theorem TauCeti.Quaternion.exists_unit_conj_of_mul_self_eq_neg_one {u v : Quaternion ℝ} (hu : u * u = -1) (hv : v * v = -1) : ∃ (w : (Quaternion ℝ)ˣ), v = ↑w * u * ↑w⁻¹

Any two square roots of -1 in ℍ[ℝ] are conjugate by a unit of ℍ[ℝ]: both are conjugate to i.

theorem TauCeti.Quaternion.exists_unit_conj_complexAlgHom (f g : ℂ →ₐ[ℝ] Quaternion ℝ) : ∃ (w : (Quaternion ℝ)ˣ), ∀ (z : ℂ), g z = ↑w * f z * ↑w⁻¹

Noncentral Skolem-Noether for ℂ ⊆ ℍ[ℝ]: any two ℝ-algebra maps ℂ →ₐ[ℝ] ℍ[ℝ] are conjugate by a unit of ℍ[ℝ]. The source ℂ is simple but not central over ℝ, so TauCeti.skolemNoether does not apply and the conjugating unit is produced directly, from the conjugacy of the square roots of -1.

theorem TauCeti.Quaternion.ofComplex_conjAe (z : ℂ) : Quaternion.ofComplex (Complex.conjAe z) = ↑jUnit * Quaternion.ofComplex z * ↑jUnit⁻¹

Complex conjugation on ℂ ⊆ ℍ[ℝ] is conjugation by j, the roadmap's statement, with the explicit witness in place of the existential of TauCeti.Quaternion.exists_unit_conj_complexAlgHom.