doc-next-gen

Mathlib.FieldTheory.IntermediateField.Algebraic

Module docstring

{"# Results on finite dimensionality and algebraicity of intermediate fields. "}

IntermediateField.coe_isIntegral_iff theorem
{R : Type*} [CommRing R] [Algebra R K] [Algebra R L] [IsScalarTower R K L] {x : S} : IsIntegral R (x : L) ↔ IsIntegral R x
Full source 
theorem IntermediateField.coe_isIntegral_iff {R : Type*} [CommRing R] [Algebra R K] [Algebra R L]
    [IsScalarTower R K L] {x : S} : IsIntegralIsIntegral R (x : L) ↔ IsIntegral R x :=
  isIntegral_algHom_iff (S.val.restrictScalars R) Subtype.val_injective
Integrality Criterion for Intermediate Field Elements
Informal description
Let $R$ be a commutative ring, $K$ and $L$ be fields with $K \subseteq L$, and $S$ be an intermediate field between $K$ and $L$. Suppose there are algebra structures $R \to K \to L$ forming a scalar tower. Then for any element $x \in S$, the following are equivalent: 1. $x$ is integral over $R$ when viewed as an element of $L$ (i.e., $\text{IsIntegral}_R (x : L)$) 2. $x$ is integral over $R$ in $S$ (i.e., $\text{IsIntegral}_R x$)
Subalgebra.IsAlgebraic.toIntermediateField definition
{S : Subalgebra K L} (hS : S.IsAlgebraic) : IntermediateField K L
Full source 
/-- Turn an algebraic subalgebra into an intermediate field, `Subalgebra.IsAlgebraic` version. -/
def Subalgebra.IsAlgebraic.toIntermediateField {S : Subalgebra K L} (hS : S.IsAlgebraic) :
    IntermediateField K L where
  toSubalgebra := S
  inv_mem' x hx := Algebra.adjoin_le_iff.mpr
    (Set.singleton_subset_iff.mpr hx) (hS x hx).isIntegral.inv_mem_adjoin
Intermediate field from algebraic subalgebra
Informal description
Given an algebraic subalgebra \( S \) of a field extension \( L \) over \( K \), this function constructs an intermediate field between \( K \) and \( L \) from \( S \). Specifically, for any element \( x \in S \), the inverse \( x^{-1} \) is also contained in the resulting intermediate field, ensuring the structure is closed under field operations.
Algebra.IsAlgebraic.toIntermediateField abbrev
(S : Subalgebra K L) [Algebra.IsAlgebraic K S] : IntermediateField K L
Full source 
/-- Turn an algebraic subalgebra into an intermediate field, `Algebra.IsAlgebraic` version. -/
abbrev Algebra.IsAlgebraic.toIntermediateField (S : Subalgebra K L) [Algebra.IsAlgebraic K S] :
    IntermediateField K L := (S.isAlgebraic_iff.mpr ‹_›).toIntermediateField
Construction of Intermediate Field from Algebraic Subalgebra
Informal description
Given a subalgebra $S$ of a field extension $L$ over $K$ such that $S$ is algebraic over $K$, the function constructs an intermediate field between $K$ and $L$ from $S$.
IntermediateField.isAlgebraic_tower_top instance
[Algebra.IsAlgebraic K L] : Algebra.IsAlgebraic S L
Full source 
instance isAlgebraic_tower_top [Algebra.IsAlgebraic K L] : Algebra.IsAlgebraic S L :=
  Algebra.IsAlgebraic.tower_top (K := K) S
Algebraicity of Field Extensions over Intermediate Fields
Informal description
For any intermediate field $S$ between fields $K$ and $L$, if $L$ is algebraic over $K$, then $L$ is also algebraic over $S$.
IntermediateField.finiteDimensional_left instance
[FiniteDimensional K L] : FiniteDimensional K F
Full source 
instance finiteDimensional_left [FiniteDimensional K L] : FiniteDimensional K F := .left K F L
Finite-Dimensionality of Intermediate Fields in Finite Extensions
Informal description
For any intermediate field $F$ between fields $K$ and $L$, if $L$ is finite-dimensional as a vector space over $K$, then $F$ is also finite-dimensional as a vector space over $K$.
IntermediateField.finiteDimensional_right instance
[FiniteDimensional K L] : FiniteDimensional F L
Full source 
instance finiteDimensional_right [FiniteDimensional K L] : FiniteDimensional F L := .right K F L
Finite-Dimensionality of Field Extensions over Intermediate Fields
Informal description
For any intermediate field $F$ between fields $K$ and $L$, if $L$ is finite-dimensional as a vector space over $K$, then $L$ is also finite-dimensional as a vector space over $F$.
IntermediateField.rank_eq_rank_subalgebra theorem
: Module.rank K F.toSubalgebra = Module.rank K F
Full source 
@[simp]
theorem rank_eq_rank_subalgebra : Module.rank K F.toSubalgebra = Module.rank K F :=
  rfl
Rank Equality for Intermediate Field and Its Subalgebra
Informal description
For any intermediate field $F$ between fields $K$ and $L$, the rank of $F$ as a $K$-module is equal to the rank of its underlying $K$-subalgebra. In other words, $\text{rank}_K(F) = \text{rank}_K(F_{\text{subalg}})$, where $F_{\text{subalg}}$ denotes $F$ viewed as a subalgebra over $K$.
IntermediateField.finrank_eq_finrank_subalgebra theorem
: finrank K F.toSubalgebra = finrank K F
Full source 
@[simp]
theorem finrank_eq_finrank_subalgebra : finrank K F.toSubalgebra = finrank K F :=
  rfl
