Grace/Cumulus/Algebra/Ring/Core.g17

Open in Workbench Download source

Imports

Group.Basic · Defs

Declarations

Source

1-- Core ring theory2-- 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.Algebra.Ring.Core8import Group.Basic9import Defs1011theorem IsSemiring.distributive (A add zero mul one : Set)12  requires h : IsSemiring(A, add, zero, mul, one)13  shows Distributive(A, add, mul)14proof15  simp [IsSemiring]1617theorem IsRing.additive (A add zero neg mul one : Set)18  requires h : IsRing(A, add, zero, neg, mul, one)19  shows IsAbelianGroup(A, add, zero, neg)20proof21  simp [IsRing]2223theorem IsRing.multiplicative (A add zero neg mul one : Set)24  requires h : IsRing(A, add, zero, neg, mul, one)25  shows IsMonoid(A, mul, one)26proof27  simp [IsRing]2829theorem IsRing.distributive (A add zero neg mul one : Set)30  requires h : IsRing(A, add, zero, neg, mul, one)31  shows Distributive(A, add, mul)32proof33  simp [IsRing]3435theorem IsRing.add_closed (A add zero neg mul one x y : Set)36  requires ring : IsRing(A, add, zero, neg, mul, one)37  requires xInA : x ∈ A38  requires yInA : y ∈ A39  shows call2(add, x, y) ∈ A40proof41  have additive := IsRing.additive with ring42  have group := IsAbelianGroup.group with additive43  have monoid := IsGroup.monoid with group44  exact IsMonoid.closed with monoid, xInA, yInA4546theorem IsRing.neg_closed (A add zero neg mul one x : Set)47  requires ring : IsRing(A, add, zero, neg, mul, one)48  requires xInA : x ∈ A49  shows neg(x) ∈ A50proof51  have additive := IsRing.additive with ring52  have group := IsAbelianGroup.group with additive53  exact IsGroup.inverse_closed with group, xInA5455theorem IsRing.zero_in_carrier (A add zero neg mul one : Set)56  requires ring : IsRing(A, add, zero, neg, mul, one)57  shows zero ∈ A58proof59  have additive := IsRing.additive with ring60  have group := IsAbelianGroup.group with additive61  have monoid := IsGroup.monoid with group62  exact IsMonoid.unit_in_carrier with monoid6364theorem IsRing.add_associative (A add zero neg mul one : Set)65  requires ring : IsRing(A, add, zero, neg, mul, one)66  shows Associative(A, add)67proof68  have additive := IsRing.additive with ring69  have group := IsAbelianGroup.group with additive70  have monoid := IsGroup.monoid with group71  exact IsMonoid.associative with monoid7273theorem IsRing.add_left_identity (A add zero neg mul one x : Set)74  requires ring : IsRing(A, add, zero, neg, mul, one)75  requires xInA : x ∈ A76  shows call2(add, zero, x) = x77proof78  have additive := IsRing.additive with ring79  have group := IsAbelianGroup.group with additive80  have monoid := IsGroup.monoid with group81  exact IsMonoid.left_identity with monoid, xInA8283theorem IsRing.add_right_identity (A add zero neg mul one x : Set)84  requires ring : IsRing(A, add, zero, neg, mul, one)85  requires xInA : x ∈ A86  shows call2(add, x, zero) = x87proof88  have additive := IsRing.additive with ring89  have group := IsAbelianGroup.group with additive90  have monoid := IsGroup.monoid with group91  exact IsMonoid.right_identity with monoid, xInA9293theorem IsRing.add_inverse_left (A add zero neg mul one x : Set)94  requires ring : IsRing(A, add, zero, neg, mul, one)95  requires xInA : x ∈ A96  shows call2(add, neg(x), x) = zero97proof98  have additive := IsRing.additive with ring99  have group := IsAbelianGroup.group with additive100  exact IsGroup.inverse_left with group, xInA101102theorem IsRing.add_inverse_right (A add zero neg mul one x : Set)103  requires ring : IsRing(A, add, zero, neg, mul, one)104  requires xInA : x ∈ A105  shows call2(add, x, neg(x)) = zero106proof107  have additive := IsRing.additive with ring108  have group := IsAbelianGroup.group with additive109  exact IsGroup.inverse_right with group, xInA110111theorem IsRing.mul_closed (A add zero neg mul one x y : Set)112  requires ring : IsRing(A, add, zero, neg, mul, one)113  requires xInA : x ∈ A114  requires yInA : y ∈ A115  shows call2(mul, x, y) ∈ A116proof117  have multiplicative := IsRing.multiplicative with ring118  exact IsMonoid.closed with multiplicative, xInA, yInA119120theorem IsRing.zero_mul (A add zero neg mul one x : Set)121  requires ring : IsRing(A, add, zero, neg, mul, one)122  requires xInA : x ∈ A123  shows call2(mul, zero, x) = zero124proof125  have zeroInA := IsRing.zero_in_carrier with ring126  have productInA := IsRing.mul_closed with ring, zeroInA, xInA127  have distributive := IsRing.distributive with ring128  obtain ⟨leftLaw, rightLaw⟩ := distributive with zero, zeroInA, zero, zeroInA, x, xInA129  have zeroPlusZero := IsRing.add_left_identity with ring, zeroInA130  rw zeroPlusZero at rightLaw131  have negProductInA := IsRing.neg_closed with ring, productInA132  have associative := IsRing.add_associative with ring133  have reassociate := Associative.law with associative, negProductInA, productInA, productInA134  have inverse := IsRing.add_inverse_left with ring, productInA135  have identity := IsRing.add_left_identity with ring, productInA136  cc137138theorem IsRing.mul_zero (A add zero neg mul one x : Set)139  requires ring : IsRing(A, add, zero, neg, mul, one)140  requires xInA : x ∈ A141  shows call2(mul, x, zero) = zero142proof143  have zeroInA := IsRing.zero_in_carrier with ring144  have productInA := IsRing.mul_closed with ring, xInA, zeroInA145  have distributive := IsRing.distributive with ring146  obtain ⟨leftLaw, rightLaw⟩ := distributive with x, xInA, zero, zeroInA, zero, zeroInA147  have zeroPlusZero := IsRing.add_left_identity with ring, zeroInA148  rw zeroPlusZero at leftLaw149  have negProductInA := IsRing.neg_closed with ring, productInA150  have associative := IsRing.add_associative with ring151  have reassociate := Associative.law with associative, negProductInA, productInA, productInA152  have inverse := IsRing.add_inverse_left with ring, productInA153  have identity := IsRing.add_left_identity with ring, productInA154  cc155156theorem IsRing.neg_mul (A add zero neg mul one x y : Set)157  requires ring : IsRing(A, add, zero, neg, mul, one)158  requires xInA : x ∈ A159  requires yInA : y ∈ A160  shows call2(mul, neg(x), y) = neg(call2(mul, x, y))161proof162  have additive := IsRing.additive with ring163  have group := IsAbelianGroup.group with additive164  have monoid := IsGroup.monoid with group165  have negXInA := IsRing.neg_closed with ring, xInA166  have productInA := IsRing.mul_closed with ring, xInA, yInA167  have negProductInA := IsRing.neg_closed with ring, productInA168  have candidateInA := IsRing.mul_closed with ring, negXInA, yInA169  have distributive := IsRing.distributive with ring170  obtain ⟨leftLaw, rightLaw⟩ := distributive with neg(x), negXInA, x, xInA, y, yInA171  have inverseX := IsRing.add_inverse_left with ring, xInA172  have zeroProduct := IsRing.zero_mul with ring, yInA173  rw [inverseX, zeroProduct] at rightLaw174  have commutative := IsAbelianGroup.commutative with additive175  have candidateSwap := commutative with176    call2(mul, neg(x), y), candidateInA,177    call2(mul, x, y), productInA178  have candidateLeft : call2(add,179      call2(mul, neg(x), y), call2(mul, x, y)) = zero180    cc181  have candidateRight : call2(add,182      call2(mul, x, y), call2(mul, neg(x), y)) = zero183    cc184  have canonical : IsInverse(A, add, zero,185      call2(mul, x, y), neg(call2(mul, x, y)))186    unfold IsInverse187    refine ⟨productInA, negProductInA, _, _⟩188    . exact IsRing.add_inverse_left at189        A, add, zero, neg, mul, one, call2(mul, x, y) with ring, productInA190    . exact IsRing.add_inverse_right at191        A, add, zero, neg, mul, one, call2(mul, x, y) with ring, productInA192  have candidate : IsInverse(A, add, zero,193      call2(mul, x, y), call2(mul, neg(x), y))194    unfold IsInverse195    refine ⟨productInA, candidateInA, candidateLeft, candidateRight⟩196  have unique := IsInverse.unique with monoid, canonical, candidate197  cc198199theorem CommSemiring.semiring (A add zero mul one : Set)200  requires h : CommSemiring(A, add, zero, mul, one)201  shows IsSemiring(A, add, zero, mul, one)202proof203  simp [CommSemiring]204205theorem CommSemiring.commutative (A add zero mul one : Set)206  requires h : CommSemiring(A, add, zero, mul, one)207  shows Commutative(A, mul)208proof209  simp [CommSemiring]210211theorem IsCommRing.ring (A add zero neg mul one : Set)212  requires h : IsCommRing(A, add, zero, neg, mul, one)213  shows IsRing(A, add, zero, neg, mul, one)214proof215  simp [IsCommRing]216217theorem IsCommRing.commutative (A add zero neg mul one : Set)218  requires h : IsCommRing(A, add, zero, neg, mul, one)219  shows Commutative(A, mul)220proof221  simp [IsCommRing]222223theorem IsCommRing.add_commutative (A add zero neg mul one : Set)224  requires ring : IsCommRing(A, add, zero, neg, mul, one)225  shows Commutative(A, add)226proof227  have ordinary := IsCommRing.ring with ring228  have additive := IsRing.additive with ordinary229  exact IsAbelianGroup.commutative with additive230231-- Direct equational laws used by checked polynomial normalization.232theorem IsCommRing.add_comm (A add zero neg mul one x y : Set)233  requires ring : IsCommRing(A, add, zero, neg, mul, one)234  requires hx : x ∈ A235  requires hy : y ∈ A236  shows call2(add, x, y) = call2(add, y, x)237proof238  have comm := IsCommRing.add_commutative with ring239  exact comm with x, hx, y, hy240241theorem IsCommRing.add_assoc (A add zero neg mul one x y z : Set)242  requires ring : IsCommRing(A, add, zero, neg, mul, one)243  requires hx : x ∈ A244  requires hy : y ∈ A245  requires hz : z ∈ A246  shows call2(add, call2(add, x, y), z) = call2(add, x, call2(add, y, z))247proof248  have ordinary := IsCommRing.ring with ring249  have associative := IsRing.add_associative with ordinary250  exact Associative.law with associative, hx, hy, hz251252theorem IsCommRing.add_swap (A add zero neg mul one x y z : Set)253  requires ring : IsCommRing(A, add, zero, neg, mul, one)254  requires hx : x ∈ A255  requires hy : y ∈ A256  requires hz : z ∈ A257  shows call2(add, x, call2(add, y, z)) = call2(add, y, call2(add, x, z))258proof259  have xy := IsCommRing.add_comm with ring, hx, hy260  have lhs := IsCommRing.add_assoc with ring, hx, hy, hz261  have rhs := IsCommRing.add_assoc with ring, hy, hx, hz262  cc263264theorem IsCommRing.neg_add (A add zero neg mul one x y : Set)265  requires ring : IsCommRing(A, add, zero, neg, mul, one)266  requires hx : x ∈ A267  requires hy : y ∈ A268  shows neg(call2(add, x, y)) = call2(add, neg(x), neg(y))269proof270  have ordinary := IsCommRing.ring with ring271  have group := IsRing.additive with ordinary272  exact IsAbelianGroup.inverse_op with group, hx, hy273274theorem IsCommRing.neg_neg (A add zero neg mul one x : Set)275  requires ring : IsCommRing(A, add, zero, neg, mul, one)276  requires hx : x ∈ A277  shows neg(neg(x)) = x278proof279  have ordinary := IsCommRing.ring with ring280  have additive := IsRing.additive with ordinary281  have group := IsAbelianGroup.group with additive282  exact IsGroup.inverse_involutive with group, hx283284theorem IsCommRing.neg_zero (A add zero neg mul one : Set)285  requires ring : IsCommRing(A, add, zero, neg, mul, one)286  shows neg(zero) = zero287proof288  have ordinary := IsCommRing.ring with ring289  have additive := IsRing.additive with ordinary290  have group := IsAbelianGroup.group with additive291  exact IsGroup.inverse_unit with group292293theorem IsCommRing.mul_comm (A add zero neg mul one x y : Set)294  requires ring : IsCommRing(A, add, zero, neg, mul, one)295  requires hx : x ∈ A296  requires hy : y ∈ A297  shows call2(mul, x, y) = call2(mul, y, x)298proof299  have comm := IsCommRing.commutative with ring300  exact comm with x, hx, y, hy301302theorem IsCommRing.mul_assoc (A add zero neg mul one x y z : Set)303  requires ring : IsCommRing(A, add, zero, neg, mul, one)304  requires hx : x ∈ A305  requires hy : y ∈ A306  requires hz : z ∈ A307  shows call2(mul, call2(mul, x, y), z) = call2(mul, x, call2(mul, y, z))308proof309  have ordinary := IsCommRing.ring with ring310  have multiplicative := IsRing.multiplicative with ordinary311  have associative := IsMonoid.associative with multiplicative312  exact Associative.law with associative, hx, hy, hz313314theorem IsCommRing.mul_swap (A add zero neg mul one x y z : Set)315  requires ring : IsCommRing(A, add, zero, neg, mul, one)316  requires hx : x ∈ A317  requires hy : y ∈ A318  requires hz : z ∈ A319  shows call2(mul, x, call2(mul, y, z)) = call2(mul, y, call2(mul, x, z))320proof321  have xy := IsCommRing.mul_comm with ring, hx, hy322  have lhs := IsCommRing.mul_assoc with ring, hx, hy, hz323  have rhs := IsCommRing.mul_assoc with ring, hy, hx, hz324  cc325326theorem IsCommRing.one_left (A add zero neg mul one x : Set)327  requires ring : IsCommRing(A, add, zero, neg, mul, one)328  requires hx : x ∈ A329  shows call2(mul, one, x) = x330proof331  have ordinary := IsCommRing.ring with ring332  have monoid := IsRing.multiplicative with ordinary333  exact IsMonoid.left_identity with monoid, hx334335theorem IsCommRing.one_right (A add zero neg mul one x : Set)336  requires ring : IsCommRing(A, add, zero, neg, mul, one)337  requires hx : x ∈ A338  shows call2(mul, x, one) = x339proof340  have ordinary := IsCommRing.ring with ring341  have monoid := IsRing.multiplicative with ordinary342  exact IsMonoid.right_identity with monoid, hx343344theorem IsCommRing.mul_add (A add zero neg mul one x y z : Set)345  requires ring : IsCommRing(A, add, zero, neg, mul, one)346  requires hx : x ∈ A347  requires hy : y ∈ A348  requires hz : z ∈ A349  shows call2(mul, x, call2(add, y, z)) =350    call2(add, call2(mul, x, y), call2(mul, x, z))351proof352  have ordinary := IsCommRing.ring with ring353  have distributive := IsRing.distributive with ordinary354  obtain ⟨left, right⟩ := distributive with x, hx, y, hy, z, hz355  exact left356357theorem IsCommRing.add_mul (A add zero neg mul one x y z : Set)358  requires ring : IsCommRing(A, add, zero, neg, mul, one)359  requires hx : x ∈ A360  requires hy : y ∈ A361  requires hz : z ∈ A362  shows call2(mul, call2(add, x, y), z) =363    call2(add, call2(mul, x, z), call2(mul, y, z))364proof365  have ordinary := IsCommRing.ring with ring366  have distributive := IsRing.distributive with ordinary367  obtain ⟨left, right⟩ := distributive with x, hx, y, hy, z, hz368  exact right369370theorem IsCommRing.mul_neg (A add zero neg mul one x y : Set)371  requires commRing : IsCommRing(A, add, zero, neg, mul, one)372  requires xInA : x ∈ A373  requires yInA : y ∈ A374  shows call2(mul, x, neg(y)) = neg(call2(mul, x, y))375proof376  have ring := IsCommRing.ring with commRing377  have negYInA := IsRing.neg_closed with ring, yInA378  have commutative := IsCommRing.commutative with commRing379  have leftSwap := commutative with x, xInA, neg(y), negYInA380  have rightSwap := commutative with x, xInA, y, yInA381  have negated := IsRing.neg_mul with ring, yInA, xInA382  cc383384theorem IsCommRing.neg_mul_neg (A add zero neg mul one x y : Set)385  requires commRing : IsCommRing(A, add, zero, neg, mul, one)386  requires xInA : x ∈ A387  requires yInA : y ∈ A388  shows call2(mul, neg(x), neg(y)) = call2(mul, x, y)389proof390  have ring := IsCommRing.ring with commRing391  have additive := IsRing.additive with ring392  have group := IsAbelianGroup.group with additive393  have negYInA := IsRing.neg_closed with ring, yInA394  have outerNeg := IsRing.neg_mul with ring, xInA, negYInA395  have innerNeg := IsCommRing.mul_neg with commRing, xInA, yInA396  have productInA := IsRing.mul_closed with ring, xInA, yInA397  have involutive := IsGroup.inverse_involutive with group, productInA398  cc399400theorem Nontrivial.distinct (A zero one : Set)401  requires h : Nontrivial(A, zero, one)402  shows zero ≠ one403proof404  simp [Nontrivial]405406theorem IsIntegralDomain.comm_ring (A add zero neg mul one : Set)407  requires h : IsIntegralDomain(A, add, zero, neg, mul, one)408  shows IsCommRing(A, add, zero, neg, mul, one)409proof410  simp [IsIntegralDomain]411412theorem IsIntegralDomain.nontrivial (A add zero neg mul one : Set)413  requires h : IsIntegralDomain(A, add, zero, neg, mul, one)414  shows Nontrivial(A, zero, one)415proof416  simp [IsIntegralDomain]417418theorem IsIntegralDomain.no_zero_divisors (A add zero neg mul one : Set)419  requires h : IsIntegralDomain(A, add, zero, neg, mul, one)420  shows NoZeroDivisors(A, mul, zero)421proof422  simp [IsIntegralDomain]423