This repository was archived by the owner on Jul 24, 2024. It is now read-only.
basic.lean
1
/-
2
Copyright (c) 2018 Kenny Lau. All rights reserved.
3
Released under Apache 2.0 license as described in the file LICENSE.
4
Authors: Kenny Lau, Yury Kudryashov
6
import algebra.module.basic
7
import algebra.module.ulift
8
import algebra.ne_zero
9
import algebra.punit_instances
10
import algebra.ring.aut
11
import algebra.ring.ulift
12
import algebra.char_zero.lemmas
13
import linear_algebra.basic
14
import ring_theory.subring.basic
15
import tactic.abel
18
# Algebras over commutative semirings
20
> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
21
> Any changes to this file require a corresponding PR to mathlib4.
22
23
In this file we define associative unital `algebra`s over commutative (semi)rings, algebra
24
homomorphisms `alg_hom`, and algebra equivalences `alg_equiv`.
25
26
`subalgebra`s are defined in `algebra.algebra.subalgebra`.
28
For the category of `R`-algebras, denoted `Algebra R`, see the file
29
`algebra/category/Algebra/basic.lean`.
31
See the implementation notes for remarks about non-associative and non-unital algebras.
32
33
## Main definitions:
34
35
* `algebra R A`: the algebra typeclass.
36
* `algebra_map R A : R →+* A`: the canonical map from `R` to `A`, as a `ring_hom`. This is the
37
preferred spelling of this map, it is also available as:
38
* `algebra.linear_map R A : R →ₗ[R] A`, a `linear_map`.
39
* `algebra.of_id R A : R →ₐ[R] A`, an `alg_hom` (defined in a later file).
40
* Instances of `algebra` in this file:
41
* `algebra.id`
42
* `algebra_nat`
43
* `algebra_int`
44
* `algebra_rat`
45
* `mul_opposite.algebra`
46
* `module.End.algebra`
47
48
## Implementation notes
49
50
Given a commutative (semi)ring `R`, there are two ways to define an `R`-algebra structure on a
51
(possibly noncommutative) (semi)ring `A`:
52
* By endowing `A` with a morphism of rings `R →+* A` denoted `algebra_map R A` which lands in the
53
center of `A`.
54
* By requiring `A` be an `R`-module such that the action associates and commutes with multiplication
55
as `r • (a₁ * a₂) = (r • a₁) * a₂ = a₁ * (r • a₂)`.
56
57
We define `algebra R A` in a way that subsumes both definitions, by extending `has_smul R A` and
58
requiring that this scalar action `r • x` must agree with left multiplication by the image of the
59
structure morphism `algebra_map R A r * x`.
60
61
As a result, there are two ways to talk about an `R`-algebra `A` when `A` is a semiring:
62
1. ```lean
63
variables [comm_semiring R] [semiring A]
64
variables [algebra R A]
65
```
66
2. ```lean
67
variables [comm_semiring R] [semiring A]
68
variables [module R A] [smul_comm_class R A A] [is_scalar_tower R A A]
69
```
71
The first approach implies the second via typeclass search; so any lemma stated with the second set
72
of arguments will automatically apply to the first set. Typeclass search does not know that the
73
second approach implies the first, but this can be shown with:
74
```lean
75
example {R A : Type*} [comm_semiring R] [semiring A]
76
[module R A] [smul_comm_class R A A] [is_scalar_tower R A A] : algebra R A :=
77
algebra.of_module smul_mul_assoc mul_smul_comm
78
```
79
80
The advantage of the first approach is that `algebra_map R A` is available, and `alg_hom R A B` and
81
`subalgebra R A` can be used. For concrete `R` and `A`, `algebra_map R A` is often definitionally
82
convenient.
83
84
The advantage of the second approach is that `comm_semiring R`, `semiring A`, and `module R A` can
85
all be relaxed independently; for instance, this allows us to:
86
* Replace `semiring A` with `non_unital_non_assoc_semiring A` in order to describe non-unital and/or
87
non-associative algebras.
88
* Replace `comm_semiring R` and `module R A` with `comm_group R'` and `distrib_mul_action R' A`,
89
which when `R' = Rˣ` lets us talk about the "algebra-like" action of `Rˣ` on an
90
`R`-algebra `A`.
92
While `alg_hom R A B` cannot be used in the second approach, `non_unital_alg_hom R A B` still can.
93
94
You should always use the first approach when working with associative unital algebras, and mimic
95
the second approach only when you need to weaken a condition on either `R` or `A`.
96
99
universes u v w u₁ v₁
100
101
open_locale big_operators
103
section prio
104
-- We set this priority to 0 later in this file
105
set_option extends_priority 200 /- control priority of
106
`instance [algebra R A] : has_smul R A` -/
109
An associative unital `R`-algebra is a semiring `A` equipped with a map into its center `R → A`.
111
See the implementation notes in this file for discussion of the details of this definition.
113
@[nolint has_nonempty_instance]
114
class algebra (R : Type u) (A : Type v) [comm_semiring R] [semiring A]
115
extends has_smul R A, R →+* A :=
116
(commutes' : ∀ r x, to_fun r * x = x * to_fun r)
117
(smul_def' : ∀ r x, r • x = to_fun r * x)
118
end prio
120
/-- Embedding `R →+* A` given by `algebra` structure. -/
121
def algebra_map (R : Type u) (A : Type v) [comm_semiring R] [semiring A] [algebra R A] : R →+* A :=
122
algebra.to_ring_hom
124
namespace algebra_map
125
126
def has_lift_t (R A : Type*) [comm_semiring R] [semiring A] [algebra R A] :
127
has_lift_t R A := ⟨λ r, algebra_map R A r⟩
128
129
attribute [instance, priority 900] algebra_map.has_lift_t
130
131
section comm_semiring_semiring
132
133
variables {R A : Type*} [comm_semiring R] [semiring A] [algebra R A]
134
135
@[simp, norm_cast] lemma coe_zero : (↑(0 : R) : A) = 0 := map_zero (algebra_map R A)
136
@[simp, norm_cast] lemma coe_one : (↑(1 : R) : A) = 1 := map_one (algebra_map R A)
137
@[norm_cast] lemma coe_add (a b : R) : (↑(a + b : R) : A) = ↑a + ↑b :=
138
map_add (algebra_map R A) a b
139
@[norm_cast] lemma coe_mul (a b : R) : (↑(a * b : R) : A) = ↑a * ↑b :=
140
map_mul (algebra_map R A) a b
141
@[norm_cast] lemma coe_pow (a : R) (n : ℕ) : (↑(a ^ n : R) : A) = ↑a ^ n :=
142
map_pow (algebra_map R A) _ _
143
144
end comm_semiring_semiring
145
146
section comm_ring_ring
147
148
variables {R A : Type*} [comm_ring R] [ring A] [algebra R A]
149
150
@[norm_cast] lemma coe_neg (x : R) : (↑(-x : R) : A) = -↑x :=
151
map_neg (algebra_map R A) x
152
153
end comm_ring_ring
154
155
section comm_semiring_comm_semiring
156
157
variables {R A : Type*} [comm_semiring R] [comm_semiring A] [algebra R A]
158
159
open_locale big_operators
160
161
-- direct to_additive fails because of some mix-up with polynomials
162
@[norm_cast] lemma coe_prod {ι : Type*} {s : finset ι} (a : ι → R) :
163
(↑( ∏ (i : ι) in s, a i : R) : A) = ∏ (i : ι) in s, (↑(a i) : A) :=
164
map_prod (algebra_map R A) a s
165
166
-- to_additive fails for some reason
167
@[norm_cast] lemma coe_sum {ι : Type*} {s : finset ι} (a : ι → R) :
168
↑(( ∑ (i : ι) in s, a i)) = ∑ (i : ι) in s, (↑(a i) : A) :=
169
map_sum (algebra_map R A) a s
170
171
attribute [to_additive] coe_prod
172
173
end comm_semiring_comm_semiring
174
175
section field_nontrivial
176
variables {R A : Type*} [field R] [comm_semiring A] [nontrivial A] [algebra R A]
177
178
@[norm_cast, simp] lemma coe_inj {a b : R} : (↑a : A) = ↑b ↔ a = b :=
179
(algebra_map R A).injective.eq_iff
180
181
@[norm_cast, simp] lemma lift_map_eq_zero_iff (a : R) : (↑a : A) = 0 ↔ a = 0 :=
182
map_eq_zero_iff _ (algebra_map R A).injective
183
184
end field_nontrivial
185
186
section semifield_semidivision_ring
187
variables {R : Type*} (A : Type*) [semifield R] [division_semiring A] [algebra R A]
188
189
@[norm_cast] lemma coe_inv (r : R) : ↑(r⁻¹) = ((↑r)⁻¹ : A) :=
190
map_inv₀ (algebra_map R A) r
191
192
@[norm_cast] lemma coe_div (r s : R) : ↑(r / s) = (↑r / ↑s : A) :=
193
map_div₀ (algebra_map R A) r s
194
195
@[norm_cast] lemma coe_zpow (r : R) (z : ℤ) : ↑(r ^ z) = (↑r ^ z : A) :=
196
map_zpow₀ (algebra_map R A) r z
197
198
end semifield_semidivision_ring
199
200
section field_division_ring
201
variables (R A : Type*) [field R] [division_ring A] [algebra R A]
202
203
@[norm_cast] lemma coe_rat_cast (q : ℚ) : ↑(q : R) = (q : A) :=
204
map_rat_cast (algebra_map R A) q
205
206
end field_division_ring
207
208
end algebra_map
209
210
/-- Creating an algebra from a morphism to the center of a semiring. -/
211
def ring_hom.to_algebra' {R S} [comm_semiring R] [semiring S] (i : R →+* S)
212
(h : ∀ c x, i c * x = x * i c) :
213
algebra R S :=
214
{ smul := λ c x, i c * x,
215
commutes' := h,
216
smul_def' := λ c x, rfl,
217
to_ring_hom := i}
219
/-- Creating an algebra from a morphism to a commutative semiring. -/
220
def ring_hom.to_algebra {R S} [comm_semiring R] [comm_semiring S] (i : R →+* S) :
221
algebra R S :=
222
i.to_algebra' $ λ _, mul_comm _
223
224
lemma ring_hom.algebra_map_to_algebra {R S} [comm_semiring R] [comm_semiring S]
225
(i : R →+* S) :
226
@algebra_map R S _ _ i.to_algebra = i :=
227
rfl
228
229
namespace algebra
230
231
variables {R : Type u} {S : Type v} {A : Type w} {B : Type*}
233
/-- Let `R` be a commutative semiring, let `A` be a semiring with a `module R` structure.
234
If `(r • 1) * x = x * (r • 1) = r • x` for all `r : R` and `x : A`, then `A` is an `algebra`
235
over `R`.
236
237
See note [reducible non-instances]. -/
238
@[reducible]
239
def of_module' [comm_semiring R] [semiring A] [module R A]
240
(h₁ : ∀ (r : R) (x : A), (r • 1) * x = r • x)
241
(h₂ : ∀ (r : R) (x : A), x * (r • 1) = r • x) : algebra R A :=
242
{ to_fun := λ r, r • 1,
243
map_one' := one_smul _ _,
244
map_mul' := λ r₁ r₂, by rw [h₁, mul_smul],
245
map_zero' := zero_smul _ _,
246
map_add' := λ r₁ r₂, add_smul r₁ r₂ 1,
247
commutes' := λ r x, by simp only [h₁, h₂],
248
smul_def' := λ r x, by simp only [h₁] }
249
250
/-- Let `R` be a commutative semiring, let `A` be a semiring with a `module R` structure.
251
If `(r • x) * y = x * (r • y) = r • (x * y)` for all `r : R` and `x y : A`, then `A`
252
is an `algebra` over `R`.
253
254
See note [reducible non-instances]. -/
255
@[reducible]
256
def of_module [comm_semiring R] [semiring A] [module R A]
257
(h₁ : ∀ (r : R) (x y : A), (r • x) * y = r • (x * y))
258
(h₂ : ∀ (r : R) (x y : A), x * (r • y) = r • (x * y)) : algebra R A :=
259
of_module' (λ r x, by rw [h₁, one_mul]) (λ r x, by rw [h₂, mul_one])
261
section semiring
263
variables [comm_semiring R] [comm_semiring S]
264
variables [semiring A] [algebra R A] [semiring B] [algebra R B]
266
/-- We keep this lemma private because it picks up the `algebra.to_has_smul` instance
267
which we set to priority 0 shortly. See `smul_def` below for the public version. -/
268
private lemma smul_def'' (r : R) (x : A) : r • x = algebra_map R A r * x :=
269
algebra.smul_def' r x
270
271
/--
272
To prove two algebra structures on a fixed `[comm_semiring R] [semiring A]` agree,
273
it suffices to check the `algebra_map`s agree.
274
-/
275
-- We'll later use this to show `algebra ℤ M` is a subsingleton.
276
@[ext]
277
lemma algebra_ext {R : Type*} [comm_semiring R] {A : Type*} [semiring A] (P Q : algebra R A)
278
(w : ∀ (r : R), by { haveI := P, exact algebra_map R A r } =
279
by { haveI := Q, exact algebra_map R A r }) :
280
P = Q :=
281
begin
282
unfreezingI { rcases P with @⟨⟨P⟩⟩, rcases Q with @⟨⟨Q⟩⟩ },
283
congr,
284
{ funext r a,
285
replace w := congr_arg (λ s, s * a) (w r),
286
simp only [←smul_def''] at w,
287
apply w, },
288
{ ext r,
289
exact w r, },
290
{ apply proof_irrel_heq, },
291
{ apply proof_irrel_heq, },
292
end
293
294
@[priority 200] -- see Note [lower instance priority]
295
instance to_module : module R A :=
296
{ one_smul := by simp [smul_def''],
297
mul_smul := by simp [smul_def'', mul_assoc],
298
smul_add := by simp [smul_def'', mul_add],
299
smul_zero := by simp [smul_def''],
300
add_smul := by simp [smul_def'', add_mul],
301
zero_smul := by simp [smul_def''] }
302
303
-- From now on, we don't want to use the following instance anymore.
304
-- Unfortunately, leaving it in place causes deterministic timeouts later in mathlib.
305
attribute [instance, priority 0] algebra.to_has_smul
307
lemma smul_def (r : R) (x : A) : r • x = algebra_map R A r * x :=
308
algebra.smul_def' r x
310
lemma algebra_map_eq_smul_one (r : R) : algebra_map R A r = r • 1 :=
311
calc algebra_map R A r = algebra_map R A r * 1 : (mul_one _).symm
312
... = r • 1 : (algebra.smul_def r 1).symm
313
314
lemma algebra_map_eq_smul_one' : ⇑(algebra_map R A) = λ r, r • (1 : A) :=
315
funext algebra_map_eq_smul_one
316
317
/-- `mul_comm` for `algebra`s when one element is from the base ring. -/
318
theorem commutes (r : R) (x : A) : algebra_map R A r * x = x * algebra_map R A r :=
319
algebra.commutes' r x
321
/-- `mul_left_comm` for `algebra`s when one element is from the base ring. -/
322
theorem left_comm (x : A) (r : R) (y : A) :
323
x * (algebra_map R A r * y) = algebra_map R A r * (x * y) :=
324
by rw [← mul_assoc, ← commutes, mul_assoc]
326
/-- `mul_right_comm` for `algebra`s when one element is from the base ring. -/
327
theorem right_comm (x : A) (r : R) (y : A) :
328
(x * algebra_map R A r) * y = (x * y) * algebra_map R A r :=
329
by rw [mul_assoc, commutes, ←mul_assoc]
330
331
instance _root_.is_scalar_tower.right : is_scalar_tower R A A :=
332
⟨λ x y z, by rw [smul_eq_mul, smul_eq_mul, smul_def, smul_def, mul_assoc]⟩
333
334
/-- This is just a special case of the global `mul_smul_comm` lemma that requires less typeclass
335
search (and was here first). -/
336
@[simp] protected lemma mul_smul_comm (s : R) (x y : A) :
337
x * (s • y) = s • (x * y) :=
338
-- TODO: set up `is_scalar_tower.smul_comm_class` earlier so that we can actually prove this using
339
-- `mul_smul_comm s x y`.
340
by rw [smul_def, smul_def, left_comm]
341
342
/-- This is just a special case of the global `smul_mul_assoc` lemma that requires less typeclass
343
search (and was here first). -/
344
@[simp] protected lemma smul_mul_assoc (r : R) (x y : A) :
345
(r • x) * y = r • (x * y) :=
346
smul_mul_assoc r x y
348
@[simp]
349
lemma _root_.smul_algebra_map {α : Type*} [monoid α] [mul_distrib_mul_action α A]
350
[smul_comm_class α R A] (a : α) (r : R) : a • algebra_map R A r = algebra_map R A r :=
351
by rw [algebra_map_eq_smul_one, smul_comm a r (1 : A), smul_one]
352
354
variables {r : R} {a : A}
356
@[simp] lemma bit0_smul_one : bit0 r • (1 : A) = bit0 (r • (1 : A)) :=
357
by simp [bit0, add_smul]
358
lemma bit0_smul_one' : bit0 r • (1 : A) = r • 2 :=
359
by simp [bit0, add_smul, smul_add]
360
@[simp] lemma bit0_smul_bit0 : bit0 r • bit0 a = r • (bit0 (bit0 a)) :=
361
by simp [bit0, add_smul, smul_add]
362
@[simp] lemma bit0_smul_bit1 : bit0 r • bit1 a = r • (bit0 (bit1 a)) :=
363
by simp [bit0, add_smul, smul_add]
364
@[simp] lemma bit1_smul_one : bit1 r • (1 : A) = bit1 (r • (1 : A)) :=
365
by simp [bit1, add_smul]
366
lemma bit1_smul_one' : bit1 r • (1 : A) = r • 2 + 1 :=
367
by simp [bit1, bit0, add_smul, smul_add]
368
@[simp] lemma bit1_smul_bit0 : bit1 r • bit0 a = r • (bit0 (bit0 a)) + bit0 a :=
369
by simp [bit1, add_smul, smul_add]
370
@[simp] lemma bit1_smul_bit1 : bit1 r • bit1 a = r • (bit0 (bit1 a)) + bit1 a :=
371
by { simp only [bit0, bit1, add_smul, smul_add, one_smul], abel }
372
373
end
374
375
variables (R A)
376
377
/--
378
The canonical ring homomorphism `algebra_map R A : R →* A` for any `R`-algebra `A`,
379
packaged as an `R`-linear map.
380
-/
381
protected def linear_map : R →ₗ[R] A :=
382
{ map_smul' := λ x y, by simp [algebra.smul_def],
383
..algebra_map R A }
384
385
@[simp]
386
lemma linear_map_apply (r : R) : algebra.linear_map R A r = algebra_map R A r := rfl
387
388
lemma coe_linear_map : ⇑(algebra.linear_map R A) = algebra_map R A := rfl
389
390
instance id : algebra R R := (ring_hom.id R).to_algebra
391
392
variables {R A}
396
@[simp] lemma map_eq_id : algebra_map R R = ring_hom.id _ := rfl
397
398
lemma map_eq_self (x : R) : algebra_map R R x = x := rfl
400
@[simp] lemma smul_eq_mul (x y : R) : x • y = x * y := rfl
401
402
end id
404
section punit
405
406
instance _root_.punit.algebra : algebra R punit :=
407
{ to_fun := λ x, punit.star,
408
map_one' := rfl,
409
map_mul' := λ _ _, rfl,
410
map_zero' := rfl,
411
map_add' := λ _ _, rfl,
412
commutes' := λ _ _, rfl,
413
smul_def' := λ _ _, rfl }
414
415
@[simp] lemma algebra_map_punit (r : R) : algebra_map R punit r = punit.star := rfl
416
417
end punit
418
419
section ulift
420
421
instance _root_.ulift.algebra : algebra R (ulift A) :=
422
{ to_fun := λ r, ulift.up (algebra_map R A r),
423
commutes' := λ r x, ulift.down_injective $ algebra.commutes r x.down,
424
smul_def' := λ r x, ulift.down_injective $ algebra.smul_def' r x.down,
425
.. ulift.module',
426
.. (ulift.ring_equiv : ulift A ≃+* A).symm.to_ring_hom.comp (algebra_map R A) }
427
428
lemma _root_.ulift.algebra_map_eq (r : R) :
429
algebra_map R (ulift A) r = ulift.up (algebra_map R A r) := rfl
430
431
@[simp] lemma _root_.ulift.down_algebra_map (r : R) :
432
(algebra_map R (ulift A) r).down = algebra_map R A r := rfl
433
434
end ulift
435
436
/-- Algebra over a subsemiring. This builds upon `subsemiring.module`. -/
437
instance of_subsemiring (S : subsemiring R) : algebra S A :=
439
commutes' := λ r x, algebra.commutes r x,
440
smul_def' := λ r x, algebra.smul_def r x,
441
.. (algebra_map R A).comp S.subtype }
443
lemma algebra_map_of_subsemiring (S : subsemiring R) :
444
(algebra_map S R : S →+* R) = subsemiring.subtype S := rfl
445
446
lemma coe_algebra_map_of_subsemiring (S : subsemiring R) :
447
(algebra_map S R : S → R) = subtype.val := rfl
448
449
lemma algebra_map_of_subsemiring_apply (S : subsemiring R) (x : S) :
450
algebra_map S R x = x := rfl
451
452
/-- Algebra over a subring. This builds upon `subring.module`. -/
453
instance of_subring {R A : Type*} [comm_ring R] [ring A] [algebra R A]
454
(S : subring R) : algebra S A :=
455
{ smul := (•),
456
.. algebra.of_subsemiring S.to_subsemiring,
457
.. (algebra_map R A).comp S.subtype }
458
459
lemma algebra_map_of_subring {R : Type*} [comm_ring R] (S : subring R) :
460
(algebra_map S R : S →+* R) = subring.subtype S := rfl
461
462
lemma coe_algebra_map_of_subring {R : Type*} [comm_ring R] (S : subring R) :
463
(algebra_map S R : S → R) = subtype.val := rfl
464
465
lemma algebra_map_of_subring_apply {R : Type*} [comm_ring R] (S : subring R) (x : S) :
466
algebra_map S R x = x := rfl
468
/-- Explicit characterization of the submonoid map in the case of an algebra.
469
`S` is made explicit to help with type inference -/
470
def algebra_map_submonoid (S : Type*) [semiring S] [algebra R S]
471
(M : submonoid R) : submonoid S :=
472
M.map (algebra_map R S)
474
lemma mem_algebra_map_submonoid_of_mem {S : Type*} [semiring S] [algebra R S] {M : submonoid R}
475
(x : M) : (algebra_map R S x) ∈ algebra_map_submonoid S M :=
476
set.mem_image_of_mem (algebra_map R S) x.2
477
480
section comm_semiring
482
variables [comm_semiring R]
483
484
lemma mul_sub_algebra_map_commutes [ring A] [algebra R A] (x : A) (r : R) :
485
x * (x - algebra_map R A r) = (x - algebra_map R A r) * x :=
486
by rw [mul_sub, ←commutes, sub_mul]
487
488
lemma mul_sub_algebra_map_pow_commutes [ring A] [algebra R A] (x : A) (r : R) (n : ℕ) :
489
x * (x - algebra_map R A r) ^ n = (x - algebra_map R A r) ^ n * x :=
490
begin
491
induction n with n ih,
492
{ simp },
493
{ rw [pow_succ, ←mul_assoc, mul_sub_algebra_map_commutes, mul_assoc, ih, ←mul_assoc] }
496
end comm_semiring
497
498
section ring
499
variables [comm_ring R]
500
501
variables (R)
502
503
/-- A `semiring` that is an `algebra` over a commutative ring carries a natural `ring` structure.
504
See note [reducible non-instances]. -/
505
@[reducible]
506
def semiring_to_ring [semiring A] [algebra R A] : ring A :=
507
{ ..module.add_comm_monoid_to_add_comm_group R,
508
..(infer_instance : semiring A) }
509
510
end ring
511
512
end algebra
513
514
namespace mul_opposite
515
516
variables {R A : Type*} [comm_semiring R] [semiring A] [algebra R A]
517
518
instance : algebra R Aᵐᵒᵖ :=
519
{ to_ring_hom := (algebra_map R A).to_opposite $ λ x y, algebra.commutes _ _,
520
smul_def' := λ c x, unop_injective $
521
by { dsimp, simp only [op_mul, algebra.smul_def, algebra.commutes, op_unop] },
522
commutes' := λ r, mul_opposite.rec $ λ x, by dsimp; simp only [← op_mul, algebra.commutes],
523
.. mul_opposite.has_smul A R }
525
@[simp] lemma algebra_map_apply (c : R) : algebra_map R Aᵐᵒᵖ c = op (algebra_map R A c) := rfl
527
end mul_opposite
529
namespace module
530
variables (R : Type u) (M : Type v) [comm_semiring R] [add_comm_monoid M] [module R M]
532
instance : algebra R (module.End R M) :=
533
algebra.of_module smul_mul_assoc (λ r f g, (smul_comm r f g).symm)
535
lemma algebra_map_End_eq_smul_id (a : R) :
536
(algebra_map R (End R M)) a = a • linear_map.id := rfl
537
538
@[simp] lemma algebra_map_End_apply (a : R) (m : M) :
539
(algebra_map R (End R M)) a m = a • m := rfl
540
541
@[simp] lemma ker_algebra_map_End (K : Type u) (V : Type v)
542
[field K] [add_comm_group V] [module K V] (a : K) (ha : a ≠ 0) :
543
((algebra_map K (End K V)) a).ker = ⊥ :=
544
linear_map.ker_smul _ _ ha
545
546
section
547
548
variables {R M}
549
550
lemma End_is_unit_apply_inv_apply_of_is_unit {f : module.End R M} (h : is_unit f) (x : M) :
551
f (h.unit.inv x) = x :=
552
show (f * h.unit.inv) x = x, by simp
553
554
lemma End_is_unit_inv_apply_apply_of_is_unit {f : module.End R M} (h : is_unit f) (x : M) :
555
h.unit.inv (f x) = x :=
556
(by simp : (h.unit.inv * f) x = x)
557
558
lemma End_is_unit_iff (f : module.End R M) :
559
is_unit f ↔ function.bijective f :=
560
⟨λ h, function.bijective_iff_has_inverse.mpr $
561
⟨h.unit.inv, ⟨End_is_unit_inv_apply_apply_of_is_unit h,
562
End_is_unit_apply_inv_apply_of_is_unit h⟩⟩,
563
λ H, let e : M ≃ₗ[R] M := { ..f, ..(equiv.of_bijective f H)} in
564
⟨⟨_, e.symm, linear_map.ext e.right_inv, linear_map.ext e.left_inv⟩, rfl⟩⟩
565
566
lemma End_algebra_map_is_unit_inv_apply_eq_iff
567
{x : R} (h : is_unit (algebra_map R (module.End R M) x)) (m m' : M) :
568
h.unit⁻¹ m = m' ↔ m = x • m' :=
569
{ mp := λ H, ((congr_arg h.unit H).symm.trans (End_is_unit_apply_inv_apply_of_is_unit h _)).symm,
570
mpr := λ H, H.symm ▸
571
begin
572
apply_fun h.unit using ((module.End_is_unit_iff _).mp h).injective,
573
erw [End_is_unit_apply_inv_apply_of_is_unit],
574
refl,
575
end }
576
577
lemma End_algebra_map_is_unit_inv_apply_eq_iff'
578
{x : R} (h : is_unit (algebra_map R (module.End R M) x)) (m m' : M) :
579
m' = h.unit⁻¹ m ↔ m = x • m' :=
580
{ mp := λ H, ((congr_arg h.unit H).trans (End_is_unit_apply_inv_apply_of_is_unit h _)).symm,
581
mpr := λ H, H.symm ▸
582
begin
583
apply_fun h.unit using ((module.End_is_unit_iff _).mp h).injective,
584
erw [End_is_unit_apply_inv_apply_of_is_unit],
585
refl,
586
end }
587
588
end
589
590
end module
591
592
namespace linear_map
593
594
variables {R : Type*} {A : Type*} {B : Type*} [comm_semiring R] [semiring A] [semiring B]
595
[algebra R A] [algebra R B]
596
597
/-- An alternate statement of `linear_map.map_smul` for when `algebra_map` is more convenient to
598
work with than `•`. -/
599
lemma map_algebra_map_mul (f : A →ₗ[R] B) (a : A) (r : R) :
600
f (algebra_map R A r * a) = algebra_map R B r * f a :=
601
by rw [←algebra.smul_def, ←algebra.smul_def, map_smul]
602
603
lemma map_mul_algebra_map (f : A →ₗ[R] B) (a : A) (r : R) :
604
f (a * algebra_map R A r) = f a * algebra_map R B r :=
605
by rw [←algebra.commutes, ←algebra.commutes, map_algebra_map_mul]
606
607
end linear_map
608
609
section nat
610
611
variables {R : Type*} [semiring R]
612
613
-- Lower the priority so that `algebra.id` is picked most of the time when working with
614
-- `ℕ`-algebras. This is only an issue since `algebra.id` and `algebra_nat` are not yet defeq.
615
-- TODO: fix this by adding an `of_nat` field to semirings.
616
/-- Semiring ⥤ ℕ-Alg -/
617
@[priority 99] instance algebra_nat : algebra ℕ R :=
618
{ commutes' := nat.cast_commute,
619
smul_def' := λ _ _, nsmul_eq_mul _ _,
620
to_ring_hom := nat.cast_ring_hom R }
621
622
instance nat_algebra_subsingleton : subsingleton (algebra ℕ R) :=
623
⟨λ P Q, by { ext, simp, }⟩
624
625
end nat
626
627
namespace ring_hom
628
629
variables {R S : Type*}
630
631
-- note that `R`, `S` could be `semiring`s but this is useless mathematically speaking -
632
-- a ℚ-algebra is a ring. furthermore, this change probably slows down elaboration.
633
@[simp] lemma map_rat_algebra_map [ring R] [ring S] [algebra ℚ R] [algebra ℚ S]
634
(f : R →+* S) (r : ℚ) : f (algebra_map ℚ R r) = algebra_map ℚ S r :=
635
ring_hom.ext_iff.1 (subsingleton.elim (f.comp (algebra_map ℚ R)) (algebra_map ℚ S)) r
636
637
end ring_hom
638
641
instance algebra_rat {α} [division_ring α] [char_zero α] : algebra ℚ α :=
642
{ smul := (•),
643
smul_def' := division_ring.qsmul_eq_mul',
644
to_ring_hom := rat.cast_hom α,
645
commutes' := rat.cast_commute }
646
647
/-- The two `algebra ℚ ℚ` instances should coincide. -/
648
example : algebra_rat = algebra.id ℚ := rfl
650
@[simp] theorem algebra_map_rat_rat : algebra_map ℚ ℚ = ring_hom.id ℚ :=
651
subsingleton.elim _ _
652
653
instance algebra_rat_subsingleton {α} [semiring α] :
654
subsingleton (algebra ℚ α) :=
655
⟨λ x y, algebra.algebra_ext x y $ ring_hom.congr_fun $ subsingleton.elim _ _⟩
656
659
section int
660
661
variables (R : Type*) [ring R]
663
-- Lower the priority so that `algebra.id` is picked most of the time when working with
664
-- `ℤ`-algebras. This is only an issue since `algebra.id ℤ` and `algebra_int ℤ` are not yet defeq.
665
-- TODO: fix this by adding an `of_int` field to rings.
666
/-- Ring ⥤ ℤ-Alg -/
667
@[priority 99] instance algebra_int : algebra ℤ R :=
668
{ commutes' := int.cast_commute,
669
smul_def' := λ _ _, zsmul_eq_mul _ _,
670
to_ring_hom := int.cast_ring_hom R }
672
/-- A special case of `eq_int_cast'` that happens to be true definitionally -/
673
@[simp] lemma algebra_map_int_eq : algebra_map ℤ R = int.cast_ring_hom R := rfl
674
675
variables {R}
677
instance int_algebra_subsingleton : subsingleton (algebra ℤ R) :=
678
⟨λ P Q, by { ext, simp, }⟩
682
namespace no_zero_smul_divisors
683
684
variables {R A : Type*}
685
686
open algebra
687
688
/-- If `algebra_map R A` is injective and `A` has no zero divisors,
689
`R`-multiples in `A` are zero only if one of the factors is zero.
690
691
Cannot be an instance because there is no `injective (algebra_map R A)` typeclass.
692
-/
693
lemma of_algebra_map_injective
694
[comm_semiring R] [semiring A] [algebra R A] [no_zero_divisors A]
695
(h : function.injective (algebra_map R A)) : no_zero_smul_divisors R A :=
696
⟨λ c x hcx, (mul_eq_zero.mp ((smul_def c x).symm.trans hcx)).imp_left
697
(map_eq_zero_iff (algebra_map R A) h).mp⟩
698
699
variables (R A)
700
lemma algebra_map_injective [comm_ring R] [ring A] [nontrivial A]
701
[algebra R A] [no_zero_smul_divisors R A] :
702
function.injective (algebra_map R A) :=
703
suffices function.injective (λ (c : R), c • (1 : A)),
704
by { convert this, ext, rw [algebra.smul_def, mul_one] },
705
smul_left_injective R one_ne_zero
706
707
lemma _root_.ne_zero.of_no_zero_smul_divisors (n : ℕ) [comm_ring R] [ne_zero (n : R)] [ring A]
708
[nontrivial A] [algebra R A] [no_zero_smul_divisors R A] : ne_zero (n : A) :=
709
ne_zero.nat_of_injective $ no_zero_smul_divisors.algebra_map_injective R A
710
711
variables {R A}
712
lemma iff_algebra_map_injective [comm_ring R] [ring A] [is_domain A] [algebra R A] :
713
no_zero_smul_divisors R A ↔ function.injective (algebra_map R A) :=
714
⟨@@no_zero_smul_divisors.algebra_map_injective R A _ _ _ _,
715
no_zero_smul_divisors.of_algebra_map_injective⟩
716
717
@[priority 100] -- see note [lower instance priority]
718
instance char_zero.no_zero_smul_divisors_nat [semiring R] [no_zero_divisors R] [char_zero R] :
719
no_zero_smul_divisors ℕ R :=
720
no_zero_smul_divisors.of_algebra_map_injective $ (algebra_map ℕ R).injective_nat
721
722
@[priority 100] -- see note [lower instance priority]
723
instance char_zero.no_zero_smul_divisors_int [ring R] [no_zero_divisors R] [char_zero R] :
724
no_zero_smul_divisors ℤ R :=
725
no_zero_smul_divisors.of_algebra_map_injective $ (algebra_map ℤ R).injective_int
726
727
section field
728
729
variables [field R] [semiring A] [algebra R A]
730
731
@[priority 100] -- see note [lower instance priority]
732
instance algebra.no_zero_smul_divisors [nontrivial A] [no_zero_divisors A] :
733
no_zero_smul_divisors R A :=
734
no_zero_smul_divisors.of_algebra_map_injective (algebra_map R A).injective
735
736
end field
737
738
end no_zero_smul_divisors
739
740
section is_scalar_tower
741
742
variables {R : Type*} [comm_semiring R]
743
variables (A : Type*) [semiring A] [algebra R A]
744
variables {M : Type*} [add_comm_monoid M] [module A M] [module R M] [is_scalar_tower R A M]
745
variables {N : Type*} [add_comm_monoid N] [module A N] [module R N] [is_scalar_tower R A N]
746
747
lemma algebra_compatible_smul (r : R) (m : M) : r • m = ((algebra_map R A) r) • m :=
748
by rw [←(one_smul A m), ←smul_assoc, algebra.smul_def, mul_one, one_smul]
749
750
@[simp] lemma algebra_map_smul (r : R) (m : M) : ((algebra_map R A) r) • m = r • m :=
751
(algebra_compatible_smul A r m).symm
752
753
lemma int_cast_smul {k V : Type*} [comm_ring k] [add_comm_group V] [module k V] (r : ℤ) (x : V) :
754
(r : k) • x = r • x :=
755
algebra_map_smul k r x
756
757
lemma no_zero_smul_divisors.trans (R A M : Type*) [comm_ring R] [ring A] [is_domain A] [algebra R A]
758
[add_comm_group M] [module R M] [module A M] [is_scalar_tower R A M] [no_zero_smul_divisors R A]
759
[no_zero_smul_divisors A M] : no_zero_smul_divisors R M :=
760
begin
761
refine ⟨λ r m h, _⟩,
762
rw [algebra_compatible_smul A r m] at h,
763
cases smul_eq_zero.1 h with H H,
764
{ have : function.injective (algebra_map R A) :=
765
no_zero_smul_divisors.iff_algebra_map_injective.1 infer_instance,
766
left,
767
exact (injective_iff_map_eq_zero _).1 this _ H },
768
{ right,
769
exact H }
770
end
771
772
variable {A}
773
774
@[priority 100] -- see Note [lower instance priority]
775
instance is_scalar_tower.to_smul_comm_class : smul_comm_class R A M :=
776
⟨λ r a m, by rw [algebra_compatible_smul A r (a • m), smul_smul, algebra.commutes, mul_smul,
777
←algebra_compatible_smul]⟩
779
@[priority 100] -- see Note [lower instance priority]
780
instance is_scalar_tower.to_smul_comm_class' : smul_comm_class A R M :=
781
smul_comm_class.symm _ _ _
783
@[priority 200] -- see Note [lower instance priority]
784
instance algebra.to_smul_comm_class {R A} [comm_semiring R] [semiring A] [algebra R A] :
785
smul_comm_class R A A :=
786
is_scalar_tower.to_smul_comm_class
787
788
lemma smul_algebra_smul_comm (r : R) (a : A) (m : M) : a • r • m = r • a • m :=
789
smul_comm _ _ _
791
namespace linear_map
793
instance coe_is_scalar_tower : has_coe (M →ₗ[A] N) (M →ₗ[R] N) :=
794
⟨restrict_scalars R⟩
795
796
variables (R) {A M N}
797
798
@[simp, norm_cast squash] lemma coe_restrict_scalars_eq_coe (f : M →ₗ[A] N) :
799
(f.restrict_scalars R : M → N) = f := rfl
800
801
@[simp, norm_cast squash] lemma coe_coe_is_scalar_tower (f : M →ₗ[A] N) :
802
((f : M →ₗ[R] N) : M → N) = f := rfl
803
804
/-- `A`-linearly coerce a `R`-linear map from `M` to `A` to a function, given an algebra `A` over
805
a commutative semiring `R` and `M` a module over `R`. -/
806
def lto_fun (R : Type u) (M : Type v) (A : Type w)
807
[comm_semiring R] [add_comm_monoid M] [module R M] [comm_ring A] [algebra R A] :
808
(M →ₗ[R] A) →ₗ[A] (M → A) :=
809
{ to_fun := linear_map.to_fun,
810
map_add' := λ f g, rfl,
811
map_smul' := λ c f, rfl }
812
813
end linear_map
814
815
end is_scalar_tower
816
817
/-! TODO: The following lemmas no longer involve `algebra` at all, and could be moved closer
818
to `algebra/module/submodule.lean`. Currently this is tricky because `ker`, `range`, `⊤`, and `⊥`
819
are all defined in `linear_algebra/basic.lean`. -/
820
section module
821
open module
823
variables (R S M N : Type*) [semiring R] [semiring S] [has_smul R S]
824
variables [add_comm_monoid M] [module R M] [module S M] [is_scalar_tower R S M]
825
variables [add_comm_monoid N] [module R N] [module S N] [is_scalar_tower R S N]
827
variables {S M N}
829
@[simp]
830
lemma linear_map.ker_restrict_scalars (f : M →ₗ[S] N) :
831
(f.restrict_scalars R).ker = f.ker.restrict_scalars R :=
832
rfl
833
836
example {R A} [comm_semiring R] [semiring A]
837
[module R A] [smul_comm_class R A A] [is_scalar_tower R A A] : algebra R A :=
838
algebra.of_module smul_mul_assoc mul_smul_comm