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 f {D : Type} [DivisionRing D] [Algebra ℝ D] [hD' : IsSimpleRing D] (k : SubField ℝ D) (e : ↥k ≃ₐ[ℝ] ℂ) : ↥k →ₐ[ℝ] ↥k

Equations

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

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

@[simp]

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

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

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

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

theorem x2_comm_k {D : Type} [DivisionRing D] [Algebra ℝ D] [hD' : IsSimpleRing 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 xsq_ink {D : Type} [DivisionRing D] [Algebra ℝ D] [hD : Algebra.IsCentral ℝ D] [hD' : IsSimpleRing D] (k : SubField ℝ D) (e : ↥k ≃ₐ[ℝ] ℂ) [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 indep' {D : Type} [DivisionRing D] [Algebra ℝ D] [hD : Algebra.IsCentral ℝ D] [hD' : IsSimpleRing D] (k : SubField ℝ D) (e : ↥k ≃ₐ[ℝ] ℂ) [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 IsBasis {D : Type} [DivisionRing D] [Algebra ℝ D] [hD : Algebra.IsCentral ℝ D] [hD' : IsSimpleRing D] (k : SubField ℝ D) (e : ↥k ≃ₐ[ℝ] ℂ) [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) : Basis (Fin (Nat.succ 0).succ) ℝ ↥k

Equations

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

@[simp]

theorem IsBasis0 {D : Type} [DivisionRing D] [Algebra ℝ D] [hD : Algebra.IsCentral ℝ D] [hD' : IsSimpleRing D] (k : SubField ℝ D) (e : ↥k ≃ₐ[ℝ] ℂ) [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

@[simp]

theorem IsBasis1 {D : Type} [DivisionRing D] [Algebra ℝ D] [hD : Algebra.IsCentral ℝ D] [hD' : IsSimpleRing D] (k : SubField ℝ D) (e : ↥k ≃ₐ[ℝ] ℂ) [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 x2_is_real {D : Type} [DivisionRing D] [Algebra ℝ D] [hD : Algebra.IsCentral ℝ D] [hD' : IsSimpleRing D] (k : SubField ℝ D) (e : ↥k ≃ₐ[ℝ] ℂ) [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 V {D : Type} [DivisionRing D] [Algebra ℝ D] : Set D

Equations

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

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

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

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

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

theorem j_mul_j {D : Type} [DivisionRing D] [Algebra ℝ D] [hD : Algebra.IsCentral ℝ D] [hD' : IsSimpleRing D] (k : SubField ℝ D) (e : ↥k ≃ₐ[ℝ] ℂ) [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 jij_eq_negi {D : Type} [DivisionRing D] [Algebra ℝ D] [hD : Algebra.IsCentral ℝ D] [hD' : IsSimpleRing D] (k : SubField ℝ D) (e : ↥k ≃ₐ[ℝ] ℂ) [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 k_sq_eq_negone {D : Type} [DivisionRing D] [Algebra ℝ D] [hD : Algebra.IsCentral ℝ D] [hD' : IsSimpleRing D] (k : SubField ℝ D) (e : ↥k ≃ₐ[ℝ] ℂ) [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 i_mul_i {D : Type} [DivisionRing D] [Algebra ℝ D] [hD' : IsSimpleRing D] (k : SubField ℝ D) (e : ↥k ≃ₐ[ℝ] ℂ) : ↑(e.symm { re := 0, im := 1 }) * ↑(e.symm { re := 0, im := 1 }) = -1 • 1

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

theorem j_ne_zero {D : Type} [DivisionRing D] [Algebra ℝ D] [hD : Algebra.IsCentral ℝ D] [hD' : IsSimpleRing D] (k : SubField ℝ D) (e : ↥k ≃ₐ[ℝ] ℂ) [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 k_ne_zero {D : Type} [DivisionRing D] [Algebra ℝ D] [hD : Algebra.IsCentral ℝ D] [hD' : IsSimpleRing D] (k : SubField ℝ D) (e : ↥k ≃ₐ[ℝ] ℂ) [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 j_mul_i_eq_neg_i_mul_j {D : Type} [DivisionRing D] [Algebra ℝ D] [hD : Algebra.IsCentral ℝ D] [hD' : IsSimpleRing D] (k : SubField ℝ D) (e : ↥k ≃ₐ[ℝ] ℂ) [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 toFun {D : Type} [DivisionRing D] [Algebra ℝ D] [hD : Algebra.IsCentral ℝ D] [hD' : IsSimpleRing D] (k : SubField ℝ D) (e : ↥k ≃ₐ[ℝ] ℂ) [FiniteDimensional ℝ D] (x : Dˣ) (hx : ∀ (z : ↥k), (↑x)⁻¹ * ↑((f k e) z) * ↑x = k.val z) (hDD : Module.finrank ℝ D = 4) : Quaternion ℝ →ₐ[ℝ] D

Equations

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

@[reducible, inline]

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

Equations

• basisijk k e x hx hDD = Fin.cons (↑(e.symm { re := 0, im := 1 }) * ((algebraMap ℝ D) (√⋯.choose)⁻¹ * ↑x)) (Fin.cons ((algebraMap ℝ D) (√⋯.choose)⁻¹ * ↑x) ![1, ↑(e.symm { re := 0, im := 1 })])

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

theorem linindep1ij {D : Type} [DivisionRing D] [Algebra ℝ D] [hD : Algebra.IsCentral ℝ D] [hD' : IsSimpleRing D] (k : SubField ℝ D) (e : ↥k ≃ₐ[ℝ] ℂ) [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 linindepijk {D : Type} [DivisionRing D] [Algebra ℝ D] [hD : Algebra.IsCentral ℝ D] [hD' : IsSimpleRing D] (k : SubField ℝ D) (e : ↥k ≃ₐ[ℝ] ℂ) [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 isBasisijk {D : Type} [DivisionRing D] [Algebra ℝ D] [hD : Algebra.IsCentral ℝ D] [hD' : IsSimpleRing D] (k : SubField ℝ D) (e : ↥k ≃ₐ[ℝ] ℂ) [FiniteDimensional ℝ D] (x : Dˣ) (hx : ∀ (z : ↥k), (↑x)⁻¹ * ↑((f k e) z) * ↑x = k.val z) (h : Module.finrank ℝ D = 4) : Basis (Fin 4) ℝ D

Equations

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

@[reducible, inline]

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

Equations

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

theorem toFun_i_eq {D : Type} [DivisionRing D] [Algebra ℝ D] [hD : Algebra.IsCentral ℝ D] [hD' : IsSimpleRing D] (k : SubField ℝ D) (e : ↥k ≃ₐ[ℝ] ℂ) [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) (-1)) 1) = ↑(e.symm { re := 0, im := 1 })

@[simp]

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

theorem linEquivH_eq_toFun {D : Type} [DivisionRing D] [Algebra ℝ D] [hD : Algebra.IsCentral ℝ D] [hD' : IsSimpleRing D] (k : SubField ℝ D) (e : ↥k ≃ₐ[ℝ] ℂ) [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 bij_tofun {D : Type} [DivisionRing D] [Algebra ℝ D] [hD : Algebra.IsCentral ℝ D] [hD' : IsSimpleRing D] (k : SubField ℝ D) (e : ↥k ≃ₐ[ℝ] ℂ) [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 rank4_iso_H {D : Type} [DivisionRing D] [Algebra ℝ D] [hD : Algebra.IsCentral ℝ D] [hD' : IsSimpleRing D] (k : SubField ℝ D) (e : ↥k ≃ₐ[ℝ] ℂ) [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 SmulCA (A : Type) [DivisionRing A] [Algebra ℝ A] [FiniteDimensional ℝ A] (e : ℂ ≃ₐ[ℝ] ↥(Subalgebra.center ℝ A)) : ℂ →+* A

Equations

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

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

Equations

• AlgCA A e = Algebra.mk (SmulCA A e) ⋯ ⋯

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

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

@[reducible, inline]

noncomputable abbrev iSup_chain_subfield (D : Type) [DivisionRing D] [Algebra ℝ D] (α : Set (SubField ℝ D)) [Nonempty ↑α] (hα : IsChain (fun (x1 x2 : SubField ℝ D) => x1 ≤ x2) α) : SubField ℝ D

Equations

• iSup_chain_subfield D α hα = { toSubalgebra := ⨆ (L : ↑α), (↑L).toSubalgebra, mul_comm := ⋯, inverse := ⋯ }

theorem exitsmaxsub (D : Type) [DivisionRing D] [Algebra ℝ D] : ∃ (L : SubField ℝ D), IsMaximalSubfield ℝ D L

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