IntermediateField.isAlgebraic_iSup
theorem IntermediateField.isAlgebraic_iSup :
∀ {K : Type u} [inst : Field K] {L : Type u_3} [inst_1 : Field L] [inst_2 : Algebra K L] {ι : Type u_4}
{t : ι → IntermediateField K L}, (∀ (i : ι), Algebra.IsAlgebraic K ↥(t i)) → Algebra.IsAlgebraic K ↥(⨆ i, t i)
This theorem states that if we have an algebraic extension of a field `K` into a field `L` (specified by a function `t` from an index set `ι` to intermediate fields between `K` and `L`), and each of these extensions is algebraic (meaning that every element in the extension is a root of some polynomial with coefficients in `K`), then the compositum of these extensions (represented by the supremum `⨆ i, t i` over the index set `ι`) is also an algebraic extension of `K`. In simpler terms, the compositum of algebraic extensions remains algebraic.
More concisely: If `K` is a field and `L` is the compositum of a family `(t i : Field | i ∈ ι)` of algebraic extensions of `K`, then `L` is an algebraic extension of `K`.
|
PowerBasis.equivAdjoinSimple.proof_2
theorem PowerBasis.equivAdjoinSimple.proof_2 :
∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] (pb : PowerBasis K L),
minpoly K (IntermediateField.adjoin.powerBasis ⋯).gen = minpoly K pb.gen
This theorem states that for any given types 'K' and 'L' where 'K' is a field, 'L' is a field, and there's an algebra structure over 'K' and 'L', and given a power basis 'pb' over 'K' and 'L', the minimal polynomial of the generator of the power basis formed by adjoining an element to 'K' is the same as the minimal polynomial of the generator of the original power basis 'pb'. In other words, the process of creating a power basis by adjoining an element to a field doesn't change the minimal polynomial of the power basis generator.
More concisely: Given fields K and L with an algebra structure, a power basis pb over K and L, and an element a adjoined to K, the minimal polynomials of the generators of the original and new power bases are equal.
|
IntermediateField.adjoin_simple_isCompactElement
theorem IntermediateField.adjoin_simple_isCompactElement :
∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] (x : E),
CompleteLattice.IsCompactElement F⟮x⟯
The theorem `IntermediateField.adjoin_simple_isCompactElement` states that for any field `F` and `E`, where `E` is an `F`-algebra, and for any element `x` in `E`, the intermediate field adjoined by the element `x` is a compact element in the complete lattice structure of intermediate fields. Here, a compact element `k` is such that if any set has a supremum (`sSup`) above `k`, then there exists a finite subset whose supremum is also above `k`.
More concisely: Given a field `F`, an `F`-algebra `E` and an element `x` in `E`, the intermediate field adjoined by `x` is a compact element in the complete lattice of intermediate fields over `F`, meaning that if this intermediate field has a supremum above it, then there exists a finite set of intermediate fields whose supremum is also above it.
|
IntermediateField.adjoin_toSubalgebra_of_isAlgebraic
theorem IntermediateField.adjoin_toSubalgebra_of_isAlgebraic :
∀ {F : Type u_1} [inst : Field F] (E : Type u_2) [inst_1 : Field E] [inst_2 : Algebra F E] {K : Type u_3}
[inst_3 : Field K] [inst_4 : Algebra F K] [inst_5 : Algebra E K] [inst_6 : IsScalarTower F E K]
(L : IntermediateField F K),
Algebra.IsAlgebraic F E ∨ Algebra.IsAlgebraic F ↥L →
(IntermediateField.adjoin E ↑L).toSubalgebra = Algebra.adjoin E ↑L
The theorem `IntermediateField.adjoin_toSubalgebra_of_isAlgebraic` states that given a tower of field extensions `K / E / F`, and an intermediate field `L` of `K / F`, if either the extension `E / F` or `L / F` is algebraic (i.e., every element is a root of a non-zero polynomial with coefficients in `F`), then the field obtained by adjoining `E` and `L` is the same as the subalgebra generated by adjoining `E` and `L`.
More concisely: If fields `K/F`, `E/F`, and `L/F` are such that either `E/F` or `L/F` is algebraic, then `K = F[E] ⊥ F[L]`. (Here, `F[E]` and `F[L]` denote the subfields generated by `E` and `L` over `F`, and `⊥` denotes the subalgebra generated by their union.)
|
IntermediateField.adjoin_simple_eq_bot_iff
theorem IntermediateField.adjoin_simple_eq_bot_iff :
∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] {α : E},
F⟮α⟯ = ⊥ ↔ α ∈ ⊥
This theorem states that for any two fields `F` and `E`, where `E` is an algebra over `F`, and a given element `α` of `E`, the intermediate field generated by `F` and `α` is the bottom field if and only if `α` is an element of the bottom field. In other words, adding `α` to field `F` creates the smallest possible field (the bottom field) if and only if `α` itself is from the smallest possible field.
More concisely: The intermediate field generated by a field `F` and an element `α` in a field extension `E` is the constant field `F` if and only if `α` is already in `F`.
|
IntermediateField.subset_adjoin
theorem IntermediateField.subset_adjoin :
∀ (F : Type u_1) [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] (S : Set E),
S ⊆ ↑(IntermediateField.adjoin F S)
This theorem states that for any set `S` of elements from a type `E` (which is a field and also an `F`-algebra), when we extend a field `F` by adjoining the set `S` using the function `IntermediateField.adjoin`, the set `S` is a subset of the resulting intermediate field. In other words, all elements in the set `S` are elements of the intermediate field created by adjoining `S` to `F`.
More concisely: For any set `S` of elements from a field `F` that is also an `F-algebra,` the set `S` is contained in the intermediate field obtained by adjoining `S` to `F` using `IntermediateField.adjoin.`
|
IntermediateField.bot_eq_top_of_rank_adjoin_eq_one
theorem IntermediateField.bot_eq_top_of_rank_adjoin_eq_one :
∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E],
(∀ (x : E), Module.rank F ↥F⟮x⟯ = 1) → ⊥ = ⊤
The theorem states that if for a given field `F` and another field `E` (over which `F` is an algebra), the dimension of the field extension `F⟮x⟯` (obtained by adjoining an element `x` from `E` to `F`) is `1` over `F` for every `x` in `E`, then the bottom field `⊥` (which represents `F`) is equal to the top field `⊤` (which represents `E`). In other words, if every element of `E` can be obtained by adjoining elements from `F` such that the resulting field extension has dimension `1`, then `F` and `E` are the same field.
More concisely: If every element of an algebraic field extension `F<-E` has dimension 1 over `F`, then `F` and `E` are equal fields.
|
Polynomial.irreducible_comp
theorem Polynomial.irreducible_comp :
∀ {K : Type u} [inst : Field K] {f g : Polynomial K},
f.Monic →
g.Monic →
Irreducible f →
(∀ (E : Type u) [inst_1 : Field E] [inst_2 : Algebra K E] (x : E),
minpoly K x = f →
Irreducible
(Polynomial.map (algebraMap K ↥K⟮x⟯) g - Polynomial.C (IntermediateField.AdjoinSimple.gen K x))) →
Irreducible (f.comp g)
This theorem states that for any field K, given two monic polynomials `f` and `g` over K, if `f` is irreducible, and `g(x) - α` is irreducible in `K⟮α⟯` where `α` is a root of `f`, then the composition `f(g(x))` is also irreducible. In simpler terms, the composition of an irreducible polynomial with another properly constructed irreducible polynomial remains irreducible. This theorem is applicable under the algebraic structure of fields where the operations of addition, subtraction, multiplication and division (except by zero) are always possible and satisfy certain laws. It involves the notion of ring homomorphisms, monic polynomials, and irreducible polynomials.
More concisely: If `f` is an irreducible monic polynomial over a field `K`, and `α` is a root of `f` in an extension `K⟮α⟯`, then the composition `f ∘ g` is irreducible for any monic polynomial `g` over `K` such that `g(x) - α` is irreducible in `K⟮α⟯`.
|
IntermediateField.biSup_adjoin_simple
theorem IntermediateField.biSup_adjoin_simple :
∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] (S : Set E),
⨆ x ∈ S, F⟮x⟯ = IntermediateField.adjoin F S
The theorem `IntermediateField.biSup_adjoin_simple` states that for any given field `F`, and an extension of this field `E`, with an algebra structure defined over `F` and `E`, and for any set `S` of elements from `E`, the supremum of the adjoined fields created by each individual element `x` in the set `S` is equal to the intermediate field created by adjoining the entire set `S` to the field `F`. In more mathematical terms, this can be written as $\bigvee_{x \in S} F⟮x⟯ = \text{IntermediateField.adjoin} \, F \, S$. This statement essentially describes the equivalence between adjoining each individual element from a set to a field and adjoining the entire set at once.
More concisely: The supremum of the fields obtained by adjoining each element in a set to a field is equal to the intermediate field obtained by adjoining the entire set.
|
IntermediateField.adjoin_rank_le_of_isAlgebraic
theorem IntermediateField.adjoin_rank_le_of_isAlgebraic :
∀ {F : Type u_1} [inst : Field F] (E : Type u_2) [inst_1 : Field E] [inst_2 : Algebra F E] {K : Type u_3}
[inst_3 : Field K] [inst_4 : Algebra F K] [inst_5 : Algebra E K] [inst_6 : IsScalarTower F E K]
(L : IntermediateField F K),
Algebra.IsAlgebraic F E ∨ Algebra.IsAlgebraic F ↥L →
Module.rank E ↥(IntermediateField.adjoin E ↑L) ≤ Module.rank F ↥L
This theorem is about field extensions and algebraic elements. It states that if you have a tower of field extensions `K / E / F`, with `L` as an intermediate field of `K / F`, and if either `E / F` or `L / F` is algebraic (meaning all their elements are roots of some non-zero polynomial with coefficients in `F`), then the dimension of the field extension `E(L)` over `E` is less than or equal to the dimension of the field extension `L` over `F`. This is a corollary of `Subalgebra.adjoin_rank_le` since in this case `E(L)` is equal to `E[L]`.
More concisely: If `K` is a field extension of `F`, `L` is an intermediate field of `K/F`, and either `L/F` or `E/F` is algebraic, then the dimension of `E(L)` over `E` is less than or equal to the dimension of `L` over `F`.
|
IntermediateField.adjoin.powerBasis_gen
theorem IntermediateField.adjoin.powerBasis_gen :
∀ {K : Type u} [inst : Field K] {L : Type u_3} [inst_1 : Field L] [inst_2 : Algebra K L] {x : L}
(hx : IsIntegral K x), (IntermediateField.adjoin.powerBasis hx).gen = IntermediateField.AdjoinSimple.gen K x
This theorem states that for any fields `K` and `L` with `L` being an algebra over `K`, and for any element `x` of `L` that is integral over `K`, the generator of the power basis of `K⟮x⟯` is equivalent to the generator of `F⟮α⟯`. In other words, the element that generates the power basis, which is composed of powers of `x` up to the degree of its minimal polynomial, coincides with `x` itself when it is considered as an element adjoined to `K`.
More concisely: For any field extension `L` over `K` and any element `x` in `L` integral over `K`, the generator of the power basis of `K[x]` equals `x` itself.
|
IntermediateField.restrictScalars_adjoin_of_algEquiv
theorem IntermediateField.restrictScalars_adjoin_of_algEquiv :
∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] {L : Type u_3}
{L' : Type u_4} [inst_3 : Field L] [inst_4 : Field L'] [inst_5 : Algebra F L] [inst_6 : Algebra L E]
[inst_7 : Algebra F L'] [inst_8 : Algebra L' E] [inst_9 : IsScalarTower F L E] [inst_10 : IsScalarTower F L' E]
(i : L ≃ₐ[F] L'),
⇑(algebraMap L E) = ⇑(algebraMap L' E) ∘ ⇑i →
∀ (S : Set E),
IntermediateField.restrictScalars F (IntermediateField.adjoin L S) =
IntermediateField.restrictScalars F (IntermediateField.adjoin L' S)
The theorem `IntermediateField.restrictScalars_adjoin_of_algEquiv` states that if we have two field extension towers `E / L / F` and `E / L' / F`, where `L ≃ₐ[F] L'` is an isomorphism compatible with `E / L` and `E / L'`, then for any subset `S` of `E`, the intermediate fields `L(S)` and `L'(S)` generated by adjoining `S` to `L` and `L'` respectively, when restricted to `F`, are equal.
This theorem is about the equality of intermediate fields under certain conditions. It highlights the relationship between the structures of the field extensions and the properties of the algebra isomorphism between the two intermediate fields. The theorem essentially says that if there is an algebra isomorphism between two intermediate fields in their respective field extension towers, then the intermediate fields obtained by adjoining the same set to these intermediate fields are equal when they are both viewed as extensions of the base field.
More concisely: If `E / L / F` and `E / L' / F` are field extensions with `L ≃ₐ[F] L'` and `S ⊆ E`, then `L(S) ∣ F` is equal to `L'(S) ∣ F`.
|
IntermediateField.adjoin_adjoin_comm
theorem IntermediateField.adjoin_adjoin_comm :
∀ (F : Type u_1) [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] (S T : Set E),
IntermediateField.restrictScalars F (IntermediateField.adjoin (↥(IntermediateField.adjoin F S)) T) =
IntermediateField.restrictScalars F (IntermediateField.adjoin (↥(IntermediateField.adjoin F T)) S)
The theorem `IntermediateField.adjoin_adjoin_comm` states that for any field `F` and any two sets `S` and `T` of elements in an extension field `E` of `F`, the intermediate field formed by adjoining `S` to `F` and then adjoining `T` to the result is the same as the intermediate field formed by adjoining `T` to `F` and then adjoining `S` to the result. In other words, the order of adjoining does not affect the resulting intermediate field, so `F[S][T] = F[T][S]`. This is expressed in Lean code as equality between the intermediate fields `IntermediateField.restrictScalars F (IntermediateField.adjoin (↥(IntermediateField.adjoin F S)) T)` and `IntermediateField.restrictScalars F (IntermediateField.adjoin (↥(IntermediateField.adjoin F T)) S)`.
More concisely: The theorem asserts that for any field extension F : Type, and sets S and T of elements in an extension field E of F, the intermediate fields F[S][T] and F[T][S] are equal.
|
IntermediateField.bot_eq_top_of_finrank_adjoin_le_one
theorem IntermediateField.bot_eq_top_of_finrank_adjoin_le_one :
∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E]
[inst_3 : FiniteDimensional F E], (∀ (x : E), FiniteDimensional.finrank F ↥F⟮x⟯ ≤ 1) → ⊥ = ⊤
The theorem `IntermediateField.bot_eq_top_of_finrank_adjoin_le_one` states that for any fields `F` and `E` where `F` is a subfield of `E` and `E` is a finite-dimensional vector space over `F`, if the dimension of the extension field `F⟮x⟯` (generated by adjoining any element `x` from `E` to `F`) over `F` is less than or equal to 1 for all `x` in `E`, then `F` must be equal to `E` (i.e., `F` is not a proper subfield of `E`). This is indicated by `⊥ = ⊤`, where `⊥` represents the smallest field (in this case `F`) and `⊤` represents the largest field (here `E`).
More concisely: If a subfield `F` of a finite-dimensional extension field `E` has finite dimension less than or equal to 1 for every element `x` in `E`, then `F` is equal to `E`.
|
IntermediateField.adjoin_algebraic_toSubalgebra
theorem IntermediateField.adjoin_algebraic_toSubalgebra :
∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] {S : Set E},
(∀ x ∈ S, IsAlgebraic F x) → (IntermediateField.adjoin F S).toSubalgebra = Algebra.adjoin F S
This theorem states that for any set `S` of elements from a field extension `E` over a field `F` where every element of `S` is algebraic over `F`, the subalgebra obtained by adjoining `S` to `F` using the intermediate field construction (`IntermediateField.adjoin`) is equal to the subalgebra obtained by adjoining `S` to `F` using the algebra construction (`Algebra.adjoin`). In simpler terms, this theorem asserts the equality of two different methods of extending a field by adjoining a set of algebraic elements.
More concisely: For any set `S` of algebraic elements over a field `F` in a field extension `E`, the subalgebras obtained by intermediately extending `F` with `S` and by directly extending `F` with `S` using the algebra construction are equal.
|
IntermediateField.gc
theorem IntermediateField.gc :
∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E],
GaloisConnection (IntermediateField.adjoin F) fun x => ↑x
The theorem `IntermediateField.gc` states that for any field `F` and any extension `E` of this field (where `E` is an algebra over `F`), there exists a Galois connection between the function `IntermediateField.adjoin F`, which extends `F` by adjoining a set, and the function that takes an intermediate field `x` and yields the set of elements in `x`. In other words, for any subset `S` of `E` and any intermediate field `x`, `S` is contained in `x` if and only if the field obtained by adjoining `S` to `F` is contained in `x`.
More concisely: For any field extension E of F, there exists a Galois connection between the function that maps an intermediate field x to the set of elements it contains from E, and the function that maps a subset S of E to the subfield of F generated by S and F.
|
IntermediateField.eq_adjoin_of_eq_algebra_adjoin
theorem IntermediateField.eq_adjoin_of_eq_algebra_adjoin :
∀ (F : Type u_1) [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] (S : Set E)
(K : IntermediateField F E), K.toSubalgebra = Algebra.adjoin F S → K = IntermediateField.adjoin F S
This theorem states that for any field `F`, type `E` which is also a field and an algebra over `F`, and a set `S` of type `E`, if the subalgebra of an intermediate field `K` is equal to the subalgebra obtained by adjoining `S` to `F`, then `K` itself must be equal to the intermediate field obtained by adjoining `S` to `F`. In other words, if the algebraic structure of `K` is the same as the algebraic structure generated by `F` and `S`, then `K` and the field generated by `F` and `S` are the same.
More concisely: If `F` is a field, `E` is a field and an algebra over `F`, `S` is a set of type `E`, and the subalgebras of an intermediate field `K` generated by `F` and by `F ∪ S` are equal, then `K` is equal to the field generated by `F` and `S`.
|
IntermediateField.mem_top
theorem IntermediateField.mem_top :
∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] {x : E}, x ∈ ⊤ := by
sorry
The theorem `IntermediateField.mem_top` states that for any two types `F` and `E` where both are fields and `E` is an algebra over `F`, any element `x` of `E` belongs to the top intermediate field. Here, the top intermediate field (denoted by `⊤`) refers to the intermediate field that contains all elements of `E`.
More concisely: For any fields `F` and `E` with `E` being an algebra over `F`, every element `x` in `E` lies in the top intermediate field `⊤`.
|
IntermediateField.adjoin_eq_top_of_adjoin_eq_top
theorem IntermediateField.adjoin_eq_top_of_adjoin_eq_top :
∀ (F : Type u_1) [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] {K : Type u}
[inst_3 : Field K] [inst_4 : Algebra F K] [inst_5 : Algebra E K] [inst_6 : IsScalarTower F E K] {S : Set K},
IntermediateField.adjoin F S = ⊤ → IntermediateField.adjoin E S = ⊤
The theorem `IntermediateField.adjoin_eq_top_of_adjoin_eq_top` states that given a tower of field extensions `K / E / F`, and a subset `S` of `K` such that the field `F` adjoined with the set `S` equals `K` (denoted as `F(S) = K`), then the field `E` adjoined with the set `S` also equals `K` (denoted as `E(S) = K`). In other words, if adjoining a set `S` to a field `F` results in the field `K`, then adjoining the same set `S` to any intermediate field `E` in the extension tower also results in the field `K`.
More concisely: If a field extension `K` is obtained by adjoining a set `S` to `F`, and `E` is an intermediate field in the extension `K / F`, then `E(S) = K`.
|
IntermediateField.finiteDimensional_adjoin
theorem IntermediateField.finiteDimensional_adjoin :
∀ {K : Type u} [inst : Field K] {L : Type u_3} [inst_1 : Field L] [inst_2 : Algebra K L] {S : Set L}
[inst_3 : Finite ↑S], (∀ x ∈ S, IsIntegral K x) → FiniteDimensional K ↥(IntermediateField.adjoin K S)
This theorem states that given a field extension `L / K`, and a finite subset `S` of `L` such that every element of `S` is integral (or algebraic) over `K`, the field `K(S)` obtained by adjoining `S` to `K` forms a finite extension over `K`. This is a direct corollary of the theorem `finiteDimensional_iSup_of_finite`. In other words, if we extend the field `K` by a finite set of elements that are roots of some monic polynomial in `K`, the resulting field extension is finite-dimensional.
More concisely: Given a field extension `L/K` and a finite subset `S` of `L` consisting of elements integral over `K`, the field `K(S)` is a finite extension of `K`.
|
IntermediateField.rank_bot
theorem IntermediateField.rank_bot :
∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E], Module.rank F ↥⊥ = 1
This theorem, named `IntermediateField.rank_bot`, states that for all fields `F` and `E`, where `E` is an algebra over `F`, the rank of the module `F` over the bottom intermediate field (`⊥`) is always equal to 1. The bottom intermediate field is the smallest possible subfield of `E` that contains `F`. The rank of a module, in this context, is a measure of the "size" or "dimensionality" of that module.
More concisely: For any field extension E over F, the rank of F as a module over the bottom intermediate field is equal to 1.
|
IntermediateField.adjoin_simple_toSubalgebra_of_integral
theorem IntermediateField.adjoin_simple_toSubalgebra_of_integral :
∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] {α : E},
IsIntegral F α → F⟮α⟯.toSubalgebra = Algebra.adjoin F {α}
The given theorem, `IntermediateField.adjoin_simple_toSubalgebra_of_integral`, states that for any fields `F` and `E` with `F` being an algebra over `E`, and any element `α` from `E` that is integral over `F`, the subalgebra generated by adjoining `α` to `F` corresponds to the minimal subalgebra that includes the set containing `α`. So, when `α` is integral over `F`, there is no difference between adjoining `α` and explicitly constructing the minimal subalgebra that includes `α`.
More concisely: For any field extension `F` of `E` and any element `α` in `E` integral over `F`, the subalgebra generated by `α` over `F` is equal to the minimal subalgebra containing `α`.
|
IntermediateField.adjoin_finset_isCompactElement
theorem IntermediateField.adjoin_finset_isCompactElement :
∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] (S : Finset E),
CompleteLattice.IsCompactElement (IntermediateField.adjoin F ↑S)
The theorem `IntermediateField.adjoin_finset_isCompactElement` states that for any field `F`, another field `E`, where `F` is a subfield of `E`, and any finite set `S` of elements from `E`, the operation of adjoining `S` to `F` creates an intermediate field that is a compact element in the lattice of intermediate fields. In other words, if we extend the field `F` by adjoining the set `S`, and if any set of intermediate fields has a supremum above the adjoined field, then there exists a finite subset of these intermediate fields whose supremum is also above the adjoined field. This theorem shows the finiteness condition (compactness) of the extension of a field by adjoining a finite set of elements.
More concisely: Given a field extension `F` ⊆ `E` and a finite set `S` �subset `E`, the algebraic closure `F(S)` is a compact element in the lattice of intermediate fields of `F` in `E`.
|
IntermediateField.sup_toSubalgebra_of_isAlgebraic
theorem IntermediateField.sup_toSubalgebra_of_isAlgebraic :
∀ {K : Type u_3} {L : Type u_4} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
(E1 E2 : IntermediateField K L),
Algebra.IsAlgebraic K ↥E1 ∨ Algebra.IsAlgebraic K ↥E2 →
(E1 ⊔ E2).toSubalgebra = E1.toSubalgebra ⊔ E2.toSubalgebra
This theorem states that for any two intermediate fields `E1` and `E2` of some algebra `L` over a field `K`, the compositum of `E1` and `E2` (denoted as `E1 ⊔ E2`) is equal to the compositum of their corresponding subalgebras, provided that one of the intermediate fields is algebraic over the base field `K`. Here, a field is considered algebraic if all its elements are algebraic.
More concisely: If one of the intermediate fields `E1` and `E2` of algebra `L` over field `K` is algebraic, then `E1 ⊔ E2` equals the compositum of their subalgebras.
|
IntermediateField.adjoin.mono
theorem IntermediateField.adjoin.mono :
∀ (F : Type u_1) [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] (S T : Set E),
S ⊆ T → IntermediateField.adjoin F S ≤ IntermediateField.adjoin F T
This theorem, `IntermediateField.adjoin.mono`, asserts that for any field `F` and any field extension `E` over `F` with the property that `E` is an `F`-algebra, if `S` and `T` are two subsets of `E` such that `S` is a subset of `T`, then the intermediate field generated by adjoining `S` to `F` is a subfield of the intermediate field generated by adjoining `T` to `F`. In other words, adjoins operation on subsets of `E` is monotone with respect to the subset inclusion relation.
More concisely: If `F` is a field, `E` is a field extension of `F` that is an `F`-algebra, and `S` is a subset of `T` in `E`, then the subfield generated by `S` over `F` is contained in the subfield generated by `T` over `F`.
|
IntermediateField.exists_lt_finrank_of_infinite_dimensional
theorem IntermediateField.exists_lt_finrank_of_infinite_dimensional :
∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E],
Algebra.IsAlgebraic F E →
¬FiniteDimensional F E → ∀ (n : ℕ), ∃ L, FiniteDimensional F ↥L ∧ n < FiniteDimensional.finrank F ↥L
The theorem states that if `E / F` is an infinite algebraic extension, meaning that `E` is an algebraic extension of `F` and `E` does not have finite dimension over `F`, then for any natural number `n`, there exists an intermediate field `L / F` such that `L` has finite dimension over `F` and the rank or dimension of `L` over `F` is greater than `n`.
In other words, no matter how large a natural number we choose, we can always find an intermediate field of the algebraic extension whose dimension is larger than that number, indicating the infinite capacity of the algebraic extension.
More concisely: For any infinite algebraic extension `E/F`, there exists an intermediate field `L/F` with finite dimension and larger rank than any given natural number `n`.
|
IntermediateField.adjoin_univ
theorem IntermediateField.adjoin_univ :
∀ (F : Type u_3) (E : Type u_4) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E],
IntermediateField.adjoin F Set.univ = ⊤
This theorem states that for any field `F` and any field `E`, if `E` is an algebra over `F`, then the intermediate field obtained by adjoining the universal set (which includes all elements of `E`) to `F` is the top element of the lattice of intermediate fields (i.e., it is the field `E` itself). In other words, if you extend `F` by all elements of `E`, you get `E` itself.
More concisely: For any field extension `E` of a field `F`, the field obtained by adjoining all elements of `E` to `F` is equal to `E`.
|
IntermediateField.finrank_eq_one_iff
theorem IntermediateField.finrank_eq_one_iff :
∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E]
{K : IntermediateField F E}, FiniteDimensional.finrank F ↥K = 1 ↔ K = ⊥
The theorem `IntermediateField.finrank_eq_one_iff` states that, for any field `F`, field `E`, and algebra structure for `E` over `F`, and for any intermediate field `K` of `E` over `F`, the rank of the module `K` over `F` (or in other words, the finite dimension of the vector space `K` over `F`) is equal to 1 if and only if `K` is the bottom intermediate field. The "bottom intermediate field" here refers to the smallest possible intermediate field, usually containing just the zero element and the multiplicative identity.
More concisely: For any field extension `F`⊆`E` and algebra structure on `E` over `F`, the rank of the intermediate field `K` over `F` equals 1 if and only if `K` is the smallest intermediate field containing only the zero element and the multiplicative identity.
|
IntermediateField.adjoin_le_subfield
theorem IntermediateField.adjoin_le_subfield :
∀ (F : Type u_1) [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] (S : Set E)
{K : Subfield E}, Set.range ⇑(algebraMap F E) ⊆ ↑K → S ⊆ ↑K → (IntermediateField.adjoin F S).toSubfield ≤ K
The theorem `IntermediateField.adjoin_le_subfield` asserts that for any two types `F` and `E` that have `Field` and `Algebra` structures, a set `S` of type `E`, and a subfield `K` of `E`, if the image of the algebra map from `F` to `E` is contained in `K` and the set `S` is also contained in `K`, then the subfield obtained by adjoining `S` to `F` (denoted as `IntermediateField.adjoin F S`) is a subset of (or, is contained in) `K`. In mathematical terms, if `F` is a field and `S` is a subset of a larger field `K`, then the field formed by adjoining `S` to `F` is contained in `K` provided that `F` is mapped into `K` by the algebra map and `S` is also a subset of `K`.
More concisely: If `F` is a subfield of `K`, `E` is a field containing both `F` and `S`, and the image of `F` under the algebra map from `F` to `E` is contained in `K`, then `IntermediateField.adjoin F S` is a subfield of `K`.
|
IntermediateField.top_toSubalgebra
theorem IntermediateField.top_toSubalgebra :
∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E], ⊤.toSubalgebra = ⊤ := by
sorry
This theorem states that for any two types `F` and `E` which are fields, and where `E` is an algebra over `F`, the top-level `IntermediateField` when converted to a `Subalgebra` is still the top-level object. Essentially, this theorem ensures that the process of converting a top-level intermediate field to a subalgebra does not change its 'top-level' status in the context of algebraic structures.
More concisely: Given types `F` and `E` as fields with `E` being an algebra over `F`, the conversion of `IntermediateField F E` to a `Subalgebra` results in the same top-level object.
|
IntermediateField.isSplittingField_iSup
theorem IntermediateField.isSplittingField_iSup :
∀ {K : Type u_3} {L : Type u_4} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] {ι : Type u_5}
{t : ι → IntermediateField K L} {p : ι → Polynomial K} {s : Finset ι},
(s.prod fun i => p i) ≠ 0 →
(∀ i ∈ s, Polynomial.IsSplittingField K (↥(t i)) (p i)) →
Polynomial.IsSplittingField K (↥(⨆ i ∈ s, t i)) (s.prod fun i => p i)
This theorem states that if we have a set of splitting fields, the compositum (the smallest field containing all of them) is also a splitting field. More specifically, given a field `K`, a field `L` where `K` is a subfield, a set `s` and a function `t` mapping each element of `s` to an intermediate field between `K` and `L`, and a function `p` mapping each element of `s` to a polynomial over `K`. If the product of all polynomials `p i` for `i` in `s` is not zero and each intermediate field `t i` is a splitting field for the corresponding polynomial `p i`, then the compositum of all the intermediate fields `t i` is a splitting field for the product polynomial.
More concisely: If `{T_i : i ∈ S}` is a set of fields between a field `K` and a bigger field `L`, `p_i` is a polynomial over `K` for each `i ∈ S`, and the product of `p_i`'s is not zero, then the compositum of `{T_i : i ∈ S}` is a splitting field for the product polynomial.
|
IntermediateField.minpoly_gen
theorem IntermediateField.minpoly_gen :
∀ (F : Type u_1) [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] (α : E),
minpoly F (IntermediateField.AdjoinSimple.gen F α) = minpoly F α
This theorem states that for all field `F` and `E` such that `E` is an algebra over `F`, and for any element `α` in `E`, the minimal polynomial of `α` when considered as an element of the field obtained by adjoining `α` to `F`, i.e., `F⟮α⟯`, is the same as the minimal polynomial of `α` in `F`. The minimal polynomial is the monic polynomial of least degree that has `α` as a root.
More concisely: The minimal polynomial of an element `α` in an algebra `E` over a field `F` is equal to the minimal polynomial of `α` considered as an element of the field extension `F(α)`.
|
IntermediateField.mem_adjoin_simple_self
theorem IntermediateField.mem_adjoin_simple_self :
∀ (F : Type u_1) [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] (α : E), α ∈ F⟮α⟯ := by
sorry
This theorem states that for any field `F` and any field extension `E` of `F` with a specified algebra structure, any element `α` of `E` is an element of the intermediate field generated by adjoining `α` to `F`. In mathematical terms, if we consider `F` as a subfield of `E` and `α` as an element of `E`, then `α` is indeed contained in the field `F(α)`. This is a well-known fact in field theory in algebra.
More concisely: For any field extension E of field F with an algebra structure, every element α of E is contained in the subfield generated by F and α.
|
PowerBasis.equivAdjoinSimple.proof_1
theorem PowerBasis.equivAdjoinSimple.proof_1 :
∀ {K : Type u_2} {L : Type u_1} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] (pb : PowerBasis K L),
IsIntegral K pb.gen
The theorem `PowerBasis.equivAdjoinSimple.proof_1` asserts that for any field `K`, any field `L`, and any algebra of `L` over `K` denoted by `Algebra K L`, if there's a power basis `pb : PowerBasis K L`, then the generator of the power basis, `pb.gen`, is an integral element over `K`. In other words, the generator of the power basis is a root of some monic polynomial with coefficients in `K`.
More concisely: Given a field extension `L` over `K` with a power basis `pb` having generator `pb.gen`, the generator is an integral element over `K`, that is, it is a root of some monic polynomial with coefficients in `K`.
|
IntermediateField.adjoin_finite_isCompactElement
theorem IntermediateField.adjoin_finite_isCompactElement :
∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] {S : Set E},
S.Finite → CompleteLattice.IsCompactElement (IntermediateField.adjoin F S)
This theorem states that for any given fields `F` and `E` with an algebra structure between them, and any finite set `S` of elements from `E`, the intermediate field formed by adjoining `S` to `F` is a compact element in the lattice of intermediate fields. In other words, if any set of intermediate fields has a supremum above the adjoined field, then there exists a finite subset of this set which also has a supremum above the adjoined field. This property, known as being S-compact or simply compact in lattice theory, is a key concept in many areas of mathematics, including algebra and topology.
More concisely: For any fields `F` and `E` with an algebra structure between them, and any finite subset `S` of `E`, the intermediate field generated by `F` and `S` is compact in the lattice of intermediate fields.
|
isSplittingField_iff_intermediateField
theorem isSplittingField_iff_intermediateField :
∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] {p : Polynomial F},
Polynomial.IsSplittingField F E p ↔
Polynomial.Splits (algebraMap F E) p ∧ IntermediateField.adjoin F (p.rootSet E) = ⊤
The theorem `isSplittingField_iff_intermediateField` characterizes whether a given field `E` is a splitting field over `F` for a polynomial `p` in terms of `IntermediateField.adjoin` instead of `Algebra.adjoin`. Specifically, it states that `E` is a splitting field over `F` for `p` if and only if two conditions are met: first, the polynomial `p` splits over `E` when its coefficients are mapped from `F` to `E` using the algebra structure, i.e., every irreducible factor of the mapped polynomial `p` has degree 1; and second, the intermediate field obtained by adjoining the roots of `p` in `E` to `F` equals the top element of the lattice of subfields of `E`, i.e., it equals `E` itself.
More concisely: A field extension E of F is a splitting field of a polynomial p over F if and only if p splits over E and the intermediate field obtained by adjoining the roots of p in E to F equals E itself. (Note: This statement assumes the standard definitions and context of Lean's `IsSplittingField.isSplittingField_iff_intermediateField` theorem.)
|
IntermediateField.sup_toSubalgebra
theorem IntermediateField.sup_toSubalgebra :
∀ {K : Type u_3} {L : Type u_4} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
(E1 E2 : IntermediateField K L) [inst_3 : FiniteDimensional K ↥E1],
(E1 ⊔ E2).toSubalgebra = E1.toSubalgebra ⊔ E2.toSubalgebra
This theorem states that for any two intermediate fields `E1` and `E2` of an algebra `L` over a field `K`, if `E1` is also a finite-dimensional vector space over `K`, then the subalgebra of `L` generated by taking the union of `E1` and `E2` (`(E1 ⊔ E2).toSubalgebra`) is equivalent to the subalgebra generated by separately taking the union of `E1.toSubalgebra` and `E2.toSubalgebra` (`E1.toSubalgebra ⊔ E2.toSubalgebra`).
More concisely: The subalgebras generated by the union of two intermediate fields `E1` and `E2` of an algebra `L` over a field `K`, when `E1` is finite-dimensional over `K`, are equivalent.
|
IntermediateField.mem_bot
theorem IntermediateField.mem_bot :
∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] {x : E},
x ∈ ⊥ ↔ x ∈ Set.range ⇑(algebraMap F E)
The theorem `IntermediateField.mem_bot` states that for all fields `F` and `E`, where `E` has an algebra structure over `F`, and for any element `x` of `E`, `x` is in the smallest subfield if and only if `x` is in the range of the algebra map from `F` to `E`. In other words, the smallest subfield of `E` over `F` consists exactly of those elements of `E` that can be obtained by applying the algebra map to some element of `F`.
More concisely: The smallest subfield of a field `E` algebraically extended by a field `F` equals the image of `F` under the algebra map.
|
IntermediateField.adjoin_minpoly_coeff_of_exists_primitive_element
theorem IntermediateField.adjoin_minpoly_coeff_of_exists_primitive_element :
∀ (F : Type u_1) [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] {α : E}
[inst_3 : FiniteDimensional F E],
F⟮α⟯ = ⊤ →
∀ (K : IntermediateField F E),
IntermediateField.adjoin F ↑(Polynomial.map (algebraMap (↥K) E) (minpoly (↥K) α)).frange = K
The theorem `IntermediateField.adjoin_minpoly_coeff_of_exists_primitive_element` states that if `E / F` is a finite field extension and `E` is generated by a single element `α` (i.e., `E = F(α)`), then for any intermediate field `K` between `F` and `E`, the field `F` adjoined with the coefficients of the minimal polynomial of `α` over `K` is exactly `K` itself. Here, the minimal polynomial of `α` over `K` is the polynomial with coefficients in `K` of least degree that has `α` as a root.
More concisely: For a finite field extension `E/F` with `E = F(α)` and any intermediate field `K` between `F` and `E`, the field `F` adjoined with the coefficients of the minimal polynomial of `α` over `K` equals `K`.
|
IntermediateField.adjoin.finrank
theorem IntermediateField.adjoin.finrank :
∀ {K : Type u} [inst : Field K] {L : Type u_3} [inst_1 : Field L] [inst_2 : Algebra K L] {x : L},
IsIntegral K x → FiniteDimensional.finrank K ↥K⟮x⟯ = (minpoly K x).natDegree
The theorem `IntermediateField.adjoin.finrank` states that for any fields `K` and `L`, where `L` is an algebra over `K`, and any element `x` in `L` that is integral over `K`, the rank of the field resulting from adjoining `x` to `K` (denoted by `K⟮x⟯`), when considered as a module over `K`, equals the natural degree of the minimal polynomial of `x` over `K` (i.e., the smallest degree of any polynomial with coefficients in `K` that `x` is a root of). In other words, for a given integral element `x`, the dimension of `K⟮x⟯` as a vector space over `K` is equal to the degree of `x`'s minimal polynomial.
More concisely: The rank of the field extension K⟮x⟯ as a K-module equals the degree of the minimal polynomial of x over K.
|
IntermediateField.adjoin_adjoin_left
theorem IntermediateField.adjoin_adjoin_left :
∀ (F : Type u_1) [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] (S T : Set E),
IntermediateField.restrictScalars F (IntermediateField.adjoin (↥(IntermediateField.adjoin F S)) T) =
IntermediateField.adjoin F (S ∪ T)
The theorem `IntermediateField.adjoin_adjoin_left` states that for any two sets `S` and `T` of elements from a field extension `E` over a field `F`, the field obtained by first adjoining `S` to `F` and then adjoining `T` to the result is the same as the field obtained by adjoining the union of `S` and `T` to `F`. In other words, the process of adjoining is associative with respect to the union of sets. This is written in mathematical notation as `F[S][T] = F[S ∪ T]`.
The field `F` and the field extension `E` are both assumed to be algebraically structured over `F`.
More concisely: The theorem asserts that for any sets S and T of elements from a field extension E over a field F, the fields F[S][T] and F[S ∪ T] are equal.
|
IntermediateField.sup_toSubalgebra_of_isAlgebraic_right
theorem IntermediateField.sup_toSubalgebra_of_isAlgebraic_right :
∀ {K : Type u_3} {L : Type u_4} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
(E1 E2 : IntermediateField K L),
Algebra.IsAlgebraic K ↥E2 → (E1 ⊔ E2).toSubalgebra = E1.toSubalgebra ⊔ E2.toSubalgebra
The theorem `IntermediateField.sup_toSubalgebra_of_isAlgebraic_right` states that for any two `IntermediateField`s `E1` and `E2` of a field extension `L` over a field `K`, where all elements of `E2` are algebraic over `K`, the subalgebra corresponding to the supremum of `E1` and `E2` (denoted as `(E1 ⊔ E2).toSubalgebra`) is equal to the supremum of the subalgebras corresponding to `E1` and `E2` (denoted as `E1.toSubalgebra ⊔ E2.toSubalgebra`). This means when `E2` is algebraic over `K`, we can commute the operations of taking supremum and converting to a subalgebra between two intermediate fields.
More concisely: Given an interval `[E1, E2]` of `IntermediateField`s over a field `K` with `E2` algebraic over `K`, the subalgebras of `K` generated by `E1` and `E2` respectively, `E1.toSubalgebra` and `E2.toSubalgebra`, have the same supremum, i.e., `(E1 ⊔ E2).toSubalgebra = E1.toSubalgebra ⊔ E2.toSubalgebra`.
|
IntermediateField.adjoin_le_iff
theorem IntermediateField.adjoin_le_iff :
∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] {S : Set E}
{T : IntermediateField F E}, IntermediateField.adjoin F S ≤ T ↔ S ≤ ↑T
This theorem states that for any fields `F` and `E`, with `E` being an algebra over `F`, and any set `S` of elements from `E`, and any intermediate field `T` between `F` and `E`, the intermediate field formed by adjoining `S` to `F` is a subset of `T` if and only if `S` is a subset of the set of elements of `T`. In other words, the extension of a field `F` by a set `S` is contained within an intermediate field `T` between `F` and `E` if and only if the set `S` is contained within the field `T`.
More concisely: The theorem asserts that the subfield of `E` generated by `F` and a set `S` is contained in an intermediate field `T` between `F` and `E` if and only if `S` is contained in `T`.
|