← Verification

.lake/packages/mathlib/Mathlib/Algebra/Module/Submodule/Defs.lean

Download original source

Read-only source copy. Line numbers are navigation aids.

1/-
2Copyright (c) 2015 Nathaniel Thomas. All rights reserved.
3Released under Apache 2.0 license as described in the file LICENSE.
4Authors: Nathaniel Thomas, Jeremy Avigad, Johannes Hölzl, Mario Carneiro
5-/
6module
7
8public import Mathlib.Algebra.Group.Subgroup.Defs
9public import Mathlib.GroupTheory.GroupAction.SubMulAction
10public import Mathlib.Algebra.Group.Submonoid.Basic
11
12/-!
13
14# Submodules of a module
15
16In this file we define
17
18* `Submodule R M` : a subset of a `Module` `M` that contains zero and is closed with respect to
19 addition and scalar multiplication.
20
21* `Subspace k M` : an abbreviation for `Submodule` assuming that `k` is a `Field`.
22
23## Tags
24
25submodule, subspace, linear map
26-/
27
28@[expose] public section
29
30assert_not_exists DivisionRing
31
32open Function
33
34universe u'' u' u v w
35
36variable {G : Type u''} {S : Type u'} {R : Type u} {M : Type v}
37
38/-- A submodule of a module is one which is closed under vector operations.
39 This is a sufficient condition for the subset of vectors in the submodule
40 to themselves form a module. -/
41structure Submodule (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] [Module R M] : Type v
42 extends AddSubmonoid M, SubMulAction R M
43
44/-- Reinterpret a `Submodule` as an `AddSubmonoid`. -/
45add_decl_doc Submodule.toAddSubmonoid
46
47/-- Reinterpret a `Submodule` as a `SubMulAction`. -/
48add_decl_doc Submodule.toSubMulAction
49
50namespace Submodule
51
52variable [Semiring R] [AddCommMonoid M] [Module R M]
53
54instance setLike : SetLike (Submodule R M) M where
55 coe s := s.carrier
56 coe_injective p q h := by cases p; cases q; congr; exact SetLike.coe_injective h
57
58instance : PartialOrder (Submodule R M) := .ofSetLike (Submodule R M) M
59
60initialize_simps_projections Submodule (carrier → coe, as_prefix coe)
61
62@[simp] lemma carrier_eq_coe (s : Submodule R M) : s.carrier = s := rfl
63
64/-- The actual `Submodule` obtained from an element of a `SMulMemClass` and `AddSubmonoidClass`. -/
65@[simps]
66def ofClass {S R M : Type*} [Semiring R] [AddCommMonoid M] [Module R M] [SetLike S M]
67 [AddSubmonoidClass S M] [SMulMemClass S R M] (s : S) : Submodule R M where
68 carrier := s
69 add_mem' := add_mem
70 zero_mem' := zero_mem _
71 smul_mem' := SMulMemClass.smul_mem
72
73/-- Construct a submodule from closure under two-element linear combinations.
74I.e., a nonempty set closed under two-element linear combinations is a submodule. -/
75@[simps]
76def ofLinearComb (C : Set M) (nonempty : C.Nonempty)
77 (linearComb : ∀ x ∈ C, ∀ y ∈ C, ∀ a b : R, a • x + b • y ∈ C) :
78 Submodule R M where
79 carrier := C
80 zero_mem' := by
81 obtain ⟨x, hx⟩ := nonempty
82 simpa [zero_smul, add_zero] using linearComb x hx x hx 0 0
83 add_mem' {x y} hx hy := by simpa [one_smul] using linearComb x hx y hy 1 1
84 smul_mem' c x hx := by simpa using linearComb x hx x hx c 0
85
86instance (priority := 100) : CanLift (Set M) (Submodule R M) (↑)
87 (fun s ↦ 0 ∈ s ∧ (∀ {x y}, x ∈ s → y ∈ s → x + y ∈ s) ∧ ∀ (r : R) {x}, x ∈ s → r • x ∈ s) where
88 prf s h :=
89 ⟨ { carrier := s
90 zero_mem' := h.1
91 add_mem' := h.2.1
92 smul_mem' := h.2.2 },
93 rfl ⟩
94
95instance addSubmonoidClass : AddSubmonoidClass (Submodule R M) M where
96 zero_mem _ := AddSubmonoid.zero_mem' _
97 add_mem := AddSubsemigroup.add_mem' _
98
99instance smulMemClass : SMulMemClass (Submodule R M) R M where
100 smul_mem {s} c _ h := SubMulAction.smul_mem' s.toSubMulAction c h
101
102@[simp]
103theorem mem_toAddSubmonoid (p : Submodule R M) (x : M) : x ∈ p.toAddSubmonoid ↔ x ∈ p :=
104 Iff.rfl
105
106variable {p q : Submodule R M}
107
108@[simp]
109theorem mem_mk {S : AddSubmonoid M} {x : M} (h) : x ∈ (⟨S, h⟩ : Submodule R M) ↔ x ∈ S :=
110 Iff.rfl
111
112@[simp]
113theorem coe_set_mk (S : AddSubmonoid M) (h) : ((⟨S, h⟩ : Submodule R M) : Set M) = S :=
114 rfl
115
116@[simp] theorem eta (h) : ({ p with smul_mem' := h } : Submodule R M) = p :=
117 rfl
118
119@[simp]
120theorem mk_le_mk {S S' : AddSubmonoid M} (h h') :
121 (⟨S, h⟩ : Submodule R M) ≤ (⟨S', h'⟩ : Submodule R M) ↔ S ≤ S' :=
122 Iff.rfl
123
124@[ext]
125theorem ext (h : ∀ x, x ∈ p ↔ x ∈ q) : p = q :=
126 SetLike.ext h
127
128/-- Copy of a submodule with a new `carrier` equal to the old one. Useful to fix definitional
129equalities. -/
130@[simps]
131protected def copy (p : Submodule R M) (s : Set M) (hs : s = ↑p) : Submodule R M where
132 carrier := s
133 zero_mem' := by simp [hs]
134 add_mem' := hs.symm ▸ p.add_mem'
135 smul_mem' := by simpa [hs] using p.smul_mem'
136
137theorem copy_eq (S : Submodule R M) (s : Set M) (hs : s = ↑S) : S.copy s hs = S :=
138 SetLike.coe_injective hs
139
140theorem toAddSubmonoid_injective : Injective (toAddSubmonoid : Submodule R M → AddSubmonoid M) :=
141 fun p q h => SetLike.ext'_iff.2 (show (p.toAddSubmonoid : Set M) = q from SetLike.ext'_iff.1 h)
142
143@[simp]
144theorem toAddSubmonoid_inj : p.toAddSubmonoid = q.toAddSubmonoid ↔ p = q :=
145 toAddSubmonoid_injective.eq_iff
146
147@[simp]
148theorem coe_toAddSubmonoid (p : Submodule R M) : (p.toAddSubmonoid : Set M) = p :=
149 rfl
150
151theorem toSubMulAction_injective : Injective (toSubMulAction : Submodule R M → SubMulAction R M) :=
152 fun p q h => SetLike.ext'_iff.2 (show (p.toSubMulAction : Set M) = q from SetLike.ext'_iff.1 h)
153
154theorem toSubMulAction_inj : p.toSubMulAction = q.toSubMulAction ↔ p = q :=
155 toSubMulAction_injective.eq_iff
156
157@[simp]
158theorem coe_toSubMulAction (p : Submodule R M) : (p.toSubMulAction : Set M) = p :=
159 rfl
160
161/-- `Submodule R M` almost never has decidable equality.
162Given an element `m ≠ 0` in `M`, `Submodule R M` has decidable equality iff
163all propositions are decidable. We add a global instance that `Submodule R M` has decidable
164equality, coming from the choice axiom, so that we don't have to provide
165`[DecidableEq (Submodule R M)]` arguments in lemma statements. -/
166noncomputable instance decidableEq : DecidableEq (Submodule R M) := Classical.typeDecidableEq _
167
168end Submodule
169
170namespace SMulMemClass
171
172variable [Semiring R] [AddCommMonoid M] [Module R M] {A : Type*} [SetLike A M]
173 [AddSubmonoidClass A M] [SMulMemClass A R M] (S' : A)
174
175-- Prefer subclasses of `Module` over `SMulMemClass`.
176/-- A submodule of a `Module` is a `Module`. -/
177instance (priority := 75) toModule : Module R S' := fast_instance%
178 Subtype.coe_injective.module R (AddSubmonoidClass.subtype S') (SetLike.val_smul S')
179
180/-- This can't be an instance because Lean wouldn't know how to find `R`, but we can still use
181this to manually derive `Module` on specific types. -/
182@[instance_reducible]
183def toModule' (S R' R A : Type*) [Semiring R] [NonUnitalNonAssocSemiring A]
184 [Module R A] [Semiring R'] [SMul R' R] [Module R' A] [IsScalarTower R' R A]
185 [SetLike S A] [AddSubmonoidClass S A] [SMulMemClass S R A] (s : S) :
186 Module R' s :=
187 haveI : SMulMemClass S R' A := SMulMemClass.ofIsScalarTower S R' R A
188 SMulMemClass.toModule s
189
190end SMulMemClass
191
192namespace Submodule
193
194section AddCommMonoid
195
196variable [Semiring R] [AddCommMonoid M]
197
198-- We can infer the module structure implicitly from the bundled submodule,
199-- rather than via typeclass resolution.
200variable {module_M : Module R M}
201variable {p : Submodule R M}
202variable {r : R} {x y : M}
203variable (p)
204
205theorem mem_carrier : x ∈ p.carrier ↔ x ∈ (p : Set M) :=
206 Iff.rfl
207
208protected theorem zero_mem : (0 : M) ∈ p :=
209 zero_mem _
210
211protected theorem add_mem (h₁ : x ∈ p) (h₂ : y ∈ p) : x + y ∈ p :=
212 add_mem h₁ h₂
213
214theorem smul_mem (r : R) (h : x ∈ p) : r • x ∈ p :=
215 p.smul_mem' r h
216
217theorem smul_of_tower_mem [SMul S R] [SMul S M] [IsScalarTower S R M] (r : S) (h : x ∈ p) :
218 r • x ∈ p :=
219 p.toSubMulAction.smul_of_tower_mem r h
220
221@[simp]
222theorem smul_mem_iff' [Group G] [MulAction G M] [SMul G R] [IsScalarTower G R M] (g : G) :
223 g • x ∈ p ↔ x ∈ p :=
224 p.toSubMulAction.smul_mem_iff' g
225
226@[simp]
227lemma smul_mem_iff'' [Invertible r] :
228 r • x ∈ p ↔ x ∈ p := by
229 refine ⟨fun h ↦ ?_, p.smul_mem r⟩
230 rw [← invOf_smul_smul r x]
231 exact p.smul_mem _ h
232
233lemma smul_mem_iff_of_isUnit (hr : IsUnit r) :
234 r • x ∈ p ↔ x ∈ p :=
235 let _ : Invertible r := hr.invertible
236 smul_mem_iff'' p
237
238instance add : Add p :=
239 ⟨fun x y => ⟨x.1 + y.1, add_mem x.2 y.2⟩⟩
240
241instance zero : Zero p :=
242 ⟨⟨0, zero_mem _⟩⟩
243
244instance inhabited : Inhabited p :=
245 ⟨0⟩
246
247instance smul [SMul S R] [SMul S M] [IsScalarTower S R M] : SMul S p :=
248 ⟨fun c x => ⟨c • x.1, smul_of_tower_mem _ c x.2⟩⟩
249
250instance isScalarTower [SMul S R] [SMul S M] [IsScalarTower S R M] : IsScalarTower S R p :=
251 p.toSubMulAction.isScalarTower
252
253instance isScalarTower' {S' : Type*} [SMul S R] [SMul S M] [SMul S' R] [SMul S' M] [SMul S S']
254 [IsScalarTower S' R M] [IsScalarTower S S' M] [IsScalarTower S R M] : IsScalarTower S S' p :=
255 p.toSubMulAction.isScalarTower'
256
257protected theorem nonempty : (p : Set M).Nonempty :=
258 ⟨0, p.zero_mem⟩
259
260@[simp]
261theorem mk_eq_zero {x} (h : x ∈ p) : (⟨x, h⟩ : p) = 0 ↔ x = 0 :=
262 Subtype.ext_iff
263
264variable {p}
265
266@[norm_cast]
267theorem coe_eq_zero {x : p} : (x : M) = 0 ↔ x = 0 :=
268 (SetLike.coe_eq_coe : (x : M) = (0 : p) ↔ x = 0)
269
270@[simp, norm_cast]
271theorem coe_add (x y : p) : (↑(x + y) : M) = ↑x + ↑y :=
272 rfl
273
274@[simp, norm_cast]
275theorem coe_zero : ((0 : p) : M) = 0 :=
276 rfl
277
278@[norm_cast]
279theorem coe_smul (r : R) (x : p) : ((r • x : p) : M) = r • (x : M) :=
280 rfl
281
282@[simp, norm_cast]
283theorem coe_smul_of_tower [SMul S R] [SMul S M] [IsScalarTower S R M] (r : S) (x : p) :
284 ((r • x : p) : M) = r • (x : M) :=
285 rfl
286
287@[norm_cast]
288theorem coe_mk (x : M) (hx : x ∈ p) : ((⟨x, hx⟩ : p) : M) = x :=
289 rfl
290
291theorem coe_mem (x : p) : (x : M) ∈ p :=
292 x.2
293
294variable (p)
295
296instance addCommMonoid : AddCommMonoid p := AddSubmonoidClass.toAddCommMonoid p
297
298instance module' [Semiring S] [SMul S R] [Module S M] [IsScalarTower S R M] :
299 Module S p := fast_instance%
300 { (show MulAction S p from p.toSubMulAction.mulAction') with
301 smul_zero := fun a => by ext; simp
302 zero_smul := fun a => by ext; simp
303 add_smul := fun a b x => by ext; simp [add_smul]
304 smul_add := fun a x y => by ext; simp [smul_add] }
305
306instance module : Module R p :=
307 p.module'
308
309end AddCommMonoid
310
311section AddCommGroup
312
313variable [Ring R] [AddCommGroup M]
314variable {module_M : Module R M}
315variable (p p' : Submodule R M)
316variable {x y : M}
317
318instance addSubgroupClass [Module R M] : AddSubgroupClass (Submodule R M) M :=
319 { Submodule.addSubmonoidClass with neg_mem := fun p {_} => p.toSubMulAction.neg_mem }
320
321protected theorem neg_mem (hx : x ∈ p) : -x ∈ p :=
322 neg_mem hx
323
324/-- Reinterpret a submodule as an additive subgroup. -/
325@[reducible]
326def toAddSubgroup : AddSubgroup M :=
327 { p.toAddSubmonoid with neg_mem' := fun {_} => p.neg_mem }
328
329@[simp]
330theorem coe_toAddSubgroup : (p.toAddSubgroup : Set M) = p :=
331 rfl
332
333theorem mem_toAddSubgroup : x ∈ p.toAddSubgroup ↔ x ∈ p :=
334 Iff.rfl
335
336theorem toAddSubgroup_injective : Injective (toAddSubgroup : Submodule R M → AddSubgroup M)
337 | _, _, h => SetLike.ext (SetLike.ext_iff.1 h :)
338
339theorem toAddSubgroup_inj : p.toAddSubgroup = p'.toAddSubgroup ↔ p = p' :=
340 toAddSubgroup_injective.eq_iff
341
342protected theorem sub_mem : x ∈ p → y ∈ p → x - y ∈ p :=
343 sub_mem
344
345protected theorem neg_mem_iff : -x ∈ p ↔ x ∈ p :=
346 neg_mem_iff
347
348protected theorem add_mem_iff_left : y ∈ p → (x + y ∈ p ↔ x ∈ p) :=
349 add_mem_cancel_right
350
351protected theorem add_mem_iff_right : x ∈ p → (x + y ∈ p ↔ y ∈ p) :=
352 add_mem_cancel_left
353
354protected theorem coe_neg (x : p) : ((-x : p) : M) = -x :=
355 NegMemClass.coe_neg _
356
357protected theorem coe_sub (x y : p) : (↑(x - y) : M) = ↑x - ↑y :=
358 AddSubgroupClass.coe_sub _ _
359
360theorem sub_mem_iff_left (hy : y ∈ p) : x - y ∈ p ↔ x ∈ p := by
361 rw [sub_eq_add_neg, p.add_mem_iff_left (p.neg_mem hy)]
362
363theorem sub_mem_iff_right (hx : x ∈ p) : x - y ∈ p ↔ y ∈ p := by
364 rw [sub_eq_add_neg, p.add_mem_iff_right hx, p.neg_mem_iff]
365
366instance addCommGroup : AddCommGroup p := AddSubgroupClass.toAddCommGroup p
367
368end AddCommGroup
369
370end Submodule
371
372namespace SubmoduleClass
373
374instance (priority := 75) module' {T : Type*} [Semiring R] [AddCommMonoid M] [Semiring S]
375 [Module R M] [SMul S R] [Module S M] [IsScalarTower S R M] [SetLike T M] [AddSubmonoidClass T M]
376 [SMulMemClass T R M] (t : T) : Module S t where
377 one_smul _ := by ext; simp
378 mul_smul _ _ _ := by ext; simp [mul_smul]
379 smul_zero _ := by ext; simp
380 zero_smul _ := by ext; simp
381 add_smul _ _ _ := by ext; simp [add_smul]
382 smul_add _ _ _ := by ext; simp [smul_add]
383
384instance (priority := 75) module [Semiring R] [AddCommMonoid M] [Module R M] [SetLike S M]
385 [AddSubmonoidClass S M] [SMulMemClass S R M] (s : S) : Module R s :=
386 module' s
387
388end SubmoduleClass