-- Complex inverses by the positive real squared modulus, in ZF.
-- Part of Cumulus, the Grace17 mathematics library.
-- Copyright (c) 2026 Grant Passmore.
-- Released under the Apache License 2.0. See LICENSE in the repository root.
-- Authors: Grant Passmore

module Grace.Cumulus.Complex.Field
import Ring
import Algebra.Ring.Basic
import Numeral

-- The squared modulus vanishes exactly at the origin.
theorem complex.norm_zero_iff (a b : Real)
  shows a * a + b * b = 0 ↔ a = 0 ∧ b = 0
proof
  constructor
  . intro zeroSum
    have aNonnegative := realMulValue.square_nonnegative at a with *
    have bNonnegative := realMulValue.square_nonnegative at b with *
    have aZero := realAddValue.nonnegative_eq_zero at a * a, b * b with *
    have swapped : b * b + a * a = 0 by linear_combination zeroSum
    have bZero := realAddValue.nonnegative_eq_zero at b * b, a * a with *
    have first := realMulValue.square_eq_zero_iff.forward with aZero
    have second := realMulValue.square_eq_zero_iff.forward with bZero
    refine ⟨first, second⟩
  . intro coordinates
    rw [coordinates.left, coordinates.right]
    ring

section Complexes
notation ring ℂ := (complexCarrier, complexAdd, complexZero, complexNeg, complexMul, complexOne)
notation ring R := (ℝ, realAdd, realZero, realNeg, realMul, realOne)

theorem complex.inverse_pair (a b : Real)
  requires nonzero : (a, b) ≠ complexZero
  shows IsInverse(complexCarrier, complexMul, complexOne, (a, b), (R[a * realInvValue(R[a * a + b * b])], R[-b * realInvValue(R[a * a + b * b])]))
proof
  have normNonzero : R[a * a + b * b] ≠ R[0]
    intro vanishes
    have coordinates := complex.norm_zero_iff.forward with *
    apply nonzero
    simp [complexZero]
  have inverseLaw := realInvValue.mul_right with normNonzero
  have original := complexCarrier.pair at a, b with *
  have inverse := complexCarrier.pair at R[a * realInvValue(R[a * a + b * b])], R[-b * realInvValue(R[a * a + b * b])] with *
  have horizontal : R[a * (a * realInvValue(R[a * a + b * b])) - b * (-b * realInvValue(R[a * a + b * b]))] = R[1]
    linear_combination inverseLaw
  have vertical : R[a * (-b * realInvValue(R[a * a + b * b])) + b * (a * realInvValue(R[a * a + b * b]))] = R[0]
    ring
  have right : ℂ[(a, b) * (R[a * realInvValue(R[a * a + b * b])], R[-b * realInvValue(R[a * a + b * b])])] = ℂ[1]
    simp [complexMul.pair, complexOne]
  have commutes := complexMul.commutative
  have swap := commutes with (a, b), original, (R[a * realInvValue(R[a * a + b * b])], R[-b * realInvValue(R[a * a + b * b])]), inverse
  unfold IsInverse
  refine ⟨original, inverse, ?_⟩
  constructor
  . cc
  . exact right

theorem complexes.nontrivial
  shows Nontrivial(ℂ)
proof
  unfold Nontrivial
  refine ⟨complexZero.member, complexOne.member, ?_⟩
  intro same
  unfold complexZero at same
  unfold complexOne at same
  have coordinates := orderedPair.injective with same
  have distinct := Nontrivial.distinct with reals.nontrivial
  exact distinct with coordinates.left

theorem complexes.is_field
  shows IsField(ℂ)
proof
  unfold IsField
  refine ⟨complexes.comm_ring, complexes.nontrivial, ?_⟩
  intros x member nonzero
  obtain ⟨a, aReal, b, bReal, shape⟩ := complexCarrier.cases with member
  rw shape at nonzero
  have inverse := complex.inverse_pair with *
  witness (R[a * realInvValue(R[a * a + b * b])], R[-b * realInvValue(R[a * a + b * b])])
  rwa shape

end Complexes

-- The bundled complex ring: the carrier ℝ × ℝ with complex addition, zero,
-- negation, multiplication, and one; a commutative ring and a field.
def complexRing : Set :=
  Ring.mk(complexCarrier, complexAdd, complexZero, complexNeg, complexMul, complexOne)

theorem complexRing.carrierOf
  shows Ring.carrier(complexRing) = complexCarrier
proof
  simp [complexRing, Ring.mk.carrier]

instance complexRing.comm_ring
  shows CommRing(complexRing)
proof
  have parts := complexes.comm_ring
  unfold complexRing
  exact CommRing.of_parts with parts

instance complexRing.field
  shows Field(complexRing)
proof
  have parts := complexes.is_field
  unfold complexRing
  exact Field.of_parts with parts