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

Commit 32b08ef

Browse files
gebnergebner
committed
feat: add_monoid_with_one, add_group_with_one (#12182)
Adds two type classes `add_monoid_with_one R` and `add_group_with_one R` with operations for `ℕ → R` and `ℤ → R`, resp. The type classes extend `add_monoid` and `add_group` because those seem to be the weakest type classes where such a `+₀₁`-homomorphism is guaranteed to exist. The `nat.cast` function as well as `coe : ℕ → R` are implemented in terms of `add_monoid_with_one R`, removing the infamous `nat.cast` diamond. Fixes #946. Some lemmas are less general now because the algebraic hierarchy is not fine-grained enough, or because the lawful coercion only exists for monoids and above. This generality was not used in mathlib as far as I could tell. For example: - `char_p.char_p_to_char_zero` now requires a group instead of a left-cancellative monoid, because we don't have the `add_left_cancel_monoid_with_one` class - `nat.norm_cast_le` now requires a seminormed ring instead of a seminormed group, because we don't have `semi_normed_group_with_one`
1 parent 871fcd8 commit 32b08ef

202 files changed

Lines changed: 2147 additions & 1350 deletions

File tree

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

‎archive/100-theorems-list/16_abel_ruffini.lean‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -78,11 +78,11 @@ begin
7878
interval_cases n with hn;
7979
simp only [Φ, coeff_X_pow, coeff_C, int.coe_nat_dvd.mpr, hpb, if_true, coeff_C_mul, if_false,
8080
nat.zero_ne_bit1, eq_self_iff_true, coeff_X_zero, hpa, coeff_add, zero_add, mul_zero,
81-
int.nat_cast_eq_coe_nat, coeff_sub, sub_self, nat.one_ne_zero, add_zero, coeff_X_one, mul_one,
81+
coeff_sub, sub_self, nat.one_ne_zero, add_zero, coeff_X_one, mul_one,
8282
zero_sub, dvd_neg, nat.one_eq_bit1, bit0_eq_zero, neg_zero, nat.bit0_ne_bit1,
8383
dvd_mul_of_dvd_left, nat.bit1_eq_bit1, nat.one_ne_bit0, nat.bit1_ne_zero], },
8484
{ simp only [degree_Phi, ←with_bot.coe_zero, with_bot.coe_lt_coe, nat.succ_pos'] },
85-
{ rw [coeff_zero_Phi, span_singleton_pow, mem_span_singleton, int.nat_cast_eq_coe_nat],
85+
{ rw [coeff_zero_Phi, span_singleton_pow, mem_span_singleton],
8686
exact mt int.coe_nat_dvd.mp hp2b },
8787
all_goals { exact monic.is_primitive (monic_Phi a b) },
8888
end

‎archive/100-theorems-list/30_ballot_problem.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -502,7 +502,7 @@ begin
502502
{ apply ne_of_gt,
503503
norm_cast,
504504
linarith },
505-
field_simp [h₄, h₅, h₆],
505+
field_simp [h₄, h₅, h₆] at *,
506506
ring },
507507
all_goals { refine (ennreal.mul_lt_top (measure_lt_top _ _).ne _).ne,
508508
simp [ne.def, ennreal.div_eq_top] } }

‎archive/imo/imo2013_q5.lean‎

Lines changed: 5 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -209,15 +209,17 @@ begin
209209
{ exact (lt_irrefl 0 hn).elim },
210210
induction n with pn hpn,
211211
{ simp only [one_mul, nat.cast_one] },
212-
calc (↑pn + 1 + 1) * f x
213-
= ((pn : ℝ) + 1) * f x + 1 * f x : add_mul (↑pn + 1) 1 (f x)
212+
calc ↑(pn + 2) * f x
213+
= (↑pn + 1 + 1) * f x : by norm_cast
214+
... = ((pn : ℝ) + 1) * f x + 1 * f x : add_mul (↑pn + 1) 1 (f x)
214215
... = (↑pn + 1) * f x + f x : by rw one_mul
215216
... ≤ f ((↑pn.succ) * x) + f x : by exact_mod_cast add_le_add_right
216217
(hpn pn.succ_pos) (f x)
217218
... ≤ f ((↑pn + 1) * x + x) : by exact_mod_cast H2 _ _
218219
(mul_pos pn.cast_add_one_pos hx) hx
219220
... = f ((↑pn + 1) * x + 1 * x) : by rw one_mul
220-
... = f ((↑pn + 1 + 1) * x) : congr_arg f (add_mul (↑pn + 1) 1 x).symm },
221+
... = f ((↑pn + 1 + 1) * x) : congr_arg f (add_mul (↑pn + 1) 1 x).symm
222+
... = f (↑(pn + 2) * x) : by norm_cast },
221223
have H4 : ∀ n : ℕ, 0 < n → (n : ℝ) ≤ f n,
222224
{ intros n hn,
223225
have hf1 : 1 ≤ f 1,

‎archive/imo/imo2019_q4.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -80,7 +80,7 @@ begin
8080
have := imo2019_q4_upper_bound hk h,
8181
interval_cases n,
8282
/- n = 1 -/
83-
{ left, congr, norm_num at h, norm_cast at h, rw [factorial_eq_one] at h, apply antisymm h,
83+
{ left, congr, norm_num at h, rw [factorial_eq_one] at h, apply antisymm h,
8484
apply succ_le_of_lt hk },
8585
/- n = 2 -/
8686
{ right, congr, norm_num [prod_range_succ] at h, norm_cast at h, rw [← factorial_inj],

‎counterexamples/phillips.lean‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -281,8 +281,8 @@ begin
281281
union_diff_left],
282282
rw [nat.succ_eq_add_one, this, f.additive],
283283
swap, { rw disjoint.comm, apply disjoint_diff },
284-
calc ((n + 1) : ℝ) * (ε / 2) = ε / 2 + n * (ε / 2) : by ring
285-
... ≤ f ((s (n + 1)) \ (s n)) + f (s n) : add_le_add (I1 n) IH } },
284+
calc ((n + 1 : ℕ) : ℝ) * (ε / 2) = ε / 2 + n * (ε / 2) : by simp only [nat.cast_succ]; ring
285+
... ≤ f ((s (n + 1 : ℕ)) \ (s n)) + f (s n) : add_le_add (I1 n) IH } },
286286
rcases exists_nat_gt (f.C / (ε / 2)) with ⟨n, hn⟩,
287287
have : (n : ℝ) ≤ f.C / (ε / 2),
288288
by { rw le_div_iff (half_pos ε_pos), exact (I2 n).trans (f.le_bound _) },

