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) [Field F] [Field K] [Field L] [Algebra F K] [Algebra F L] : IntermediateField F L

The normal closure of K in L.

Equations

• normalClosure F K L = ⨆ (f : K →ₐ[F] L), AlgHom.fieldRange f

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) : AlgHom.fieldRange f ≤ normalClosure F K 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] : normalClosure F K L = ⨆ (x : K), IntermediateField.adjoin F (Polynomial.rootSet (minpoly F x) 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 }

Equations

• normalClosure.normal = normalClosure.normal.proof_1

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] : FiniteDimensional F { x // x ∈ normalClosure F K L }

Equations

• normalClosure.is_finiteDimensional = normalClosure.is_finiteDimensional.proof_1

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 }

Equations

• One or more equations did not get rendered due to their size.

instance normalClosure.instIsScalarTowerSubtypeMemIntermediateFieldInstMembershipInstSetLikeIntermediateFieldNormalClosureToSMulToCommSemiringToSemifieldToSemiringToDivisionSemiringToSemifieldToSMulToCommSemiringToSemiringToSemiringToDivisionSemiringToSemifieldToSubalgebraAlgebraToSMulAlgebra (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] : IsScalarTower F K { x // x ∈ normalClosure F K L }

Equations

• One or more equations did not get rendered due to their size.

instance normalClosure.instIsScalarTowerSubtypeMemIntermediateFieldInstMembershipInstSetLikeIntermediateFieldNormalClosureToSMulToCommSemiringToSemifieldToSemiringToCommSemiringToSemifieldToSemiringToDivisionSemiringToSemifieldToSubalgebraAlgebraInstSMulSubtypeMemSubalgebraInstMembershipInstSetLikeSubalgebraToSMulToCommSemiringId (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] : IsScalarTower K { x // x ∈ normalClosure F K L } L

Equations

• One or more equations did not get rendered due to their size.

theorem normalClosure.restrictScalars_eq (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] : IntermediateField.restrictScalars F (AlgHom.fieldRange (IsScalarTower.toAlgHom K { x // x ∈ normalClosure F K L } L)) = 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) : ↑(IntermediateField.closureOperator F L) K = normalClosure F { x // x ∈ K } L

noncomputable def IntermediateField.closureOperator (F : Type u_1) (L : Type u_3) [Field F] [Field L] [Algebra F L] [Normal F L] : ClosureOperator (IntermediateField F L)

normalClosure as a ClosureOperator.

Equations

• One or more equations did not get rendered due to their size.

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