How to use variables properly

Stream: new members

[Ben Whitmore]

I'm trying to figure out how to use variables in a way that aligns with normal mathematics writing. For example suppose I want to write "Let k \in N, let R = Z/(2^k Z), and let f: R -> R, f(x) = 2^x".

My attempt at writing this in Lean 4 is:

import Mathlib.Data.ZMod.Basic
import Mathlib.Data.ZMod.Defs

section foo
  variable (k : ℕ)
  def R := ZMod (2 ^ k)
  def f : R -> R := fun x => 2 ^ x.val
end foo

But:

1. I was under the impression that defining variables like this would mean you don't have to keep writing out all the variables that a definition depends on every time you use them, but apparently I need to keep writing R k instead of R, even though I already defined R as a single type depending on k, not as a function from ℕ to types (I thought this generalization would happen outside of the section once the variable k is no longer in scope, but not inside the section). This seems unnecessarily annoying to have to deal with, because it means I also have to keep referring to f as f k everywhere too.

2. My definition of R (or R k) seems to have "forgotten" everything about ZMod. For example, converting from ℕ to ZMod (2 ^ 8) is trivial: def x : ZMod (2 ^ 8) := 10, but converting from ℕ to R 8 where R k := ZMod (2 ^ k) doesn't work: def x : R 8 := 10 results in

failed to synthesize instance
  OfNat (R 8) 10

Surely I am doing something wrong and there is a trivial solution to these problems.

[Damiano Testa]

Using abbrev R might help with the instance. The explicitness of k is set by the parentheses in the variable command. I'm not sure that making k implicit is a good idea, though, since lean would not know what natural to use otherwise.

[Kevin Buzzard]

Just to pick up on a pedantic point here, what do you mean by "let f: R -> R, f(x)=2^x"? I would argue that this function is not well-defined on the quotient, because, for example, 0 and 2^k are equal elements of the domain, but f(0)=2^0=1 and f(2^k)=2^(2^k) are not congruent modulo 2^k, so the function does not naturally descend to a map on the quotient. We might have different mental models of Z/nZ here? Are you actually talking about Fin n?