-
Notifications
You must be signed in to change notification settings - Fork 298
/
prod.lean
133 lines (102 loc) · 5.44 KB
/
prod.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
/-
Copyright (c) 2018 Simon Hudon. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Simon Hudon, Patrick Massot, Eric Wieser
-/
import algebra.group.prod
import group_theory.group_action.defs
/-!
# Prod instances for additive and multiplicative actions
This file defines instances for binary product of additive and multiplicative actions and provides
scalar multiplication as a homomorphism from `α × β` to `β`.
## Main declarations
* `smul_mul_hom`/`smul_monoid_hom`: Scalar multiplication bundled as a multiplicative/monoid
homomorphism.
## See also
* `group_theory.group_action.option`
* `group_theory.group_action.pi`
* `group_theory.group_action.sigma`
* `group_theory.group_action.sum`
-/
variables {M N P E α β : Type*}
namespace prod
section
variables [has_smul M α] [has_smul M β] [has_smul N α] [has_smul N β] (a : M) (x : α × β)
@[to_additive prod.has_vadd] instance : has_smul M (α × β) := ⟨λa p, (a • p.1, a • p.2)⟩
@[simp, to_additive] theorem smul_fst : (a • x).1 = a • x.1 := rfl
@[simp, to_additive] theorem smul_snd : (a • x).2 = a • x.2 := rfl
@[simp, to_additive] theorem smul_mk (a : M) (b : α) (c : β) : a • (b, c) = (a • b, a • c) := rfl
@[to_additive] theorem smul_def (a : M) (x : α × β) : a • x = (a • x.1, a • x.2) := rfl
@[simp, to_additive] theorem smul_swap : (a • x).swap = a • x.swap := rfl
variables [has_pow α E] [has_pow β E]
@[to_additive has_smul] instance has_pow : has_pow (α × β) E :=
{ pow := λ p c, (p.1 ^ c, p.2 ^ c) }
@[simp, to_additive smul_snd, to_additive_reorder 6]
lemma pow_fst (p : α × β) (c : E) : (p ^ c).fst = p.fst ^ c := rfl
@[simp, to_additive smul_snd, to_additive_reorder 6]
lemma pow_snd (p : α × β) (c : E) : (p ^ c).snd = p.snd ^ c := rfl
/- Note that the `c` arguments to this lemmas cannot be in the more natural right-most positions due
to limitations in `to_additive` and `to_additive_reorder`, which will silently fail to reorder more
than two adjacent arguments -/
@[simp, to_additive smul_mk, to_additive_reorder 6]
lemma pow_mk (c : E) (a : α) (b : β) : (prod.mk a b) ^ c = prod.mk (a ^ c) (b ^ c) := rfl
@[to_additive smul_def, to_additive_reorder 6]
lemma pow_def (p : α × β) (c : E) : p ^ c = (p.1 ^ c, p.2 ^ c) := rfl
@[simp, to_additive smul_swap, to_additive_reorder 6]
lemma pow_swap (p : α × β) (c : E) : (p ^ c).swap = p.swap ^ c := rfl
instance [has_smul M N] [is_scalar_tower M N α] [is_scalar_tower M N β] :
is_scalar_tower M N (α × β) :=
⟨λ x y z, mk.inj_iff.mpr ⟨smul_assoc _ _ _, smul_assoc _ _ _⟩⟩
@[to_additive] instance [smul_comm_class M N α] [smul_comm_class M N β] :
smul_comm_class M N (α × β) :=
{ smul_comm := λ r s x, mk.inj_iff.mpr ⟨smul_comm _ _ _, smul_comm _ _ _⟩ }
instance [has_smul Mᵐᵒᵖ α] [has_smul Mᵐᵒᵖ β] [is_central_scalar M α] [is_central_scalar M β] :
is_central_scalar M (α × β) :=
⟨λ r m, prod.ext (op_smul_eq_smul _ _) (op_smul_eq_smul _ _)⟩
@[to_additive]
instance has_faithful_smul_left [has_faithful_smul M α] [nonempty β] :
has_faithful_smul M (α × β) :=
⟨λ x y h, let ⟨b⟩ := ‹nonempty β› in eq_of_smul_eq_smul $ λ a : α, by injection h (a, b)⟩
@[to_additive]
instance has_faithful_smul_right [nonempty α] [has_faithful_smul M β] :
has_faithful_smul M (α × β) :=
⟨λ x y h, let ⟨a⟩ := ‹nonempty α› in eq_of_smul_eq_smul $ λ b : β, by injection h (a, b)⟩
end
@[to_additive]
instance smul_comm_class_both [has_mul N] [has_mul P] [has_smul M N] [has_smul M P]
[smul_comm_class M N N] [smul_comm_class M P P] :
smul_comm_class M (N × P) (N × P) :=
⟨λ c x y, by simp [smul_def, mul_def, mul_smul_comm]⟩
instance is_scalar_tower_both [has_mul N] [has_mul P] [has_smul M N] [has_smul M P]
[is_scalar_tower M N N] [is_scalar_tower M P P] :
is_scalar_tower M (N × P) (N × P) :=
⟨λ c x y, by simp [smul_def, mul_def, smul_mul_assoc]⟩
@[to_additive] instance {m : monoid M} [mul_action M α] [mul_action M β] : mul_action M (α × β) :=
{ mul_smul := λ a₁ a₂ p, mk.inj_iff.mpr ⟨mul_smul _ _ _, mul_smul _ _ _⟩,
one_smul := λ ⟨b, c⟩, mk.inj_iff.mpr ⟨one_smul _ _, one_smul _ _⟩ }
instance {R M N : Type*} {r : monoid R} [add_monoid M] [add_monoid N]
[distrib_mul_action R M] [distrib_mul_action R N] : distrib_mul_action R (M × N) :=
{ smul_add := λ a p₁ p₂, mk.inj_iff.mpr ⟨smul_add _ _ _, smul_add _ _ _⟩,
smul_zero := λ a, mk.inj_iff.mpr ⟨smul_zero _, smul_zero _⟩ }
instance {R M N : Type*} {r : monoid R} [monoid M] [monoid N]
[mul_distrib_mul_action R M] [mul_distrib_mul_action R N] : mul_distrib_mul_action R (M × N) :=
{ smul_mul := λ a p₁ p₂, mk.inj_iff.mpr ⟨smul_mul' _ _ _, smul_mul' _ _ _⟩,
smul_one := λ a, mk.inj_iff.mpr ⟨smul_one _, smul_one _⟩ }
end prod
/-! ### Scalar multiplication as a homomorphism -/
section bundled_smul
/-- Scalar multiplication as a multiplicative homomorphism. -/
@[simps]
def smul_mul_hom [monoid α] [has_mul β] [mul_action α β] [is_scalar_tower α β β]
[smul_comm_class α β β] :
(α × β) →ₙ* β :=
{ to_fun := λ a, a.1 • a.2,
map_mul' := λ a b, (smul_mul_smul _ _ _ _).symm }
/-- Scalar multiplication as a monoid homomorphism. -/
@[simps]
def smul_monoid_hom [monoid α] [mul_one_class β] [mul_action α β] [is_scalar_tower α β β]
[smul_comm_class α β β] :
α × β →* β :=
{ map_one' := one_smul _ _,
.. smul_mul_hom }
end bundled_smul