English
The adjoin operation for a finite set s ⊆ K yields the minimal finite Galois intermediate field containing s. Equivalently, for any FGIF L, s ⊆ L.toIntermediateField implies adjoin_k(s) ≤ L.
Русский
Операция приёма порождает минимальное конечное Галуа-подполе, содержащее множество s. Другими словами, если s ⊆ L, то adjoin_k(s) ≤ L.
LaTeX
$$$ \text{adjoin}_k(s) \text{ is the minimal FGIF containing } s, \quad \forall L, (s \subseteq L.toIntermediateField) \Rightarrow \text{adjoin}_k(s) \le L. $$$
Lean4
/-- The minimal (finite) Galois intermediate field containing a finite set `s : Set K` in a
Galois extension `K/k` defined as the normal closure of the field obtained by adjoining
the set `s : Set K` to `k`. -/
noncomputable def adjoin [IsGalois k K] (s : Set K) [Finite s] : FiniteGaloisIntermediateField k K :=
{
normalClosure k (IntermediateField.adjoin k (s : Set K))
K with
finiteDimensional :=
letI : FiniteDimensional k (IntermediateField.adjoin k (s : Set K)) :=
IntermediateField.finiteDimensional_adjoin <| fun z _ =>
IsAlgebraic.isIntegral (Algebra.IsAlgebraic.isAlgebraic z)
normalClosure.is_finiteDimensional k (IntermediateField.adjoin k (s : Set K)) K
isGalois := IsGalois.normalClosure k (IntermediateField.adjoin k (s : Set K)) K }
