LeanPool.BrauerGroupNew.BrauerOverR

Imported Lean Pool material for LeanPool.BrauerGroupNew.BrauerOverR.

@[reducible, inline]

noncomputable abbrev toEndMapAux (q1 q2 : Quaternion ℝ) : Module.End ℝ (Quaternion ℝ)

Left multiplication by q1 and right multiplication by star q2 as a real-linear endomorphism.

Equations

• toEndMapAux q1 q2 = { toFun := fun (x : Quaternion ℝ) => q1 * x * star q2, map_add' := ⋯, map_smul' := ⋯ }

@[reducible, inline]

noncomputable abbrev toEndMapAux' (q1 : Quaternion ℝ) : Quaternion ℝ →ₗ[ℝ] Module.End ℝ (Quaternion ℝ)

The second argument of toEndMapAux packaged as a real-linear map to endomorphisms.

Equations

• toEndMapAux' q1 = { toFun := fun (q2 : Quaternion ℝ) => toEndMapAux q1 q2, map_add' := ⋯, map_smul' := ⋯ }

@[reducible, inline]

noncomputable abbrev toEndMap : TensorProduct ℝ (Quaternion ℝ) (Quaternion ℝ) →ₗ[ℝ] Module.End ℝ (Quaternion ℝ)

The real-linear map ℍ ⊗ ℍ → End_R(ℍ) induced by two-sided quaternion multiplication.

Equations

• toEndMap = TensorProduct.lift { toFun := fun (q1 : Quaternion ℝ) => toEndMapAux' q1, map_add' := ⋯, map_smul' := ⋯ }

theorem toEndMap.map_mul (x1 x2 : TensorProduct ℝ (Quaternion ℝ) (Quaternion ℝ)) : toEndMap (x1 * x2) = toEndMap x1 * toEndMap x2

@[reducible, inline]

noncomputable abbrev toEnd : TensorProduct ℝ (Quaternion ℝ) (Quaternion ℝ) →ₐ[ℝ] Module.End ℝ (Quaternion ℝ)

The algebra homomorphism ℍ ⊗ ℍ → End_R(ℍ) from two-sided quaternion multiplication.

Equations

• toEnd = { toFun := ⇑toEndMap, map_one' := toEnd._proof_1, map_mul' := toEndMap.map_mul, map_zero' := toEnd._proof_5, map_add' := toEnd._proof_6, commutes' := ⋯ }

instance instIsCentralRealQuaternion_leanPool : Algebra.IsCentral ℝ (Quaternion ℝ)

theorem toEnd_bij : Function.Bijective ⇑toEnd

noncomputable def QuaternionTensorEquivMatrix : TensorProduct ℝ (Quaternion ℝ) (Quaternion ℝ) ≃ₐ[ℝ] Matrix (Fin 4) (Fin 4) ℝ

The tensor square of Hamilton's quaternions is equivalent to 4 × 4 real matrices.

Equations

• QuaternionTensorEquivMatrix = (AlgEquiv.ofBijective toEnd toEnd_bij).trans (algEquivMatrix (QuaternionAlgebra.basisOneIJK (-1) 0 (-1)))

theorem QuaternionTensorEquivOne : IsBrauerEquivalent { toAlgCat := ↧(TensorProduct ℝ (Quaternion ℝ) (Quaternion ℝ)), isCentral := ⋯, isSimple := ⋯, fin_dim := ⋯ } { toAlgCat := ↧ℝ, isCentral := ⋯, isSimple := ⋯, fin_dim := ⋯ }

theorem QuaternionNotEquivR : ¬IsBrauerEquivalent { toAlgCat := ↧(Quaternion ℝ), isCentral := instIsCentralRealQuaternion_leanPool, isSimple := ⋯, fin_dim := ⋯ } { toAlgCat := ↧ℝ, isCentral := ⋯, isSimple := ⋯, fin_dim := ⋯ }

theorem BrauerOverR (A : CSA ℝ) : IsBrauerEquivalent A { toAlgCat := ↧ℝ, isCentral := ⋯, isSimple := ⋯, fin_dim := ⋯ } ∨ IsBrauerEquivalent A { toAlgCat := ↧(Quaternion ℝ), isCentral := instIsCentralRealQuaternion_leanPool, isSimple := ⋯, fin_dim := ⋯ }

@[reducible, inline]

noncomputable abbrev toC2 : Additive (BrauerGroup ℝ) →+ ZMod 2

Classifies a real Brauer class as split or quaternionic, giving an element of ZMod 2.

Equations

• toC2 = { toFun := Quotient.lift (fun (A : CSA ℝ) => if h1 : IsBrauerEquivalent A BrauerGroup.oneIn' then 0 else 1) ⋯, map_zero' := toC2._proof_6, map_add' := ⋯ }

@[reducible, inline]

noncomputable abbrev C2toBrauerOverR : ZMod 2 →+ Additive (BrauerGroup ℝ)

Sends 0 to the split Brauer class and 1 to Hamilton's quaternion class.

Equations

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

theorem toC2.left_inv : Function.LeftInverse ⇑C2toBrauerOverR ⇑toC2

theorem toC2.right_inv : Function.RightInverse ⇑C2toBrauerOverR ⇑toC2

noncomputable def BrauerGroupOverR : Additive (BrauerGroup ℝ) ≃+ ZMod 2

The real Brauer group is the cyclic group of order two, generated by Hamilton's quaternions.

Equations

• BrauerGroupOverR = { toFun := ⇑toC2, invFun := ⇑C2toBrauerOverR, left_inv := toC2.left_inv, right_inv := toC2.right_inv, map_add' := BrauerGroupOverR._proof_1 }