## Stream: general

### Topic: modp setoid

#### Johan Commelin (Jun 06 2019 at 00:58):

Can something like this be made to work?

namespace modp
variables (α : Type*) [comm_ring α] (p : ℕ) (hp : nat.prime p)

def rel : setoid α := submodule.quotient_rel (ideal.span ({p} : set α))

local attribute [instance] rel

variables {α p}
lemma pow_add (a b : α) : (a + b)^p ≈ a^p + b^p :=
_

end modp


#### Chris Hughes (Jun 06 2019 at 01:04):

Look at add_pow_char in algebra.char_p

#### Chris Hughes (Jun 06 2019 at 01:05):

and use quotient_ring.quotient instead of submodule.quotient

#### Chris Hughes (Jun 06 2019 at 01:06):

Or ideal.quotient. I forget the name.

#### Johan Commelin (Jun 06 2019 at 01:06):

I guess I should clarify (-;

#### Johan Commelin (Jun 06 2019 at 01:06):

I want to use the relation.

#### Johan Commelin (Jun 06 2019 at 01:06):

Point is that I want to do some computations with mv_polynomials over the integers, modulo p.

#### Johan Commelin (Jun 06 2019 at 01:06):

And using this relation would make for readable calc proofs

#### Reid Barton (Jun 06 2019 at 01:07):

Can you use mv_polynomials over the integers modulo p?

#### Chris Hughes (Jun 06 2019 at 01:07):

But isn't it easier to map everything into the quotient and use equality?

#### Johan Commelin (Jun 06 2019 at 01:07):

Otherwise you'll have ideal.quotient.mk (ideal.span ({p} : set (mv_polynomial int _)) all over the place...

use notation

#### Johan Commelin (Jun 06 2019 at 01:08):

I guess I could define a local notation for that... but then the proof state is still ugly

#### Chris Hughes (Jun 06 2019 at 01:08):

I don't like the fact that we can't quotient mod p without things being ugly.

#### Reid Barton (Jun 06 2019 at 01:12):

I was hoping you could use parameter but it doesn't seem to help

#### Johan Commelin (Jun 06 2019 at 01:12):

I would like to write

calc [mod p] foo = bar : blah
... = xyzzy : etc


#### Johan Commelin (Jun 06 2019 at 01:12):

And then coercions should take care of the rest

#### Reid Barton (Jun 06 2019 at 01:13):

You should at least be able to write calc foo =[p]= bar : blah ... = xyzzy : etc using notation

#### Reid Barton (Jun 06 2019 at 01:14):

though at that point I guess you should just define notation which depends on p

#### Johan Commelin (Jun 06 2019 at 01:16):

Isn't that what you are doing in your example?

#### Johan Commelin (Jun 06 2019 at 06:33):

Is interactive calc in core or in mathlib? I couldn't find it easily

#### Kevin Buzzard (Jun 06 2019 at 06:35):

Must be in core because it's in TPIL

#### Johan Commelin (Jun 06 2019 at 06:40):

Is that interactive calc or term-mode calc?

#### Reid Barton (Jun 06 2019 at 07:29):

I mean in a section you can define local notation which depends on a variable, so you don't need to write this funny =[p]= stuff.

#### Johan Commelin (Jun 06 2019 at 07:33):

I am currently experimenting with

notation x  modᵢ  I := ideal.quotient.mk I x
notation x  modₛ  s := ideal.quotient.mk (ideal.span s) x
notation x  modₑ  a := ideal.quotient.mk (ideal.span ({a})) x


#### Johan Commelin (Jun 06 2019 at 07:34):

This can probably be improved quite a bit, using priorities etc... but I've no idea what would be sensible.

#### Johan Commelin (Jun 06 2019 at 07:40):

namespace modp
variables {α : Type*} [comm_ring α] {p : ℕ} (hp : nat.prime p)

notation x  modᵢ  I := ideal.quotient.mk I x
notation x  modₛ  s := ideal.quotient.mk (ideal.span s) x
notation x  modₑ  a := ideal.quotient.mk (ideal.span ({a})) x

include hp
instance (h : ¬ is_unit (p : α)) : char_p (ideal.span ({p} : set α)).quotient p :=
⟨begin
intro n,
have helper : ∀ m : ℕ, (m : (ideal.span ({p} : set α)).quotient) =
ideal.quotient.mk (ideal.span ({p} : set α)) (m : α),
{ intro m, induction m with m ih, {refl}, simp [ih] },
split,
{ intro H,
rw [helper, ideal.quotient.eq_zero_iff_mem, ideal.mem_span_singleton] at H,
rcases H with ⟨c, hc⟩,
cases nat.coprime_or_dvd_of_prime hp n with hn hn,
swap, {exact hn},
have key := nat.gcd_eq_gcd_ab p n,
delta nat.coprime at hn, rw hn at key,
replace key := congr_arg (λ k : ℤ, (k : α)) key,
simp only [int.cast_coe_nat, int.cast_add, int.coe_nat_zero, int.cast_mul, int.cast_one,
int.coe_nat_succ, zero_add, hc] at key,
rw [mul_assoc, ← mul_add] at key,
exfalso, apply h,
rw is_unit_iff_exists_inv,
exact ⟨_, key.symm⟩ },
{ rintro ⟨c, rfl⟩,
apply eq_zero_of_zero_dvd,
use p,
rw [zero_mul, helper (p*c), ideal.quotient.eq_zero_iff_mem, nat.cast_mul],
exact ideal.mul_mem_right _ (ideal.subset_span \$ set.mem_singleton p) }
end⟩
.

example (a b : α) : ((a + b)^p modₑ (p : α)) = (a^p modₑ (p : α)) + (b^p modₑ (p : α)) :=
begin
sorry
end

end modp


#### Johan Commelin (Jun 06 2019 at 07:42):

Does simp see through notation?

#### Reid Barton (Jun 06 2019 at 07:47):

Everything sees through notation

Last updated: Dec 20 2023 at 11:08 UTC