# Zulip Chat Archive

## Stream: general

### Topic: characteristic refactor?

#### Julian Külshammer (Apr 06 2021 at 10:38):

Issue #4688 asks for the characteristic of a (semi)ring to be refactored. Unifying the definition of `char_p`

and `char_zero`

. In #6753 Damiano has recently suggested that it would make sense to redefine `ring_char`

in terms of `add_order_of (1 : R)`

. I had similar thoughts, but since this would be a major refactor, I wanted to ask for opinions whether this is desirable at all and what the concrete suggestion would be.

Like I said, I would imagine that `ring_char R = add_order_of (1 : R)`

and then one could let `char_p R p`

be the class defined by the condition `(h : ring_char R = p)`

. `char_zero`

would then not exist separatly but be the special case `char_p R 0`

.

(I assume that another option would be to work with something like `[fact(ring_char R = p)]`

but I assumed this was ruled out before since `char_p`

is used a lot).

What do you think? Are there any suggestions how to make this more managable?

#### Anne Baanen (Apr 06 2021 at 10:41):

I think this refactor is a good idea. For the transition, my first suggestion would be to do it in multiple steps: change the definition of `char_p`

, change the definition of `char_zero`

, replace usages of `char_zero`

with `char_p 0`

.

#### Anne Baanen (Apr 06 2021 at 10:43):

As long as you keep a definition docs#char_p.cast_eq_zero_iff, I expect that you will only need to tweak the instance definitions, no usages.

#### Anne Baanen (Apr 06 2021 at 10:45):

`add_order_of 1`

doesn't work for `add_monoid`

s, right? So we do not satisfy point 2 of #4688.

#### Damiano Testa (Apr 06 2021 at 10:51):

I quickly thought about this and was wondering how to define the "order" of an element `a`

in a `semigroup/monoid`

. I probably would define it to be the smallest gap between two repeated values of the iterated operation of the element on itself:

the sequence

`a`

, `a.a`

, `a.a.a`

,...

either

- never repeats itself, in which case the order would be zero, or
- repeats a value at some point and the gap between the first repeated values would be the order.

It seems to me that this should be a reasonable definition, but I have no experience of working with something like this mathematically. It might be that someone doing dynamics has a better idea, given that the one outlined above is related to pre-periodic points.

#### Julian Külshammer (Apr 06 2021 at 10:54):

@Anne Baanen Of course it has to be `[add_monoid R] [has_one R]`

, but this is anyway the minimal assumptions one can put to make sense of `ring_char`

, whatever the definition is. Thanks to previous PRs this definition would typecheck.

#### Anne Baanen (Apr 06 2021 at 10:57):

I was just wondering whether the supremum of `add_order_of`

would work 1) as another definition, and 2) have a useful meaning outside of semirings.

#### Julian Külshammer (Apr 06 2021 at 10:59):

@Damiano Testa At the moment `add_order_of a`

is defined to be the smallest positive number such that `n \smul\N a=0`

if it exists and `0`

otherwise. There is a suggestion by Yury to redefine it in terms of docs#function.minimal_period, so that `to_additive`

works in more cases and some statements are for free from the general theory, but I guess this refactor could be done independently or first (I don't imagine it to be terribly difficult. I've changed the definition of `order_of`

before and not that much breaks, the API is pretty robust.)

#### Damiano Testa (Apr 06 2021 at 11:01):

Ok, using `add_order_of`

for now sounds like a good plan. I am not really sure that I know good examples of semirings where `minimal_period`

would give me more leverage than `add_order_of`

!

#### Damiano Testa (Apr 06 2021 at 11:03):

Also, I think that `add_order_of`

is relatively "new" as a definition in mathilb. Working with it may also start showing how useful it is in practice.

#### Julian Külshammer (Apr 06 2021 at 11:04):

Indeed, it is #6770, merged 5 days ago.

#### Julian Külshammer (Apr 06 2021 at 12:59):

@Anne Baanen Your supremum definition makes sense if we want to generalise to non-unital rings.

#### Oliver Nash (Apr 06 2021 at 13:13):

Julian Külshammer said:

Anne Baanen Your supremum definition makes sense if we want to generalise to non-unital rings.

We still don't have these :cry:

#### Julian Külshammer (Apr 06 2021 at 14:40):

@Oliver Nash That's a pity, but for me the question is, how to redefine `ring_char`

so that when they arrive, it is only a matter of replacing `semiring`

by `non_unital_semiring`

in a few places. To me this feels more natural than defining it for `[add_monoid R] [has_one R]`

for which I know no example.

#### Damiano Testa (Apr 07 2021 at 07:30):

Dear All,

I have been experimenting with the definition and it seems that what is below can be made to work. Following Anne's suggestion, it seems to make sense to define the "characteristic" of an `add_monoid R`

as the smallest natural number `n`

such that `∀ a : R, n • a = 0`

, or `0`

if the set of such `n`

s is empty.

This is also called, I believe, the exponent, at least in the case of a (commutative) group. So, should we define `exponent R`

?

What I started with is playing around with the "annihilating set" for all of `R`

:

