Absolute Normal Closure

Stream: Is there code for X?

[Artie Khovanov]

docs#IsSepClosure and docs#IsAlgClosure come with their respective absolute constructions docs#SeparableClosure and docs#AlgebraicClosure. But docs#IsNormalClosure does not appear to come with such a construction. I suppose it's something likeIntermediateField.normalClosure F K (AlgebraicClosure K), but of course that won't have API. Am I missing something, or is "NormalClosure" not yet in Mathlib?

[Aaron Liu]

Artie Khovanov said:

I suppose it's something likeIntermediateField.normalClosure F K (AlgebraicClosure K), but of course that won't have API.

What kind of API are you looking for?

[Artie Khovanov]

Well, for a start, that it actually satisfies IsNormalClosure

[Artie Khovanov]

tbh that's all I need
but the instance doesn't fire

[Artie Khovanov]

failed to synthesize instance of type class Nonempty (F →ₐ[F] ↥(IntermediateField.normalClosure F K (AlgebraicClosure K)))
(because you need to chain together the inclusions)

[Aaron Liu]

Nonempty (F →ₐ[F] ↥(IntermediateField.normalClosure F K (AlgebraicClosure K))) should be immediate, right?

[Aaron Liu]

It's just docs#Algebra.ofId

[Artie Khovanov]

Yeah - I'm not sure why the instance isn't synthesised automatically. That's really what I'm asking, does it already work somehow for a reason I missed, or do I need to add more lemmas?

[Aaron Liu]

maybe it's just a missing instance

[Artie Khovanov]

just tried it again in my actual context and it appears to just work? who knows lol