algebraic closure

Stream: general

[Kenny Lau]

I have a new idea to construct an algebraic closure of a field F: for each (monic (irreducible)) polynomial p let Fp be a splitting field of p over F, and take the tensor product of all the Fp together (there is a construction of tensor product without direct limit but the direct limit construction might grant us quicker the fact that the ring is nonzero), and then quotient by a maximal ideal

[Neil Strickland]

I'd suggest something similar but a tiny bit different. If p is monic of degree n, let A_p be the quotient of F[a_1,..,a_n] by the coefficients of p - (x - a_1) * ... * (x - a_n). The splitting field L_p is then the quotient of A_p by a maximal ideal. Let A be the tensor product of all the A_p, and let B be the tensor product of all the L_p. You are proposing to take the quotient of B by a maximal ideal, but it works just as well to take the quotient of A by a maximal ideal. Moreover, you can specify a basis for A_p over F depending only on the degree of p, whereas the dimension of L_p depends in a delicate way on the Galois theoretic properties of p. This makes it easier to deal with A. Also, you can define A without explicit recourse to tensor products: you just take a polynomial ring over F with generators a_{p,i} for i < deg (p) and take an appropriate quotient.

[Kenny Lau]

but we already have splitting fields

[Neil Strickland]

I know we have splitting fields. But if you want to use splitting fields then you need to deal with colimits and tensor products, which you can avoid by the approach that I suggested. And you will need to work a bit harder to verify that the relevant ring is nonzero.

[Kenny Lau]

import linear_algebra.basis
import ring_theory.algebra_operations

universe u

