Grace/Cumulus/Complex/Ring.g17

Open in Workbench Download source

Imports

Core

Declarations

Source

1-- The commutative ring laws for the usual concrete complex operations.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.Ring8import Core910section Coordinates11notation ring ℂ := (complexCarrier, complexAdd, complexZero, complexNeg, complexMul, complexOne)12notation ring R := (ℝ, realAdd, realZero, realNeg, realMul, realOne)1314theorem complex.add_associative_pair (a b c d e f : Real)15  shows ℂ[ℂ[(a, b) + (c, d)] + (e, f)] = ℂ[(a, b) + ℂ[(c, d) + (e, f)]]16proof17  have horizontal : R[(a+c)+e] = R[a+(c+e)] by ring18  have vertical : R[(b+d)+f] = R[b+(d+f)] by ring19  simp [complexAdd.pair]2021theorem complex.add_commutative_pair (a b c d : Real)22  shows ℂ[(a, b) + (c, d)] = ℂ[(c, d) + (a, b)]23proof24  have horizontal : R[a+c] = R[c+a] by ring25  have vertical : R[b+d] = R[d+b] by ring26  simp [complexAdd.pair]2728theorem complex.add_zero_pair (a b : Real)29  shows ℂ[(a, b) + 0] = (a, b)30proof31  have horizontal : R[a+0] = R[a] by ring32  have vertical : R[b+0] = R[b] by ring33  simp [complexZero, complexAdd.pair]3435theorem complex.add_neg_pair (a b : Real)36  shows ℂ[(a, b) + ℂ[-(a, b)]] = ℂ[0]37proof38  have horizontal : R[a+(-a)] = R[0] by ring39  have vertical : R[b+(-b)] = R[0] by ring40  simp [complexZero, complexNeg.pair, complexAdd.pair]4142theorem complex.mul_associative_pair (a b c d e f : Real)43  shows ℂ[ℂ[(a, b) * (c, d)] * (e, f)] = ℂ[(a, b) * ℂ[(c, d) * (e, f)]]44proof45  have horizontal : R[(a*c-b*d)*e-(a*d+b*c)*f] = R[a*(c*e-d*f)-b*(c*f+d*e)] by ring46  have vertical : R[(a*c-b*d)*f+(a*d+b*c)*e] = R[a*(c*f+d*e)+b*(c*e-d*f)] by ring47  simp [complexMul.pair]4849theorem complex.mul_commutative_pair (a b c d : Real)50  shows ℂ[(a, b) * (c, d)] = ℂ[(c, d) * (a, b)]51proof52  have horizontal : R[a*c-b*d] = R[c*a-d*b] by ring53  have vertical : R[a*d+b*c] = R[c*b+d*a] by ring54  simp [complexMul.pair]5556theorem complex.mul_one_pair (a b : Real)57  shows ℂ[(a, b) * 1] = (a, b)58proof59  have horizontal : R[a*1-b*0] = R[a] by ring60  have vertical : R[a*0+b*1] = R[b] by ring61  simp [complexOne, complexMul.pair]6263theorem complex.distributive_pair (a b c d e f : Real)64  shows ℂ[(a, b) * ℂ[(c, d) + (e, f)]] = ℂ[ℂ[(a, b) * (c, d)] + ℂ[(a, b) * (e, f)]]65proof66  have horizontal : R[a*(c+e)-b*(d+f)] = R[(a*c-b*d)+(a*e-b*f)] by ring67  have vertical : R[a*(d+f)+b*(c+e)] = R[(a*d+b*c)+(a*f+b*e)] by ring68  simp [complexAdd.pair, complexMul.pair]6970theorem complexAdd.associative71  shows Associative(complexCarrier, complexAdd)72proof73  intros x hx y hy z hz74  obtain ⟨a, aReal, b, bReal, xShape⟩ := complexCarrier.cases with hx75  rw xShape76  obtain ⟨c, cReal, d, dReal, yShape⟩ := complexCarrier.cases with hy77  rw yShape78  obtain ⟨e, eReal, f, fReal, zShape⟩ := complexCarrier.cases with hz79  rw zShape80  exact complex.add_associative_pair with *8182theorem complexAdd.commutative83  shows Commutative(complexCarrier, complexAdd)84proof85  intros x hx y hy86  obtain ⟨a, aReal, b, bReal, xShape⟩ := complexCarrier.cases with hx87  rw xShape88  obtain ⟨c, cReal, d, dReal, yShape⟩ := complexCarrier.cases with hy89  rw yShape90  exact complex.add_commutative_pair with *9192theorem complexMul.associative93  shows Associative(complexCarrier, complexMul)94proof95  intros x hx y hy z hz96  obtain ⟨a, aReal, b, bReal, xShape⟩ := complexCarrier.cases with hx97  rw xShape98  obtain ⟨c, cReal, d, dReal, yShape⟩ := complexCarrier.cases with hy99  rw yShape100  obtain ⟨e, eReal, f, fReal, zShape⟩ := complexCarrier.cases with hz101  rw zShape102  exact complex.mul_associative_pair with *103104theorem complexMul.commutative105  shows Commutative(complexCarrier, complexMul)106proof107  intros x hx y hy108  obtain ⟨a, aReal, b, bReal, xShape⟩ := complexCarrier.cases with hx109  rw xShape110  obtain ⟨c, cReal, d, dReal, yShape⟩ := complexCarrier.cases with hy111  rw yShape112  exact complex.mul_commutative_pair with *113114theorem complexZero.member115  shows complexZero ∈ complexCarrier116proof117  unfold complexZero118  exact complexCarrier.pair with realZero.real, realZero.real119120theorem complexOne.member121  shows complexOne ∈ complexCarrier122proof123  unfold complexOne124  exact complexCarrier.pair with realOne.real, realZero.real125126theorem complexAdd.identity127  shows Identity(complexCarrier, complexAdd, complexZero)128proof129  unfold Identity130  refine ⟨complexZero.member, ?_⟩131  intros x member132  obtain ⟨a, aReal, b, bReal, shape⟩ := complexCarrier.cases with member133  have right := complex.add_zero_pair at a, b with *134  rw ← shape at right135  have commutes := complexAdd.commutative136  have swap := commutes with complexZero, complexZero.member, x, member137  constructor138  . cc139  . exact right140141theorem complexMul.identity142  shows Identity(complexCarrier, complexMul, complexOne)143proof144  unfold Identity145  refine ⟨complexOne.member, ?_⟩146  intros x member147  obtain ⟨a, aReal, b, bReal, shape⟩ := complexCarrier.cases with member148  have right := complex.mul_one_pair at a, b with *149  rw ← shape at right150  have commutes := complexMul.commutative151  have swap := commutes with complexOne, complexOne.member, x, member152  constructor153  . cc154  . exact right155156theorem complexNeg.inverse157  shows Inverse(complexCarrier, complexAdd, complexZero, complexNeg)158proof159  unfold Inverse160  refine ⟨complexNeg.function, ?_⟩161  intros x member162  obtain ⟨a, aReal, b, bReal, shape⟩ := complexCarrier.cases with member163  have right := complex.add_neg_pair at a, b with *164  rw ← shape at right165  have negative : complexNeg(x) ∈ complexCarrier166    exact FunctionBetween.apply_closed with complexNeg.function, member167  have commutes := complexAdd.commutative168  have swap := commutes with complexNeg(x), negative, x, member169  constructor170  . cc171  . exact right172173theorem complexMul.distributive174  shows Distributive(complexCarrier, complexAdd, complexMul)175proof176  intros x hx y hy z hz177  obtain ⟨a, aReal, b, bReal, xShape⟩ := complexCarrier.cases with hx178  obtain ⟨c, cReal, d, dReal, yShape⟩ := complexCarrier.cases with hy179  obtain ⟨e, eReal, f, fReal, zShape⟩ := complexCarrier.cases with hz180  have left := complex.distributive_pair at a, b, c, d, e, f with *181  rw [← xShape, ← yShape, ← zShape] at left182  have other := complex.distributive_pair at e, f, a, b, c, d with *183  rw [← xShape, ← yShape, ← zShape] at other184  have sum : complexAdd(x, y) ∈ complexCarrier185    unfold call2186    have pair := product.pair with hx, hy187    exact FunctionBetween.apply_closed with complexAdd.function, pair188  have commutes := complexMul.commutative189  have outer := commutes with z, hz, complexAdd(x, y), sum190  have first := commutes with z, hz, x, hx191  have second := commutes with z, hz, y, hy192  constructor193  . exact left194  . cc195196instance complexes.comm_ring197  shows IsCommRing(ℂ)198proof199  constructor200    constructor201      constructor202        constructor203          constructor204            constructor205              exact complexAdd.function206            . exact complexAdd.associative207          . exact complexAdd.identity208        . exact complexNeg.inverse209      . exact complexAdd.commutative210    . constructor211        constructor212          constructor213            exact complexMul.function214          . exact complexMul.associative215        . exact complexMul.identity216      . exact complexMul.distributive217  . exact complexMul.commutative218219end Coordinates220