```
import algebra.iterate_hom
variables {R : Type*} [add_monoid R]
def ann (R : Type*) [add_monoid R] : set ℕ :=
{ n | ∀ a : R, ((+) a)^[n] a = (0 : R) }
@[simp]
lemma ann_exists {R : Type*} [add_monoid R] : ann R = { n | ∀ a : R, ((+) a)^[n] a = (0 : R) } :=
rfl
```

NB: the elements of `ann R`

are *one less* than what I would call the annihilator! Thus, the exponent would have to be defined as

```
exponent R = if (ann R) = ∅ then 0 else (min (ann R)) + 1
```

but written in a way that works in Lean.

#### Damiano Testa (Apr 07 2021 at 07:30):

In my experiments, I have started to prove that `ann (zmod n)`

contains `n - 1`

and, so far, it has not been too rough.

#### Damiano Testa (Apr 07 2021 at 07:32):

I also proved with little effort that, if `R`

is a `semiring`

, then the "annihilator of 1" annihilates the whole `semiring`

.

#### Kevin Buzzard (Apr 07 2021 at 07:34):

By natural number you mean positive integer?

#### Eric Wieser (Apr 07 2021 at 07:55):

Why `(+ a)^[n] n`

and not `n \smul a`

or `n \smul\N a`

?

#### Eric Wieser (Apr 07 2021 at 07:55):

That would eliminate the off-by-one error you observed!

#### Damiano Testa (Apr 07 2021 at 07:56):

Here is a further expansion (I only now read Kevin and Eric's comments).

```
import data.zmod.basic
import algebra.iterate_hom
section char
variables {R : Type*} [add_monoid R]
def ann (R : Type*) [add_monoid R] : set ℕ :=
{ n | ∀ a : R, ((+) a)^[n] a = (0 : R) }
@[simp]
lemma ann_exists {R : Type*} [add_monoid R] : ann R = { n | ∀ a : R, ((+) a)^[n] a = (0 : R) } :=
rfl
lemma zmod.pred_eq_neg_one (n : ℕ) [h : fact (0 < n)] : ((n.pred) : zmod n) = - 1 :=
begin
casesI n,
{ exact (lt_irrefl 0 h.1).elim },
{ exact add_eq_zero_iff_eq_neg.mp (zmod.nat_cast_self' _) }
end
lemma zmod_pred_ann {n : ℕ} [h : fact (0 < n)] : n - 1 ∈ ann (zmod n) :=
λ a, by rw [add_left_iterate, nsmul_eq_mul, ← nat.pred_eq_sub_one, zmod.pred_eq_neg_one,
neg_mul_eq_neg_mul_symm, one_mul, add_left_neg]
lemma not_ann {k n : ℕ} [h : fact (0 < n)] (kn : k < n - 1) : ¬ (k : zmod n) = -1 :=
begin
rw [← add_eq_zero_iff_eq_neg, ← nat.cast_one, ← nat.cast_add, zmod.nat_coe_zmod_eq_zero_iff_dvd],
rintros ⟨j, hj⟩,
cases j,
{ have : 0 < k + 1 := k.succ_pos,
rw [hj, mul_zero] at this,
exact nat.lt_asymm this this },
have nk : n ≤ k + 1,
{ refine le_trans _ hj.ge,
nth_rewrite 0 ← mul_one n,
exact (mul_le_mul_left h.1).mpr (nat.succ_pos _) },
have kn : k + 1 < n := nat.add_lt_of_lt_sub_right kn,
exact lt_irrefl n (nk.trans_lt kn),
end
lemma zmod_not_ann {k n : ℕ} [h : fact (0 < n)] (kn : k < n - 1) : k ∉ ann (zmod n) :=
begin
simp,
refine ⟨1, _⟩,
rw [mul_one, add_eq_zero_iff_eq_neg],
exact not_ann kn,
end
```

#### Damiano Testa (Apr 07 2021 at 07:57):

Kevin, yes, I meant positive integer! The "off-by-one" thing confused me! Although, it seems that Eric's suggestion will make this better!

#### Damiano Testa (Apr 07 2021 at 07:58):

Anyway, I now have to meet students: I will be quiet for a while!

#### Julian Külshammer (Apr 07 2021 at 08:17):

I did some experiments with `minimal_period`

and my conclusion was that I'd like to introduce the predicate `is_of_finite_order`

which seems similar to your findings. I can push around lunch tiime.

#### Julian Külshammer (Apr 07 2021 at 09:39):

#7082 shows the status of the minimal_period refactor right now. Comments welcome, keep in mind it is in an early stage.

#### Julian Külshammer (Apr 11 2021 at 15:59):

According to the strategy which @Anne Baanen and @Damiano Testa suggested, after #7082 gets hopefully merged, the next natural step would be to define the exponent of a group (or a monoid). Again we would want that this makes sense for infinite groups. The exponent of a group is the lcm of all the orders of elements of a group. This is a potentially infinite set. As far as I can see, there is only the lcm of a multiset and a finset. Would it make sense to define the lcm of an infinite set as 0 and otherwise as the lcm of the corresponding finset? It looks a bit like what was done for finprod/finsum recently.

#### Kevin Buzzard (Apr 11 2021 at 16:04):

These adjectives "lowest" and "highest" are really unfortunate. The "lowest" common multiple of a bunch of naturals should be the unique natural which is a multiple of all of them and which divides all the other naturals which are a multiple of all of them, ie the lowest under the divisibility relation. This is what is always used in practice. So I completely agree that 0 is a good choice here.

#### Damiano Testa (Apr 11 2021 at 17:09):

I would have made the same choice: if the `set`

of orders is not finite, define the `exponent`

as zero. Clearly no finite group will have exponent zero, so, that should also cause no confusion with mathematicians!

#### Damiano Testa (Apr 14 2021 at 16:45):

@Yury G. Kudryashov , you had asked to be reminded about PR #7082, which I am doing now. However, do not feel pressured to look at it: I can understand that it is not a priority!

As a side note, I have also made sure that the PR is compatible with Sébastien's refactor.

#### Damiano Testa (Apr 14 2021 at 16:48):

[I thought that it built successfully, but now CI seems to still be going at it. However, it is in the final Linting/Testing stage]

#### Yury G. Kudryashov (Apr 14 2021 at 17:14):

Thank you for the reminder!

#### Julian Külshammer (Apr 16 2021 at 09:26):

Any comments on the following definition of exponent of a group before I start proving stuff about it?

```
import data.finset.gcd
import data.set.finite
import data.nat.gcd
import group_theory.order_of_element
universe u
variables {M : Type u} [comm_cancel_monoid_with_zero M] [nontrivial M] [gcd_monoid M]
open_locale classical
noncomputable def set.lcm (S : set M) : M :=
if h : S.finite then finset.lcm h.to_finset id else 0
variables {G : Type u} [monoid G]
noncomputable def exponent (G : Type u) [monoid G] : ℕ := lcm {n | ∃(x : G), n = order_of x }
```

#### Johan Commelin (Apr 16 2021 at 09:27):

Hmm, I guess that works. But I would probably have used `nat.find`

.

#### Johan Commelin (Apr 16 2021 at 09:28):

Something like

```
def exponent_exists : \ex n, n < 0, \all g, n \bu g = 0
def exponent :=
if h : exponent_exists then nat.find h else 0
```

#### Johan Commelin (Apr 16 2021 at 09:34):

With your definition, you will also need to develop an API for `set.lcm`

. Which is fine, of course. `nat.find`

has 3 lemmas, that's it's total API. So that's maybe also quite minimalistic.

#### Julian Külshammer (Apr 16 2021 at 09:34):

That also makes sense. The equivalence of both would be one of the first things to prove.

#### Julian Külshammer (Apr 16 2021 at 09:35):

Your approach also has the advantage that I already know all the `nat.find`

API :-)

