Results on finite dimensionality and algebraicity of intermediate fields. #
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 ↥F
Equations
- ⋯ = ⋯
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 (↥F) L
Equations
- ⋯ = ⋯
@[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 ↥F.toSubalgebra = Module.rank K ↥F
@[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)
:
Module.finrank K ↥F.toSubalgebra = Module.finrank K ↥F
@[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}
:
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 ↥E]
(h_le : F ≤ E)
(h_finrank : Module.finrank K ↥E ≤ Module.finrank K ↥F)
:
F = E
If F ≤ E
are two intermediate fields of L / K
such that [E : K] ≤ [F : K]
are finite,
then F = E
.
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 ↥E]
(h_le : F ≤ E)
(h_finrank : Module.finrank K ↥F = Module.finrank K ↥E)
:
F = E
If F ≤ E
are two intermediate fields of L / K
such that [F : K] = [E : K]
are finite,
then F = E
.
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 (↥F) L]
(h_le : F ≤ E)
(h_finrank : Module.finrank (↥F) L ≤ Module.finrank (↥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
.
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 (↥F) L]
(h_le : F ≤ E)
(h_finrank : Module.finrank (↥F) L = Module.finrank (↥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
.
theorem
IntermediateField.isAlgebraic_iff
{K : Type u_1}
{L : Type u_2}
[Field K]
[Field L]
[Algebra K L]
{S : IntermediateField K L}
{x : ↥S}
:
IsAlgebraic K x ↔ IsAlgebraic K ↑x
theorem
IntermediateField.isIntegral_iff
{K : Type u_1}
{L : Type u_2}
[Field K]
[Field L]
[Algebra K L]
{S : IntermediateField K L}
{x : ↥S}
:
IsIntegral K x ↔ IsIntegral K ↑x
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
@[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}
:
@[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}
: