noncomputable instance instModuleRealEndQuaternion_brauerGroup : Module ℝ (Module.End ℝ (Quaternion ℝ))

Equations

• instModuleRealEndQuaternion_brauerGroup = inferInstance

noncomputable instance instAlgebraRealEndQuaternion_brauerGroup : Algebra ℝ (Module.End ℝ (Quaternion ℝ))

Equations

• instAlgebraRealEndQuaternion_brauerGroup = inferInstance

@[reducible, inline]

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

Equations

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

@[reducible, inline]

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

Equations

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

@[reducible, inline]

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

Equations

• toEnd_map = TensorProduct.lift { toFun := fun (q1 : Quaternion ℝ) => toEnd_map_aux' q1, map_add' := toEnd_map.proof_2, map_smul' := toEnd_map.proof_3 }

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

@[reducible, inline]

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

Equations

• toEnd = { toFun := ⇑toEnd_map, map_one' := toEnd.proof_1, map_mul' := toEnd_map.map_mul, map_zero' := toEnd.proof_2, map_add' := toEnd.proof_3, commutes' := toEnd.proof_4 }

instance instIsCentralRealQuaternion_brauerGroup : Algebra.IsCentral ℝ (Quaternion ℝ)

instance instIsSimpleRingTensorProductRealQuaternion_brauerGroup : IsSimpleRing (TensorProduct ℝ (Quaternion ℝ) (Quaternion ℝ))

theorem toEnd_bij : Function.Bijective ⇑toEnd

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

Equations

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

theorem QuaternionTensorEquivOne : IsBrauerEquivalent (CSA.mk (TensorProduct ℝ (Quaternion ℝ) (Quaternion ℝ))) (CSA.mk ℝ)

theorem QuaternionNotEquivR : ¬IsBrauerEquivalent (CSA.mk (Quaternion ℝ)) (CSA.mk ℝ)

theorem BrauerOverR (A : CSA ℝ) : IsBrauerEquivalent A (CSA.mk ℝ) ∨ IsBrauerEquivalent A (CSA.mk (Quaternion ℝ))

@[reducible, inline]

noncomputable abbrev toC2 : Additive BrauerGroup.BrGroup →+ ZMod 2

Equations

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

@[reducible, inline]

noncomputable abbrev C2toBrauerOverR : ZMod 2 →+ Additive BrauerGroup.BrGroup

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.BrGroup ≃+ ZMod 2

Equations

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