private def monic_irred (F : Type u) [discrete_field F] : Type u :=
{ p : polynomial F // p.monic ∧ irreducible p }

@[reducible] private def big_ring (F : Type u) [discrete_field F] : Type u :=
mv_polynomial (monic_irred F) F

@[reducible] private def big_ideal (F : Type u) [discrete_field F] : ideal (big_ring F) :=
ideal.span { q | ∃ p : monic_irred F, p.1.eval₂ mv_polynomial.C (mv_polynomial.X p) = q }

private def big_basis (F : Type u) [discrete_field F] : set (big_ideal F).quotient :=
{ q | ∃ p : monic_irred F, ∃ n < p.1.nat_degree, ideal.quotient.mk _ ((mv_polynomial.X p)^n) = q }

instance asdf (F : Type u) [discrete_field F] : module F (big_ring F) :=
sorry

instance ghjk (F : Type u) [discrete_field F] : module F (big_ideal F).quotient :=
sorry

private theorem big_basis.is_basis (F : Type u) [discrete_field F] : is_basis F (big_basis F) :=
sorry

[Kenny Lau]

when you want to rejoin Lean but you remember the frustration of maximum class-instance resolution depth has been reached

[Kevin Buzzard]

It's usually user error :-/

[Johan Commelin]

@Kenny Lau I suggest you talk with @Chris Hughes about this. I was under the impression that he was almost done with algebraic closures, and that it would happen in about a week (or two) after the exams were over. He was planning to use your open PRs

[Johan Commelin]

I've been working on those PRs, and at least #734 is waiting for review by others.

[Kevin Buzzard]

...or can be fixed by pretending there isn't a problem and bumping up the number

[Sebastien Gouezel]

I had to bump it to 250 in #1085 !

[Keeley Hoek]

:O

[Keeley Hoek]

Typeclass resolution is actually garbage

[Keeley Hoek]

In 4 we could write our own, right?

[Johan Commelin]

We had a recent effort to make things irreducible after their API's had been reasonably fleshed out. Would that help in keeping this number in check?

[Sebastien Gouezel]

I don't really know why it has to be that huge here. It is probably related to products and to the fact that things are rather unbundled: the definition of a topological module is

class topological_module (α : Type u) (β : Type v)
  [ring α] [topological_space α]
  [topological_space β] [add_comm_group β]
  [module α β]
  extends topological_semimodule α β : Prop

You can see how many typeclasses this depends on.

[Kevin Buzzard]

instance asdf (F : Type u) [discrete_field F] : module F (big_ring F) :=
sorry

instance qwer : add_comm_group ((big_ideal F).quotient) := by apply_instance
/-
synthesized type class instance is not definitionally equal to expression inferred by typing rules, synthesized
  ⁇
inferred
  mv_polynomial.comm_ring
-/

Could this be something to do with it?

[Kevin Buzzard]

no wait, that's my user error (no F)

[Kevin Buzzard]

set_option class.instance_max_depth 36 -- and no lower
instance asdf (F : Type u) [discrete_field F] : module F (big_ring F) :=
by apply_instance

set_option class.instance_max_depth 86 -- and no lower
instance zxcv (F : Type u) [discrete_field F] :
  add_comm_group (big_ideal F) := by apply_instance

Why is this nonsense happening?

[Kevin Buzzard]

set_option class.instance_max_depth 36 -- and no lower
instance asdf (F : Type u) [discrete_field F] : module F (big_ring F) :=
by apply_instance

set_option class.instance_max_depth 86 -- and no lower
instance zxcv (F : Type u) [discrete_field F] :
  add_comm_group (big_ideal F) := by apply_instance

instance wert (F : Type u) [discrete_field F] :
  comm_ring (big_ideal F).quotient := by apply_instance

instance qwer (F : Type u) [discrete_field F] :
module F (big_ideal F) := by apply_instance -- fails

[Kevin Buzzard]

@Kenny Lau is the issue simply this:

example (R S M : Type*) [comm_ring R] [comm_ring S] [module R S]
  [add_comm_group M] [module S M] : module R M := by apply_instance -- fails

This should probably fail, because Lean does not know that the R-module structure on S has anything to do with the ring structure.

[Kevin Buzzard]

Aah, but this also fails:

example (R S M : Type*) [comm_ring R] [comm_ring S] [algebra R S]
  [add_comm_group M] [module S M] : module R M := by apply_instance -- fails

[Kevin Buzzard]

We humans are too clever. We synthesize the instance automatically.

[Kevin Buzzard]

example (R S M : Type*) [comm_ring R] [comm_ring S] [algebra R S]
  [add_comm_group M] [module S M] : has_scalar R M := by apply_instance -- fails

Are there just some missing instances? Should these even be instances? There is no mention of S in the conclusion.

[Kevin Buzzard]

@Kenny Lau you know the instance "map" for this stuff better than me -- is this the issue?

[Kenny Lau]

oh I'm stupid

[Kenny Lau]

@Chris Hughes what is your progress on algebraic closure?

[Chris Hughes]

Mostly done, although I am refactoring. I proved it is algebraically closed, and am just refactoring to make it neater to show that there is a hom from any algebraic extension into the closure. This refactoring is much slower than expected however, and I'm bundling homs right now to make it easier.

I did sorry a couple of facts, the fact that adjoin_root is an algebraic extension, and the fact that an algebraic extension of an algebraic extension is algebraic over the first field. I was hoping that you were close to proving these, as some of your PRs looked like they were leading to this.

[Kenny Lau]

I thought I already proved that result

[Kenny Lau]

oh it was meant to be the PR after #756

[Kenny Lau]

@Chris Hughes #1087

[Casper Putz]

@Chris Hughes What is the status on the algebraic closure? I am interested in working with algebraic extensions in mathlib. Are you planning on putting it into mathlib anytime in the future?

[Chris Hughes]

I pushed some stuff to the algebraic closure branch of community mathlib.
The file field_theory/algebraic_closure is the closest thing to compiling.

It looks like I was half way through changing a bunch of assumptions from is_algebraically_closed to contains all the roots of polynomials in the base field.

There is another file in there algebraic_closure2 or something, where I am halfway through a refactor, that might make some of the proofs a bit shorter, but probably isn't worth the effort.

I was planning a refactor to use algebra homs instead of field homs, and also a refactor to use Kenny's definition is_integral instead of the predicate I defined.

I'd be very happy to pass this on. Honestly, I won't have that much time to look at it, but I'm very happy to answer questions from anyone who wants to take it on.

Sorry for the delay.

[Johan Commelin]

@Casper Putz :up:

[Chris Hughes]

I've started playing with algebraic closure again.

One issue is that direct limit is not set up very well for bundled homomorphisms currently. It should probably be done using category theory. I'd like to use bundled algebra homs, but the definition directed_system is only defined on functions, not bundled homs. I think I'm going to have to refactor. I was taking a direct limit where the indexing type was large, which won't sit too well with the category theory library currently.

[Casper Putz]

Sorry for the late response. I was on holiday.
Thanks for your updates. I also don't have a lot of time to delve into.

[Casper Putz]

For the things I am doing it seemed more natural to not carry around an algebraic closure when talking about algebraic field extensions. So I am now working with field homs now. But of course we still need the algebraic at some point.

[Scott Morrison]

Can you explain about the size of the indexing type? (I don't know how you're doing algebraic closure.)

[Chris Hughes]

I had this type, and took the maximal element of this type using zorn. I had to use direct limit to prove the condition for Zorn's lemma. The indexing type was extension K. I would then prove the type was isomorphic to something in Type u and transfer the field structure

structure extension (K : Type u) [discrete_field K] : Type (u+1) :=
(carrier : Type u)
[field : discrete_field carrier]
(embedding : carrier ↪ big_type K)
(lift : K → carrier)
[is_field_hom : is_field_hom lift]
(algebraic : ∀ x, algebraic lift x)

I'm not following this approach any more, I'll just use a smaller type for extension, where the field structure has to be on a subset of big_type : Type u. This involves slightly more transferring field structures across isomorphisms, but shouldn't be that much more effort, if at all.

[Chris Hughes]

I believe I could probably get a version of algebraic closure done this weekend with a few sorries. The structure of the proof will all be there, so anyone will be able to help fill in the sorries without having to understand the entire approach.

[Chris Hughes]

#1297

[Johan Commelin]

@Chris Hughes What is the status here? If we fill in all the sorries in algebraic_closure.lean, then we are done right?

[Johan Commelin]

We've had some nice community efforts recently. This might be a good one for the end of this month.

[Chris Hughes]

Yes. However, it would be nicer to do some refactoring first, and get direct_limit to use bundled ring homs.

[Chris Hughes]

Because I really don't want to make the refactor that will have to be done way harder by adding a bunch of stuff with unbundled homs.

[Johan Commelin]

Ok, I'll work on the top few sorries (min polynomials)

[Johan Commelin]

That should be independent, I guess.

[Chris Hughes]

Just realised one of them is false.

[Chris Hughes]

That was sloppy of me.

[Johan Commelin]

No worries

[Amelia Livingston]

I can make a PR today changing semiring_hom to ring_hom if that'd help - I'm thinking of removing semiring_hom completely and just adding good docstrings to say that ring_hom should be used for semiring homs too, unless there's a better way.

[Johan Commelin]

I just pushed a change

[Johan Commelin]

I put minimal_polynomial in its own file. The top of the file now contains a whole bunch of stuff that should move to polynomial.lean.

[Johan Commelin]

I've filled in all the sorries about minimal polynomials.

[Johan Commelin]

Removed the next sorry as well.

[Chris Hughes]

How about putting the minimal polynomial stuff in a separate PR?

[Johan Commelin]

I'm fine with that

[Johan Commelin]

Anyone who wants to join in can help

[Johan Commelin]

I was hoping that we could push this like we did with sensitivity and the IMO problems

[Johan Commelin]

There are already a whole lot of -- move this comments that could also be put into a separate PR

[Johan Commelin]

I pushed more stuff to this branch. I moved an instance up a bit, and generalised if from discrete fields to rings. Now Lean is unhappy.

[Johan Commelin]

Need to catch a train. Will look at this later.

[Johan Commelin]

Removed another sorry, and pushed.

[Johan Commelin]

Merged two sorries. Pushed.

[Johan Commelin]

I can make a PR today changing semiring_hom to ring_hom if that'd help - I'm thinking of removing semiring_hom completely and just adding good docstrings to say that ring_hom should be used for semiring homs too, unless there's a better way.

@Amelia Livingston Thanks for all your hard work! I'm pretty sure this is going to pay off in the long run.

[Amelia Livingston]

No problem! Thanks for reviewing it.

[Johan Commelin]

The file on algebraic closures is quite a tangle. I'm not sure if bundled homs will be used this time. I still haven't understood which parts of the file are essential, and which ones aren't.

[Johan Commelin]

It would be nice if it were easier to explore such dependency graphs... for example in VScode....

[Chris Hughes]

The file on algebraic closures is quite a tangle. I'm not sure if bundled homs will be used this time. I still haven't understood which parts of the file are essential, and which ones aren't.

I think all parts of the file on algebraic closures are essential, except perhaps one def where there is a comment saying it might be unnecessary.

[Johan Commelin]

I feel like you never use the direct limit stuff

[Johan Commelin]

In the end you just write an explicit union

[Chris Hughes]

But I need the direct limit to put a field structure on it.

[Johan Commelin]

Aah, right, now I see.

[Chris Hughes]

I could have done that without direct limit, but the argument was actually quite hard, even thought it's "obvious".

[Johan Commelin]

@Chris Hughes I'm confused about the preorder that you put on extension K

[Johan Commelin]

Don't you want the inclusions to be algebra homs, instead of merely ring homs?

[Johan Commelin]

Or am I missing something?

[Chris Hughes]

You'd have thought so, but the proof seems to go through without it. I was surprised as well.

[Chris Hughes]

Can you not prove the maximal extension is algebraic without it?

[Chris Hughes]

Makes sense that you wouldn't be able to do that.

[Johan Commelin]

I'm currently refactoring it, to include the assumption

[Chris Hughes]

Perhaps it's useful to make an is_alg_hom predicate if there isn't one already?

[Johan Commelin]

Ok, for the existence of an algebraic closure, there is 1 sorry left.

[Johan Commelin]

For the ump there are still a few more.

[Johan Commelin]

(UMP = every algebraic extension embeds into K-bar)

[Chris Hughes]

What is the one sorry?

[Johan Commelin]

That being an algebraic extension is transitive.

[Johan Commelin]

@Kenny Lau Do we have anything of the form M/L is fg and L/K is fg, hence M/K is fg?

[Johan Commelin]

Where M/L/K is a tower of algebras (or subalgebras)...

[Kenny Lau]

I think so

[Patrick Massot]

(deleted)

[Patrick Massot]

(deleted)

[Patrick Massot]

(deleted)

[Johan Commelin]

Here is what I have now:

lemma adjoin_root.algebraic (x : adjoin_root f) : is_integral K x :=
begin
  rcases adjoin_root.is_integral hif.ne_zero x with ⟨p, pmonic, hp⟩,
  let S : set (adjoin_root f) :=
    (↑((finset.range (f.nat_degree + 1)).image (λ i, (f.coeff i : adjoin_root f))) : set (adjoin_root f)),
  let B := algebra.adjoin K S,
  have Bfg : submodule.fg (B : submodule K (adjoin_root f)),
  { apply fg_adjoin_of_finite,
    { apply finset.finite_to_set },
    { intros x hx,
      rw [finset.mem_coe, finset.mem_image] at hx,
      rcases hx with ⟨i, hi, rfl⟩,
      rcases L.algebraic (f.coeff i) with ⟨q, qmonic, hq⟩,
      use [q, qmonic],
      replace hq := congr_arg (coe : L.carrier → adjoin_root f) hq,
      convert hq using 1,
      { symmetry, exact polynomial.hom_eval₂ _ _ _ _ },
      { symmetry, exact is_ring_hom.map_zero _ } } },

  -- (1) we know that x is integral over L, by adjoin_root.is_integral
  -- (2) we know that B is fg over K
  -- (3) we want to say that adjoin B {x} is fg over B, because (1)
  -- (4) hence adjoin B {x} is fg over K
  -- (5) and then we are done by is_integral_of_mem_of_fg

  -- refine is_integral_of_mem_of_fg (algebra.adjoin K S) _ x (algebra.subset_adjoin $ mem_insert _ _),
  sorry
end

[Johan Commelin]

Any help with removing this sorry is very much appreciated.

[Johan Commelin]

I need to start moving to a train now

[Johan Commelin]

This is the final sorry in the definition of the algebraic closure...

[Johan Commelin]

Transitivity of fg is here: https://github.com/leanprover-community/mathlib/blob/d2c5309d0bc66bdf813b4510dfe0a1d7523cad0a/src/ring_theory/adjoin.lean#L109

[Johan Commelin]

All in all, this is becoming a very sad experience.

[Johan Commelin]

I've reduced the final sorry to a content-free battle against the type-class system.

[Johan Commelin]

There are now 4 goals left of the form is_monoid_hom coe.

[Johan Commelin]

And whatever I do: deterministic timeout.

[Johan Commelin]

If someone wants to help me out, that would be much appreciated.

[Johan Commelin]

I need to go to bed now.

[Johan Commelin]

I've pushed all my changes to https://github.com/leanprover-community/mathlib/blob/algebraic_closure/src/field_theory/algebraic_closure.lean

[Patrick Massot]

The evil combination "coercion + hom" is the mostly effective way to bring Lean 3 to its limit.

[Chris Hughes]

What is the coe in question?

[Patrick Massot]

Are we talking about https://github.com/leanprover-community/mathlib/blob/f3620a68e9e1913ba42fa2951c44e70c63b37785/src/field_theory/algebraic_closure.lean#L604? Even without reading anything or running Lean, it's clear that something is not yet setup right

[Chris Hughes]

Bundled homs is the solution.

[Chris Hughes]

Also I think that coe might be bad.

[Johan Commelin]

Bundled homs are a major pain. For example, I've tried to use subalgebra.val B, which is a bundled algebra hom. But the coercion to function doesn't fire (even with 23 type ascriptions and up arrows). So I fall back to algebra_map.

[Johan Commelin]

Another data point:

function expected at
  aeval ↥(L.carrier) (adjoin_root f) x
term has type
  polynomial ↥(L.carrier) →ₐ[↥(L.carrier)] adjoin_root f

Stupid Lean!!! If you expect a function, why don't you try to see if you can coerce the stupid thing??

[Johan Commelin]

Maybe it's not actually bundled homs that we need, but bundled algebras

[Johan Commelin]

@Chris Hughes Do you remember why you need these instances for adjoin_root?
https://github.com/leanprover-community/mathlib/blob/f3620a68e9e1913ba42fa2951c44e70c63b37785/src/field_theory/algebraic_closure.lean#L586

[Johan Commelin]

Is this something with putting them at the top of the stack, so that they are found faster?

[Johan Commelin]

Because those instances already exist, right...

[Chris Hughes]

I guess it must be just so that they are found faster, or at all. At some point I was going to go through the file and make all the instances local, since they're about private defs anyway.

[Johan Commelin]

Another data point:

function expected at
  aeval ↥(L.carrier) (adjoin_root f) x
term has type
  polynomial ↥(L.carrier) →ₐ[↥(L.carrier)] adjoin_root f

Stupid Lean!!! If you expect a function, why don't you try to see if you can coerce the stupid thing??

@Mario Carneiro Do you have any idea why these things happen?

[Mario Carneiro]

The usual reason is because there are metavariables in the type that is being coerced to a function

[Mario Carneiro]

I don't see them in this snippet but it's possible they are hidden in an implicit

[Johan Commelin]

I'll try some more

[Mario Carneiro]

It's probably the up arrow

[Johan Commelin]

lemma algebraic_trans (B_alg : ∀ x : B, is_integral A x) :
  ∀ x : comap R A B, is_integral R x :=
λ x, is_integral_trans A_alg x (B_alg x)

[Johan Commelin]

lemma adjoin_root.algebraic (x : adjoin_root f) : is_integral K x :=
is_integral_trans L.algebraic x $ adjoin_root.is_integral hif.ne_zero x

[Johan Commelin]

That's everything that's left of the big mess that I complained about earlier.

[Johan Commelin]

In particular, we have a sorry-free definition of the algebraic closure!

[Patrick Massot]

Does it have any property, or is it only a type build out of a field?

[Johan Commelin]

It is an algebraically closed field that is algebraic over the field you start with.

[Johan Commelin]

What remains is to show that every algebraic extension embeds into it.

[Patrick Massot]

Nice!

[Johan Commelin]

I just pushed

[Patrick Massot]

Did you learn any useful new trick? Or is it the old trick of being more patient than Lean?

[Johan Commelin]

Generalising, and proving helper lemmas...

[Johan Commelin]

extract_goal is very useful @Simon Hudon

[Johan Commelin]

It should just come with a bit more VScode glue, so that it write all my code for me (-;

[Patrick Massot]

I still see lines like refine @eval_map _ _ _ _ _ _ _ _ (by exact is_ring_hom.is_semiring_hom _) _ that show some suffering

[Patrick Massot]

especially since that line is actually closing a goal

[Johan Commelin]

(1) It should cook up a meaningul name. (2) It should paste the code above the current declaration. (3) It should take into account existing variables. (4) It should gracefully handle let statements. (5) It should apply the extracted lemma at the location of calling extract_goal, in order to close the goal in question.

[Patrick Massot]

and make some coffee

[Johan Commelin]

True, there was still a small amount of suffering involved. Probably because I'm cheating there.

[Patrick Massot]

What kind of cheating?

[Johan Commelin]

I'm identifying comap R A B with B. I should probably use the ring homs to_comap and of_comap to move between the two.

[Johan Commelin]

@Simon Hudon I realise that those 5 feature requests have very different orders of feasability. I just posted them in a random order to stimulate your imagination (-;

[Patrick Massot]

For instance, it could also pat the author on the back after succeeding.

[Johan Commelin]

Wait, you mean that extract_goal doesn't yet buy Simon a beer each time it's called?

[Patrick Massot]

I meant your back

[Patrick Massot]

I'd love Lean to congratulate me more often when I win a big fight

[Patrick Massot]

The "goals accomplished" congratulation is too generic

[Johan Commelin]

But if you win the fight using Simon's tools. Doesn't he also deserve a pat on the back? Especially if he doesn't even know you're using his tools.

[Patrick Massot]

and using extract_goal is a clear big fight indication

[Patrick Massot]

Sure

[Simon Hudon]

:) I'm glad you're enjoying the tool

[Simon Hudon]

I don't think I have an approach on any of those features (except for making coffee :P). I'm not familiar with the writing of tools in VS code so that doesn't make things easier but even in emacs, I'm not sure how I would do them

[Patrick Massot]

I thought you knew about hole commands

[Patrick Massot]

I remember you writing some

[Simon Hudon]

Yes I know about hole commands but they don't mix well with tactic proofs and I don't think they can affect any of the text outside of the {! !} brackets

[Simon Hudon]

To write those features, we need an editor plugin with a notion of where declarations begin and end

[Patrick Massot]

https://images-na.ssl-images-amazon.com/images/I/61JxY8tH-yL._SL1000_.jpg looks promising

[Simon Hudon]

As for treating variables better, I had a look a couple of weeks ago into adding some introspection into the variable mechanism in Lean 3.5 and it was more complicated than expected and I didn't pursue it

[Patrick Massot]

Oh sorry, you meant the other features

[Patrick Massot]

I guess we would need a coffee monad in order to handle real-world side effects

[Simon Hudon]

Easy peasy!

[Wojciech Nawrocki]

Sorry, the (almost) anagram was too tempting

[Johan Commelin]

You should sneak Erdos into that picture (-;

[Johan Commelin]

@Kenny Lau How hard is it to fill in this hole?

namespace subalgebra
open set lattice
variables {R : Type*} {A : Type*} {B : Type*}
variables [comm_ring R] [comm_ring A] [algebra R A] [comm_ring B] [algebra R B]

def Sup.desc (Ss : set (subalgebra R A)) (f : Π S : Ss, (S : subalgebra R A) →ₐ[R] B)
  (hf : ∀ S₁ S₂ : Ss, ∃ h : (S₁ : subalgebra R A) ≤ S₂, (f S₂) ∘ inclusion h = f S₁) :
  (Sup Ss : subalgebra R A) →ₐ[R] B :=
_

end subalgebra

[Johan Commelin]

Never mind, it's more painful than that.

[Johan Commelin]

@Kenny Lau How about this one?

namespace algebra
open set polynomial
variables {R : Type*} {A : Type*} {B : Type*}
variables [decidable_eq R] [decidable_eq A] [decidable_eq B]
variables [comm_ring R] [comm_ring A] [algebra R A] [comm_ring B] [algebra R B]

def adjoin_singleton_desc (x : A) (hx : is_integral R x)
  (y : B) (hy : aeval R B y (minimal_polynomial hx) = 0) :
adjoin R ({x} : set A) →ₐ[R] B :=
_

end algebra

[Johan Commelin]

I'm going to bed now. Modulo my challenge to Kenny, the remaining sorries should be rather straightforward.

[Johan Commelin]

Feel free to fill them in while I'm asleep.

[Chris Hughes]

polynomial.map is hellish

[Johan Commelin]

What are you struggling with?

[Johan Commelin]

I agree that I've often wished that map was defined in terms of finsupp.map_codomain or whatever the thing is called.

[Johan Commelin]

Btw, in the end I didn't use your subfield_and_hom structure. I hope you don't mind. I think you would have to add the requirement that the field embeddings are compatible in the ordering. So you can't use preorder.lift, and hence you also can't apply the other maximal_chain thingies.

[Johan Commelin]

So I ended up defining subfield_with_hom, which I found a more intuitive approach. But that's a personal thing

[Chris Hughes]

polynomial.map is hellish

That's weird. I posted that comment yesterday after you were talking about map. It's showing as posted just now. I'm not doing anything with map right now.

[Chris Hughes]

Which of the sorries did you get stuck on when you used subfield_and_hom? I agree that using subalgebras is more natural, but I was hoping I'd be able to reuse a bunch of stuff.

[Chris Hughes]

I guess this one -- Given K:L:M, if M is algebraic over K it is algebraic over L (names are different)

[Johan Commelin]

It's not clear how to define the embedding into the algebraically closed field from the union of a bunch of subfields if those subfields don't have compatible embeddings into the algebraically closed field.

[Chris Hughes]

You might still be able to do it my way. You just need to add to the order (do we know that intersection of preorders is a preorder?), and add one extra proof to maximal_subfield_and_hom_chain to prove some commutativity property from the direct limit.

[Chris Hughes]

Maybe I'm trying too hard to save lines.

[Johan Commelin]

@Chris Hughes Do you have any clue why I get red squiglly lines under E in the type?

namespace subalgebra
variables {K : Type u} {L : Type v} [discrete_field K] [discrete_field L] [algebra K L]
variables (L_alg : ∀ x:L, is_integral K x)

instance (E : subalgebra K L) : discrete_field (E : Type v) := _

end subalgebra

[Johan Commelin]

It says max type class depth error

[Johan Commelin]

But it should just coerce it to type... and I don't see what other type class search might be going on

[Chris Hughes]

There's no has_coe_to_sort instance for subalgbra.

[Johan Commelin]

This line doesn't give errors:

instance (E : subalgebra K L) : discrete_field (subtype E.carrier) := _

[Johan Commelin]

Aha... that's weird. Because I've been using it all over the place

[Johan Commelin]

It can coerce to set, and then subtype. Both coercions exist. Why doesn't it chain them?

[Chris Hughes]

No idea.

[Johan Commelin]

@Mario Carneiro Any clue?

[Johan Commelin]

I'm still mystified by things like this

[Mario Carneiro]

If you write E : Type v then it will look for a coe to Type v rather than a coe_to_sort

[Mario Carneiro]

does it work without the annotation?

[Mario Carneiro]

The simplest mechanism is probably to write the funny up arrow (not the regular one, the one with a flat bottom)

[Mario Carneiro]

I'm not even sure it has a latex shortcut, but it's short for coe_sort

[Chris Hughes]

@Johan Commelin I really think you made a mistake deleting subfield_and_hom. If you add the commutativity property to the preorder, all but one of the remaining sorries are just the UMP of direct limit or adjoin root. maximal_extension_chain is still maximal with respect to the new preorder. The algebraicness sorry should also be easy, because now that the homs commute, you just map the minimial polynomial from one field to another. You can still reuse a lot of the zorny stuff from the construction of the algebraic closure.

[Johan Commelin]

Feel free to revert it

[Johan Commelin]

All help is appreciated

[Chris Hughes]

I'll have a go at finishing it at the weekend.

[Anthony Bordg]

Why does algebraic closure in Lean seem tricky ? Are you aiming for a constructive proof (i.e. not using AC but a weaker axiom ) ?
My student Paulo Emilio de Vilhena gave a classical proof in Isabelle last summer during his internship.
His work is available on GitHub.
@Kevin Buzzard

[Johan Commelin]

No, we're not constructive at all

[Johan Commelin]

I think one of the issues is that Chris has been really busy doing 25 other things at the same time.

[Kevin Buzzard]

Yes Chris has been doing a summer project on something completely different. One issue is that the native approach to algebraic closure involves taking a limit over a type of extensions which is so big the the limit is in a higher universe than you want it to be.

[Kevin Buzzard]

Yes Chris has been doing a summer project on something completely different. One issue is that the native approach to algebraic closure involves taking a limit over a type of extensions which is so big the the limit is in a higher universe than you want it to be.

[Johan Commelin]

Of course Chris isn't the only one who could/should/wants to do this

[Johan Commelin]

But all the others seem to be suffering the same things...

[Chris Hughes]

The other issue is that I want to do it right, and that involves a bit of refactoring of mathlib first ideally.

[Mario Carneiro]

From what I can tell, Chris's proof is not longer than Paulo's if we are just talking about the parts that are actually constructing the alg closure

[Mario Carneiro]

But of course the number of lines does not always compare to the thought that went into those lines

[Johan Commelin]

Hooray, we have minimal polynomials. The first of several preparatory PRs for algebraic closures

[Johan Commelin]

#1519 another preparatory PR for algebraic closures: algebraic field extensions and transitivity of algebraicity

[Johan Commelin]

If you are a regular contributor to mathlib, and you find it embarrassing that the master branch still doesn't know what an algebraic closure is: please review #1519. It is one of the little steps towards closure.

[Kevin Buzzard]

@Chris Hughes told me at Xena last Thurs that he was reluctant to continue with alg closure until we had limits in category theory. So there is perhaps still a long way to go! Chris said that there was no point building up some special case of a general machine when we need the general machine anyway. I agree with him. I think this might be an interesting case. Mario has always wanted to see a use for all the category theory stuff and maybe this is it. In the past I've tried to use the category theory library and got frustrated, probably because I don't know how to steer it and Scott lives in an inconvenient time zone so is usually asleep when I need help :-) But then the frustration passes and I remember that this really what we should be doing. Chris, can you be more precise about what is needed in category theory?

[Sebastien Gouezel]

I put it as ready-to-merge, but there are merge conflicts...

[Johan Commelin]

Thanks, I'll look at them (tomorrow, probably)

[Johan Commelin]

Categorical (co)limits are there. I guess Chris wants a good interface for directed/filtered colimits of algebras. This means that we need the category of algebras (easy), define filtered index categories (requires a bit of planning, but I don't see any obstacles), and we have to show that the category of algebras has filtered colimits (should be easy, just lift them from CommRing).

[Scott Morrison]

Sorry I've been mostly away from Lean for a while. I'm keen to contribute to making this happen; perhaps when things settle down a bit here I can talk to Chris directly about doing this.