Documentation

Mathlib.FieldTheory.IntermediateField.Algebraic

Results on finite dimensionality and algebraicity of intermediate fields. #

source
instance IntermediateField.finiteDimensional_left {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (F : IntermediateField K L) [FiniteDimensional K L] :
FiniteDimensional K { x : L // x ∈ F }
Equations
  • ⋯ = ⋯
source
instance IntermediateField.finiteDimensional_right {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (F : IntermediateField K L) [FiniteDimensional K L] :
FiniteDimensional { x : L // x ∈ F } L
Equations
  • ⋯ = ⋯
source
@[simp]
theorem IntermediateField.rank_eq_rank_subalgebra {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (F : IntermediateField K L) :
Module.rank K { x : L // x ∈ F.toSubalgebra } = Module.rank K { x : L // x ∈ F }
source
@[simp]
theorem IntermediateField.finrank_eq_finrank_subalgebra {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (F : IntermediateField K L) :
FiniteDimensional.finrank K { x : L // x ∈ F.toSubalgebra } = FiniteDimensional.finrank K { x : L // x ∈ F }
source
@[simp]
theorem IntermediateField.toSubalgebra_eq_iff {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {F : IntermediateField K L} {E : IntermediateField K L} :
F.toSubalgebra = E.toSubalgebra ↔ F = E
source
theorem IntermediateField.eq_of_le_of_finrank_le {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {F : IntermediateField K L} {E : IntermediateField K L} [hfin : FiniteDimensional K { x : L // x ∈ E }] (h_le : F ≤ E) (h_finrank : FiniteDimensional.finrank K { x : L // x ∈ E } ≤ FiniteDimensional.finrank K { x : L // x ∈ F }) :
F = E

If F ≤ E are two intermediate fields of L / K such that [E : K] ≤ [F : K] are finite, then F = E.

source
theorem IntermediateField.eq_of_le_of_finrank_eq {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {F : IntermediateField K L} {E : IntermediateField K L} [FiniteDimensional K { x : L // x ∈ E }] (h_le : F ≤ E) (h_finrank : FiniteDimensional.finrank K { x : L // x ∈ F } = FiniteDimensional.finrank K { x : L // x ∈ E }) :
F = E

If F ≤ E are two intermediate fields of L / K such that [F : K] = [E : K] are finite, then F = E.

source
theorem IntermediateField.eq_of_le_of_finrank_le' {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {F : IntermediateField K L} {E : IntermediateField K L} [FiniteDimensional { x : L // x ∈ F } L] (h_le : F ≤ E) (h_finrank : FiniteDimensional.finrank { x : L // x ∈ F } L ≤ FiniteDimensional.finrank { x : L // x ∈ E } L) :
F = E

If F ≤ E are two intermediate fields of L / K such that [L : F] ≤ [L : E] are finite, then F = E.

source
theorem IntermediateField.eq_of_le_of_finrank_eq' {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {F : IntermediateField K L} {E : IntermediateField K L} [FiniteDimensional { x : L // x ∈ F } L] (h_le : F ≤ E) (h_finrank : FiniteDimensional.finrank { x : L // x ∈ F } L = FiniteDimensional.finrank { x : L // x ∈ E } L) :
F = E

If F ≤ E are two intermediate fields of L / K such that [L : F] = [L : E] are finite, then F = E.

source
theorem IntermediateField.isAlgebraic_iff {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {S : IntermediateField K L} {x : { x : L // x ∈ S }} :
IsAlgebraic K x ↔ IsAlgebraic K ↑x
source
theorem IntermediateField.isIntegral_iff {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {S : IntermediateField K L} {x : { x : L // x ∈ S }} :
IsIntegral K x ↔ IsIntegral K ↑x
source
theorem IntermediateField.minpoly_eq {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {S : IntermediateField K L} (x : { x : L // x ∈ S }) :
minpoly K x = minpoly K ↑x
source
def subalgebraEquivIntermediateField {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] [Algebra.IsAlgebraic K L] :
Subalgebra K L ≃o IntermediateField K L

If L/K is algebraic, the K-subalgebras of L are all fields.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem mem_subalgebraEquivIntermediateField {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] [Algebra.IsAlgebraic K L] {S : Subalgebra K L} {x : L} :
    x ∈ subalgebraEquivIntermediateField S ↔ x ∈ S
    source
    @[simp]
    theorem mem_subalgebraEquivIntermediateField_symm {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] [Algebra.IsAlgebraic K L] {S : IntermediateField K L} {x : L} :
    x ∈ subalgebraEquivIntermediateField.symm S ↔ x ∈ S