## Stream: new members

### Topic: Syntax question: purely inseparable field extension

#### Jakob Scholbach (Feb 23 2021 at 19:24):

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 (Feb 23 2021 at 19:25):

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

#### Kenny Lau (Feb 23 2021 at 19:25):

you should make p an explicit argument

#### Jakob Scholbach (Feb 23 2021 at 19:31):

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

#### Adam Topaz (Feb 23 2021 at 19:31):

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

#### Kenny Lau (Feb 23 2021 at 19:33):

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 (Feb 23 2021 at 19:33):

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 (Feb 23 2021 at 19:34):

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

#### Adam Topaz (Feb 23 2021 at 19:35):

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

#### Adam Topaz (Feb 23 2021 at 19:36):

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 (Feb 23 2021 at 19:41):

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

Last updated: May 14 2021 at 12:18 UTC