This is part of a port of
https://github.com/laughinggas/p-adic-L-functions/blob/main/src/dirichlet_character/basic.lean

Is there a specific reason for not using MulChar (ZMod n) R as the definition of DirichletCharacter R n?

Also, there is maybe some ambiguity as to what should be the correct definition of a "Dirichlet character mod n".
I'm more used to it being defined as a map from the integers to (some monoid with zero) R that is obtained as the composition of the reduction map $\mathbb Z \to \mathbb Z/n \mathbb Z$ and a multiplicative character on $\mathbb Z/n \mathbb Z$. Of course, both versions are equivalent, and it is perhaps a question of what is more convenient...

Is there a specific reason for not using MulChar (ZMod n) R as the definition of DirichletCharacter R n?

I thought it makes sense to give it a separate name since there will be a few files on it. Also, I think MulChar is more in sync with asso_dirichlet_character, which has now been replaced in terms of ofUnitHom.

Also, there is maybe some ambiguity as to what should be the correct definition of a "Dirichlet character mod n". I'm more used to it being defined as a map from the integers to (some monoid with zero) R that is obtained as the composition of the reduction map Z→Z/nZ and a multiplicative character on Z/nZ. Of course, both versions are equivalent, and it is perhaps a question of what is more convenient...

I have at least 300-500 lines of code (in the folder dirichlet_character here : https://github.com/laughinggas/p-adic-L-functions/tree/main/src/dirichlet_character ) based on this definition. It comes with a lot of nice properties such as change_level, which is a monoid homomorphism. One can choose to make a second definition as a function from the integers (I am happy to contribute to that!), and show the equivalence of the two definitions.

This PR/issue depends on:

• [Merged by Bors] - feat: ZMod.castHom_self #7013
  By Dependent Issues (🤖). Happy coding!

Is there a specific reason for not using MulChar (ZMod n) R as the definition of DirichletCharacter R n?

I thought it makes sense to give it a separate name since there will be a few files on it. Also, I think MulChar is more in sync with asso_dirichlet_character, which has now been replaced in terms of ofUnitHom.

It certainly makes sense to give it a separate name. What I mean is why not define it as

@[reducible] def DirichletCharacter (R : Type) [CommMonoidWithZero R] (n : ℕ) := MulChar (ZMod n) R

instead? The rationale being that in many (most?) applications, you also want to evaluate the characters at non-units. (And, of course, that there is already an API for MulChars.)

Also, there is maybe some ambiguity as to what should be the correct definition of a "Dirichlet character mod n". I'm more used to it being defined as a map from the integers to (some monoid with zero) R that is obtained as the composition of the reduction map Z→Z/nZ and a multiplicative character on Z/nZ. Of course, both versions are equivalent, and it is perhaps a question of what is more convenient...

I have at least 300-500 lines of code (in the folder dirichlet_character here : https://github.com/laughinggas/p-adic-L-functions/tree/main/src/dirichlet_character ) based on this definition. It comes with a lot of nice properties such as change_level, which is a monoid homomorphism. One can choose to make a second definition as a function from the integers (I am happy to contribute to that!), and show the equivalence of the two definitions.

After some consideration, I think it is best to use MulChar (ZMod n) R (as opposed to maps from integers to R), since if χ is an object of this type, χ a for an integer a just works. And, as you indicate, this definition seems to be better suited for proving properties (which, I think, comes down to the fact that the units of ZMod n are a thing, whereas their preimage in the integers isn't really).

Is there a specific reason for not using MulChar (ZMod n) R as the definition of DirichletCharacter R n?

I thought it makes sense to give it a separate name since there will be a few files on it. Also, I think MulChar is more in sync with asso_dirichlet_character, which has now been replaced in terms of ofUnitHom.

It certainly makes sense to give it a separate name. What I mean is why not define it as

@[reducible] def DirichletCharacter (R : Type) [CommMonoidWithZero R] (n : ℕ) := MulChar (ZMod n) R

instead? The rationale being that in many (most?) applications, you also want to evaluate the characters at non-units. (And, of course, that there is already an API for MulChars.)

If you look at the following : https://github.com/laughinggas/p-adic-L-functions/blob/88c5750b71f90ae9a9964968f4eabcb994d6d279/src/dirichlet_character/basic.lean#L54 , I think the definition of MulChar is related more to asso_dirichlet_character. I removed the definition of asso_dirichlet_character from this port and have instead used the properties of MulChar instead.

Defining it as (ZMod n)ˣ →* Rˣ has the conceptual advantage of defining it on the smallest possible object, instead of either on ZMod n or even \Z with extra conditions. I agree that we should have convenient api to switch between the different incarnations.

OK; I guess the one reason why you want to work with homomorphisms on the unit group is that this gives you the correct notion of changing the level. I would suggest using the MulChar definition as the main one and then go via the equivalence to "unit homs" (toUnitHom/ofUnitHom) to do the level change etc:

def ZMod.unitsMap {n m : ℕ} (hm : n ∣ m) : (ZMod m)ˣ →* (ZMod n)ˣ := Units.map (ZMod.castHom hm (ZMod n))

@[reducible]
def DirichletCharacter (R : Type) [CommMonoidWithZero R] (n : ℕ) := MulChar (ZMod n) R

namespace DirichletCharacter

noncomputable def change_level {R : Type} [CommMonoidWithZero R] {n m : ℕ} (hm : n ∣ m) :
    DirichletCharacter R n →* DirichletCharacter R m :=
  { toFun := fun ψ ↦ MulChar.ofUnitHom (ψ.toUnitHom.comp (ZMod.unitsMap hm)),
    map_one' := by ext; simp,
    map_mul' := fun ψ₁ ψ₂ ↦ by ext; simp }

(I was working on that while you were already answering; this refers to the earlier point.
EDIT: (hopefully) corrected units_map to unitsMap...)

OK; I guess the one reason why you want to work with homomorphisms on the unit group is that this gives you the correct notion of changing the level. I would suggest using the MulChar definition as the main one and then go via the equivalence to "unit homs" (toUnitHom/ofUnitHom) to do the level change etc:

def ZMod.unitsMap {n m : ℕ} (hm : n ∣ m) : (ZMod m)ˣ →* (ZMod n)ˣ := Units.map (ZMod.castHom hm (ZMod n))

@[reducible]
def DirichletCharacter (R : Type) [CommMonoidWithZero R] (n : ℕ) := MulChar (ZMod n) R

namespace DirichletCharacter

noncomputable def change_level {R : Type} [CommMonoidWithZero R] {n m : ℕ} (hm : n ∣ m) :
    DirichletCharacter R n →* DirichletCharacter R m :=
  { toFun := fun ψ ↦ MulChar.ofUnitHom (ψ.toUnitHom.comp (ZMod.unitsMap hm)),
    map_one' := by ext; simp,
    map_mul' := fun ψ₁ ψ₂ ↦ by ext; simp }

(I was working on that while you were already answering; this refers to the earlier point. EDIT: (hopefully) corrected units_map to unitsMap...)

change_level is not the only reason I wish to work with the units. I am using Dirichlet characters to define the p-adic L-function. The definition of the p-adic L-function (attached below) and its properties (which is about 3000-5000 lines of code) depend on the Dirichlet character being defined on the units. I understand that this is equivalent to the definition you have given, however, it is not the same. Your definition coincides with the definition of the associated Dirichlet character, asso_dirichlet_character in the p-adic L-functions repository, which I reworded in terms of MulChar.ofUnitHom. The main reason why I am hesitant to completely remove the units is because it will involve rewriting a lot of proofs going ahead.

@MichaelStollBayreuth I can change the definition to be the following :
def DirichletCharacter (R : Type) [CommMonoidWithZero R] (n : ℕ) := MulChar.toUnitHom (ZMod n) R
but given the equivalence equivToUnitHom, I think it might be easier to keep the original definition?

Your help is much appreciated, thank you!

@MichaelStollBayreuth Do you think this can be merged now?

@MichaelStollBayreuth Do you think this can be merged now?

Yes.

One small comment about using the API for periodic but LGTM, thanks!

bors d+

✌️ mo271 can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

bors r+

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here.
For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

• Build
• Check all files imported
• Lint style