#### Damiano Testa (Apr 16 2021 at 09:37):

Pasting your code in my lean asks for the `lcm`

to really be a `set.lcm`

: is this not happening for you?

#### Johan Commelin (Apr 16 2021 at 09:38):

I guess `open set`

is missing

#### Julian Külshammer (Apr 16 2021 at 09:40):

Sorry, I changed a few things last minute before pasting. I had `namespace set`

there before, but I guess `set.exponent`

doesn't make much sense.

#### Damiano Testa (Apr 16 2021 at 09:41):

Ok, no worries! I also do not want to sidetrack the discussion: I was simply trying to understand whether there was something funny with my copy of Lean. Issue settled!

#### Damiano Testa (Apr 16 2021 at 09:42):

On the side of definitions, I think that I prefer Johan's version: you probably do not need to assume that `M`

is a `comm_cancel_monoid_with_zero`

with that...

#### Damiano Testa (Apr 16 2021 at 09:43):

Although I would change `n < 0`

for `0 < n`

...

#### Julian Külshammer (Apr 16 2021 at 09:43):

I don't, `nat`

is the `comm_cancel_monoid_with_zero`

, `G`

is just a monoid.

#### Damiano Testa (Apr 16 2021 at 09:47):

Ah, sorry! I had missed this! However, to define exponents with Johan's formulation, you no longer need to define the `set.lcm`

, which I think is a plus.

#### Julian Külshammer (Apr 16 2021 at 09:50):

I agree, although it might be good to have it anyway to show the equivalence.

#### Damiano Testa (Apr 16 2021 at 09:56):

I certainly think that the equivalence should be there, but the definition of `exponent`

should not need the definition of `set.lcm`

, in my opinion.

#### David Wärn (Apr 16 2021 at 10:32):

A more uniform way of defining the lcm of a set `s`

of integers (or indexed family) is to pick a generator of the ideal given by intersecting the principal ideals from `s`

#### Damiano Testa (Apr 27 2021 at 08:20):

The two waves of refactors, with `nat`

and `int`

have washed over PR #7082. I believe that I have resolved all conflicts and CI is checking this right now.

In case someone wants to take a look at this PR, I would be very grateful! In particular, I will ping @Yury G. Kudryashov , who had expressed interested in this refactor!

Thanks a lot!

Last updated: May 18 2021 at 15:14 UTC