# Documentation

Mathlib.FieldTheory.NormalClosure

# Normal closures #

The normal closure of a tower of fields L/K/F is the smallest intermediate field of L/K that contains the image of every F-algebra embedding K →ₐ[F] L.

## Main Definitions #

• normalClosure F K L a tower of fields L/K/F.
noncomputable def normalClosure (F : Type u_1) (K : Type u_2) (L : Type u_3) [] [] [] [Algebra F K] [Algebra F L] :

The normal closure of K in L.

Instances For
theorem normalClosure_def (F : Type u_1) (K : Type u_2) (L : Type u_3) [] [] [] [Algebra F K] [Algebra F L] :
= ⨆ (f : K →ₐ[F] L),
theorem normalClosure_le_iff {F : Type u_1} {K : Type u_2} {L : Type u_3} [] [] [] [Algebra F K] [Algebra F L] {K' : } :
K' ∀ (f : K →ₐ[F] L),
theorem AlgHom.fieldRange_le_normalClosure {F : Type u_1} {K : Type u_2} {L : Type u_3} [] [] [] [Algebra F K] [Algebra F L] (f : K →ₐ[F] L) :
theorem normalClosure.restrictScalars_eq_iSup_adjoin (F : Type u_1) (K : Type u_2) (L : Type u_3) [] [] [] [Algebra F K] [Algebra F L] [Algebra K L] [] [h : Normal F L] :
= ⨆ (x : K),
instance normalClosure.normal (F : Type u_1) (K : Type u_2) (L : Type u_3) [] [] [] [Algebra F K] [Algebra F L] [Algebra K L] [] [h : Normal F L] :
Normal F { x // x }
instance normalClosure.is_finiteDimensional (F : Type u_1) (K : Type u_2) (L : Type u_3) [] [] [] [Algebra F K] [Algebra F L] [] :
FiniteDimensional F { x // x }
noncomputable instance normalClosure.algebra (F : Type u_1) (K : Type u_2) (L : Type u_3) [] [] [] [Algebra F K] [Algebra F L] [Algebra K L] [] :
Algebra K { x // x }
theorem normalClosure.restrictScalars_eq (F : Type u_1) (K : Type u_2) (L : Type u_3) [] [] [] [Algebra F K] [Algebra F L] [Algebra K L] [] :
theorem IntermediateField.le_normalClosure {F : Type u_1} {L : Type u_3} [] [] [Algebra F L] (K : ) :
K normalClosure F { x // x K } L
theorem IntermediateField.normalClosure_of_normal {F : Type u_1} {L : Type u_3} [] [] [Algebra F L] (K : ) [Normal F { x // x K }] :
normalClosure F { x // x K } L = K
theorem IntermediateField.normalClosure_def' {F : Type u_1} {L : Type u_3} [] [] [Algebra F L] (K : ) [Normal F L] :
normalClosure F { x // x K } L = ⨆ (f : L →ₐ[F] L),
theorem IntermediateField.normalClosure_def'' {F : Type u_1} {L : Type u_3} [] [] [Algebra F L] (K : ) [Normal F L] :
normalClosure F { x // x K } L = ⨆ (f : L ≃ₐ[F] L),
theorem IntermediateField.normalClosure_mono {F : Type u_1} {L : Type u_3} [] [] [Algebra F L] (K : ) (K' : ) [Normal F L] (h : K K') :
normalClosure F { x // x K } L normalClosure F { x // x K' } L
@[simp]
theorem IntermediateField.closureOperator_apply (F : Type u_1) (L : Type u_3) [] [] [Algebra F L] [Normal F L] (K : ) :
= normalClosure F { x // x K } L
noncomputable def IntermediateField.closureOperator (F : Type u_1) (L : Type u_3) [] [] [Algebra F L] [Normal F L] :

normalClosure as a ClosureOperator.

Instances For
theorem IntermediateField.normal_iff_normalClosure_eq {F : Type u_1} {L : Type u_3} [] [] [Algebra F L] [Normal F L] {K : } :
Normal F { x // x K } normalClosure F { x // x K } L = K
theorem IntermediateField.normal_iff_normalClosure_le {F : Type u_1} {L : Type u_3} [] [] [Algebra F L] [Normal F L] {K : } :
Normal F { x // x K } normalClosure F { x // x K } L K
theorem IntermediateField.normal_iff_forall_fieldRange_le {F : Type u_1} {L : Type u_3} [] [] [Algebra F L] [Normal F L] {K : } :
Normal F { x // x K } ∀ (σ : { x // x K } →ₐ[F] L),
theorem IntermediateField.normal_iff_forall_map_le {F : Type u_1} {L : Type u_3} [] [] [Algebra F L] [Normal F L] {K : } :
Normal F { x // x K } ∀ (σ : L →ₐ[F] L),
theorem IntermediateField.normal_iff_forall_map_le' {F : Type u_1} {L : Type u_3} [] [] [Algebra F L] [Normal F L] {K : } :
Normal F { x // x K } ∀ (σ : L ≃ₐ[F] L), K
theorem IntermediateField.normal_iff_forall_fieldRange_eq {F : Type u_1} {L : Type u_3} [] [] [Algebra F L] [Normal F L] {K : } :
Normal F { x // x K } ∀ (σ : { x // x K } →ₐ[F] L),
theorem IntermediateField.normal_iff_forall_map_eq {F : Type u_1} {L : Type u_3} [] [] [Algebra F L] [Normal F L] {K : } :
Normal F { x // x K } ∀ (σ : L →ₐ[F] L),
theorem IntermediateField.normal_iff_forall_map_eq' {F : Type u_1} {L : Type u_3} [] [] [Algebra F L] [Normal F L] {K : } :
Normal F { x // x K } ∀ (σ : L ≃ₐ[F] L), = K