Skip to content
This repository was archived by the owner on Jul 24, 2024. It is now read-only.

Commit 8f66240

Browse files
Vierkantorcollaresericrbg
committed
feat(group_theory/group_action): define distrib_smul and smul_zero_class (#16123)
These are two new superclasses of `distrib_mul_action` that get rid of the `mul_action` part: * `smul_zero_class` is `has_smul` + `a • 0 = 0` * `distrib_smul` is `smul_zero_class` + `a • (x + y) = a • x + a • y`. The motivation for these classes is to instantiate `qsmul` on `splitting_field`: in general scalar multiplication with rational numbers is not a `distrib_mul_action` but it is a `distrib_smul`, and `distrib_smul` is sufficient to lift an action to the `splitting_field`. I set up both `distrib_mul_action` and `smul_with_zero` to be subclasses of the above classes, and unify `smul_zero` (depending on `distrib_mul_action`) and `smul_zero'` (depending on `smul_with_zero`) into one lemma. There are a few places where I need to help the elaborator because e.g. it's expecting `units.mk0 a ha • 0 = 0` (with `smul` coming from `distrib_mul_action`) and getting `a • 0 = 0` (with `smul` coming from `smul_zero_class`). Apparently having both the type and instance differ is too hard for the unifier. Because we don't have definitional eta for structures yet, setting up the inheritance is a bit more tricky than you might think; I added an `example` test case to ensure everything stays OK. Co-authored-by: Mauricio Collares <mauricio@collares.org> Co-authored-by: Eric Rodriguez <ericrboidi@gmail.com>
1 parent 249a9c9 commit 8f66240

25 files changed

Lines changed: 132 additions & 68 deletions

File tree

‎src/algebra/algebra/unitization.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -213,7 +213,7 @@ ext neg_zero.symm rfl
213213

214214
@[simp] lemma coe_smul [has_zero R] [has_zero S] [smul_with_zero S R] [has_smul S A]
215215
(r : S) (m : A) : (↑(r • m) : unitization R A) = r • m :=
216-
ext (smul_zero' _ _).symm rfl
216+
ext (smul_zero _).symm rfl
217217

218218
end
219219

‎src/algebra/category/Module/change_of_rings.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -70,7 +70,7 @@ def restrict_scalars {R : Type u₁} {S : Type u₂} [ring R] [ring S] (f : R
7070
@[simp] lemma restrict_scalars.smul_def {R : Type u₁} {S : Type u₂} [ring R] [ring S] (f : R →+* S)
7171
{M : Module.{v} S} (r : R) (m : (restrict_scalars f).obj M) : r • m = (f r • m : M) := rfl
7272

73-
@[simp] lemma restrict_scalars.smul_def' {R : Type u₁} {S : Type u₂} [ring R] [ring S] (f : R →+* S)
73+
lemma restrict_scalars.smul_def' {R : Type u₁} {S : Type u₂} [ring R] [ring S] (f : R →+* S)
7474
{M : Module.{v} S} (r : R) (m : M) : (r • m : (restrict_scalars f).obj M) = (f r • m : M) := rfl
7575

7676
@[priority 100]

‎src/algebra/module/pi.lean‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -28,14 +28,14 @@ lemma _root_.is_smul_regular.pi {α : Type*} [Π i, has_smul α $ f i] {k : α}
2828
instance smul_with_zero (α) [has_zero α]
2929
[Π i, has_zero (f i)] [Π i, smul_with_zero α (f i)] :
3030
smul_with_zero α (Π i, f i) :=
31-
{ smul_zero := λ _, funext $ λ _, smul_zero' (f _) _,
31+
{ smul_zero := λ _, funext $ λ _, smul_zero _,
3232
zero_smul := λ _, funext $ λ _, zero_smul _ _,
3333
..pi.has_smul }
3434

3535
instance smul_with_zero' {g : I → Type*} [Π i, has_zero (g i)]
3636
[Π i, has_zero (f i)] [Π i, smul_with_zero (g i) (f i)] :
3737
smul_with_zero (Π i, g i) (Π i, f i) :=
38-
{ smul_zero := λ _, funext $ λ _, smul_zero' (f _) _,
38+
{ smul_zero := λ _, funext $ λ _, smul_zero _,
3939
zero_smul := λ _, funext $ λ _, zero_smul _ _,
4040
..pi.has_smul' }
4141

‎src/algebra/module/prod.lean‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -18,13 +18,13 @@ namespace prod
1818

1919
instance smul_with_zero [has_zero R] [has_zero M] [has_zero N]
2020
[smul_with_zero R M] [smul_with_zero R N] : smul_with_zero R (M × N) :=
21-
{ smul_zero := λ r, prod.ext (smul_zero' _ _) (smul_zero' _ _),
21+
{ smul_zero := λ r, prod.ext (smul_zero _) (smul_zero _),
2222
zero_smul := λ ⟨m, n⟩, prod.ext (zero_smul _ _) (zero_smul _ _),
2323
..prod.has_smul }
2424

2525
instance mul_action_with_zero [monoid_with_zero R] [has_zero M] [has_zero N]
2626
[mul_action_with_zero R M] [mul_action_with_zero R N] : mul_action_with_zero R (M × N) :=
27-
{ smul_zero := λ r, prod.ext (smul_zero' _ _) (smul_zero' _ _),
27+
{ smul_zero := λ r, prod.ext (smul_zero _) (smul_zero _),
2828
zero_smul := λ ⟨m, n⟩, prod.ext (zero_smul _ _) (zero_smul _ _),
2929
..prod.mul_action }
3030

‎src/algebra/module/ulift.lean‎

Lines changed: 24 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -58,19 +58,34 @@ instance mul_action' [monoid R] [mul_action R M] :
5858
mul_action R (ulift M) :=
5959
{ smul := (•),
6060
mul_smul := λ r s ⟨f⟩, ext _ _ $ mul_smul _ _ _,
61-
one_smul := λ ⟨f⟩, ext _ _ $ one_smul _ _,
62-
..ulift.has_smul_left }
61+
one_smul := λ ⟨f⟩, ext _ _ $ one_smul _ _ }
62+
63+
instance smul_zero_class [has_zero M] [smul_zero_class R M] :
64+
smul_zero_class (ulift R) M :=
65+
{ smul_zero := λ _, smul_zero _,
66+
.. ulift.has_smul_left }
67+
68+
instance smul_zero_class' [has_zero M] [smul_zero_class R M] :
69+
smul_zero_class R (ulift M) :=
70+
{ smul_zero := λ c, by { ext, simp [smul_zero], } }
71+
72+
instance distrib_smul [add_zero_class M] [distrib_smul R M] :
73+
distrib_smul (ulift R) M :=
74+
{ smul_add := λ _, smul_add _ }
75+
76+
instance distrib_smul' [add_zero_class M] [distrib_smul R M] :
77+
distrib_smul R (ulift M) :=
78+
{ smul_add := λ c f g, by { ext, simp [smul_add], } }
6379

6480
instance distrib_mul_action [monoid R] [add_monoid M] [distrib_mul_action R M] :
6581
distrib_mul_action (ulift R) M :=
66-
{ smul_zero := λ _, smul_zero _,
67-
smul_add := λ _, smul_add _ }
82+
{ ..ulift.mul_action,
83+
..ulift.distrib_smul }
6884

6985
instance distrib_mul_action' [monoid R] [add_monoid M] [distrib_mul_action R M] :
7086
distrib_mul_action R (ulift M) :=
71-
{ smul_zero := λ c, by { ext, simp [smul_zero], },
72-
smul_add := λ c f g, by { ext, simp [smul_add], },
73-
..ulift.mul_action' }
87+
{ ..ulift.mul_action',
88+
..ulift.distrib_smul' }
7489

7590
instance mul_distrib_mul_action [monoid R] [monoid M] [mul_distrib_mul_action R M] :
7691
mul_distrib_mul_action (ulift R) M :=
@@ -85,13 +100,13 @@ instance mul_distrib_mul_action' [monoid R] [monoid M] [mul_distrib_mul_action R
85100

86101
instance smul_with_zero [has_zero R] [has_zero M] [smul_with_zero R M] :
87102
smul_with_zero (ulift R) M :=
88-
{ smul_zero := λ _, smul_zero' _ _,
103+
{ smul_zero := λ _, smul_zero _,
89104
zero_smul := zero_smul _,
90105
..ulift.has_smul_left }
91106

92107
instance smul_with_zero' [has_zero R] [has_zero M] [smul_with_zero R M] :
93108
smul_with_zero R (ulift M) :=
94-
{ smul_zero := λ _, ulift.ext _ _ $ smul_zero' _ _,
109+
{ smul_zero := λ _, ulift.ext _ _ $ smul_zero _,
95110
zero_smul := λ _, ulift.ext _ _ $ zero_smul _ _ }
96111

97112
instance mul_action_with_zero [monoid_with_zero R] [has_zero M] [mul_action_with_zero R M] :

‎src/algebra/order/module.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -99,7 +99,7 @@ end
9999
lemma smul_nonpos_of_nonpos_of_nonneg (hc : c ≤ 0) (ha : 0 ≤ a) : c • a ≤ 0 :=
100100
calc
101101
c • a ≤ c • 0 : smul_le_smul_of_nonpos ha hc
102-
... = 0 : smul_zero' M c
102+
... = 0 : smul_zero c
103103

104104
lemma smul_nonneg_of_nonpos_of_nonpos (hc : c ≤ 0) (ha : a ≤ 0) : 0 ≤ c • a :=
105105
@smul_nonpos_of_nonpos_of_nonneg k Mᵒᵈ _ _ _ _ _ _ hc ha

‎src/algebra/order/smul.lean‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -55,7 +55,7 @@ namespace order_dual
5555

5656
instance [has_zero R] [add_zero_class M] [h : smul_with_zero R M] : smul_with_zero R Mᵒᵈ :=
5757
{ zero_smul := λ m, order_dual.rec (zero_smul _) m,
58-
smul_zero := λ r, order_dual.rec (smul_zero' _) r,
58+
smul_zero := λ r, order_dual.rec smul_zero r,
5959
..order_dual.has_smul }
6060

6161
instance [monoid R] [mul_action R M] : mul_action R Mᵒᵈ :=
@@ -70,7 +70,7 @@ instance [monoid_with_zero R] [add_monoid M] [mul_action_with_zero R M] :
7070
instance [monoid_with_zero R] [add_monoid M] [distrib_mul_action R M] :
7171
distrib_mul_action R Mᵒᵈ :=
7272
{ smul_add := λ k a, order_dual.rec (λ a' b, order_dual.rec (smul_add _ _) b) a,
73-
smul_zero := λ r, order_dual.rec smul_zero r }
73+
smul_zero := λ r, order_dual.rec (@smul_zero _ M _ _) r }
7474

7575
instance [ordered_semiring R] [ordered_add_comm_monoid M] [smul_with_zero R M]
7676
[ordered_smul R M] :
@@ -97,7 +97,7 @@ begin
9797
end
9898

9999
lemma smul_nonneg (hc : 0 ≤ c) (ha : 0 ≤ a) : 0 ≤ c • a :=
100-
calc (0 : M) = c • (0 : M) : (smul_zero' M c).symm
100+
calc (0 : M) = c • (0 : M) : (smul_zero c).symm
101101
... ≤ c • a : smul_le_smul_of_nonneg ha hc
102102

103103
lemma smul_nonpos_of_nonneg_of_nonpos (hc : 0 ≤ c) (ha : a ≤ 0) : c • a ≤ 0 :=
@@ -115,7 +115,7 @@ lemma smul_lt_smul_iff_of_pos (hc : 0 < c) : c • a < c • b ↔ a < b :=
115115
⟨λ h, lt_of_smul_lt_smul_of_nonneg h hc.le, λ h, smul_lt_smul_of_pos h hc⟩
116116

117117
lemma smul_pos_iff_of_pos (hc : 0 < c) : 0 < c • a ↔ 0 < a :=
118-
calc 0 < c • a ↔ c • 0 < c • a : by rw smul_zero'
118+
calc 0 < c • a ↔ c • 0 < c • a : by rw smul_zero
119119
... ↔ 0 < a : smul_lt_smul_iff_of_pos hc
120120

121121
alias smul_pos_iff_of_pos ↔ _ smul_pos

‎src/algebra/smul_with_zero.lean‎

Lines changed: 4 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -42,8 +42,7 @@ variables (R M)
4242
/-- `smul_with_zero` is a class consisting of a Type `R` with `0 ∈ R` and a scalar multiplication
4343
of `R` on a Type `M` with `0`, such that the equality `r • m = 0` holds if at least one among `r`
4444
or `m` equals `0`. -/
45-
class smul_with_zero [has_zero R] [has_zero M] extends has_smul R M :=
46-
(smul_zero : ∀ r : R, r • (0 : M) = 0)
45+
class smul_with_zero [has_zero R] [has_zero M] extends smul_zero_class R M :=
4746
(zero_smul : ∀ m : M, (0 : R) • m = 0)
4847

4948
instance mul_zero_class.to_smul_with_zero [mul_zero_class R] : smul_with_zero R R :=
@@ -61,10 +60,6 @@ variables (R) {M} [has_zero R] [has_zero M] [smul_with_zero R M]
6160

6261
@[simp] lemma zero_smul (m : M) : (0 : R) • m = 0 := smul_with_zero.zero_smul m
6362

64-
variables {R} (M)
65-
/-- Note that this lemma has different typeclass assumptions to `smul_zero`. -/
66-
@[simp] lemma smul_zero' (r : R) : r • (0 : M) = 0 := smul_with_zero.smul_zero r
67-
6863
variables {R M} [has_zero R'] [has_zero M'] [has_smul R M']
6964

7065
/-- Pullback a `smul_with_zero` structure along an injective zero-preserving homomorphism.
@@ -85,7 +80,7 @@ protected def function.surjective.smul_with_zero
8580
smul_with_zero R M' :=
8681
{ smul := (•),
8782
zero_smul := λ m, by { rcases hf m with ⟨x, rfl⟩, simp [←smul] },
88-
smul_zero := λ c, by simp only [← f.map_zero, ← smul, smul_zero'] }
83+
smul_zero := λ c, by simp only [← f.map_zero, ← smul, smul_zero] }
8984

9085
variables (M)
9186

@@ -172,7 +167,7 @@ begin
172167
obtain rfl | hc := eq_or_ne c 0,
173168
{ simp only [inv_zero, zero_smul] },
174169
obtain rfl | hx := eq_or_ne x 0,
175-
{ simp only [inv_zero, smul_zero'] },
170+
{ simp only [inv_zero, smul_zero] },
176171
{ refine inv_eq_of_mul_eq_one_left _,
177172
rw [smul_mul_smul, inv_mul_cancel hc, inv_mul_cancel hx, one_smul] }
178173
end
@@ -184,5 +179,5 @@ end group_with_zero
184179
def smul_monoid_with_zero_hom {α β : Type*} [monoid_with_zero α] [mul_zero_one_class β]
185180
[mul_action_with_zero α β] [is_scalar_tower α β β] [smul_comm_class α β β] :
186181
α × β →*₀ β :=
187-
{ map_zero' := smul_zero' _ _,
182+
{ map_zero' := smul_zero _,
188183
.. smul_monoid_hom }

‎src/algebra/triv_sq_zero_ext.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -209,7 +209,7 @@ ext neg_zero.symm rfl
209209

210210
@[simp] lemma inr_smul [has_zero R] [has_zero S] [smul_with_zero S R] [has_smul S M]
211211
(r : S) (m : M) : (inr (r • m) : tsze R M) = r • inr m :=
212-
ext (smul_zero' _ _).symm rfl
212+
ext (smul_zero _).symm rfl
213213

214214
end
215215

‎src/analysis/convex/star.lean‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -301,9 +301,9 @@ lemma star_convex_zero_iff :
301301
star_convex 𝕜 0 s ↔ ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃a : 𝕜⦄, 0 ≤ a → a ≤ 1 → a • x ∈ s :=
302302
begin
303303
refine forall_congr (λ x, forall_congr $ λ hx, ⟨λ h a ha₀ ha₁, _, λ h a b ha hb hab, _⟩),
304-
{ simpa only [sub_add_cancel, eq_self_iff_true, forall_true_left, zero_add, smul_zero'] using
304+
{ simpa only [sub_add_cancel, eq_self_iff_true, forall_true_left, zero_add, smul_zero] using
305305
h (sub_nonneg_of_le ha₁) ha₀ },
306-
{ rw [smul_zero', zero_add],
306+
{ rw [smul_zero, zero_add],
307307
exact h hb (by { rw ←hab, exact le_add_of_nonneg_left ha }) }
308308
end
309309

0 commit comments

Comments
 (0)