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_monoids, 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,...

  • 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 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) }

lemma ann_exists {R : Type*} [add_monoid R] : ann R = { n |  a : R, ((+) a)^[n] a = (0 : R) } :=

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) }

lemma ann_exists {R : Type*} [add_monoid R] : ann R = { n |  a : R, ((+) a)^[n] a = (0 : R) } :=

lemma zmod.pred_eq_neg_one (n : ) [h : fact (0 < n)] : ((n.pred) : zmod n) = - 1 :=
  casesI n,
  { exact (lt_irrefl 0 h.1).elim },
  { exact add_eq_zero_iff_eq_neg.mp (zmod.nat_cast_self' _) }

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 :=
  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),

lemma zmod_not_ann {k n : } [h : fact (0 < n)] (kn : k < n - 1) : k  ann (zmod n) :=
  refine 1, _⟩,
  rw [mul_one, add_eq_zero_iff_eq_neg],
  exact not_ann kn,

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: Dec 20 2023 at 11:08 UTC