Zulip Chat Archive

Stream: maths

Topic: Implementation of multiplicative characters


Michael Stoll (Jun 16 2022 at 18:43):

This is motivated by the discussion here:

We consider multiplicative characters from one commutative ring R into another commutative ring R'.

Question: Should such an object just be a monoid_with_zero_hom (alternative (1)), or is it preferable to implement this as a monoid_hom with the additional property that it maps non-units to zero (alternative (2))?

Michael Stoll (Jun 16 2022 at 18:43):

The main advantage of alternative (2) is that one can then define a comm_group structure on mul_char R R'.

Michael Stoll (Jun 16 2022 at 18:45):

A possible disadvantage is that the restriction regarding non-units may be too strong in some contexts. For example, a Dirichlet character would not qualify as a multiplicative character. (But it could be obtained by composing ℤ → zmod n with a multiplicative character on zmod n.)

Michael Stoll (Jun 16 2022 at 18:46):

I have implemented both versions. Alternative (1) is in #14716 amd alternative (2) is in #14768.

Michael Stoll (Jun 16 2022 at 18:47):

I'd appreciate comments (at this stage, on the choice between the alternatives; fine-tuning can be done later).

Junyan Xu (Jun 16 2022 at 20:31):

Side-by-side comparison: https://github.com/leanprover-community/mathlib/compare/legendre_symbol_mul_char...variant

Anne Baanen (Jun 17 2022 at 09:55):

I'm inclined to support mul_char because it allows us to define a comm_group structure. (The objection is that monoid_with_zero_homs don't have inverses, right?)

Michael Stoll (Jun 17 2022 at 11:01):

Yes; there is a difference when the domain is not a field (i.e., when there are non-zero non-units). The unit monoid_with_zero_hom, it is is defined (I don't know if M \to*0 M' is a monoid instance), would map everything except zero to one, so when a monoid_with_zero_hom maps a nonzero non-unit to zero (or a non-unit), it does not have an inverse.

Michael Stoll (Jun 17 2022 at 15:01):

@Alex J. Best @Johan Commelin @Kevin Buzzard @Riccardo Brasca Do you have input on this?

Riccardo Brasca (Jun 17 2022 at 15:06):

monoid_with_zero_hom is a monoid, right? The unit sends 0 to 0 and everything else to 1 if I am not confused.

Michael Stoll (Jun 17 2022 at 15:22):

Hmm...

