Syntax question: purely inseparable field extension

Stream: new members

[Jakob Scholbach]

I am trying to define the notion of an inseparable field extension. Here is my attempt:

import algebra.char_p.basic
import algebra.algebra.basic

/- An element in a char. p field extension is purely inseparable if some p-power of it
lies in the smaller field. https://stacks.math.columbia.edu/tag/09HE -/
def elem_purely_inseparable {F L : Type} [field F] [field L] [ι: ring_hom F L] [p : ℕ] [char_p F p]
  (x : L) : Prop := ∃ n : ℕ, ∃ f : F, x^(p^n) = ι f

def extension_purely_inseparable {F L : Type} [field F] [field L] [ι: ring_hom F L] [p : ℕ] [char_p F p]: Prop :=
  ∀ x : L, elem_purely_inseparable x

However, the last line doesn't work, I get an error message

failed to synthesize type class instance for
F L : Type,
_inst_1 : field F,
_inst_2 : field L,
ι : F →+* L,
p : ℕ,
_inst_3 : char_p F p,
x : L
⊢ ℕ

What does that mean and how do I fix it? Thanks!

[Kenny Lau]

Lean doesn't know what the p in elem_purely_inseparable x should be

[Kenny Lau]

you should make p an explicit argument

[Jakob Scholbach]

OK, thanks. I'm still very new to this. Does "explicit argument" mean writing (p : \N) instead of [p : \N]?

[Adam Topaz]

Alternatively you can put the prime and char_p assumptions under the existential.

[Kenny Lau]

Jakob Scholbach said:

OK, thanks. I'm still very new to this. Does "explicit argument" mean writing (p : \N) instead of [p : \N]?

yes

[Adam Topaz]

import algebra.char_p.basic
import algebra.algebra.basic

/- An element in a char. p field extension is purely inseparable if some p-power of it
lies in the smaller field. https://stacks.math.columbia.edu/tag/09HE -/
def elem_purely_inseparable {F L : Type} [field F] [field L] (ι: ring_hom F L)
  (x : L) : Prop := ∃ (p : ℕ) (n : ℕ) (I : char_p F p) (f : F), x^(p^n) = ι f

def extension_purely_inseparable {F L : Type} [field F] [field L] (ι: ring_hom F L) : Prop :=
  ∀ x : L, elem_purely_inseparable ι x

[Adam Topaz]

The [ ... ] arguments are used to declare typeclass instances.

[Adam Topaz]

I.e. it's used for things like [group G], [field K], [comm_ring A], etc.

[Adam Topaz]

So, it also doesn't make sense to put $\iota$ in square brackets. If you want the typeclass system to recognize that L is an extension of Kyou can say [algebra K L].

[Jakob Scholbach]

Thanks @Adam Topaz and @Kenny Lau, got it.