bijection `range n → zmod n`?

Stream: Is there code for X?

[Michael Stoll]

Is something like the following in the library somewhere?

lemma range_to_zmod_bijective (n : ℕ) (hn : n ≠ 0) :  function.bijective (λ (a : range n), (a : zmod n)) := sorry

[Yaël Dillies]

We have something stronger, namely docs#equiv.subtype_congr

[Michael Stoll]

That does not seem to give me what I want, at least not directly. How would I use it here?

[Yaël Dillies]

↥(range n) is the subtype {m : ℕ // m ∈ range n}. zmod n is fin n, which is {m : ℕ // 0 < m}. Hence equiv.subtype_congr mem_range : ↥(range n) ≃ zmod n.

[Yaël Dillies]

If now you care about the fact that it's coe and not another function, you can try showing that it's equal to the equiv.subtype_congr above, which I believe is an API lemma already.

[Adam Topaz]

You can also just use docs#zmod.nat_cast_zmod_val along with docs#zmod.val_lt

[Michael Stoll]

equiv.subtype_congr mem_range doesn't typecheck:

type mismatch at application
  equiv.subtype_congr mem_range
term
  mem_range
has type
  ?m_1 ∈ range ?m_2 ↔ ?m_1 < ?m_2 : Prop
but is expected to have type
  {x // ?m_2 x} ≃ {x // ?m_3 x} : Type ?

[Kevin Buzzard]

@Yaël Dillies does equiv.subtype_congr say what you think it says?

[Yaël Dillies]

Oh, I do not mean equiv.subtype_congr indeed...

[Yaël Dillies]

docs#equiv.subtype_equiv_right

[Michael Stoll]

equiv.subtype_equiv_right mem_range also does not typecheck:

type mismatch at application
  equiv.subtype_equiv_right mem_range
term
  mem_range
has type
  ?m_1 ∈ range ?m_2 ↔ ?m_1 < ?m_2
but is expected to have type
  ∀ (x : ?m_1), ?m_2 x ↔ ?m_3 x

[Yaël Dillies]

Remove one explicit argument: equiv.subtype_equiv_right (λ _, mem_range)

[Michael Stoll]

equiv.subtype_equiv_right (@mem_range _) seems to look better.

[Michael Stoll]

Still, I don't see yet how to go from

{x // (λ (m : ℕ), m ∈ range n) x} ≃ {x // (λ (m : ℕ), m < n) x}

to

bijective (λ (a : ↥(range n)), ↑a)

[Adam Topaz]

docs#equiv.bijective

[Yaël Dillies]

Try convert (equiv.subtype_equiv_right $ λ _, mem_range).bijective.

[Yaël Dillies]

If you want a more mathlib-like lemma which you can't bash by the hacky approach I just gave you, here it is:

open set

variables {a n : ℕ}

lemma nat.cast_zmod_inj_on : (Ico a (a + n)).inj_on (coe : ℕ → zmod n) := sorry

[Michael Stoll]

convert (equiv.subtype_equiv_right (@mem_range n)).bijective leaves me with two goals, zmod n = {x // x < n} and (λ (a : ↥(range n)), ↑a) == ⇑(equiv.subtype_equiv_right mem_range).
I'm already having problems with the first...

[Yaël Dillies]

Oh, you must case on n first.

[Adam Topaz]

Even then you will need to apply some exts and prove that x % (n+1) = x when x < n+1.

[Yaël Dillies]

This is likely very relevant: #10888

[Yaël Dillies]

In particular, docs#nat.mod_inj_on_Ico

[Eric Wieser]

What is range here? The original question isn't a mwe

[Eric Wieser]

docs#range

[Yaël Dillies]

I assumed docs#finset.range

[Michael Stoll]

range is finset.range

[Adam Topaz]

import data.zmod.basic

lemma range_to_zmod_bijective (n : ℕ) (hn : n ≠ 0) : function.bijective (λ (a : finset.range n), (a : zmod n)) :=
begin
  cases n, contradiction,
  let e : finset.range (n+1) ≃ zmod (n+1) := (equiv.subtype_equiv_right (λ _ , finset.mem_range)),
  convert e.bijective using 1, ext ⟨x⟩, dsimp [e],
  simp only [fin.coe_of_nat_eq_mod, ne.def, nat.succ_ne_zero, not_false_iff, finset.mem_range] at *,
  exact nat.mod_eq_of_lt x_property,
end

[Adam Topaz]

But I think just proving this directly would be even shorterr

[Eric Wieser]

What's the goal after the convert there?

[Michael Stoll]

Thanks.
What do you mean by "this" or by "directly"?

[Adam Topaz]

I mean proving this just by proving that the map is injective and surjective.

[Michael Stoll]

That's what I had in mind first (and would have tried had the answer just been "no") :smile:

[Adam Topaz]

It might be worthwhile to have that equiv in mathlib in any case.

[Yaël Dillies]

Yaël Dillies said:

In particular, docs#nat.mod_inj_on_Ico

Let me insist on this.

[Adam Topaz]

What's wrong with docs#nat.mod_eq_of_lt ?

[Yaël Dillies]

I believe Michael should first prove

lemma nat.cast_zmod_inj_on : (Ico a (a + n)).inj_on (coe : ℕ → zmod n) := sorry
lemma nat.cast_zmod_bij_on : (Ico a (a + n)).bij_on (coe : ℕ → zmod n) univ := sorry

[Adam Topaz]

Ah ok.

[Michael Stoll]

I'd rather get on with putting Legendre symbols right...

[Yaël Dillies]

Welcome to mathlib :upside_down:

[Eric Wieser]

Presumably these should be proved for fin too? (from which the zmod cases follow easily by a case split)

[Michael Stoll]

BTW, what is preferred notation: ∑ (a : finset.range p), ... vs. ∑ (a : Ico 0 p), ...?

[Eric Wieser]

Probably ∑ a in finset.range p

[Michael Stoll]

OK, that's what I did:

theorem legendre_sym_sum_zero (hp : p ≠ 2) : ∑ (a : finset.range p), legendre_sym p a = 0 := sorry

[Yaël Dillies]

... which does not mean the same but is what you want, unless you need to access the proof that a < p.

[Michael Stoll]

The "old" file has lots of Icos...

[Eric Wieser]

∑ (a : finset.range p) is different to ∑ a in finset.range p

[Eric Wieser]

∑ (a : finset.range p) means ∑ a in (finset.univ : finset (finset.range p)),

[Michael Stoll]

By now, legendre_sym p a reduces to quadratic_char p (a : zmod p), so a < p is not needed.

[Yaël Dillies]

Michael Stoll said:

The "old" file has lots of Icos...

That's likely not a bad thing. How were they used?

[Michael Stoll]

For stuff related to Gauss' Lemma and Eisenstein's Lemma, mostly.

[Michael Stoll]

If I do ∑ (a ∈ finset.range p), legendre_sym p a = 0, then I get an error message

failed to synthesize type class instance for
p : ℕ,
_inst_1 : fact (prime p),
hp : p ≠ 2
⊢ fintype ℤ

Is that because somewhere p ≠ 0 is needed?

[Eric Wieser]

That's still not what I wrote

[Eric Wieser]

You need to literally write in

[Eric Wieser]

∑ (a ∈ finset.range p), is parsed by lean as ∑ a in (finset.univ : finset ℤ), ∑ a in (finset.univ : finset (a ∈ finset.range p)),

[Michael Stoll]

∑ (a in finset.range p), legendre_sym p a = 0 gives invalid expression starting at ...

[Mario Carneiro]

no parens

[Eric Wieser]

Eric Wieser said:

Probably ∑ a in finset.range p

[Yaël Dillies]

Please copy what we write literally. Syntax is demanding.

[Michael Stoll]

Now my proof breaks down... :disappointed:

[Michael Stoll]

I was using fintype.sum_bijective (to reduce to the similar sum when a runs through zmod p).

[Yaël Dillies]

That's okay. We have similar lemmas for the usual sums.

[Yaël Dillies]

docs#finset.sum_bij

[Michael Stoll]

docs#finset.sum_bij has lots of arguments; docs#fintype.sum_bijective uses bijective directly...

[Eric Wieser]

You can also use docs#finset.sum_subtype` to get to a different form

[Michael Stoll]

I somehow find this difficult to use to get from the sum over a in range p to the original sum over a : range p.
Sorry, I have not yet a lot of experience with how sums, sets, subtypes work.

[Adam Topaz]

One thing to keep in mind is that these finite sums are always sums over some finset (in fact, these are notation for docs#finset.sum ). That how I remember that \sum a : X, ... is shorthand for the sum over finset.univ : finset X, and \sum a in S, ... where S is a finset X is shorthand for the sum over the finset S itself.

[Michael Stoll]

In terms of what I am summing over, I don't really see a difference between univ (range n) and range n.

[Michael Stoll]

Is the only difference that in the first case, range n (or rather, the corresponding subtype) is considered to be the universe, and in the second case, the universe is nat?

[Mario Carneiro]

yes, they are equal, except that the type of the variable in the two cases is different so you need a .1 or \u when using it in the body

[Mario Carneiro]

there is a theorem that says they are equal which you can use if you want to recover your old proof

[Kevin Buzzard]

Yes that's right, remember that a finset is a term not a type, and the type of the finset is different in each case

[Michael Stoll]

Is that docs#finset.sum_subtype mentioned by Eric Wieser? It is not obvious to me how to use that.

[Michael Stoll]

Mario Carneiro said:

yes, they are equal, except that the type of the variable in the two cases is different so you need a .1 or \u when using it in the body

Is that docs#finset.sum_subtype mentioned by Eric Wieser? It is not obvious to me how to use that.

[Kevin Buzzard]

univ (range n) has type finset (probably some term coerced to a type) and finset.range n has type finset nat

[Kevin Buzzard]

There's this funny up-arrow which can coerce terms to types, so you can make a type out of a finset, but the question is whether it's a good idea!

[Michael Stoll]

Anyway, I am still stuck at the proof. Right now, it looks like this.

theorem legendre_sym_sum_zero (hp : p ≠ 2) : ∑ a in finset.range p, legendre_sym p a = 0 :=
begin
  rw [← quadratic_char_sum_zero p hp],
  let red : finset.range p → zmod p := λ a, a,
  have he := range_to_zmod_bijective p (nat.prime.ne_zero _inst_1.1),
  have h : ∀ (a : finset.range p), legendre_sym p a = quadratic_char p (a : zmod p) :=
  by { sorry },
  have t := finset.sum_bij (λ x _, red x)
              (λ x _, mem_univ (red x))
              (λ x _, h x)
              (λ x x' _ _ h, he.injective h)
              (λ y _, (he.surjective y).imp $ λ a h, ⟨mem_univ _, h.symm⟩),
  simp only [coe_coe] at t,
  rw ← t,
  sorry
end

[Michael Stoll]

The stuff in the have t := ...was copied from the source of fintype.sum_bijective (or rather, ...prod...); I would not claim I do really understand what it does.

[Michael Stoll]

The goal I am left with at the last sorry is
∑ (a : ℕ) in range p, legendre_sym p ↑a = ∑ (x : ↥(range p)), legendre_sym p ↑↑x

[Mario Carneiro]

Michael Stoll said:

Mario Carneiro said:

yes, they are equal, except that the type of the variable in the two cases is different so you need a .1 or \u when using it in the body

Is that docs#finset.sum_subtype mentioned by Eric Wieser? It is not obvious to me how to use that.

No, the most direct theorem stating this is docs#finset.sum_finset_coe

[Michael Stoll]

For some reason, a sum over something of the form (x : <type>) shows up again.

[Mario Carneiro]

you can see from the number of up arrows involved in the theorem statement why we prefer the right hand side to the left side

[Eric Wieser]

docs#finset.sum_coe_sort is likely a better fit

[Michael Stoll]

Apart from the order of arguments, they look the same to me.

[Michael Stoll]

OK, now I have

theorem legendre_sym_sum_zero (hp : p ≠ 2) : ∑ a in finset.range p, legendre_sym p a = 0 :=
begin
  rw [← quadratic_char_sum_zero p hp],
  let red : finset.range p → zmod p := λ a, a,
  rw ← finset.sum_finset_coe ((legendre_sym p) ∘ (@coe ℕ ℤ _)) (range p),
  refine fintype.sum_bijective red (range_to_zmod_bijective p (nat.prime.ne_zero _inst_1.1)) _ _ _,
  intro x,
  simp only [legendre_sym, red, coe_coe, int.cast_coe_nat, comp_app],
end

which looks reasonable to me.

[Eric Wieser]

What's the statement of docs#quadratic_char_sum_zero?

[Michael Stoll]

The above is not an MWE.

[Michael Stoll]

quadratic_char_sum_zero is a lemma further up in the file. The statement is

lemma quadratic_char_sum_zero (hp : p ≠ 2) : ∑ (a : zmod p), quadratic_char p a = 0 := ...

and the definition of quadratic_char is

def quadratic_char (p : ℕ) (a : zmod p) : ℤ :=
if      a = 0           then  0
else if a ^ (p / 2) = 1 then  1
                        else -1

[Michael Stoll]

I assume writing the sum over (a : zmod p) is less of an issue here, since zmod p is finite ?

[Eric Wieser]

Yes, I just wonder if it would be easier to prove the fin.range version first

[Michael Stoll]

The alternative being a in univ (zmod p) ?

[Eric Wieser]

They're identical, one is syntax for the other

[Michael Stoll]

Eric Wieser said:

Yes, I just wonder if it would be easier to prove the fin.range version first

I'm using the ring structure of zmod p in the proof.

[Michael Stoll]

The idea is that there is some b : zmod p such that quadratic_char p b = -1; use multiplicativitiy of the character and the fact that multiplication by b is a permutation of zmod p.

[Junyan Xu]

Michael Stoll said:

def quadratic_char (p : ℕ) (a : zmod p) : ℤ :=
if      a = 0           then  0
else if a ^ (p / 2) = 1 then  1
                        else -1

If I were to define this I would just do a^(p/2) which mathlib knows is a monoid_hom (docs#pow_monoid_hom), then show its image lies in the submonoid {0,1,-1} ⊆ zmod p, so I get a monoid_hom to the submonoid (docs#monoid_hom.mrange_restrict, docs#submonoid.inclusion), then compose with the monoid_hom {0,1,-1} →* ℤ (seems missing, but {0,1,-1} happens to be iso to sign_type and we have cast_hom there).

[Michael Stoll]

This would require p to be an odd prime to work, and I would like to avoid assuming this in the definition.

[Yaël Dillies]

Would it, though?

[Michael Stoll]

Well, a ^ (p /2) would not in general be 0, 1, or -1. Consider, e.g., p = 6...

[Michael Stoll]

And if p = 2, there is no difference between 1 and -1 in zmod p.

[Yaël Dillies]

But p = 2 works as expected, right?

[Michael Stoll]

Maybe. The submonoid {0,1,-1} is the same as {0,1} in zmod 2; I don't know if this would cause problems.

[Junyan Xu]

I think you only intend to use it when p is a prime, right? Otherwise it's not a character (if a ^ (p / 2) = 1 then 1 only do what you intend when p is a prime). So maybe just add p.prime as an argument of quadratic_char? I agree that p=2 needs special treatment when defining the hom from the submonoid {0,1,-1} of zmod p to ℤ, but doing a if..else on p seems better than if..else on a.

[Michael Stoll]

My impression was that it is preferred to define total functions, so that adding p.prime as an argument should be avoided.

[Eric Rodriguez]

Junyan Xu said:

Michael Stoll said:

def quadratic_char (p : ℕ) (a : zmod p) : ℤ :=
if      a = 0           then  0
else if a ^ (p / 2) = 1 then  1
                        else -1

If I were to define this I would just do a^(p/2) which mathlib knows is a monoid_hom (docs#pow_monoid_hom), then show its image lies in the submonoid {0,1,-1} ⊆ zmod p, so I get a monoid_hom to the submonoid (docs#monoid_hom.mrange_restrict, docs#submonoid.inclusion), then compose with the monoid_hom {0,1,-1} →* ℤ (seems missing, but {0,1,-1} happens to be iso to sign_type and we have cast_hom there).

(note that the sign stuff is merging today - we have mul_equiv sign_type $ fin 3 but not the zmod version - this should be doable by composing the mul_equiv from zmod to fin, but I don't think that exists, especially with the right definitional equalities)

[Michael Stoll]

At some point, one will have to show that a ^ (p / 2) is 1 or -1 when a \ne 0 and p is a prime; the question is perhaps, when. I imagine it would be a bit awkward to do that within the definition...

[Eric Rodriguez]

Michael Stoll said:

My impression was that it is preferred to define total functions, so that adding p.prime as an argument should be avoided.

this is usually if it's more convenient; it seems here that it's less so, especially as we get less bundling

[Eric Wieser]

"mul_equiv from zmod to fin" it's docs#mul_equiv.refl

[Eric Rodriguez]

of course :)

[Junyan Xu]

It's not necessarily a character when p is not prime but I guess we are fine with junk values :)

Michael Stoll said:

At some point, one will have to show that a ^ (p / 2) is 1 or -1 when a \ne 0 and p is a prime; the question is perhaps, when. I imagine it would be a bit awkward to do that within the definition...

I would first define the {0,1,-1} submonoid (and the hom to ℤ), then prove the lemma saying pow_monoid_hom (p/2) a ∈ the submonoid under the assumptions, then the proof of the submonoid inclusion should be short enough to fit in submonoid.inclusion (by { ... }).

[Junyan Xu]

Defining a monoid_hom from an arbitrary finite field F_q to ℂ would facilitate the definition of higher (cubic, etc.) characters, but it depends on the choice of a (q-1)th primitive root both in the finite field and in ℂ ...

[Eric Rodriguez]

In some way, I guess this is docs#is_cyclotomic_extension.from_zeta_aut composed with an algebra map... under our definition, is_cyclotomic_extension \C \C S for all S. We haven't made a cyclotomic_extension instance for either C or F_q (and I guess F_q is more work...)

[Eric Rodriguez]

oh, we only need the F_q instances, but I digress

[Michael Stoll]

What would be the advantage(s) of doing it the way Junyan Xu suggests over leaving the definition as is and proving suitable API lemmas (including

def quadratic_char_hom : zmod p →* ℤ :=
{ to_fun := quadratic_char p, map_one' := quadratic_char_one  p, map_mul' := quadratic_char_mul p }

)?

[Eric Wieser]

I think the main difference is that if I understand the above correctly, the latter (with suitable conditions) lets you pick a definitionally nicer to_fun that avoids the need for the ifs

[Junyan Xu]

Eric Rodriguez said:

... docs#is_cyclotomic_extension.from_zeta_aut composed with an algebra map...

I don't think there can be an algebra_map from char p to char 0 ...

The current definition of quadratic_char may be fine if it's just a standalone thing, but it doesn't seem to fit in the big picture as a special case of multiplicative characters from (the multiplicative group) of a finite field to ℂ. With the current definition the proofs may be less reusable. I could see that quadratic character is indeed somewhat special though, as it's "unique" because {1,-1} has trivial automorphism group, and it fits in ℤ with no need of ℂ, so maybe it warrants special treatment.

[Michael Stoll]

One could define quadratic_char for finite fields of odd characteristic (or maybe also define it as the indicator function of the nonzero elements when the characteristic is 2) as a monoid_hom into the integers. Maybe this is a suitable level of generality?

[Eric Rodriguez]

ah, d'ah, there is I think somewhere an induced map to the roots_of_unity, but there was some issues with +/* mixing.

[Eric Rodriguez]

I feel like I'm getting confused and talking about the wrong things right now, sorry. I feel like most of the glue is there, though.

[Michael Stoll]

Junyan Xu said:

The current definition of quadratic_char may be fine if it's just a standalone thing, but it doesn't seem to fit in the big picture as a special case of multiplicative characters from (the multiplicative group) of a finite field to ℂ. With the current definition the proofs may be less reusable. I could see that quadratic character is indeed somewhat special though, as it's "unique" because {1,-1} has trivial automorphism group, and it fits in ℤ with no need of ℂ, so maybe it warrants special treatment.

I think there should be multiplicative characters into any ring (or even monoid with zero). Why restrict to ℂ as the target?

[Michael Stoll]

As a side question, is there a way to exress that ψ is an additive character from a field F into some ring (or mutiplicative monoid) R? I.e., ψ(x+y) = ψ(x)*ψ(y) for all x y : F.

[Yaël Dillies]

You have to use docs#multiplicative, docs#additive

[Michael Stoll]

That looks a bit painful. In particular, since there are two possibilities and no obvious reason to prefer one over the other...

[Eric Wieser]

Usually the choice is obvious, and we wrap the weaker of the two types in multiplicative or additive

[Eric Wieser]

In practice we tend not to use the bundled version as the canonical API for those cases though; but it's still useful for golfing proofs

[Eric Rodriguez]

Junyan Xu said:

Eric Rodriguez said:

... docs#is_cyclotomic_extension.from_zeta_aut composed with an algebra map...

I don't think there can be an algebra_map from char p to char 0 ...

The current definition of quadratic_char may be fine if it's just a standalone thing, but it doesn't seem to fit in the big picture as a special case of multiplicative characters from (the multiplicative group) of a finite field to ℂ. With the current definition the proofs may be less reusable. I could see that quadratic character is indeed somewhat special though, as it's "unique" because {1,-1} has trivial automorphism group, and it fits in ℤ with no need of ℂ, so maybe it warrants special treatment.

the real answer to this is docs#is_primitive_root.power_basis + docs#power_basis.lift, sorry about all the nonsense I wrote before

[Eric Rodriguez]

I'm not sure if we ever figured out weaker conditions for is_primitive_root.power_basis, but I still need to write power_basis.map_conjugate (+ get back to flt regular...)

[Eric Rodriguez]

wait, no, still wrong. do we not have something that just sends the generator of a power-basis to something, and then just says "yes that's good enough"? maybe just for basis

[Michael Stoll]

I am playing around with the following.

import field_theory.finite.basic

namespace char

def quadratic_char (F : Type*) [field F] [fintype F] (a : F) : ℤ :=
if a = 0 then 0 else if a^((fintype.card F) / 2) = 1 then 1 else -1

end char

but get the complaint that Lean doesn't know how to deduce that a^((fintype.card F) / 2) = 1 is decidable.
What is the best way to get around that?

[Michael Stoll]

... and even decidable (a = 0).

[Eric Rodriguez]

decidable_eq F or just classical or something

[Michael Stoll]

[decidable_eq F] seems to be working; thanks.

[Michael Stoll]

Michael Stoll said:

Junyan Xu said:

The current definition of quadratic_char may be fine if it's just a standalone thing, but it doesn't seem to fit in the big picture as a special case of multiplicative characters from (the multiplicative group) of a finite field to ℂ. With the current definition the proofs may be less reusable. I could see that quadratic character is indeed somewhat special though, as it's "unique" because {1,-1} has trivial automorphism group, and it fits in ℤ with no need of ℂ, so maybe it warrants special treatment.

I think there should be multiplicative characters into any ring (or even monoid with zero). Why restrict to ℂ as the target?

I guess this would just be a monoid_with_zero_hom?

[Kevin Buzzard]

Note Ashvni's work on Dirichlet characters here: https://github.com/leanprover-community/mathlib/blob/p-adic/src/number_theory/dirichlet_character.lean . I was telling her to PR it only today :-)

[Junyan Xu]

monoid_with_zero_hom would be the correct type; what I am concerned with (and I think Eric also) is how to construct terms of that type. I don't think it needs to involve power basis or cyclotomic extension; since the multiplicative group of F_q is cyclic of order (q-1) so given a generator of (F_q)ˣ and an element x of another monoid satisfying x^(q-1) = 1 there's a unique monoid_with_zero_hom sending the generator to x. In the quadratic case with q odd, x is -1, and it makes no difference which generator we choose. There are some API useful for constructing the hom from (F_q)ˣ (docs#is_primitive_root.zmod_equiv_zpowers, docs#zmod.lift), but they don't include the zero element, haven't been specialized to the case of cyclic groups, and necessitates going back and forth between multiplicative and additive monoids. Although this approach involves a superfluous generator, it can be relatively easily connected to the a^(q/2) definition: the character is of order n (here n = 2) iff the its image has order n, iff its kernel is the subgroup of order (q-1)/n; since a ↦ a^((q-1)/n) has the same kernel and image the nth roots of unity, the character factors as a ↦ a^((q-1)/n) composed with a hom from the nth roots of unity in the domain to the codomain (iso onto the image of the character). I admit this is maybe too complicated for the current purpose.

Dirichlet characters have domain zmod n (n not necessarily prime) instead of a finite field, so that work seems complementary to the current discussion.

[Michael Stoll]

Kevin Buzzard said:

Note Ashvni's work on Dirichlet characters here: https://github.com/leanprover-community/mathlib/blob/p-adic/src/number_theory/dirichlet_character.lean . I was telling her to PR itI only today :-)

Is this going in the direction of Dirichlet's theorem on primes in arithmetic progressions? That would be great!

[Yaël Dillies]

@Mantas Baksys, you might be interested in this.

[Kevin Buzzard]

@Michael Stoll it's going in the direction of defining generalised Bernoulli numbers and showing that they're values of $p$-adic L-functions! Interestingly, I have seen with my own eyes a proof of Dirichlet's theorem in Lean; it was written by a computer program Metamath 0, which translated the proof which they have in metamath into a 30 megabyte unreadable but compiling Lean proof.

[Michael Stoll]

The relevant question is perhaps rather whether Dirichlet's theorem on primes in AP is in mathlib, so that one can use the statement in further work...

[Alex J. Best]

Nope, the closest we have is docs#nat.exists_prime_ge_modeq_one right now in mathlib unfortunately

[Michael Stoll]

Do we have (classical, not p-adic) L-functions?

[Riccardo Brasca]

Complex analysis didn't exist until a couple of months ago, so anything related to it is in very early stages

[Kevin Buzzard]

Michael -- the joke is that we are going to end up with p-adic zeta functions before the Riemann zeta function! Unfortunately recent progress in complex analysis has made me more worried about whether I can pull this joke off :-/

[Michael Stoll]

That's a bad joke, as far as I am concerned... :smile:

[Yaël Dillies]

@Michael Stoll, you have to click on the topic you want to respond to. Else, your message will just be lost in the stream of messages.

[Riccardo Brasca]

I've moved the message.

[Michael Stoll]

Sorry, I didn't notice I had another message in focus.

[Michael Stoll]

I'm struggling with additive characters on a (finite) field F with values in a commutative ring R, which I try to define as ψ : (multiplicative F) →* R.
Now, for a : F I would like to define the character that sends x : F to ψ (a*x) (where the multiplication is that of F).
I have got this far:

import tactic field_theory.finite.basic
variables (F : Type*) [field F] [fintype F] [decidable_eq F]
variables (R : Type*) [comm_ring R]

def mul_shift' (ψ : (multiplicative F) →* R) (a : F) : (multiplicative F) → R := λ x, let y : F := a * (x : F) in ψ y

lemma mul_shift_one (ψ : (multiplicative F) →* R) (a : F) : mul_shift' F R ψ a 1 = 1 :=
begin
  simp only [mul_shift'],
  have h₀ : (1 : multiplicative F) = (0 : F) := rfl,
  rw [h₀, mul_zero, ← h₀],
  exact ψ.map_one',
end

lemma mul_shift_mul (ψ : (multiplicative F) →* R) (a : F) (x y : multiplicative F) :
  mul_shift' F R ψ a (x * y) = mul_shift' F R ψ a x * mul_shift' F R ψ a y :=
begin
  simp only [mul_shift'],
  have h₁ : x * y = ((x + y) : F) := rfl,
  rw [h₁, mul_add],
  have h := ψ.map_mul' (a * x) (a * y),
  have h₂ : (((a * x) : F) : multiplicative F) * (a * y) = ((a * x) + (a * y) : F) := sorry,
  sorry
end

/-- Define the multiplicative shift of an additive character -/
def mul_shift (ψ : (multiplicative F) →* R) (a : F) : (multiplicative F) →* R :=
{ to_fun := mul_shift' F R ψ a, map_one' := mul_shift_one F R ψ a,
  map_mul' := mul_shift_mul F R ψ a }

I am having problems with getting the types in h₂ right: all the "outer" multiplications should be the multiplication of F, whereas the "inner" one in the left should be that of multiplicative F. But it is very hard to do this, since Lean seems to convert very eagerly between the two -- I somehow cannot get it to interpret the inner multiplication correctly.
Any suggestions?

[Eric Wieser]

You should never cast between the two types, use docs#multiplicative.to_add (so x.to_add instead of (x : F))

[Eric Wieser]

and docs#multiplicative.of_add in the other direction

[Eric Wieser]

I think in this case you just want φ.comp (add_monoid_hom.mul_right a).to_multiplicative

[Eric Wieser]

docs#add_monoid_hom.to_multiplicative

[Michael Stoll]

Ah, that makes sense. I was doing things in an overly pedestrian way...

[Kevin Buzzard]

It has taken people quite a while to figure out how to make these things work effectively. There are all sorts of issues in the background involving whether definitions should be irreducible etc, and of course figuring out how to make it all work in one theorem prover might not give you answers about how best to do it in another one. These things are often just learnt by people asking here about how to do it.