LeanPool.BrauerGroupNew.FrobeniusTheorem

Imported Lean Pool material for LeanPool.BrauerGroupNew.FrobeniusTheorem.

theorem rank_1_D_iso_R {D : Type} [DivisionRing D] [Algebra ℝ D] : Module.finrank ℝ D = 1 → Nonempty (D ≃ₐ[ℝ] ℝ)

theorem RealExtension_is_RorC (K : Type) [Field K] [Algebra ℝ K] [FiniteDimensional ℝ K] : Nonempty (K ≃ₐ[ℝ] ℝ) ∨ Nonempty (K ≃ₐ[ℝ] ℂ)

@[reducible, inline]

noncomputable abbrev BrauerGroupNew.f {D : Type} [DivisionRing D] [Algebra ℝ D] (k : SubField ℝ D) (e : ↥k ≃ₐ[ℝ] ℂ) : ↥k →ₐ[ℝ] ↥k

The conjugation automorphism of a maximal subfield identified with ℂ.

Equations

• BrauerGroupNew.f k e = { toFun := fun (kk : ↥k) => e.symm ((starRingEnd ℂ) (e kk)), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯, commutes' := ⋯ }

theorem BrauerGroupNew.f_injective {D : Type} [DivisionRing D] [Algebra ℝ D] (k : SubField ℝ D) (e : ↥k ≃ₐ[ℝ] ℂ) : Function.Injective ⇑(f k e)

@[simp]

theorem BrauerGroupNew.f_apply {D : Type} [DivisionRing D] [Algebra ℝ D] (k : SubField ℝ D) (e : ↥k ≃ₐ[ℝ] ℂ) (x : ↥k) : (f k e) x = e.symm ((starRingEnd ℂ) (e x))

theorem BrauerGroupNew.f_apply_apply {D : Type} [DivisionRing D] [Algebra ℝ D] (k : SubField ℝ D) (e : ↥k ≃ₐ[ℝ] ℂ) (z : ℂ) : (f k e) (e.symm z) = e.symm ((starRingEnd ℂ) z)

theorem BrauerGroupNew.linindep_one_xsq {D : Type} [DivisionRing D] [Algebra ℝ D] (x : Dˣ) (hxx : ↑x ^ 2 ∉ Subalgebra.center ℝ D) : LinearIndependent ℝ ![1, ↑x ^ 2]

theorem BrauerGroupNew.x2_comm_k {D : Type} [DivisionRing D] [Algebra ℝ D] (k : SubField ℝ D) (e : ↥k ≃ₐ[ℝ] ℂ) (x : Dˣ) (hx : ∀ (z : ↥k), (↑x)⁻¹ * ↑((f k e) z) * ↑x = k.val z) (y : ↥k) : ↑x ^ 2 * k.val y = k.val y * ↑x ^ 2

theorem BrauerGroupNew.i_mul_i {D : Type} [DivisionRing D] [Algebra ℝ D] (k : SubField ℝ D) (e : ↥k ≃ₐ[ℝ] ℂ) : ↑(e.symm { re := 0, im := 1 }) * ↑(e.symm { re := 0, im := 1 }) = -1 • 1

theorem BrauerGroupNew.i_ne_zero {D : Type} [DivisionRing D] [Algebra ℝ D] (k : SubField ℝ D) (e : ↥k ≃ₐ[ℝ] ℂ) : ↑(e.symm { re := 0, im := 1 }) ≠ 0

theorem BrauerGroupNew.linindep1i {D : Type} [DivisionRing D] [Algebra ℝ D] (k : SubField ℝ D) (e : ↥k ≃ₐ[ℝ] ℂ) : LinearIndependent ℝ ![1, ↑(e.symm { re := 0, im := 1 })]

theorem BrauerGroupNew.f_is_conjugation {D : Type} [DivisionRing D] [hD' : IsSimpleRing D] [Algebra ℝ D] (k : SubField ℝ D) (e : ↥k ≃ₐ[ℝ] ℂ) [Algebra.IsCentral ℝ D] [FiniteDimensional ℝ D] : ∃ (x : Dˣ), ∀ (z : ↥k), (↑x)⁻¹ * ↑((f k e) z) * ↑x = k.val z

theorem BrauerGroupNew.xsq_ink {D : Type} [DivisionRing D] [hD' : IsSimpleRing D] [Algebra ℝ D] (k : SubField ℝ D) (e : ↥k ≃ₐ[ℝ] ℂ) [Algebra.IsCentral ℝ D] [FiniteDimensional ℝ D] (x : Dˣ) (hx : ∀ (z : ↥k), (↑x)⁻¹ * ↑((f k e) z) * ↑x = k.val z) (hDD : Module.finrank ℝ D = 4) : ↑x ^ 2 ∈ k

theorem BrauerGroupNew.indep' {D : Type} [DivisionRing D] [hD' : IsSimpleRing D] [Algebra ℝ D] (k : SubField ℝ D) (e : ↥k ≃ₐ[ℝ] ℂ) [Algebra.IsCentral ℝ D] [FiniteDimensional ℝ D] (x : Dˣ) (hx : ∀ (z : ↥k), (↑x)⁻¹ * ↑((f k e) z) * ↑x = k.val z) (hDD : Module.finrank ℝ D = 4) (hxx : ↑x ^ 2 ∉ Subalgebra.center ℝ D) : LinearIndependent ℝ ![1, ⟨↑x ^ 2, ⋯⟩]

@[reducible, inline]

noncomputable abbrev BrauerGroupNew.IsBasis {D : Type} [DivisionRing D] [hD' : IsSimpleRing D] [Algebra ℝ D] (k : SubField ℝ D) (e : ↥k ≃ₐ[ℝ] ℂ) [Algebra.IsCentral ℝ D] [FiniteDimensional ℝ D] (x : Dˣ) (hx : ∀ (z : ↥k), (↑x)⁻¹ * ↑((f k e) z) * ↑x = k.val z) (hDD : Module.finrank ℝ D = 4) (hxx : ↑x ^ 2 ∉ Subalgebra.center ℝ D) : Module.Basis (Fin (Nat.succ 0).succ) ℝ ↥k

The two-element basis of a maximal subfield generated by 1 and x ^ 2.

Equations

• BrauerGroupNew.IsBasis k e x hx hDD hxx = Module.Basis.mk ⋯ ⋯

theorem BrauerGroupNew.IsBasis0 {D : Type} [DivisionRing D] [hD' : IsSimpleRing D] [Algebra ℝ D] (k : SubField ℝ D) (e : ↥k ≃ₐ[ℝ] ℂ) [Algebra.IsCentral ℝ D] [FiniteDimensional ℝ D] (x : Dˣ) (hx : ∀ (z : ↥k), (↑x)⁻¹ * ↑((f k e) z) * ↑x = k.val z) (hDD : Module.finrank ℝ D = 4) (hxx : ↑x ^ 2 ∉ Subalgebra.center ℝ D) : (IsBasis k e x hx hDD hxx) 0 = 1

theorem BrauerGroupNew.IsBasis1 {D : Type} [DivisionRing D] [hD' : IsSimpleRing D] [Algebra ℝ D] (k : SubField ℝ D) (e : ↥k ≃ₐ[ℝ] ℂ) [Algebra.IsCentral ℝ D] [FiniteDimensional ℝ D] (x : Dˣ) (hx : ∀ (z : ↥k), (↑x)⁻¹ * ↑((f k e) z) * ↑x = k.val z) (hDD : Module.finrank ℝ D = 4) (hxx : ↑x ^ 2 ∉ Subalgebra.center ℝ D) : (IsBasis k e x hx hDD hxx) 1 = ⟨↑x ^ 2, ⋯⟩

theorem BrauerGroupNew.x2_is_real {D : Type} [DivisionRing D] [hD' : IsSimpleRing D] [Algebra ℝ D] (k : SubField ℝ D) (e : ↥k ≃ₐ[ℝ] ℂ) [Algebra.IsCentral ℝ D] [FiniteDimensional ℝ D] (x : Dˣ) (hx : ∀ (z : ↥k), (↑x)⁻¹ * ↑((f k e) z) * ↑x = k.val z) (hDD : Module.finrank ℝ D = 4) : ↑x ^ 2 ∈ (algebraMap ℝ D).range

@[reducible, inline]

noncomputable abbrev BrauerGroupNew.V {D : Type} [DivisionRing D] [Algebra ℝ D] : Set D

The set of elements whose square is a negative real scalar.

Equations

• BrauerGroupNew.V = {x : D | ∃ r < 0, x ^ 2 = ↑r}

theorem BrauerGroupNew.V_def {D : Type} [DivisionRing D] [Algebra ℝ D] (x : D) : x ∈ V ↔ ∃ r < 0, x ^ 2 = (algebraMap ℝ D) r

theorem BrauerGroupNew.real_sq_in_R_or_V {D : Type} [DivisionRing D] [Algebra ℝ D] (x : D) : x ^ 2 ∈ (algebraMap ℝ D).range → x ∈ (algebraMap ℝ D).range ∨ x ∈ V

theorem BrauerGroupNew.x_is_in_V {D : Type} [DivisionRing D] [hD' : IsSimpleRing D] [Algebra ℝ D] (k : SubField ℝ D) (e : ↥k ≃ₐ[ℝ] ℂ) [Algebra.IsCentral ℝ D] [FiniteDimensional ℝ D] (x : Dˣ) (hx : ∀ (z : ↥k), (↑x)⁻¹ * ↑((f k e) z) * ↑x = k.val z) (hDD : Module.finrank ℝ D = 4) : ↑x ∈ V

theorem BrauerGroupNew.x_corre_R {D : Type} [DivisionRing D] [hD' : IsSimpleRing D] [Algebra ℝ D] (k : SubField ℝ D) (e : ↥k ≃ₐ[ℝ] ℂ) [Algebra.IsCentral ℝ D] [FiniteDimensional ℝ D] (x : Dˣ) (hx : ∀ (z : ↥k), (↑x)⁻¹ * ↑((f k e) z) * ↑x = k.val z) (hDD : Module.finrank ℝ D = 4) : ∃ (r : ℝ), (algebraMap ℝ D) r = -↑x ^ 2

theorem BrauerGroupNew.r_pos {D : Type} [DivisionRing D] [hD' : IsSimpleRing D] [Algebra ℝ D] (k : SubField ℝ D) (e : ↥k ≃ₐ[ℝ] ℂ) [Algebra.IsCentral ℝ D] [FiniteDimensional ℝ D] (x : Dˣ) (hx : ∀ (z : ↥k), (↑x)⁻¹ * ↑((f k e) z) * ↑x = k.val z) (hDD : Module.finrank ℝ D = 4) : 0 < ⋯.choose

theorem BrauerGroupNew.j_mul_j {D : Type} [DivisionRing D] [hD' : IsSimpleRing D] [Algebra ℝ D] (k : SubField ℝ D) (e : ↥k ≃ₐ[ℝ] ℂ) [Algebra.IsCentral ℝ D] [FiniteDimensional ℝ D] (x : Dˣ) (hx : ∀ (z : ↥k), (↑x)⁻¹ * ↑((f k e) z) * ↑x = k.val z) (hDD : Module.finrank ℝ D = 4) : (algebraMap ℝ D) (√⋯.choose)⁻¹ * ↑x * ((algebraMap ℝ D) (√⋯.choose)⁻¹ * ↑x) = -1 • 1

theorem BrauerGroupNew.jij_eq_negi {D : Type} [DivisionRing D] [hD' : IsSimpleRing D] [Algebra ℝ D] (k : SubField ℝ D) (e : ↥k ≃ₐ[ℝ] ℂ) [Algebra.IsCentral ℝ D] [FiniteDimensional ℝ D] (x : Dˣ) (hx : ∀ (z : ↥k), (↑x)⁻¹ * ↑((f k e) z) * ↑x = k.val z) (hDD : Module.finrank ℝ D = 4) : (algebraMap ℝ D) (√⋯.choose)⁻¹ * ↑x * ↑(e.symm { re := 0, im := 1 }) * ((algebraMap ℝ D) (√⋯.choose)⁻¹ * ↑x)⁻¹ = -↑(e.symm { re := 0, im := 1 })

theorem BrauerGroupNew.k_sq_eq_negone {D : Type} [DivisionRing D] [hD' : IsSimpleRing D] [Algebra ℝ D] (k : SubField ℝ D) (e : ↥k ≃ₐ[ℝ] ℂ) [Algebra.IsCentral ℝ D] [FiniteDimensional ℝ D] (x : Dˣ) (hx : ∀ (z : ↥k), (↑x)⁻¹ * ↑((f k e) z) * ↑x = k.val z) (hDD : Module.finrank ℝ D = 4) : (↑(e.symm { re := 0, im := 1 }) * ((algebraMap ℝ D) (√⋯.choose)⁻¹ * ↑x)) ^ 2 = -1

theorem BrauerGroupNew.j_ne_zero {D : Type} [DivisionRing D] [hD' : IsSimpleRing D] [Algebra ℝ D] (k : SubField ℝ D) (e : ↥k ≃ₐ[ℝ] ℂ) [Algebra.IsCentral ℝ D] [FiniteDimensional ℝ D] (x : Dˣ) (hx : ∀ (z : ↥k), (↑x)⁻¹ * ↑((f k e) z) * ↑x = k.val z) (hDD : Module.finrank ℝ D = 4) : (algebraMap ℝ D) (√⋯.choose)⁻¹ * ↑x ≠ 0

theorem BrauerGroupNew.k_ne_zero {D : Type} [DivisionRing D] [hD' : IsSimpleRing D] [Algebra ℝ D] (k : SubField ℝ D) (e : ↥k ≃ₐ[ℝ] ℂ) [Algebra.IsCentral ℝ D] [FiniteDimensional ℝ D] (x : Dˣ) (hx : ∀ (z : ↥k), (↑x)⁻¹ * ↑((f k e) z) * ↑x = k.val z) (hDD : Module.finrank ℝ D = 4) : ↑(e.symm { re := 0, im := 1 }) * ((algebraMap ℝ D) (√⋯.choose)⁻¹ * ↑x) ≠ 0

theorem BrauerGroupNew.j_mul_i_eq_neg_i_mul_j {D : Type} [DivisionRing D] [hD' : IsSimpleRing D] [Algebra ℝ D] (k : SubField ℝ D) (e : ↥k ≃ₐ[ℝ] ℂ) [Algebra.IsCentral ℝ D] [FiniteDimensional ℝ D] (x : Dˣ) (hx : ∀ (z : ↥k), (↑x)⁻¹ * ↑((f k e) z) * ↑x = k.val z) (hDD : Module.finrank ℝ D = 4) : (algebraMap ℝ D) (√⋯.choose)⁻¹ * ↑x * ↑(e.symm { re := 0, im := 1 }) = -(↑(e.symm { re := 0, im := 1 }) * ((algebraMap ℝ D) (√⋯.choose)⁻¹ * ↑x))

@[reducible, inline]

noncomputable abbrev BrauerGroupNew.quatBasis {D : Type} [DivisionRing D] [hD' : IsSimpleRing D] [Algebra ℝ D] (k : SubField ℝ D) (e : ↥k ≃ₐ[ℝ] ℂ) [Algebra.IsCentral ℝ D] [FiniteDimensional ℝ D] (x : Dˣ) (hx : ∀ (z : ↥k), (↑x)⁻¹ * ↑((f k e) z) * ↑x = k.val z) (hDD : Module.finrank ℝ D = 4) : QuaternionAlgebra.Basis D (-1) 0 (-1)

The quaternion basis inside D determined by the constructed elements.

Equations

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

@[reducible, inline]

noncomputable abbrev BrauerGroupNew.toFun {D : Type} [DivisionRing D] [hD' : IsSimpleRing D] [Algebra ℝ D] (k : SubField ℝ D) (e : ↥k ≃ₐ[ℝ] ℂ) [Algebra.IsCentral ℝ D] [FiniteDimensional ℝ D] (x : Dˣ) (hx : ∀ (z : ↥k), (↑x)⁻¹ * ↑((f k e) z) * ↑x = k.val z) (hDD : Module.finrank ℝ D = 4) : Quaternion ℝ →ₐ[ℝ] D

The algebra homomorphism from Hamilton quaternions determined by the constructed basis.

Equations

• BrauerGroupNew.toFun k e x hx hDD = QuaternionAlgebra.lift (BrauerGroupNew.quatBasis k e x hx hDD)

@[reducible, inline]

noncomputable abbrev BrauerGroupNew.basisijk {D : Type} [DivisionRing D] [hD' : IsSimpleRing D] [Algebra ℝ D] (k : SubField ℝ D) (e : ↥k ≃ₐ[ℝ] ℂ) [Algebra.IsCentral ℝ D] [FiniteDimensional ℝ D] (x : Dˣ) (hx : ∀ (z : ↥k), (↑x)⁻¹ * ↑((f k e) z) * ↑x = k.val z) (hDD : Module.finrank ℝ D = 4) : Fin 4 → D

The ordered quaternion basis k, j, 1, i inside the division algebra.

Equations

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

theorem BrauerGroupNew.linindep1ij {D : Type} [DivisionRing D] [hD' : IsSimpleRing D] [Algebra ℝ D] (k : SubField ℝ D) (e : ↥k ≃ₐ[ℝ] ℂ) [Algebra.IsCentral ℝ D] [FiniteDimensional ℝ D] (x : Dˣ) (hx : ∀ (z : ↥k), (↑x)⁻¹ * ↑((f k e) z) * ↑x = k.val z) (hDD : Module.finrank ℝ D = 4) : LinearIndependent ℝ (Fin.cons ((algebraMap ℝ D) (√⋯.choose)⁻¹ * ↑x) ![1, ↑(e.symm { re := 0, im := 1 })])

theorem BrauerGroupNew.linindepijk {D : Type} [DivisionRing D] [hD' : IsSimpleRing D] [Algebra ℝ D] (k : SubField ℝ D) (e : ↥k ≃ₐ[ℝ] ℂ) [Algebra.IsCentral ℝ D] [FiniteDimensional ℝ D] (x : Dˣ) (hx : ∀ (z : ↥k), (↑x)⁻¹ * ↑((f k e) z) * ↑x = k.val z) (hDD : Module.finrank ℝ D = 4) : LinearIndependent ℝ (basisijk k e x hx hDD)

@[reducible, inline]

noncomputable abbrev BrauerGroupNew.isBasisijk {D : Type} [DivisionRing D] [hD' : IsSimpleRing D] [Algebra ℝ D] (k : SubField ℝ D) (e : ↥k ≃ₐ[ℝ] ℂ) [Algebra.IsCentral ℝ D] [FiniteDimensional ℝ D] (x : Dˣ) (hx : ∀ (z : ↥k), (↑x)⁻¹ * ↑((f k e) z) * ↑x = k.val z) (h : Module.finrank ℝ D = 4) : Module.Basis (Fin 4) ℝ D

The constructed ℝ-basis of a four-dimensional central real division algebra.

Equations

• BrauerGroupNew.isBasisijk k e x hx h = Module.Basis.mk ⋯ ⋯

@[reducible, inline]

noncomputable abbrev BrauerGroupNew.linEquivH {D : Type} [DivisionRing D] [hD' : IsSimpleRing D] [Algebra ℝ D] (k : SubField ℝ D) (e : ↥k ≃ₐ[ℝ] ℂ) [Algebra.IsCentral ℝ D] [FiniteDimensional ℝ D] (x : Dˣ) (hx : ∀ (z : ↥k), (↑x)⁻¹ * ↑((f k e) z) * ↑x = k.val z) (h : Module.finrank ℝ D = 4) : Quaternion ℝ ≃ₗ[ℝ] D

The linear equivalence from Hamilton quaternions to the constructed basis.

Equations

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

theorem BrauerGroupNew.toFun_i_eq {D : Type} [DivisionRing D] [hD' : IsSimpleRing D] [Algebra ℝ D] (k : SubField ℝ D) (e : ↥k ≃ₐ[ℝ] ℂ) [Algebra.IsCentral ℝ D] [FiniteDimensional ℝ D] (x : Dˣ) (hx : ∀ (z : ↥k), (↑x)⁻¹ * ↑((f k e) z) * ↑x = k.val z) (h : Module.finrank ℝ D = 4) : (toFun k e x hx h) ((QuaternionAlgebra.basisOneIJK (-1) 0 (-1)) 1) = ↑(e.symm { re := 0, im := 1 })

theorem BrauerGroupNew.toFun_one_eq {D : Type} [DivisionRing D] [hD' : IsSimpleRing D] [Algebra ℝ D] (k : SubField ℝ D) (e : ↥k ≃ₐ[ℝ] ℂ) [Algebra.IsCentral ℝ D] [FiniteDimensional ℝ D] (x : Dˣ) (hx : ∀ (z : ↥k), (↑x)⁻¹ * ↑((f k e) z) * ↑x = k.val z) (h : Module.finrank ℝ D = 4) : (toFun k e x hx h) ((QuaternionAlgebra.basisOneIJK (-1) 0 (-1)) 0) = 1

theorem BrauerGroupNew.toFun_j_eq {D : Type} [DivisionRing D] [hD' : IsSimpleRing D] [Algebra ℝ D] (k : SubField ℝ D) (e : ↥k ≃ₐ[ℝ] ℂ) [Algebra.IsCentral ℝ D] [FiniteDimensional ℝ D] (x : Dˣ) (hx : ∀ (z : ↥k), (↑x)⁻¹ * ↑((f k e) z) * ↑x = k.val z) (h : Module.finrank ℝ D = 4) : (toFun k e x hx h) ((QuaternionAlgebra.basisOneIJK (-1) 0 (-1)) 2) = (algebraMap ℝ D) (√⋯.choose)⁻¹ * ↑x

theorem BrauerGroupNew.toFun_k_eq {D : Type} [DivisionRing D] [hD' : IsSimpleRing D] [Algebra ℝ D] (k : SubField ℝ D) (e : ↥k ≃ₐ[ℝ] ℂ) [Algebra.IsCentral ℝ D] [FiniteDimensional ℝ D] (x : Dˣ) (hx : ∀ (z : ↥k), (↑x)⁻¹ * ↑((f k e) z) * ↑x = k.val z) (h : Module.finrank ℝ D = 4) : (toFun k e x hx h) ((QuaternionAlgebra.basisOneIJK (-1) 0 (-1)) 3) = ↑(e.symm { re := 0, im := 1 }) * ((algebraMap ℝ D) (√⋯.choose)⁻¹ * ↑x)

@[simp]

theorem BrauerGroupNew.succ_two_eq_three (n : ℕ) : Fin.succ 2 = 3

theorem BrauerGroupNew.linEquivH_eq_toFun {D : Type} [DivisionRing D] [hD' : IsSimpleRing D] [Algebra ℝ D] (k : SubField ℝ D) (e : ↥k ≃ₐ[ℝ] ℂ) [Algebra.IsCentral ℝ D] [FiniteDimensional ℝ D] (x : Dˣ) (hx : ∀ (z : ↥k), (↑x)⁻¹ * ↑((f k e) z) * ↑x = k.val z) (h : Module.finrank ℝ D = 4) : ↑(linEquivH k e x hx h) = ↑(toFun k e x hx h)

theorem BrauerGroupNew.bij_tofun {D : Type} [DivisionRing D] [hD' : IsSimpleRing D] [Algebra ℝ D] (k : SubField ℝ D) (e : ↥k ≃ₐ[ℝ] ℂ) [Algebra.IsCentral ℝ D] [FiniteDimensional ℝ D] (x : Dˣ) (hx : ∀ (z : ↥k), (↑x)⁻¹ * ↑((f k e) z) * ↑x = k.val z) (h : Module.finrank ℝ D = 4) : Function.Bijective ⇑(toFun k e x hx h)

theorem BrauerGroupNew.rank4_iso_H {D : Type} [DivisionRing D] [hD' : IsSimpleRing D] [Algebra ℝ D] (k : SubField ℝ D) (e : ↥k ≃ₐ[ℝ] ℂ) [Algebra.IsCentral ℝ D] [FiniteDimensional ℝ D] (x : Dˣ) (hx : ∀ (z : ↥k), (↑x)⁻¹ * ↑((f k e) z) * ↑x = k.val z) (h : Module.finrank ℝ D = 4) : Nonempty (Quaternion ℝ ≃ₐ[ℝ] D)

@[reducible, inline]

noncomputable abbrev BrauerGroupNew.SmulCA (A : Type) [DivisionRing A] [Algebra ℝ A] (e : ℂ ≃ₐ[ℝ] ↥(Subalgebra.center ℝ A)) : ℂ →+* A

The complex scalar action induced by an isomorphism from ℂ to the center.

Equations

• BrauerGroupNew.SmulCA A e = { toFun := fun (z : ℂ) => ↑(e z), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

@[reducible, inline]

noncomputable abbrev BrauerGroupNew.AlgCA (A : Type) [DivisionRing A] [Algebra ℝ A] (e : ℂ ≃ₐ[ℝ] ↥(Subalgebra.center ℝ A)) : Algebra ℂ A

The resulting complex algebra structure on a real division algebra.

Equations

• BrauerGroupNew.AlgCA A e = { smul := fun (z : ℂ) (a : A) => (BrauerGroupNew.SmulCA A e) z * a, algebraMap := BrauerGroupNew.SmulCA A e, commutes' := ⋯, smul_def' := ⋯ }

theorem BrauerGroupNew.smulCRassoc (A : Type) [DivisionRing A] [Algebra ℝ A] (e : ℂ ≃ₐ[ℝ] ↥(Subalgebra.center ℝ A)) (r : ℝ) (z : ℂ) (a : A) : ↑(e (r • z)) * a = r • (↑(e z) * a)

theorem BrauerGroupNew.centereqvCisoC (A : Type) [DivisionRing A] [Algebra ℝ A] [FiniteDimensional ℝ A] (hA : Nonempty (↥(Subalgebra.center ℝ A) ≃ₐ[ℝ] ℂ)) : Nonempty (A ≃ₐ[ℝ] ℂ)

theorem BrauerGroupNew.center_eq_bot_of_iso_real (A : Type) [DivisionRing A] [Algebra ℝ A] [FiniteDimensional ℝ A] (hR : ↥(Subalgebra.center ℝ A) ≃ₐ[ℝ] ℝ) : Subalgebra.center ℝ A = ⊥

theorem BrauerGroupNew.subfield_finrank_one_or_two (A : Type) [DivisionRing A] [Algebra ℝ A] [FiniteDimensional ℝ A] (L : SubField ℝ A) : Module.finrank ℝ ↥L = 1 ∨ Module.finrank ℝ ↥L = 2

theorem BrauerGroupNew.not_real_subfield_of_finrank_two (A : Type) [DivisionRing A] [Algebra ℝ A] (L : SubField ℝ A) (h2 : Module.finrank ℝ ↥L = 2) (e1 : ↥L ≃ₐ[ℝ] ℝ) : False

theorem BrauerGroupNew.central_division_iso_real_or_quaternion (A : Type) [DivisionRing A] [Algebra ℝ A] [FiniteDimensional ℝ A] [Algebra.IsCentral ℝ A] : Nonempty (A ≃ₐ[ℝ] ℝ) ∨ Nonempty (A ≃ₐ[ℝ] Quaternion ℝ)

theorem BrauerGroupNew.FrobeniusTheorem (A : Type) [DivisionRing A] [Algebra ℝ A] [FiniteDimensional ℝ A] : Nonempty (A ≃ₐ[ℝ] ℂ) ∨ Nonempty (A ≃ₐ[ℝ] ℝ) ∨ Nonempty (A ≃ₐ[ℝ] Quaternion ℝ)