Grace/Cumulus/Algebra/Ring/Basic.g17

Open in Workbench Download source

Imports

Numeral · Field.Construction · OrderedField.Defs

Declarations

Source

1-- Bundled rings: a ring as one structure extending its additive abelian2-- group and its multiplicative monoid, with the commutative rings, fields,3-- and ordered fields as predicates over it and the ring notation read off4-- the hypothesis in scope5-- Part of Cumulus, the Grace17 mathematics library.6-- Copyright (c) 2026 Grant Passmore.7-- Released under the Apache License 2.0. See LICENSE in the repository root.8-- Authors: Grant Passmore910module Grace.Cumulus.Algebra.Ring.Basic11import Numeral12import Field.Construction13import OrderedField.Defs1415-- A ring extends its two parents: the additive abelian group, whose16-- operation, unit, and inverse are the ring's add, zero, and neg, and the17-- multiplicative monoid, whose operation and unit are its mul and one and18-- whose inverse slot, which Monoid does not constrain, is fixed to ∅. The19-- fields of the parents are the ring's own, so a ring is built by20-- Ring.mk(A, add, zero, neg, mul, one) and read back by R.carrier, R.add,21-- R.zero, R.neg, R.mul, and R.one; the parents are the values22-- R.additive = Group.mk(R.carrier, R.add, R.zero, R.neg) and23-- R.multiplicative = Group.mk(R.carrier, R.mul, R.one, ∅). Ring(R) says24-- that R is such a structure, that AbelianGroup(R.additive) and25-- Monoid(R.multiplicative) hold, and that multiplication distributes;26-- Ring.Data(R) is the shape alone, and Ring.intro builds a ring from its27-- six pieces, their typing, the two parents at the constructor, and28-- distributivity. The instances Ring.additive.abelian_group and29-- Ring.multiplicative.monoid make the parents' laws available wherever30-- Ring(R) is, so a theorem about abelian groups applies to R.additive.31structure Ring extends32    AbelianGroup as additive (mul := add, one := zero, inv := neg),33    Monoid as multiplicative (inv := ∅)34  where35    distributive : Distributive(carrier, add, mul)3637-- The projection laws of a constructed ring as one rewrite set, and the38-- projections of the two parents as the ring's own fields, so that a fact39-- about R.additive or R.multiplicative reads in R.add, R.zero, R.mul, R.one.40tactic ring_projections := simp [Ring.mk.carrier, Ring.mk.add, Ring.mk.zero, Ring.mk.neg, Ring.mk.mul, Ring.mk.one]41tactic ring_additive := simp [Ring.additive.carrier, Ring.additive.mul, Ring.additive.one, Ring.additive.inv]42tactic ring_multiplicative := simp [Ring.multiplicative.carrier, Ring.multiplicative.mul, Ring.multiplicative.one]4344-- The commutative rings, fields, and ordered fields as properties of the45-- same structure. Field(R) is the field as a property of the ring, with an46-- inverse for every nonzero element, so no inverse graph is part of the47-- data; OrderedField(R, lt) adds a strict linear order compatible with the48-- operations. IsRing(A, add, zero, neg, mul, one), IsCommRing(…),49-- IsField(…), IsFieldWithInverse(…, inv), and IsOrderedField(…, inv, lt)50-- remain the forms over separate pieces, bridged below.51predicate CommRing (R : Set) := Ring(R) ∧ Commutative(R.carrier, R.mul)52predicate Field (R : Set) :=53  Ring.Data(R) ∧ IsField(R.carrier, R.add, R.zero, R.neg, R.mul, R.one)54predicate OrderedField (R lt : Set) :=55  Field(R) ∧ StrictLinearOrder(R.carrier, lt) ∧56  AddStrictMono(R.carrier, R.add, lt) ∧ MulPositive(R.carrier, R.mul, R.zero, lt)5758-- The operations are written x + y, x * y, and -x wherever a hypothesis in59-- scope supplies the ring; the operands' membership in R.carrier selects60-- the ring when several are in scope, and operands of a typed carrier such61-- as ℕ or ℝ keep their own operations. Under the same hypotheses a binder62-- (x : R) is a set variable with x ∈ R.carrier, and R[0], R[1], R[2] are63-- the zero, the one, and the numerals of R. The multiplication keeps the64-- monoid's name, so x * y under Ring(R) is inherited from the parent's65-- notation; the additive group's operation is renamed, so + and - are66-- declared here.67notation infixl 60 "+" => call2(R.add, _, _) via hypothesis Ring(R) for R.carrier68notation infixl 60 "+" => call2(R.add, _, _) via hypothesis CommRing(R) for R.carrier69notation infixl 60 "+" => call2(R.add, _, _) via hypothesis Field(R) for R.carrier70notation infixl 60 "+" => call2(R.add, _, _) via hypothesis OrderedField(R, lt) for R.carrier71notation infixl 70 "*" => call2(R.mul, _, _) via hypothesis CommRing(R) for R.carrier72notation infixl 70 "*" => call2(R.mul, _, _) via hypothesis Field(R) for R.carrier73notation infixl 70 "*" => call2(R.mul, _, _) via hypothesis OrderedField(R, lt) for R.carrier74notation prefix 75 "-" => apply(R.neg, _) via hypothesis Ring(R) for R.carrier75notation prefix 75 "-" => apply(R.neg, _) via hypothesis CommRing(R) for R.carrier76notation prefix 75 "-" => apply(R.neg, _) via hypothesis Field(R) for R.carrier77notation prefix 75 "-" => apply(R.neg, _) via hypothesis OrderedField(R, lt) for R.carrier7879-- Subtraction is addition of the negation: x - y is Ring.sub(R, x, y) under80-- the same hypotheses, and Ring.sub.value unfolds it to x + (-y), the form81-- the ring tactics read.82def Ring.sub (R x y : Set) : Set := call2(Ring.add(R), x, apply(Ring.neg(R), y))8384notation infixl 60 "-" => Ring.sub(R, _, _) via hypothesis Ring(R) for R.carrier85notation infixl 60 "-" => Ring.sub(R, _, _) via hypothesis CommRing(R) for R.carrier86notation infixl 60 "-" => Ring.sub(R, _, _) via hypothesis Field(R) for R.carrier87notation infixl 60 "-" => Ring.sub(R, _, _) via hypothesis OrderedField(R, lt) for R.carrier8889-- Bridges between the structure and the forms over separate pieces. The90-- bundled-to-unbundled directions are instances, so `with *`, `typecheck`,91-- and `ring` read the unbundled form off a bundled hypothesis.92instance Ring.parts (R : Set)93  requires ring : Ring(R)94  shows IsRing(R.carrier, R.add, R.zero, R.neg, R.mul, R.one)95proof96  obtain ⟨shape, addF, zeroIn, negF, mulF, oneIn, additive, multiplicative, distributive⟩ := ring97  have abelian := AbelianGroup.parts with additive98  ring_additive at abelian99  have monoid := Monoid.parts with multiplicative100  ring_multiplicative at monoid101  unfold IsRing102  exact ⟨abelian, monoid, distributive⟩103104-- The typing of the six pieces, read off the parameterized ring.105theorem IsRing.typing_of_parts (A add zero neg mul one : Set)106  requires ring : IsRing(A, add, zero, neg, mul, one)107  shows (add : A × A → A) ∧ zero ∈ A ∧ (neg : A → A) ∧108    (mul : A × A → A) ∧ one ∈ A109proof110  have additive := IsRing.additive with ring111  have group := IsAbelianGroup.group with additive112  have monoid := IsRing.multiplicative with ring113  have addF := IsGroup.magma with group114  have zeroIn := IsRing.zero_in_carrier with ring115  obtain ⟨negF, inverses⟩ := IsGroup.inverse with group116  have mulF := IsSemigroup.magma with (IsMonoid.semigroup with monoid)117  have oneIn := IsMonoid.unit_in_carrier with monoid118  exact ⟨addF, zeroIn, negF, mulF, oneIn⟩119120theorem Ring.of_parts (A add zero neg mul one : Set)121  requires ring : IsRing(A, add, zero, neg, mul, one)122  shows Ring(Ring.mk(A, add, zero, neg, mul, one))123proof124  obtain ⟨addF, zeroIn, negF, mulF, oneIn⟩ := IsRing.typing_of_parts with ring125  have additive := AbelianGroup.of_parts with (IsRing.additive with ring)126  have multiplicative := Monoid.of_parts at A, mul, one, ∅127    with (IsRing.multiplicative with ring)128  have distributive := IsRing.distributive with ring129  exact Ring.intro with addF, zeroIn, negF, mulF, oneIn, additive,130    multiplicative, distributive131132instance CommRing.parts (R : Set)133  requires comm : CommRing(R)134  shows IsCommRing(R.carrier, R.add, R.zero, R.neg, R.mul, R.one)135proof136  obtain ⟨ring, commutative⟩ := comm137  have parts := Ring.parts with ring138  unfold IsCommRing139  exact ⟨parts, commutative⟩140141theorem CommRing.of_parts (A add zero neg mul one : Set)142  requires ring : IsCommRing(A, add, zero, neg, mul, one)143  shows CommRing(Ring.mk(A, add, zero, neg, mul, one))144proof145  have bundled := Ring.of_parts with (IsCommRing.ring with ring)146  have commutative := IsCommRing.commutative with ring147  unfold CommRing148  ring_projections149150theorem Ring.of_projections (R : Set)151  requires shape : Ring.Data(R)152  requires ring : IsRing(R.carrier, R.add, R.zero, R.neg, R.mul, R.one)153  shows Ring(R)154proof155  have eta := Ring.eta with shape156  rw eta157  exact Ring.of_parts with ring158159theorem CommRing.of_projections (R : Set)160  requires shape : Ring.Data(R)161  requires comm : IsCommRing(R.carrier, R.add, R.zero, R.neg, R.mul, R.one)162  shows CommRing(R)163proof164  have ring := Ring.of_projections with shape, (IsCommRing.ring with comm)165  have commutative := IsCommRing.commutative with comm166  unfold CommRing167  exact ⟨ring, commutative⟩168169instance CommRing.to_ring (R : Set)170  requires comm : CommRing(R)171  shows Ring(R)172proof173  obtain ⟨ring, commutative⟩ := comm174  exact ring175176instance Field.parts (R : Set)177  requires field : Field(R)178  shows IsField(R.carrier, R.add, R.zero, R.neg, R.mul, R.one)179proof180  obtain ⟨shape, isField⟩ := field181  exact isField182183theorem Field.of_parts (A add zero neg mul one : Set)184  requires field : IsField(A, add, zero, neg, mul, one)185  shows Field(Ring.mk(A, add, zero, neg, mul, one))186proof187  have shape := Ring.mk.data at A, add, zero, neg, mul, one188  unfold Field189  ring_projections190191theorem Field.of_inverse (A add zero neg mul one inv : Set)192  requires field : IsFieldWithInverse(A, add, zero, neg, mul, one, inv)193  shows Field(Ring.mk(A, add, zero, neg, mul, one))194proof195  exact Field.of_parts with (IsFieldWithInverse.is_field with field)196197instance Field.to_comm_ring (R : Set)198  requires field : Field(R)199  shows CommRing(R)200proof201  obtain ⟨shape, isField⟩ := field202  have comm := IsField.comm_ring with isField203  exact CommRing.of_projections with shape, comm204205theorem OrderedField.parts (R lt : Set)206  requires ordered : OrderedField(R, lt)207  shows IsOrderedField(R.carrier, R.add, R.zero, R.neg, R.mul, R.one,208    fieldInverse(R.carrier, R.add, R.zero, R.neg, R.mul, R.one), lt)209proof210  obtain ⟨field, order, additive, positive⟩ := ordered211  have unbundled := IsField.field with (Field.parts with field)212  unfold IsOrderedField213  exact ⟨unbundled, order, additive, positive⟩214215theorem OrderedField.of_parts (A add zero neg mul one inv lt : Set)216  requires ordered : IsOrderedField(A, add, zero, neg, mul, one, inv, lt)217  shows OrderedField(Ring.mk(A, add, zero, neg, mul, one), lt)218proof219  obtain ⟨field, order, additive, positive⟩ := ordered220  have bundled := Field.of_inverse with field221  unfold OrderedField222  ring_projections223224instance OrderedField.to_field (R lt : Set)225  requires ordered : OrderedField(R, lt)226  shows Field(R)227proof228  obtain ⟨field, rest⟩ := ordered229  exact field230231-- A ring is the constructor applied to its projections.232theorem Ring.eta_of_ring (R : Set)233  requires ring : Ring(R)234  shows R = Ring.mk(R.carrier, R.add, R.zero, R.neg, R.mul, R.one)235proof236  obtain ⟨shape, rest⟩ := ring237  exact Ring.eta with shape238239section RingLaws240variable (R : Set)241hypothesis ring : Ring(R)242243-- Closure: the operations and constants stay in the carrier. These are244-- instances, so the membership of a compound term is synthesized.245instance Ring.add_mem (x y : R)246  shows x + y ∈ R247proof248  have parts := Ring.parts with ring249  exact IsRing.add_closed with parts, *250251instance Ring.mul_mem (x y : R)252  shows x * y ∈ R253proof254  have parts := Ring.parts with ring255  exact IsRing.mul_closed with parts, *256257instance Ring.neg_mem (x : R)258  shows -x ∈ R259proof260  have parts := Ring.parts with ring261  exact IsRing.neg_closed with parts, *262263theorem Ring.sub.value (x y : R)264  shows x - y = x + (-y)265proof266  simp [Ring.sub]267268instance Ring.sub_mem (x y : R)269  shows x - y ∈ R270proof271  have negIn : -y ∈ R := Ring.neg_mem with *272  rw Ring.sub.value273  exact Ring.add_mem with *274275instance Ring.zero_mem276  shows R.zero ∈ R277proof278  have parts := Ring.parts with ring279  exact IsRing.zero_in_carrier with parts280281instance Ring.one_mem282  shows R.one ∈ R283proof284  have monoid := IsRing.multiplicative with (Ring.parts with ring)285  exact IsMonoid.unit_in_carrier with monoid286287instance Ring.numeral_mem (n : Nat)288  shows ringNat(R.add, R.zero, R.one, n) ∈ R289proof290  have parts := Ring.parts with ring291  exact IsRing.numeral_closed with parts292293end RingLaws294