coercion into algebraic closure?

Stream: Is there code for X?

[Michael Stoll]

The following gives me an error message:

import tactic
import field_theory.is_alg_closed.algebraic_closure

example {F} [field F] (a : F) : a = 0 ↔ (coe : F → algebraic_closure F) a = 0 := sorry

results in

failed to synthesize type class instance for
F : Type ?,
_inst_1 : field F,
a : F
⊢ has_lift_t F (algebraic_closure F)

Is this really not there, or am I missing something?

[Michael Stoll]

Trying this as a work-around:

import tactic
import field_theory.is_alg_closed.algebraic_closure

variables {F : Type*} [field F]

def Fbar := algebraic_closure F

noncomputable def FtoFbar : F →+* Fbar :=
ring_hom.comp (algebraic_closure.of_step F 0) (algebraic_closure.to_step_zero F)

example (a : F) : a = 0 ↔ FtoFbar a = 0 := sorry

I get

failed to synthesize type class instance for
F : Type u_1,
_inst_1 : field F,
a : F
⊢ has_zero Fbar

which leaves me seriously puzzled...

[Adam Topaz]

For the second issue, try

@[derive field]
def Fbar := algebraic_closure F

[Michael Stoll]

...since there should be a field instance on algebraic_closure F: docs#algebraic_closure.field

[Michael Stoll]

OK, this works, but why is it necessary?

[Johan Commelin]

When you make a new definition, Lean doesn't automatically transport all instances.

[Michael Stoll]

This does not solve my original question, though.

[Johan Commelin]

That's actually good. Otherwise you wouldn't be able to make copies of objects with different structures (such as a copy of the reals with the discrete topology, or a copy of a poset with the dual order, etc...)

[Johan Commelin]

So you could make Fbar a piece of notation and then everything should work. Or you use derive like Adam said.

[Michael Stoll]

My original #mwe didn't have that problem, though.

[Johan Commelin]

Is that coercion defined somewhere in mathlib?

[Michael Stoll]

That's the question, I guess.

[Michael Stoll]

I didn't find it in field_theory.is_alg_closed.algebraic_closure, which is where I would expect it.

[Johan Commelin]

I think nobody defined it.

[Michael Stoll]

(I did find the material for the clumsy workaround above.)

[Johan Commelin]

Instead, I guess you can use algebra_map. But of course that's ~10 chars extra.

[Johan Commelin]

You could add a has_coe instance, if you want.

[Michael Stoll]

I think that would make sense.

[Johan Commelin]

The benefit of algebra_map is that it's already a ring hom. So you get map_zero and friends for free.

[Eric Wieser]

Or we could revisit the suggestion to add notation for algebra_map

[Michael Stoll]

So I would write (algebra_map F Fbar) a instead of a : Fbar.

[Michael Stoll]

That seems to work.

[Michael Stoll]

However, as a mathematician, I would prefer to be able to write a : Fbar (and get the compatibility properties of the coercion w.r.t. the field structure automatically).

[Johan Commelin]

If you are using it a lot, I think it makes sense to add notation for (algebra_map F Fbar).

[Michael Stoll]

Now I have a proof obligation for function.injective ⇑(algebra_map F Fbar) (I'm applying the coercion to an equality I want to prove). What is the best way of dealing with that?

[Michael Stoll]

Ah, OK, suggest was successful for once... :smile:

[Michael Stoll]

Johan Commelin said:

If you are using it a lot, I think it makes sense to add notation for (algebra_map F Fbar).

Not really at this point. I'm just using it within a part of one proof at the moment.
(I'm trying to do the Gauss sum proof for the second supplement to quadratic reciprocity.)

[Anne Baanen]

Eric Wieser said:

Or we could revisit the suggestion to add notation for algebra_map

I agree, in fact the notation for algebra_map should be ↑!