example {M M' : Type*} [monoid_with_zero M] [monoid_with_zero M'] (f : M →*₀ M') : M →*₀ M' := f ^ 0

gives

failed to synthesize type class instance for
M : Type ?,
M' : Type ?,
_inst_1 : monoid_with_zero M,
_inst_2 : monoid_with_zero M',
f : M →*₀ M'
 has_pow (M →*₀ M') 

but a monoid should have has_pow, right?

Michael Stoll (Jun 17 2022 at 15:22):

(Same with f * f and has_mulor 1 and has_one.)

Michael Stoll (Jun 17 2022 at 15:23):

So it looks like the monoid instance on monoid_with_zero_hom M M' is missing.

Riccardo Brasca (Jun 17 2022 at 15:33):

It's missing, but it's true?

Riccardo Brasca (Jun 17 2022 at 15:33):

It seems so

Yaël Dillies (Jun 17 2022 at 16:01):

Do you not need the monoids to be commutative?

Riccardo Brasca (Jun 17 2022 at 16:36):

Yes yes, in applications the monoids will be commutative

Kevin Buzzard (Jun 17 2022 at 17:18):

Wait isn't the issue that you need source and target to be equal?

Michael Stoll (Jun 17 2022 at 17:29):

Kevin Buzzard said:

Wait isn't the issue that you need source and target to be equal?

No, you just multiply the values: mul f g = λ x, f x * g x.

Michael Stoll (Jun 17 2022 at 17:32):

Yaël Dillies said:

Do you not need the monoids to be commutative?

You need the target to be commutative for the product to be a homomorphism again:
(fg)(xy)=f(xy)g(xy)=f(x)f(y)g(x)g(y)=!f(x)g(x)f(y)g(y)=(fg)(x)(fg)(y) (f \cdot g)(x \cdot y) = f(x \cdot y) \cdot g(x \cdot y) = f(x) \cdot f(y) \cdot g(x) \cdot g(y) \stackrel{!}{=} f(x) \cdot g(x) \cdot f(y) \cdot g(y) = (f \cdot g)(x) \cdot (f \cdot g)(y)

But even with [comm_monoid_with_zero M'], the has_one instance is not found.

Michael Stoll (Jun 17 2022 at 17:33):

But it does find has_mul...

Adam Topaz (Jun 17 2022 at 17:45):

Isn't the trivial monoid a monoid with zero where 1=01 = 0? If so, then this doesn't hold for silly reasons because the set of monoid-with-zero-homs from this trivial monoid_with_zero to the monoid_with_zero {0,1}\{0,1\} is empty

Adam Topaz (Jun 17 2022 at 17:46):

OTOH if you have a group_with_zero as the source, then it should be okay because I think those have an assumption that 010 \neq 1.

Adam Topaz (Jun 17 2022 at 17:46):

Or maybe assuming [nontrivial] is enough

Michael Stoll (Jun 17 2022 at 17:57):

In any case, this seems to point in the direction that defining mul_char such that mult. characters form a group is the right way to go.

Eric Wieser (Jun 17 2022 at 22:15):

does docs#monoid_with_zero_hom.monoid not exist?

Yaël Dillies (Jun 17 2022 at 22:17):

It would be monoid_with_zero_hom.comm_monoid at any rate.

Eric Wieser (Jun 17 2022 at 22:59):

I'm wondering if we have the monoid of endomorphisms

Reid Barton (Jun 17 2022 at 23:00):

docs#monoid.End

Reid Barton (Jun 17 2022 at 23:01):

oh maybe you mean of something else

Junyan Xu (Jun 17 2022 at 23:01):

no docs#monoid_with_zero.End ...

Reid Barton (Jun 17 2022 at 23:02):

here you go docs#category_theory.End

Michael Stoll (Jun 23 2022 at 23:42):

It looks like the consensus is to go with mul_char as monoid_hom sending nonunits to zero.
I have therefore closed #14716. There is a new version of #14768, where the assumptions are weakened: the domain is a comm_monoid and the target is a comm_monoid_with_zero (we need zero in the target, since we map nonunits to zero). In this setting, it is still true that mul_char R R' has a structure as a comm_group.
@Riccardo Brasca @Anne Baanen @Yaël Dillies @Kevin Buzzard I have removed the "WIP" label and would like to start the review process on #14768.

Michael Stoll (Jun 27 2022 at 17:50):

@Riccardo Brasca @Anne Baanen @Yaël Dillies @Kevin Buzzard @Johan Commelin I see two :+1: on the previous message, but no comments so far on #14768. I'm not sure how to interpret this.

One thing I'd like to know is whether the way I have set up mul_char. mul_char_class and the commutative group structure is OK for mathlib. (I haven't done something similar before. For mul_char_class, I basically copied existing code and modified it.)

Kevin Buzzard (Jun 27 2022 at 18:00):

Do you know about fun_like? I don't really understand it properly; here is the documentation.

Kevin Buzzard (Jun 27 2022 at 18:01):

I ask because you've defined ext and ext' and neither of them look like the thing in the documentation, but as I say I don't understand this properly yet.

Michael Stoll (Jun 27 2022 at 18:27):

I think what I do is more similar to this later part of the file, building on monoid_hom.
The rationale behind ext' and ext is that you want to only check equality on units (since nonunits are mapped to zero anyway) -- this is what ext does, but its proof needs a version of ext'. In particular, I want ext to be the [@ext] lemma, so that I can write ext a ha in my proofs to get the goal something a = something_other a under the assumption ha : is_unit a.

Kevin Buzzard (Jun 27 2022 at 19:11):

I reviewed -- mostly superficial comments. Thanks a lot!

Michael Stoll (Jun 27 2022 at 19:21):

Kevin Buzzard said:

I reviewed -- mostly superficial comments. Thanks a lot!

Thanks!

Michael Stoll (Jun 27 2022 at 20:02):

How do I get the current mathlib version into my branch? I tried leanproject up, but this does not seem to havethe desired effect. (Concretely, I would like to have #14873 available, so that I can remove some decidability stuff.)

Patrick Massot (Jun 27 2022 at 20:05):

leanproject up won't do that if you are not on the master branch. You should rebase your PR branch on top of master and then get the cache.

Michael Stoll (Jun 27 2022 at 20:07):

I could try to look this up, but it will be faster if you just tell me the relevant git commands :smile:

Patrick Massot (Jun 27 2022 at 20:10):

If you don't know git then you should probably make a copy of your mathlib folder just in case. Then git rebase master and then leanproject get-cache --fallback download-first. Of course you won't get cache for your branch, only the latest master cache

Michael Stoll (Jun 27 2022 at 20:15):

Error: No such option: --fallback
Without the --fallback ..., it says

Trying to download https://oleanstorage.azureedge.net/mathlib/cad5c63bb1a52569d2fe913534c18f983819201b.tar.xz to /home/mstoll/.mathlib/cad5c63bb1a52569d2fe913534c18f983819201b.tar.xz
Trying to download https://oleanstorage.azureedge.net/mathlib/cad5c63bb1a52569d2fe913534c18f983819201b.tar.gz to /home/mstoll/.mathlib/cad5c63bb1a52569d2fe913534c18f983819201b.tar.gz
Trying to download https://oleanstorage.azureedge.net/mathlib/cad5c63bb1a52569d2fe913534c18f983819201b.tar.bz2 to /home/mstoll/.mathlib/cad5c63bb1a52569d2fe913534c18f983819201b.tar.bz2
Looking for GitHub mathlib oleans
Info: No github section found in 'git config', we will use GitHub with no authentication
Failed to fetch mathlib oleans

Patrick Massot (Jun 27 2022 at 20:17):

Can you tell me the result of leanproject --version?

Michael Stoll (Jun 27 2022 at 20:18):

leanproject, version 0.0.8

Patrick Massot (Jun 27 2022 at 20:19):

That's ancient!

Patrick Massot (Jun 27 2022 at 20:19):

You should update mathlibtools

Patrick Massot (Jun 27 2022 at 20:19):

Something like pip install -U mathlibtools

Michael Stoll (Jun 27 2022 at 20:23):

leanproject, version 1.1.1

Michael Stoll (Jun 27 2022 at 20:24):

I seem to have installed the old version when I played around with the Natural Numbers Game a couple years back...

Michael Stoll (Jun 27 2022 at 20:29):

OK, now I don't get an error message any more, but the PR I was looking for is still not there.

Patrick Massot (Jun 27 2022 at 20:34):

I don't understand what "the PR I was looking for is still not there" means

Michael Stoll (Jun 27 2022 at 20:36):

What I mean is, the addition to algebra.group.units that was merged with #14873 this morning is not visible in the mathlib version I have after leanproject get-cache --fallback download-first-

Bart Michels (Jun 27 2022 at 20:52):

I think leanproject get-cache only gets the oleans (not .lean files) up to the commit where your (local) leanproject is. So you need to rebase first, and get-cache after that.

Patrick Massot (Jun 27 2022 at 20:55):

Indeed, did you follow my instruction to git rebase? Maybe I should have been more explicit and tell you to first update your master branch. Something like git checkout master && git pull && git checkout your_branch_name && git rebase master

Patrick Massot (Jun 27 2022 at 20:55):

(you can probably do that in one command, but I never remember those more complicated commands)

Michael Stoll (Jun 27 2022 at 21:01):

OK, after all this (including leanproject get-cache ...), it seems to be there. Thanks for your help!

Riccardo Brasca (Jun 27 2022 at 21:09):

I am very busy this week, sorry for the delay!

Riccardo Brasca (Jun 27 2022 at 21:09):

I will have a look this weekend

Michael Stoll (Jun 27 2022 at 21:12):

Now I get an error message when I try to push my latest commits... (something along the lines of "the head of my branch is behind its external counterpart" [I get the message in German, so this is only a rough approximation to the English version]).

Kevin Buzzard (Jun 27 2022 at 21:13):

Try pulling again?

Michael Stoll (Jun 27 2022 at 21:14):

This gives me (roughly): "fatal: fast forward impossible, abort."

Patrick Massot (Jun 27 2022 at 21:15):

Of course git complains that things diverged but this isn't a big issue. Is this a PR that is already opened?

Michael Stoll (Jun 27 2022 at 21:16):

Yes. (#14768)

Patrick Massot (Jun 27 2022 at 21:19):

Ok, I think you can force push. This will mess up with Kevin's review but he won't mind.

Patrick Massot (Jun 27 2022 at 21:19):

so git push -f

Patrick Massot (Jun 27 2022 at 21:19):

from your PR branch

Michael Stoll (Jun 27 2022 at 21:19):

OK; this gives at least no error messages...

Patrick Massot (Jun 27 2022 at 21:20):

That's the magic of --force in general...

Patrick Massot (Jun 27 2022 at 21:20):

Can you check that https://github.com/leanprover-community/mathlib/pull/14768/files looks like what you would hope for?

Michael Stoll (Jun 27 2022 at 21:22):

It looks like it. (It is a new file, so all of its is green, but it does have the latest change.)

Patrick Massot (Jun 27 2022 at 21:22):

By the way, since the whole PR is simply adding one file, you should have no trouble using the olean cache from master

Michael Stoll (Jun 27 2022 at 21:22):

Is this what leanproject get-cache does?

Michael Stoll (Jun 27 2022 at 21:23):

Should I issue some more gitcommands to avoid problems like the one I just had with future commit/push actions?

Patrick Massot (Jun 27 2022 at 21:25):

Yes, get-cache got you the latest olean leanproject could find, and that would be the ones from master in your situation.

Patrick Massot (Jun 27 2022 at 21:26):

You won't have further git issues since GitHub and your local repository now agree (unless you rebase again, but I don't see why you would do that).

Michael Stoll (Jun 27 2022 at 21:26):

OK. Thanks again!
Now I should get some sleep...

Junyan Xu (Jun 27 2022 at 21:49):

first update your master branch. Something like git checkout master && git pull && git checkout your_branch_name && git rebase master

I usually do something like git fetch && git merge origin/master; this way you don't need to switch out of your branch and back again. If I understand it correctly, git fetch will update the information of all remote branches to their respectively latest commit, then git merge origin/master will merge all new commits in the remote branch origin/masterinto the currently checked out local branch. I prefer merge over rebase becausemerge preserves the history of the current branch, so you don't need to force-push after a merge.

Bart Michels (Jun 27 2022 at 21:53):

Junyan Xu said:

first update your master branch. Something like git checkout master && git pull && git checkout your_branch_name && git rebase master

I usually do something like git fetch && git merge origin/master; this way you don't need to switch out of your branch and back again. If I understand it correctly, git fetch will update the information of all remote branches to their respectively latest commit, then git merge origin/master will merge all new commits in the remote branch origin/masterinto the currently checked out local branch. I prefer merge over rebase becausemerge preserves the history of the current branch, so you don't need to force-push after a merge.

If you do that, don't the commit stats of your branch get messed up? Something like 1000 commits behind, 1001 commits ahead?

Bart Michels (Jun 27 2022 at 21:53):

Also (sorry for the basic questions), do those merge commits show up in pull requests or does GitHub ignore them?

Junyan Xu (Jun 27 2022 at 21:56):

If you do that, don't the commit stats of your branch get messed up? Something like 1000 commits behind, 1001 commits ahead?

I never see that happen. After you merge and push, it should say 0 commits behind, assuming no commits are added to master in the meantime.

Junyan Xu (Jun 27 2022 at 21:59):

Merge commits do show up in the PR page, e.g. you can see two of them in #14967, and currently branch#graded_algebra_timeout' is 8 commits ahead / 8 behind master.

Bart Michels (Jun 27 2022 at 22:04):

Thanks. I read that fetch+merge creates new commits rather than rewrite history, so wasn't sure how git deals with the fact that they're not technically the same commits.

Junyan Xu (Jun 27 2022 at 22:28):

merge creates a new commit (for example this) that has two parent commits, namely the latest commit in you local branch and the latest in the remote master branch. rebase produces a linear history by stacking you local commits on top of the latest commit of the remote master; if you create a branch from master at its 10th commit and add 8 commits to it, then rebase to master when it's at the 20th commit, then your 8 commits will now be connected to the 20th commit and no longer the 10th commit, so the history is changed and your 8 commits will get different hashes. The linear history produced by rebase may be prettier than the directed acyclic graph produced by merge and preferred in some repositories, but it doesn't matter for mathlib since all PRs will be squashed merged into master.

Michael Stoll (Jul 14 2022 at 19:05):

Now that multiplicative characters are there, I think it makes sense to review quadratic characters and redefine them as mul_chars. Roughly, define quadratic_char' like quadratic_char is now defined (as a map from a monoid_with_zero to the integers), prove the relevant properties (most importantly multiplicativity when the domain is a finite field), and then define quadratic_char to be of type mul_char F ℤ. Then the API for multiplicative characters can be used to prove further properties; this should simplify the code in number_theory/legendre_symbol/quadratic_char.lean.

@Riccardo Brasca @Anne Baanen @Yaël Dillies @Kevin Buzzard @Johan Commelin
Does this sound reasonable to you?

Michael Stoll (Jul 14 2022 at 20:03):

In the same way, zmod.χ₄ and friends should be defined as mul_char (zmod 4) ℤ etc.

Michael Stoll (Jul 14 2022 at 20:12):

In the end, there is not that much simplification in quadratic_char.lean, but at least the proof of quadratic_char_sum_zero is now a one-liner.

Michael Stoll (Jul 16 2022 at 11:23):

#15418

Johan Commelin (Jul 16 2022 at 17:19):

Next week I hope to do a lot of PR reviewing. For now, I will just "request review" myself.

Michael Stoll (Jul 16 2022 at 18:40):

OK, thanks! I'll look at additive characters next...

Michael Stoll (Jul 16 2022 at 20:52):

Of course, @Riccardo Brasca @Anne Baanen @Kevin Buzzard you are also welcome to have a look at #15418!

Riccardo Brasca (Jul 16 2022 at 21:07):

I've left a review.

Michael Stoll (Jul 18 2022 at 11:45):

Hmm. bors if failing with an error message

Error: /home/lean/actions-runner/_work/mathlib/mathlib/src/algebra/module/localized_module.lean:167:26:
unknown identifier 'has_scalar'

that refers to a completely unrelated file.

Yaël Dillies (Jul 18 2022 at 11:46):

has_scalar was renamed to has_smul recently. Try merging master.

Michael Stoll (Jul 18 2022 at 11:47):

Did that happen between CI being satisfied earlier today and bors trying to merge?

Yaël Dillies (Jul 18 2022 at 11:47):

Satisfied where?

Michael Stoll (Jul 18 2022 at 11:48):

I mean, the PR was green before I told bors to merge it...

Riccardo Brasca (Jul 18 2022 at 11:49):

It's not your fault, just ignore the message

Yaël Dillies (Jul 18 2022 at 11:49):

You know how bors works, right? It puts PRs in batches and when a batch fails it splits it up. The batch your PR was in failed, but that doesn't mean it comes from your PR (here bors says it is "retrying...").

Riccardo Brasca (Jul 18 2022 at 11:49):

Your PR was included in a batch that failed, because of another PR (#14470 I think)

Michael Stoll (Jul 18 2022 at 11:52):

That sounds plausible, that PR is on module localization...
OK; I'll wait and see (have to teach soon anyway...)

Michael Stoll (Jul 18 2022 at 18:34):

I'm now doing additive characters. I'll open a separate topic for that.

Michael Stoll (Jul 18 2022 at 18:36):

See here.


Last updated: Dec 20 2023 at 11:08 UTC