Units of zmod 1

Stream: general

[Bolton Bailey]

The whole thread on fintypes got started because my computer failed to derive fintype for units (zmod n). I see why now: it works for units (zmod (n+1)) because data.zmod.basic has an instance of fintype only for [fact (0 < n)], but this doesn't work for units (zmod 0).

I'm trying to figure out how/if I can write an case-by-case instantiation for instance : Π (n : ℕ), fintype (units (zmod n))? I'm a bit weirded out by the n=1 case. Here, zmod 1 is defined as fin 1. But later in data.zmod.basic we have instance comm_ring : Π (n : ℕ), comm_ring (zmod n). comm_ring extends comm_monoid, which extends monoid which extends mul_one_class which extends has_one. Does this mean zmod 1 has_one? Does mathlib consider 1 to be 0 for this ring? Is 0 then a unit of zmod 1?

[Eric Wieser]

Yes, zmod 1 has 0 = 1

[Eric Wieser]

So I guess 0 is a unit there

[Bolton Bailey]

This means that p.prime ↔ fintype.card (units (zmod p)) = p - 1 is technically true, even for p=1, since the right hand side is miraculously false due to zmod 1 having this unit. Do I just write the theorem this way, or do I put an unnecessary (hp : 1 < p) to warn the user?

[Yakov Pechersky]

zmod 1 \~- fin 1 \~- unit are all the trivial ring

[Yakov Pechersky]

What do you mean by "warn the user"?

[Adam Topaz]

And what do you mean by "unnecessary"?

[Yakov Pechersky]

fintype.card (units (zmod 1)) = 1 because 0 = 1.

[Adam Topaz]

I don't see the issue with $p = 1$.

[Adam Topaz]

$1$ is not prime, and fintype.card (units (zmod 1)) = 1 which is different from 1 - 1.

[Mario Carneiro]

import data.zmod.basic

noncomputable instance units_zmod.fintype : Π n, fintype (units (zmod n))
| 0     := units_int.fintype
| (n+1) := units.fintype

[Mario Carneiro]

you can do a bit better here and make this a computable instance since being a unit in zmod n is decidable

[Bolton Bailey]

Yakov Pechersky said:

What do you mean by "warn the user"?

I figured it would save time for someone who is accidentally trying to prove a theorem that is false for n=1, but I guess if that happens you just include 1 < p in your own theorem.

[Bolton Bailey]

For example, I sometimes do library_search for a theorem, get no results, waste some time trying to implement the lemma myself, only to realize I was missing an edge case precondition, and with that precondition, library_search works instantly.

[Mario Carneiro]

slim_check can be useful for catching edge cases / missing preconditions, but it only works on computable predicates, generally theorems about lists and nat

[Mario Carneiro]

it's not likely to be able to show that your group is not actually finite

[Yakov Pechersky]

For the precondition case, sometimes "suggest" is able to suggest partial proofs

[Bolton Bailey]

Using this instance, I hit a snag soon after. Here is the mwe:

import data.zmod.basic
import data.fintype.basic
import field_theory.finite.basic
import group_theory.order_of_element

noncomputable instance units_zmod.fintype : Π n, fintype (units (zmod n))
| 0     := units_int.fintype
| (n+1) := units.fintype

lemma prime_iff_card_units (p : ℕ) :
  p.prime ↔ fintype.card (units (zmod p)) = p - 1
:=
begin
  split,
    { intro p_prime,
      exact @zmod.card_units p ({out := p_prime}),
    },
end

I get a long error message:

invalid type ascription, term has type
  @fintype.card
      (@units (zmod p)
         (@ring.to_monoid (zmod p)
            (@division_ring.to_ring (zmod p) (@field.to_division_ring (zmod p) (@zmod.field p _)))))
      (@units.fintype (zmod p)
         (@ring.to_monoid (zmod p)
            (@division_ring.to_ring (zmod p) (@field.to_division_ring (zmod p) (@zmod.field p _))))
         (@zmod.fintype p _)) =
    p - 1
but is expected to have type
  @fintype.card (@units (zmod p) (@ring.to_monoid (zmod p) (@comm_ring.to_ring (zmod p) (zmod.comm_ring p))))
      (units_zmod.fintype p) =
    p - 1

With one talking about fields and the other not, it seems to me like this could be an issue with the instance code. What causes this and how can it be fixed?

[Ruben Van de Velde]

I don't understand the error, but convert can avoid it:

    { intro p_prime,
      haveI := fact.mk p_prime,
      convert zmod.card_units p },

[Bolton Bailey]

Cool, thank you

[Eric Wieser]

`cases p_prime would probably work too

[Eric Wieser]

(deleted)

[Eric Wieser]

`cases p_prime would probably work too

[Ruben Van de Velde]

@Bolton Bailey did you manage to prove the other direction? I found it surprisingly hard

[Bolton Bailey]

I have made a PR and I am working on it. Currently I am working in the direction of proving that the totient of p is p-1 iff p is prime.

[Bolton Bailey]

#8820

[Eric Rodriguez]

@Bolton Bailey , you may be interested in branch#mul_ind (not sure what the PR number is)

[Eric Rodriguez]

the issue btw is that you have a fintype diamond, and it's using two different instances

[Eric Rodriguez]

this'll do your other half:

    { haveI := fact.mk h,
      intro h,
      replace h : @fintype.card (units (zmod p)) (units.fintype) = p - 1,
      { convert h },
      rw zmod.card_units_eq_totient at h,
      rw nat.totient_prime_iff,
      exact h } }

[Ruben Van de Velde]

My code is here if you want to reuse anything - https://gist.github.com/Ruben-VandeVelde/a9f81b2ec21f21a0b4d7f6ac29fbb023

[Bolton Bailey]

Eric Rodriguez said:

this'll do your other half:

I'm a bit confused by this - if I just plug this in I get unknown identifier h. What is h here?

[Bolton Bailey]

Perhaps h : 0 < p?

[Bolton Bailey]

Yep, this was it.

[Bolton Bailey]

I'm encountering a few more diamonds here: I found I can avoid them by just getting rid of the instance of units_zmod.fintype and simply introducing [fact (0 < p)] at the top of the file.

[Yakov Pechersky]

What diamond? fintype is a subsingleton btw.

[Bolton Bailey]

I was told the cause of my issues above was a diamond. Since I was encountering more bugs that manifested in exactly the same way, I assume the cause was the same.
I'm not sure I understand well enough to say exactly what the diamond is. I understand a diamond is when instances inherit from each other in a diamond shaped pattern, but I don't know why this causes problems. Perhaps @Eric Rodriguez can explain to me and all of us what exactly the instances involved in this diamond were.

[Eric Rodriguez]

you had two instances; units_zmod.fintype and the default one units.fintype (fintype → fintype on units). Most fintype card stuff is written with units.fintype, whilst if you don't sprinkle that fact in, you'll be getting units_zmod.fintype; this means you'll have to use convert/congr a lot, even with case analysis

[Eric Rodriguez]

(convert + congr work because, as Yakov said, fintype is a subsingleton)