‎src/algebra/algebra/operations.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -304,6 +304,7 @@ instance : semiring (submodule R A) :=
304304
mul_zero := mul_bot,
305305
left_distrib := mul_sup,
306306
right_distrib := sup_mul,
307+
..add_monoid_with_one.unary,
307308
..submodule.pointwise_add_comm_monoid,
308309
..submodule.has_one,
309310
..submodule.has_mul }

‎src/algebra/algebra/subalgebra/basic.lean‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1078,8 +1078,8 @@ variables {R : Type*} [ring R]
10781078

10791079
/-- A subring is a `ℤ`-subalgebra. -/
10801080
def subalgebra_of_subring (S : subring R) : subalgebra ℤ R :=
1081-
{ algebra_map_mem' := λ i, int.induction_on i S.zero_mem
1082-
(λ i ih, S.add_mem ih S.one_mem)
1081+
{ algebra_map_mem' := λ i, int.induction_on i (by simpa using S.zero_mem)
1082+
(λ i ih, by simpa using S.add_mem ih S.one_mem)
10831083
(λ i ih, show ((-i - 1 : ℤ) : R) ∈ S, by { rw [int.cast_sub, int.cast_one],
10841084
exact S.sub_mem ih S.one_mem }),
10851085
.. S }

‎src/algebra/big_operators/basic.lean‎

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -1722,23 +1722,23 @@ end multiset
17221722

17231723
namespace nat
17241724

1725-
@[simp, norm_cast] lemma cast_list_sum [add_monoid β] [has_one β] (s : list ℕ) :
1725+
@[simp, norm_cast] lemma cast_list_sum [add_monoid_with_one β] (s : list ℕ) :
17261726
(↑(s.sum) : β) = (s.map coe).sum :=
17271727
map_list_sum (cast_add_monoid_hom β) _
17281728

17291729
@[simp, norm_cast] lemma cast_list_prod [semiring β] (s : list ℕ) :
17301730
(↑(s.prod) : β) = (s.map coe).prod :=
17311731
map_list_prod (cast_ring_hom β) _
17321732

1733-
@[simp, norm_cast] lemma cast_multiset_sum [add_comm_monoid β] [has_one β] (s : multiset ℕ) :
1733+
@[simp, norm_cast] lemma cast_multiset_sum [add_comm_monoid_with_one β] (s : multiset ℕ) :
17341734
(↑(s.sum) : β) = (s.map coe).sum :=
17351735
map_multiset_sum (cast_add_monoid_hom β) _
17361736

17371737
@[simp, norm_cast] lemma cast_multiset_prod [comm_semiring β] (s : multiset ℕ) :
17381738
(↑(s.prod) : β) = (s.map coe).prod :=
17391739
map_multiset_prod (cast_ring_hom β) _
17401740

1741-
@[simp, norm_cast] lemma cast_sum [add_comm_monoid β] [has_one β] (s : finset α) (f : α → ℕ) :
1741+
@[simp, norm_cast] lemma cast_sum [add_comm_monoid_with_one β] (s : finset α) (f : α → ℕ) :
17421742
↑(∑ x in s, f x : ℕ) = (∑ x in s, (f x : β)) :=
17431743
map_sum (cast_add_monoid_hom β) _ _
17441744

@@ -1750,23 +1750,23 @@ end nat
17501750

17511751
namespace int
17521752

1753-
@[simp, norm_cast] lemma cast_list_sum [add_group β] [has_one β] (s : list ℤ) :
1753+
@[simp, norm_cast] lemma cast_list_sum [add_group_with_one β] (s : list ℤ) :
17541754
(↑(s.sum) : β) = (s.map coe).sum :=
17551755
map_list_sum (cast_add_hom β) _
17561756

17571757
@[simp, norm_cast] lemma cast_list_prod [ring β] (s : list ℤ) :
17581758
(↑(s.prod) : β) = (s.map coe).prod :=
17591759
map_list_prod (cast_ring_hom β) _
17601760

1761-
@[simp, norm_cast] lemma cast_multiset_sum [add_comm_group β] [has_one β] (s : multiset ℤ) :
1761+
@[simp, norm_cast] lemma cast_multiset_sum [add_comm_group_with_one β] (s : multiset ℤ) :
17621762
(↑(s.sum) : β) = (s.map coe).sum :=
17631763
map_multiset_sum (cast_add_hom β) _
17641764

17651765
@[simp, norm_cast] lemma cast_multiset_prod {R : Type*} [comm_ring R] (s : multiset ℤ) :
17661766
(↑(s.prod) : R) = (s.map coe).prod :=
17671767
map_multiset_prod (cast_ring_hom R) _
17681768

1769-
@[simp, norm_cast] lemma cast_sum [add_comm_group β] [has_one β] (s : finset α) (f : α → ℤ) :
1769+
@[simp, norm_cast] lemma cast_sum [add_comm_group_with_one β] (s : finset α) (f : α → ℤ) :
17701770
↑(∑ x in s, f x : ℤ) = (∑ x in s, (f x : β)) :=
17711771
map_sum (cast_add_hom β) _ _
17721772

‎src/algebra/big_operators/pi.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -89,7 +89,7 @@ variables [Π i, non_assoc_semiring (f i)]
8989
@[ext] lemma ring_hom.functions_ext [fintype I] (G : Type*) [non_assoc_semiring G]
9090
(g h : (Π i, f i) →+* G) (w : ∀ (i : I) (x : f i), g (single i x) = h (single i x)) : g = h :=
9191
ring_hom.coe_add_monoid_hom_injective $
92-
add_monoid_hom.functions_ext G (g : (Π i, f i) →+ G) h w
92+
@add_monoid_hom.functions_ext I _ f _ _ G _ (g : (Π i, f i) →+ G) h w
9393

9494
end ring_hom
9595

‎src/algebra/category/Ring/colimits.lean‎

Lines changed: 52 additions & 30 deletions
Original file line numberDiff line numberDiff line change
@@ -127,15 +127,11 @@ The underlying type of the colimit of a diagram in `CommRing`.
127127
@[derive inhabited]
128128
def colimit_type : Type v := quotient (colimit_setoid F)
129129

130-
instance : comm_ring (colimit_type F) :=
130+
instance : add_group (colimit_type F) :=
131131
{ zero :=
132132
begin
133133
exact quot.mk _ zero
134134
end,
135-
one :=
136-
begin
137-
exact quot.mk _ one
138-
end,
139135
neg :=
140136
begin
141137
fapply @quot.lift,
@@ -163,24 +159,6 @@ instance : comm_ring (colimit_type F) :=
163159
{ exact relation.add_1 _ _ _ r },
164160
{ refl } },
165161
end,
166-
mul :=
167-
begin
168-
fapply @quot.lift _ _ ((colimit_type F) → (colimit_type F)),
169-
{ intro x,
170-
fapply @quot.lift,
171-
{ intro y,
172-
exact quot.mk _ (mul x y) },
173-
{ intros y y' r,
174-
apply quot.sound,
175-
exact relation.mul_2 _ _ _ r } },
176-
{ intros x x' r,
177-
funext y,
178-
induction y,
179-
dsimp,
180-
apply quot.sound,
181-
{ exact relation.mul_1 _ _ _ r },
182-
{ refl } },
183-
end,
184162
zero_add := λ x,
185163
begin
186164
induction x,
@@ -197,28 +175,71 @@ instance : comm_ring (colimit_type F) :=
197175
apply relation.add_zero,
198176
refl,
199177
end,
200-
one_mul := λ x,
178+
add_left_neg := λ x,
201179
begin
202180
induction x,
203181
dsimp,
204182
apply quot.sound,
205-
apply relation.one_mul,
183+
apply relation.add_left_neg,
206184
refl,
207185
end,
208-
mul_one := λ x,
186+
add_assoc := λ x y z,
209187
begin
210188
induction x,
189+
induction y,
190+
induction z,
211191
dsimp,
212192
apply quot.sound,
213-
apply relation.mul_one,
193+
apply relation.add_assoc,
194+
refl,
214195
refl,
196+
refl,
197+
end }
198+
199+
instance : add_group_with_one (colimit_type F) :=
200+
{ one :=
201+
begin
202+
exact quot.mk _ one
215203
end,
216-
add_left_neg := λ x,
204+
.. colimit_type.add_group F }
205+
206+
instance : comm_ring (colimit_type F) :=
207+
{ one :=
208+
begin
209+
exact quot.mk _ one
210+
end,
211+
mul :=
212+
begin
213+
fapply @quot.lift _ _ ((colimit_type F) → (colimit_type F)),
214+
{ intro x,
215+
fapply @quot.lift,
216+
{ intro y,
217+
exact quot.mk _ (mul x y) },
218+
{ intros y y' r,
219+
apply quot.sound,
220+
exact relation.mul_2 _ _ _ r } },
221+
{ intros x x' r,
222+
funext y,
223+
induction y,
224+
dsimp,
225+
apply quot.sound,
226+
{ exact relation.mul_1 _ _ _ r },
227+
{ refl } },
228+
end,
229+
one_mul := λ x,
217230
begin
218231
induction x,
219232
dsimp,
220233
apply quot.sound,
221-
apply relation.add_left_neg,
234+
apply relation.one_mul,
235+
refl,
236+
end,
237+
mul_one := λ x,
238+
begin
239+
induction x,
240+
dsimp,
241+
apply quot.sound,
242+
apply relation.mul_one,
222243
refl,
223244
end,
224245
add_comm := λ x y,
@@ -288,7 +309,8 @@ instance : comm_ring (colimit_type F) :=
288309
refl,
289310
refl,
290311
refl,
291-
end, }
312+
end,
313+
.. colimit_type.add_group_with_one F }
292314

293315
@[simp] lemma quot_zero : quot.mk setoid.r zero = (0 : colimit_type F) := rfl
294316
@[simp] lemma quot_one : quot.mk setoid.r one = (1 : colimit_type F) := rfl

0 commit comments

Comments
 (0)