How to use ring_hom for fields

Stream: new members

[Keyao Peng]

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]

Use #backticks like this

```
code here
```

[Johan Commelin]

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

[Johan Commelin]

Build the category of fields and overfields?

[Johan Commelin]

What do you want to use them for?

[Johan Commelin]

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]

I am trying to prove some theorems for Galois theory

[Johan Commelin]

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]

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]

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]

We have algebra for field extensions.