Implementation of multiplicative characters

Stream: maths

[Michael Stoll]

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]

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

[Michael Stoll]

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]

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

[Michael Stoll]

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

[Junyan Xu]

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

[Anne Baanen]

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]

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]

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

[Riccardo Brasca]

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]

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]

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

[Michael Stoll]

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

[Riccardo Brasca]

It's missing, but it's true?

[Riccardo Brasca]

It seems so

[Yaël Dillies]

Do you not need the monoids to be commutative?

[Riccardo Brasca]

Yes yes, in applications the monoids will be commutative

[Kevin Buzzard]

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

[Michael Stoll]

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]

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:
$(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]

But it does find has_mul...

[Adam Topaz]

Isn't the trivial monoid a monoid with zero where $1 = 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\}$ is empty

[Adam Topaz]

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

[Adam Topaz]

Or maybe assuming [nontrivial] is enough

[Michael Stoll]

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]

does docs#monoid_with_zero_hom.monoid not exist?

[Yaël Dillies]

It would be monoid_with_zero_hom.comm_monoid at any rate.

[Eric Wieser]

I'm wondering if we have the monoid of endomorphisms

[Reid Barton]

docs#monoid.End

[Reid Barton]

oh maybe you mean of something else

[Junyan Xu]

no docs#monoid_with_zero.End ...

[Reid Barton]

here you go docs#category_theory.End

[Michael Stoll]

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]

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

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

[Kevin Buzzard]

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]

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]

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

[Michael Stoll]

Kevin Buzzard said:

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

Thanks!

[Michael Stoll]

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]

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]

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

[Patrick Massot]

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]

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]

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

[Michael Stoll]

leanproject, version 0.0.8

[Patrick Massot]

That's ancient!

[Patrick Massot]

You should update mathlibtools

[Patrick Massot]

Something like pip install -U mathlibtools

[Michael Stoll]

leanproject, version 1.1.1

[Michael Stoll]

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

[Michael Stoll]

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

[Patrick Massot]

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

[Michael Stoll]

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]

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]

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]

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

[Michael Stoll]

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

[Riccardo Brasca]

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

[Riccardo Brasca]

I will have a look this weekend

[Michael Stoll]

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]

Try pulling again?

[Michael Stoll]

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

[Patrick Massot]

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

[Michael Stoll]

Yes. (#14768)

[Patrick Massot]

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

[Patrick Massot]

so git push -f

[Patrick Massot]

from your PR branch

[Michael Stoll]

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

[Patrick Massot]

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

[Patrick Massot]

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

[Michael Stoll]

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

[Patrick Massot]

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]

Is this what leanproject get-cache does?

[Michael Stoll]

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

[Patrick Massot]

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

[Patrick Massot]

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]

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

[Junyan Xu]

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]

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]

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

[Junyan Xu]

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]

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]

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]

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]

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]

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

[Michael Stoll]

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]

#15418

[Johan Commelin]

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

[Michael Stoll]

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

[Michael Stoll]

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

[Riccardo Brasca]

I've left a review.

[Michael Stoll]

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]

has_scalar was renamed to has_smul recently. Try merging master.

[Michael Stoll]

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

[Yaël Dillies]

Satisfied where?

[Michael Stoll]

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

[Riccardo Brasca]

It's not your fault, just ignore the message

[Yaël Dillies]

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]

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

[Michael Stoll]

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

[Michael Stoll]

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

[Michael Stoll]

See here.