UniMath
Galois groupoid
What about skipping the Galois group and introducing the Galois groupoid, instead? Is there any reason to artificially single out a particular splitting field?
To add a bit of context: a Galois extension L/K would still have a Galois group, but a separable polynomial over K would just have a Galois groupoid, whose objects are all of its splitting fields.
I think that's right: For a separable (monic) polynomial over a separably factorial field, there's no designated splitting field, except in special cases, e.g., over number fields (where we can take the splitting field inside the algebraic numbers inside in the complex numbers).
Another viewpoint is via the universal splitting algebra A/k, which always has the full symmetric group as automorphism group, and from which we recover splitting fields as factors in a decomposition of A as a product of fields over k, corresponding to factoring the minimal polynomial for A/k as a product of irreducibles in k[X], but there's no designated ordering of these factors in general.
