Grace/Cumulus/Complex/Field.g17

Open in Workbench Download source

Imports

Ring · Algebra.Ring.Basic · Numeral

Declarations

• complex.norm_zero_iff theorem derivation
• complex.inverse_pair theorem derivation
• complexes.nontrivial theorem derivation
• complexes.is_field theorem derivation
• complexRing def
• complexRing.carrierOf theorem derivation
• complexRing.comm_ring instance derivation
• complexRing.field instance derivation

Source

1-- Complex inverses by the positive real squared modulus, in ZF.2-- Part of Cumulus, the Grace17 mathematics library.3-- Copyright (c) 2026 Grant Passmore.4-- Released under the Apache License 2.0. See LICENSE in the repository root.5-- Authors: Grant Passmore67module Grace.Cumulus.Complex.Field8import Ring9import Algebra.Ring.Basic10import Numeral1112-- The squared modulus vanishes exactly at the origin.13theorem complex.norm_zero_iff (a b : Real)14  shows a * a + b * b = 0 ↔ a = 0 ∧ b = 015proof16  constructor17  . intro zeroSum18    have aNonnegative := realMulValue.square_nonnegative at a with *19    have bNonnegative := realMulValue.square_nonnegative at b with *20    have aZero := realAddValue.nonnegative_eq_zero at a * a, b * b with *21    have swapped : b * b + a * a = 0 by linear_combination zeroSum22    have bZero := realAddValue.nonnegative_eq_zero at b * b, a * a with *23    have first := realMulValue.square_eq_zero_iff.forward with aZero24    have second := realMulValue.square_eq_zero_iff.forward with bZero25    refine ⟨first, second⟩26  . intro coordinates27    rw [coordinates.left, coordinates.right]28    ring2930section Complexes31notation ring ℂ := (complexCarrier, complexAdd, complexZero, complexNeg, complexMul, complexOne)32notation ring R := (ℝ, realAdd, realZero, realNeg, realMul, realOne)3334theorem complex.inverse_pair (a b : Real)35  requires nonzero : (a, b) ≠ complexZero36  shows IsInverse(complexCarrier, complexMul, complexOne, (a, b), (R[a * realInvValue(R[a * a + b * b])], R[-b * realInvValue(R[a * a + b * b])]))37proof38  have normNonzero : R[a * a + b * b] ≠ R[0]39    intro vanishes40    have coordinates := complex.norm_zero_iff.forward with *41    apply nonzero42    simp [complexZero]43  have inverseLaw := realInvValue.mul_right with normNonzero44  have original := complexCarrier.pair at a, b with *45  have inverse := complexCarrier.pair at R[a * realInvValue(R[a * a + b * b])], R[-b * realInvValue(R[a * a + b * b])] with *46  have horizontal : R[a * (a * realInvValue(R[a * a + b * b])) - b * (-b * realInvValue(R[a * a + b * b]))] = R[1]47    linear_combination inverseLaw48  have vertical : R[a * (-b * realInvValue(R[a * a + b * b])) + b * (a * realInvValue(R[a * a + b * b]))] = R[0]49    ring50  have right : ℂ[(a, b) * (R[a * realInvValue(R[a * a + b * b])], R[-b * realInvValue(R[a * a + b * b])])] = ℂ[1]51    simp [complexMul.pair, complexOne]52  have commutes := complexMul.commutative53  have swap := commutes with (a, b), original, (R[a * realInvValue(R[a * a + b * b])], R[-b * realInvValue(R[a * a + b * b])]), inverse54  unfold IsInverse55  refine ⟨original, inverse, ?_⟩56  constructor57  . cc58  . exact right5960theorem complexes.nontrivial61  shows Nontrivial(ℂ)62proof63  unfold Nontrivial64  refine ⟨complexZero.member, complexOne.member, ?_⟩65  intro same66  unfold complexZero at same67  unfold complexOne at same68  have coordinates := orderedPair.injective with same69  have distinct := Nontrivial.distinct with reals.nontrivial70  exact distinct with coordinates.left7172theorem complexes.is_field73  shows IsField(ℂ)74proof75  unfold IsField76  refine ⟨complexes.comm_ring, complexes.nontrivial, ?_⟩77  intros x member nonzero78  obtain ⟨a, aReal, b, bReal, shape⟩ := complexCarrier.cases with member79  rw shape at nonzero80  have inverse := complex.inverse_pair with *81  witness (R[a * realInvValue(R[a * a + b * b])], R[-b * realInvValue(R[a * a + b * b])])82  rwa shape8384end Complexes8586-- The bundled complex ring: the carrier ℝ × ℝ with complex addition, zero,87-- negation, multiplication, and one; a commutative ring and a field.88def complexRing : Set :=89  Ring.mk(complexCarrier, complexAdd, complexZero, complexNeg, complexMul, complexOne)9091theorem complexRing.carrierOf92  shows Ring.carrier(complexRing) = complexCarrier93proof94  simp [complexRing, Ring.mk.carrier]9596instance complexRing.comm_ring97  shows CommRing(complexRing)98proof99  have parts := complexes.comm_ring100  unfold complexRing101  exact CommRing.of_parts with parts102103instance complexRing.field104  shows Field(complexRing)105proof106  have parts := complexes.is_field107  unfold complexRing108  exact Field.of_parts with parts109