Stream: new members

Topic: How to use ring_hom for fields

Keyao Peng (Jun 26 2020 at 10:04):

when I try to define the category of field,

structure fields : Type (u+1) :=
(k : Type u)
(fStruc : field k)
instance fields_has_hom : has_hom fields :=
{ hom:= λ a b, ring_hom a.k b.k a.fStruc b.fStruc }


There would be an error, it seems like a field instance can't be regarded as semiring?
But this structure has no Error,

structure fieldsOver (L : Type u) [𝕃 :field L] : Type (u+1):=
(k : Type u)
(𝕜 : field k)
(L2k : L →+* k )


why?

Johan Commelin (Jun 26 2020 at 10:05):

Use #backticks like this


code here



Johan Commelin (Jun 26 2020 at 10:05):

Can you explain in text what you are trying to do?

Johan Commelin (Jun 26 2020 at 10:06):

Build the category of fields and overfields?

Johan Commelin (Jun 26 2020 at 10:06):

What do you want to use them for?

Johan Commelin (Jun 26 2020 at 10:06):

The error is that ou are passing the structures to ring_hom, but it only takes a.k and b.k as explicit arguments.

Keyao Peng (Jun 26 2020 at 10:07):

I am trying to prove some theorems for Galois theory

Johan Commelin (Jun 26 2020 at 10:07):

However, you have to explicitly tell lean to regard a.k as a field with

instance (a : fields) : [field a.k] := a.fStruc


Johan Commelin (Jun 26 2020 at 10:08):

Keyao Peng said:

I am trying to prove some theorems for Galois theory

I doubt whether these categories will make your life easier.

Keyao Peng (Jun 26 2020 at 10:12):

Johan Commelin said:

However, you have to explicitly tell lean to regard a.k as a field with

instance (a : fields) : [field a.k] := a.fStruc


Thanks, this works.

Kenny Lau (Jun 26 2020 at 10:19):

We have algebra for field extensions.

Last updated: May 10 2021 at 00:31 UTC