MAT3253 Complex Variables

1.5. Complex numbers have no ordering🔗

The complex numbers cannot be given a linear order that is compatible with its field structure.

Recall that a linear order is a total order that satisfies: for any a,b, either a ≤ b or b ≤ a.

A strict ordered ring is a ring that satisfies:

if a < b, then a + c < b + c for any c,
if a < b and c > 0, then ac < bc.

LinearOrder.{u_2} (α : Type u_2) : Type u_2#check LinearOrder
IsStrictOrderedRing.{u_1} (R : Type u_1) [Semiring R] [PartialOrder R] : Prop#check IsStrictOrderedRing

/--
Prove that the complex numbers cannot be given a
linear order that is compatible with its field structure.
-/
theorem not_linearOrderedField_complex
  (h1: LinearOrder ℂ) (h2: IsStrictOrderedRing ℂ)
    :  False := byh1:LinearOrder ℂh2:IsStrictOrderedRing ℂ⊢ False

  -- In a linear ordered ring, every square is ≥ 0.
  have h0_le_I_sq : (0 : ℂ) ≤ I * I := byh1:LinearOrder ℂh2:IsStrictOrderedRing ℂ⊢ False
    -- `mul_self_nonneg` says `0 ≤ x * x`
    -- in any linear ordered ring.
    simpa using (mul_self_nonneg I)All goals completed! 🐙

  -- But in ℂ we know `I * I = -1`.
  have h0_le_neg1 : (0 : ℂ) ≤ -1 := byh1:LinearOrder ℂh2:IsStrictOrderedRing ℂ⊢ False
    simpa [I_mul_I] using h0_le_I_sqAll goals completed! 🐙

  -- Add 1 to both sides: 0 + 1 ≤ -1 + 1, so 1 ≤ 0.
  have h1_le_0 : (1 : ℂ) ≤ 0 := byh1:LinearOrder ℂh2:IsStrictOrderedRing ℂ⊢ False
    have := add_le_add_right h0_le_neg1 1h1:LinearOrder ℂh2:IsStrictOrderedRing ℂh0_le_I_sq:0 ≤ I * Ih0_le_neg1:0 ≤ -1this:1 + 0 ≤ 1 + -1⊢ 1 ≤ 0
    -- Simplify both sides.
    simpa [add_comm, add_left_comm, add_assoc] using thisAll goals completed! 🐙

  -- In a linear ordered ring we must have 0 < 1.
  have h0_lt_1 : (0 : ℂ) < 1 := byh1:LinearOrder ℂh2:IsStrictOrderedRing ℂ⊢ False norm_numAll goals completed! 🐙

  -- Combining: 1 < 1, contradiction.
  have : (1:ℂ) < 1 := lt_of_le_of_lt h1_le_0 h0_lt_1h1:LinearOrder ℂh2:IsStrictOrderedRing ℂh0_le_I_sq:0 ≤ I * Ih0_le_neg1:0 ≤ -1h1_le_0:1 ≤ 0h0_lt_1:0 < 1this:1 < 1⊢ False
  exact lt_irrefl 1 thisAll goals completed! 🐙