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 #

noncomputable def normalClosure (F : Type u_1) (K : Type u_2) (L : Type u_3) [Field F] [Field K] [Field L] [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) [Field F] [Field K] [Field L] [Algebra F K] [Algebra F L] :
    normalClosure F K L = ⨆ (f : K →ₐ[F] L), AlgHom.fieldRange f
    theorem normalClosure_le_iff {F : Type u_1} {K : Type u_2} {L : Type u_3} [Field F] [Field K] [Field L] [Algebra F K] [Algebra F L] {K' : IntermediateField F L} :
    normalClosure F K L K' ∀ (f : K →ₐ[F] L), AlgHom.fieldRange f K'
    theorem AlgHom.fieldRange_le_normalClosure {F : Type u_1} {K : Type u_2} {L : Type u_3} [Field F] [Field K] [Field L] [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) [Field F] [Field K] [Field L] [Algebra F K] [Algebra F L] [Algebra K L] [IsScalarTower F K L] [h : Normal F L] :
    instance normalClosure.normal (F : Type u_1) (K : Type u_2) (L : Type u_3) [Field F] [Field K] [Field L] [Algebra F K] [Algebra F L] [Algebra K L] [IsScalarTower F K L] [h : Normal F L] :
    Normal F { x // x normalClosure F K L }
    instance normalClosure.is_finiteDimensional (F : Type u_1) (K : Type u_2) (L : Type u_3) [Field F] [Field K] [Field L] [Algebra F K] [Algebra F L] [FiniteDimensional F K] :
    noncomputable instance normalClosure.algebra (F : Type u_1) (K : Type u_2) (L : Type u_3) [Field F] [Field K] [Field L] [Algebra F K] [Algebra F L] [Algebra K L] [IsScalarTower F K L] :
    Algebra K { x // x normalClosure F K L }
    theorem IntermediateField.le_normalClosure {F : Type u_1} {L : Type u_3} [Field F] [Field L] [Algebra F L] (K : IntermediateField F L) :
    K normalClosure F { x // x K } L
    theorem IntermediateField.normalClosure_of_normal {F : Type u_1} {L : Type u_3} [Field F] [Field L] [Algebra F L] (K : IntermediateField F L) [Normal F { x // x K }] :
    normalClosure F { x // x K } L = K
    theorem IntermediateField.normalClosure_def' {F : Type u_1} {L : Type u_3} [Field F] [Field L] [Algebra F L] (K : IntermediateField F L) [Normal F L] :
    normalClosure F { x // x K } L = ⨆ (f : L →ₐ[F] L), IntermediateField.map f K
    theorem IntermediateField.normalClosure_def'' {F : Type u_1} {L : Type u_3} [Field F] [Field L] [Algebra F L] (K : IntermediateField F L) [Normal F L] :
    normalClosure F { x // x K } L = ⨆ (f : L ≃ₐ[F] L), IntermediateField.map (f) K
    theorem IntermediateField.normalClosure_mono {F : Type u_1} {L : Type u_3} [Field F] [Field L] [Algebra F L] (K : IntermediateField F L) (K' : IntermediateField F L) [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) [Field F] [Field L] [Algebra F L] [Normal F L] (K : IntermediateField F L) :
    noncomputable def IntermediateField.closureOperator (F : Type u_1) (L : Type u_3) [Field F] [Field L] [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} [Field F] [Field L] [Algebra F L] [Normal F L] {K : IntermediateField F L} :
      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} [Field F] [Field L] [Algebra F L] [Normal F L] {K : IntermediateField F L} :
      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} [Field F] [Field L] [Algebra F L] [Normal F L] {K : IntermediateField F L} :
      Normal F { x // x K } ∀ (σ : { x // x K } →ₐ[F] L), AlgHom.fieldRange σ K
      theorem IntermediateField.normal_iff_forall_map_le {F : Type u_1} {L : Type u_3} [Field F] [Field L] [Algebra F L] [Normal F L] {K : IntermediateField F L} :
      Normal F { x // x K } ∀ (σ : L →ₐ[F] L), IntermediateField.map σ K K
      theorem IntermediateField.normal_iff_forall_map_le' {F : Type u_1} {L : Type u_3} [Field F] [Field L] [Algebra F L] [Normal F L] {K : IntermediateField F L} :
      Normal F { x // x K } ∀ (σ : L ≃ₐ[F] L), IntermediateField.map (σ) K K
      theorem IntermediateField.normal_iff_forall_fieldRange_eq {F : Type u_1} {L : Type u_3} [Field F] [Field L] [Algebra F L] [Normal F L] {K : IntermediateField F L} :
      Normal F { x // x K } ∀ (σ : { x // x K } →ₐ[F] L), AlgHom.fieldRange σ = K
      theorem IntermediateField.normal_iff_forall_map_eq {F : Type u_1} {L : Type u_3} [Field F] [Field L] [Algebra F L] [Normal F L] {K : IntermediateField F L} :
      Normal F { x // x K } ∀ (σ : L →ₐ[F] L), IntermediateField.map σ K = K
      theorem IntermediateField.normal_iff_forall_map_eq' {F : Type u_1} {L : Type u_3} [Field F] [Field L] [Algebra F L] [Normal F L] {K : IntermediateField F L} :
      Normal F { x // x K } ∀ (σ : L ≃ₐ[F] L), IntermediateField.map (σ) K = K