Grace/Cumulus/Algebra/Module/Basic.g17

Open in Workbench Download source

Imports

Ring.Basic

Declarations

Source

1-- Bundled modules over a ring: a module as a structure extending the2-- abelian group of its vectors by a scalar action of the ring, the module3-- notation read off the hypothesis in scope, the first laws of the action,4-- and a ring as a module over itself5-- 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.Module.Basic11import Ring.Basic1213-- A module over a ring R extends the abelian group of its vectors, whose14-- operation, unit, and inverse are the module's add, zero, and neg, by the15-- scalar action smul, a function from R.carrier × carrier to carrier. A16-- module is built by Module.mk(A, add, zero, neg, smul) and read back by17-- M.carrier, M.add, M.zero, M.neg, and M.smul; its additive group is the18-- value M.additive = Group.mk(M.carrier, M.add, M.zero, M.neg). Module(M, R)19-- says that R is a ring, that M is such a structure with20-- AbelianGroup(M.additive), and that the action distributes over both21-- additions, composes with the ring's multiplication, and fixes every22-- vector at the ring's one.23structure Module (R : Ring) extends24    AbelianGroup as additive (mul := add, one := zero, inv := neg)25  | smul : R.carrier × carrier → carrier26  where27    smul_add : ∀ r ∈ R.carrier, ∀ v w ∈ carrier,28      smul(r, add(v, w)) = add(smul(r, v), smul(r, w))29    add_smul : ∀ r s ∈ R.carrier, ∀ v ∈ carrier,30      smul(r + s, v) = add(smul(r, v), smul(s, v))31    mul_smul : ∀ r s ∈ R.carrier, ∀ v ∈ carrier,32      smul(r * s, v) = smul(r, smul(s, v))33    one_smul : ∀ v ∈ carrier, smul(R.one, v) = v3435-- The projection laws of a constructed module as one rewrite set, and the36-- projections of the additive group as the module's own fields, so that a37-- fact about M.additive reads in M.add, M.zero, and M.neg.38tactic module_projections := simp [Module.mk.carrier, Module.mk.add, Module.mk.zero, Module.mk.neg, Module.mk.smul]39tactic module_additive := simp [Module.additive.carrier, Module.additive.mul, Module.additive.one, Module.additive.inv]4041-- The addition is written v + w, the negation -v, and the action r • v42-- wherever a hypothesis in scope supplies the module; the operands'43-- membership in M.carrier selects the module's addition over the ring's.44-- Under the same hypothesis a binder (v : M) is a set variable with45-- v ∈ M.carrier.46notation infixl 60 "+" => call2(M.add, _, _) via hypothesis Module(M, R) for M.carrier47notation prefix 75 "-" => apply(M.neg, _) via hypothesis Module(M, R) for M.carrier48notation infixr 73 "•" => call2(M.smul, _, _) via hypothesis Module(M, R) for M.carrier4950-- The ring of a module, read off the typing of its parameter.51instance Module.ring (M R : Set)52  requires module : Module(M, R)53  shows Ring(R)54proof55  obtain ⟨shape, ring, rest⟩ := module56  exact ring5758section ModuleLaws59variable (R M : Set)60hypothesis ring : Ring(R)61hypothesis module : Module(M, R)6263-- The additive group of the module as a group, for the group laws below.64theorem Module.additive_group65  shows Group(M.additive)66proof67  have abelian := Module.additive.abelian_group with module68  exact AbelianGroup.to_group with abelian6970-- Closure: the operations and the zero stay in the carrier. These are71-- instances, so the membership of a compound term is synthesized. The72-- additive facts come from the group laws applied to M.additive, whose73-- membership is the instance Module.additive.mem.74instance Module.add_mem (v w : M)75  shows v + w ∈ M76proof77  have group := Module.additive_group with *78  have closed := Group.mul_mem at M.additive, v, w with group, *79  module_additive at closed80  exact closed8182instance Module.neg_mem (v : M)83  shows -v ∈ M84proof85  have group := Module.additive_group with *86  have closed := Group.inv_mem at M.additive, v with group, *87  module_additive at closed88  exact closed8990instance Module.zero_mem91  shows M.zero ∈ M92proof93  have group := Module.additive_group with *94  have closed := Group.one_mem at M.additive with group95  module_additive at closed96  exact closed9798instance Module.smul_mem (r : R) (v : M)99  shows r • v ∈ M100proof101  obtain ⟨shape, ringR, addF, zeroIn, negF, smulF, rest⟩ := module102  unfold call2103  apply FunctionBetween.apply_closed with smulF104  exact product.pair with *105106-- The laws of the structure under the notation.107theorem smul_add (r : R) (v w : M)108  shows r • (v + w) = r • v + r • w109proof110  obtain ⟨shape, ringR, addF, zeroIn, negF, smulF, additive, law,111    rest⟩ := module112  exact law with r, v, w, *113114theorem add_smul (r s : R) (v : M)115  shows (r + s) • v = r • v + s • v116proof117  obtain ⟨shape, ringR, addF, zeroIn, negF, smulF, additive, smulAdd, law,118    rest⟩ := module119  exact law with r, s, v, *120121theorem mul_smul (r s : R) (v : M)122  shows (r * s) • v = r • s • v123proof124  obtain ⟨shape, ringR, addF, zeroIn, negF, smulF, additive, smulAdd, addSmul,125    law, oneSmul⟩ := module126  exact law with r, s, v, *127128theorem one_smul (v : M)129  shows R.one • v = v130proof131  obtain ⟨shape, ringR, addF, zeroIn, negF, smulF, additive, smulAdd, addSmul,132    mulSmul, law⟩ := module133  exact law with v, *134135-- The additive laws, each a group law applied to M.additive.136theorem Module.add_comm (v w : M)137  shows v + w = w + v138proof139  have abelian := Module.additive.abelian_group with module140  have swap := mul_comm at M.additive, v, w with abelian, *141  module_additive at swap142  exact swap143144theorem Module.add_assoc (u v w : M)145  shows u + v + w = u + (v + w)146proof147  have group := Module.additive_group with *148  have assoc := mul_assoc at M.additive, u, v, w with group, *149  module_additive at assoc150  exact assoc151152theorem Module.zero_add (v : M)153  shows M.zero + v = v154proof155  have group := Module.additive_group with *156  have unit := one_mul at M.additive, v with group, *157  module_additive at unit158  exact unit159160theorem Module.add_zero (v : M)161  shows v + M.zero = v162proof163  have group := Module.additive_group with *164  have unit := mul_one at M.additive, v with group, *165  module_additive at unit166  exact unit167168theorem Module.neg_add (v : M)169  shows -v + v = M.zero170proof171  have group := Module.additive_group with *172  have cancel := Group.inv_mul at M.additive, v with group, *173  module_additive at cancel174  exact cancel175176theorem Module.eq_zero_of_add_self (v : M)177  requires doubled : v + v = v178  shows v = M.zero179proof180  have group := Module.additive_group with *181  have criterion := mul_self_eq_self at M.additive, v with group, *182  module_additive at criterion183  exact criterion.forward with doubled184185-- The action at the ring's zero and at the module's zero.186theorem zero_smul (v : M)187  shows R.zero • v = M.zero188proof189  have zeroAdd : R.zero + R.zero = R.zero :=190    IsRing.add_left_identity with (Ring.parts with ring), *191  have doubled : R.zero • v + R.zero • v = R.zero • v192    rw [← add_smul, zeroAdd]193  exact Module.eq_zero_of_add_self with *194195theorem smul_zero (r : R)196  shows r • M.zero = M.zero197proof198  have zeroAdd : M.zero + M.zero = M.zero := Module.zero_add with *199  have doubled : r • M.zero + r • M.zero = r • M.zero200    rw [← smul_add, zeroAdd]201  exact Module.eq_zero_of_add_self with *202203end ModuleLaws204205-- A ring is a module over itself: the ring's addition, zero, and negation206-- with its multiplication as the action.207def selfModule (R : Set) : Set :=208  Module.mk(Ring.carrier(R), Ring.add(R), Ring.zero(R), Ring.neg(R), Ring.mul(R))209210instance Ring.to_module (R : Set)211  requires ring : Ring(R)212  shows Module(selfModule(R), R)213proof214  have parts := Ring.parts with ring215  obtain ⟨addF, zeroIn, negF, mulF, oneIn⟩ := IsRing.typing_of_parts with parts216  have abelian := Ring.additive.abelian_group with ring217  rw Ring.additive.value at abelian218  have monoid := IsRing.multiplicative with parts219  have associative := IsMonoid.associative with monoid220  have distributive := IsRing.distributive with parts221  have smulAdd : ∀ r v w ∈ R, r * (v + w) = r * v + r * w222    intros r rIn v vIn w wIn223    obtain ⟨left, right⟩ := distributive with r, rIn, v, vIn, w, wIn224    exact left225  have addSmul : ∀ r s v ∈ R, (r + s) * v = r * v + s * v226    intros r rIn s sIn v vIn227    obtain ⟨left, right⟩ := distributive with r, rIn, s, sIn, v, vIn228    exact right229  have mulSmul : ∀ r s v ∈ R, r * s * v = r * (s * v)230    intros r rIn s sIn v vIn231    exact Associative.law with associative, rIn, sIn, vIn232  have oneSmul : ∀ v ∈ R, R.one * v = v233    intros v vIn234    exact IsMonoid.left_identity with monoid, vIn235  unfold selfModule236  exact Module.intro with ring, addF, zeroIn, negF, mulF, abelian, smulAdd,237    addSmul, mulSmul, oneSmul238