Confusion about a function returning an element of a Field

Stream: new members

[Frederik]

Hello! I guess I have some basic misunderstanding about how Fields work in Lean 4 and reading documentation did not clear it up for me.
I have the following simple example which simply proposes commutativity in $\mathbb{N}$, albeit in a bit of a weird manner:

variable (a : ℕ → ℕ)
def Z (i : ℕ): ℕ := a i
example : Z 0 + Z 1 = Z 1 + Z 0 := by sorry

Essentially, I'm trying to model variables with "indices", like $A_{0}, A_{1}$ and so on, that's why I started with the function variable in the first place. The indices are in $\mathbb{N}$ for now (more specifically they will be in some Fin n later) but the _value_ of the variable should be in a generic Field F. I tried to modify the above example to replace the codomain with F like this, but it fails:

variable {F : Type*} [Field F]
variable (a : ℕ → F)
def Z (i : ℕ): F := a i
example : Z 0 + Z 1 = Z 1 + Z 0 := by sorry

Lean complains on Z 1 + Z 0, with the following error:

typeclass instance problem is stuck, it is often due to metavariables
  HAdd (ℕ → ?m.806) (ℕ → ?m.969) ?m.1960

and I do not understand how to proceed with this error. I would appreciate any pointers to the issue and where I can learn more about the apparent basics that I am missing. Thanks!!

[Etienne Marion]

The variable command does not create a global variable in the file, it is just a shortcut to avoid adding it in all declarations. So your definition of Z is actually

def Z {F : Type*} (a : ℕ → F) (i : ℕ) : F := a i

which you can check by writing #check Z. There is no [Field F] because it is not needed in the def so not included I think.
Thus when you write Z 0 the 0 is the value you provide for a, but then lean is unable to infer F, in particular in Z 0 and Z 1 the F might be different. So what you want is rather

import Mathlib

variable {F : Type*} [Field F]
variable (a : ℕ → F)
def Z (i : ℕ) : F := a i
#check Z
example : Z a 0 + Z a 1 = Z a 1 + Z a 0 := by sorry