characteristic refactor?

Stream: general

[Julian Külshammer]

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]

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]

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]

add_order_of 1 doesn't work for add_monoids, right? So we do not satisfy point 2 of #4688.

[Damiano Testa]

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]

@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]

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]

@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]

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]

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]

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

[Julian Külshammer]

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

[Oliver Nash]

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]

@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]

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 ns 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]

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]

I also proved with little effort that, if R is a semiring, then the "annihilator of 1" annihilates the whole semiring.

[Kevin Buzzard]

By natural number you mean positive integer?

[Eric Wieser]

Why (+ a)^[n] n and not n \smul a or n \smul\N a?

[Eric Wieser]

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

[Damiano Testa]

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]

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]

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

[Julian Külshammer]

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]

#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]

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]

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]

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]

@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]

[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]

Thank you for the reminder!

[Julian Külshammer]

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]

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

[Johan Commelin]

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]

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]

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

[Julian Külshammer]

Your approach also has the advantage that I already know all the nat.find API :-)

[Damiano Testa]

Pasting your code in my lean asks for the lcm to really be a set.lcm: is this not happening for you?

[Johan Commelin]

I guess open set is missing

[Julian Külshammer]

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]

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]

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]

Although I would change n < 0 for 0 < n...

[Julian Külshammer]

I don't, nat is the comm_cancel_monoid_with_zero, G is just a monoid.

[Damiano Testa]

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]

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

[Damiano Testa]

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]

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]

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!