Results on finite dimensionality and algebraicity of intermediate fields. #
theorem
IntermediateField.coe_isIntegral_iff
{K : Type u_1}
{L : Type u_2}
[Field K]
[Field L]
[Algebra K L]
{S : IntermediateField K L}
{R : Type u_3}
[CommRing R]
[Algebra R K]
[Algebra R L]
[IsScalarTower R K L]
{x : ↥S}
:
IsIntegral R ↑x ↔ IsIntegral R x
def
Subalgebra.IsAlgebraic.toIntermediateField
{K : Type u_1}
{L : Type u_2}
[Field K]
[Field L]
[Algebra K L]
{S : Subalgebra K L}
(hS : S.IsAlgebraic)
:
Turn an algebraic subalgebra into an intermediate field, Subalgebra.IsAlgebraic
version.
Equations
- hS.toIntermediateField = { toSubalgebra := S, inv_mem' := ⋯ }
Instances For
@[reducible, inline]
abbrev
Algebra.IsAlgebraic.toIntermediateField
{K : Type u_1}
{L : Type u_2}
[Field K]
[Field L]
[Algebra K L]
(S : Subalgebra K L)
[Algebra.IsAlgebraic K ↥S]
:
Turn an algebraic subalgebra into an intermediate field, Algebra.IsAlgebraic
version.
Equations
- Algebra.IsAlgebraic.toIntermediateField S = ⋯.toIntermediateField
Instances For
instance
IntermediateField.isAlgebraic_tower_bot
{K : Type u_1}
{L : Type u_2}
[Field K]
[Field L]
[Algebra K L]
{S : IntermediateField K L}
[Algebra.IsAlgebraic K L]
:
Algebra.IsAlgebraic K ↥S
instance
IntermediateField.isAlgebraic_tower_top
{K : Type u_1}
{L : Type u_2}
[Field K]
[Field L]
[Algebra K L]
{S : IntermediateField K L}
[Algebra.IsAlgebraic K L]
:
Algebra.IsAlgebraic (↥S) L
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
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
@[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
theorem
IntermediateField.eq_of_le_of_finrank_le
{K : Type u_1}
{L : Type u_2}
[Field K]
[Field L]
[Algebra K L]
{F 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 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 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 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}
: