Zulip Chat Archive

Stream: new members

Topic: Syntax question: purely inseparable field extension


view this post on Zulip 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!

view this post on Zulip Kenny Lau (Feb 23 2021 at 19:25):

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

view this post on Zulip Kenny Lau (Feb 23 2021 at 19:25):

you should make p an explicit argument

view this post on Zulip 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]?

view this post on Zulip Adam Topaz (Feb 23 2021 at 19:31):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Adam Topaz (Feb 23 2021 at 19:34):

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

view this post on Zulip Adam Topaz (Feb 23 2021 at 19:35):

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

view this post on Zulip 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].

view this post on Zulip 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