This file places the normal-closure construction used throughout the global theory below the adelic and splitting developments that consume it. The closure is formed inside mathlib's fixed algebraic closure, and the original field is embedded by the canonical chosen lift.
The normal closure of L / K, constructed inside a fixed algebraic closure of K.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u v
variable
(K : Type u) (L : Type v)
[Field K] [NumberField K]
[Field L] [NumberField L] [Algebra K L]abbrev finiteNormalClosureSurrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u v
variable
(K : Type u) (L : Type v)
[Field K] [NumberField K]
[Field L] [NumberField L] [Algebra K L]instance finiteNormalClosure_numberField :
NumberField (finiteNormalClosure K L)Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u v
variable
(K : Type u) (L : Type v)
[Field K] [NumberField K]
[Field L] [NumberField L] [Algebra K L]instance finiteNormalClosure_isGalois :
IsGalois K (finiteNormalClosure K L)A fixed embedding of L into its normal closure.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u v
variable
(K : Type u) (L : Type v)
[Field K] [NumberField K]
[Field L] [NumberField L] [Algebra K L]def finiteNormalClosureEmbedding :
L →ₐ[K] finiteNormalClosure K LThe distinguished copy of L in its finite normal closure.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u v
variable
(K : Type u) (L : Type v)
[Field K] [NumberField K]
[Field L] [NumberField L] [Algebra K L]def finiteNormalClosureOriginalField :
IntermediateField K (finiteNormalClosure K L)The original extension is canonically equivalent to its distinguished copy in the finite normal closure.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u v
variable
(K : Type u) (L : Type v)
[Field K] [NumberField K]
[Field L] [NumberField L] [Algebra K L]def finiteNormalClosureOriginalFieldEquiv :
L ≃ₐ[K] finiteNormalClosureOriginalField K LNormal closure is invariant under replacing its source by an isomorphic field.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u v
variable
(K : Type u) (L : Type v)
[Field K] [NumberField K]
[Field L] [NumberField L] [Algebra K L]
omit [NumberField K] [NumberField L] intheorem normalClosure_eq_top_of_source_algEquiv
{M E : Type*}
[Field M] [Algebra K M]
[Field E] [Algebra K E]
(e : L ≃ₐ[K] E)
(hclosure :
IntermediateField.normalClosure K L M = ⊤) :
IntermediateField.normalClosure K E M = ⊤The distinguished copy of L generates its finite normal closure under its K-conjugates.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u v
variable
(K : Type u) (L : Type v)
[Field K] [NumberField K]
[Field L] [NumberField L] [Algebra K L]theorem finiteNormalClosureOriginalField_normalClosure_eq_top :
IntermediateField.normalClosure K
(finiteNormalClosureOriginalField K L)
(finiteNormalClosure K L) =
⊤The degree of the original extension is bounded by the degree of its finite normal closure.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u v
variable
(K : Type u) (L : Type v)
[Field K] [NumberField K]
[Field L] [NumberField L] [Algebra K L]theorem finrank_le_finiteNormalClosure :
Module.finrank K L ≤
Module.finrank K (finiteNormalClosure K L)A degree-one finite field extension is the base field as an algebra.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u v
variable
(K : Type u) (L : Type v)
[Field K] [NumberField K]
[Field L] [NumberField L] [Algebra K L]def algEquivBaseOfFinrankEqOne
(hdegree : Module.finrank K L = 1) :
L ≃ₐ[K] K