feat(number_theory/legendre_symbol/mul_character): add new file mul_character.lean
#14716
Conversation
MichaelStollBayreuth
added
awaiting-review
github-actions
bot
removed
the
awaiting-CI
| end | ||
|
|
||
| /-- A multiplicative character is *nontrivial* if it takes a value `≠ 1` on a unit -/ | ||
| def is_nontrivial (χ : R →*₀ R') : Prop := ∃ (a : R), is_unit a ∧ χ a ≠ 1 |
There was a problem hiding this comment.
I would like to be able to write χ.is_nontrivial (or even χ.nontrivial). Does anyone see a simple way of getting this? Note that χ is a monoid_with_zero_hom, but we are in the mul_char namespace (and I think this is reasonable, even if at the end of the day a mul_char is just a monoid_with_zero_hom we don't want to use this not-so-friendly name. Will notation or abbreviation work?
| /-- A multiplicative character is *quadratic* if it takes only the values `0`, `1`, `-1` -/ | ||
| def is_quadratic (χ : R →*₀ R') : Prop := ∀ a, χ a = 0 ∨ χ a = 1 ∨ χ a = -1 | ||
|
|
||
| /-- Composition with an injective ring homomorphism preserves nontriviality -/ |
There was a problem hiding this comment.
| /-- Composition with an injective ring homomorphism preserves nontriviality -/ | |
| /-- Composition with an injective ring homomorphism preserves nontriviality. -/ |
| end | ||
|
|
||
| /-- For positive `n : ℕ`, define `χ ^ n` as `χ` composed with the `n`the power homomorphism -/ | ||
| def pow_pos (χ : R →*₀ R') {n : ℕ} (hn : 0 < n) : R →*₀ R' := |
There was a problem hiding this comment.
Wait, we don't have this?! I mean R →*₀ R' should get a has_mul instance, and so a ^ n should be defined.
There was a problem hiding this comment.
It has has_mul, but not has_pow (looking at the list of instances for the latter).
I think 0 ^ 0 = 1 is a problem here; that's why we need n to be positive.
There was a problem hiding this comment.
Ah sure, nonunits would not be mapped to 0. I am still surprised that we don't have has_pow (R →*₀ R') ℕ+. You can add this instance in general (not in this file), but I really suggest you define what a mul_char is, and prove that they are a... group under multiplication (they are? it's late, but it seems they are). In this way you can take power as you want.
But you have to be careful to not create diamonds.
|
This is replaced by a version that defines multiplicative characters as |
…entation (#14768) This is an alternative version of `number_theory/legendre_symbol/mul_character.lean`. It defines `mul_character R R'` as a `monoid_hom` that sends non-units to zero. This allows to define a `comm_group` structure on `mul_character R R'`. There is an alternative implementation in #14716 ([side by side comparison](legendre_symbol_mul_char...variant)). See the [discussion on Zulip](https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Implementation.20of.20multiplicative.20characters).
YaelDillies
removed
the
awaiting-review
This adds a new file
mul_character.leanto the foldernumber_theory/legendre_symbol/. It contains statements related to multiplicative characters on finite commutative rings.This is part of a sequence of PRs leading to the Gauss sum proof of quadratic reciprocity; see this Zulip topic.
There is an alternative implementation in #14768.
See the discussion on Zulip.