Equality of Finite Ranks for Intermediate Field and its Subalgebra
Informal description
For any intermediate field $F$ between fields $K$ and $L$, the finite rank of $F$ as a $K$-subalgebra is equal to the finite rank of $F$ as a $K$-vector space, i.e., $\text{finrank}_K F.\text{toSubalgebra} = \text{finrank}_K F$.
IntermediateField.isAlgebraic_iff theorem
{x : S} : IsAlgebraic K x ↔ IsAlgebraic K (x : L)
Full source 
theorem isAlgebraic_iff {x : S} : IsAlgebraicIsAlgebraic K x ↔ IsAlgebraic K (x : L) :=
  (isAlgebraic_algebraMap_iff (algebraMap S L).injective).symm
Algebraicity Criterion for Intermediate Field Elements
Informal description
For any intermediate field $S$ between fields $K$ and $L$, and any element $x \in S$, the element $x$ is algebraic over $K$ if and only if its image under the inclusion map $S \hookrightarrow L$ is algebraic over $K$.
IntermediateField.isIntegral_iff theorem
{x : S} : IsIntegral K x ↔ IsIntegral K (x : L)
Full source 
theorem isIntegral_iff {x : S} : IsIntegralIsIntegral K x ↔ IsIntegral K (x : L) :=
  (isIntegral_algHom_iff S.val S.val.injective).symm
Integrality Criterion for Intermediate Field Elements
Informal description
For any intermediate field \( S \) between fields \( K \) and \( L \), and any element \( x \in S \), the element \( x \) is integral over \( K \) if and only if its image under the inclusion map \( S \hookrightarrow L \) is integral over \( K \).
IntermediateField.minpoly_eq theorem
(x : S) : minpoly K x = minpoly K (x : L)
Full source 
theorem minpoly_eq (x : S) : minpoly K x = minpoly K (x : L) :=
  (minpoly.algebraMap_eq (algebraMap S L).injective x).symm
Minimal Polynomial Equality for Intermediate Field Elements
Informal description
For any intermediate field $S$ between fields $K$ and $L$, and any element $x \in S$, the minimal polynomial of $x$ over $K$ is equal to the minimal polynomial of $x$ (viewed as an element of $L$) over $K$.
subalgebraEquivIntermediateField definition
[Algebra.IsAlgebraic K L] : Subalgebra K L ≃o IntermediateField K L
Full source 
/-- If `L/K` is algebraic, the `K`-subalgebras of `L` are all fields. -/
def subalgebraEquivIntermediateField [Algebra.IsAlgebraic K L] :
    SubalgebraSubalgebra K L ≃o IntermediateField K L where
  toFun S := S.toIntermediateField fun x hx => S.inv_mem_of_algebraic
    (Algebra.IsAlgebraic.isAlgebraic ((⟨x, hx⟩ : S) : L))
  invFun S := S.toSubalgebra
  left_inv _ := toSubalgebra_toIntermediateField _ _
  right_inv := toIntermediateField_toSubalgebra
  map_rel_iff' := Iff.rfl
Subalgebra-Intermediate Field Isomorphism for Algebraic Extensions
Informal description
Given an algebraic field extension \( L/K \), there is an order-preserving isomorphism between the lattice of \( K \)-subalgebras of \( L \) and the lattice of intermediate fields between \( K \) and \( L \). The isomorphism is constructed as follows: - The forward direction converts a subalgebra \( S \) to an intermediate field by adjoining inverses (using the algebraic property to ensure closure under inverses). - The backward direction forgets the field structure and retains only the subalgebra structure. - The isomorphism preserves the partial order (inclusion) in both directions.
mem_subalgebraEquivIntermediateField theorem
[Algebra.IsAlgebraic K L] {S : Subalgebra K L} {x : L} : x ∈ subalgebraEquivIntermediateField S ↔ x ∈ S
Full source 
@[simp]
theorem mem_subalgebraEquivIntermediateField [Algebra.IsAlgebraic K L] {S : Subalgebra K L}
    {x : L} : x ∈ subalgebraEquivIntermediateField Sx ∈ subalgebraEquivIntermediateField S ↔ x ∈ S :=
  Iff.rfl
Membership Preservation in Subalgebra-Intermediate Field Isomorphism for Algebraic Extensions
Informal description
Let $L/K$ be an algebraic field extension. For any $K$-subalgebra $S$ of $L$ and any element $x \in L$, we have $x$ belongs to the intermediate field corresponding to $S$ under the subalgebra-intermediate field isomorphism if and only if $x$ belongs to $S$ itself. In other words, the isomorphism preserves membership of elements.
mem_subalgebraEquivIntermediateField_symm theorem
[Algebra.IsAlgebraic K L] {S : IntermediateField K L} {x : L} : x ∈ subalgebraEquivIntermediateField.symm S ↔ x ∈ S
Full source 
@[simp]
theorem mem_subalgebraEquivIntermediateField_symm [Algebra.IsAlgebraic K L]
    {S : IntermediateField K L} {x : L} :
    x ∈ subalgebraEquivIntermediateField.symm Sx ∈ subalgebraEquivIntermediateField.symm S ↔ x ∈ S :=
  Iff.rfl
Membership Criterion for Inverse of Subalgebra-Intermediate Field Isomorphism in Algebraic Extensions
Informal description
Let $L/K$ be an algebraic field extension. For any intermediate field $S$ between $K$ and $L$ and any element $x \in L$, we have $x \in \varphi^{-1}(S)$ if and only if $x \in S$, where $\varphi$ is the order isomorphism between the lattice of $K$-subalgebras of $L$ and the lattice of intermediate fields between $K$ and $L$.