Adjoining Elements to Fields #
In this file we introduce the notion of adjoining elements to fields.
This isn't quite the same as adjoining elements to rings.
For example, algebra.adjoin K {x} might not include x⁻¹.
Main results #
adjoin_adjoin_left: adjoining S and then T is the same as adjoiningS ∪ T.bot_eq_top_of_dim_adjoin_eq_one: ifF⟮x⟯has dimension1overFfor everyxinEthenF = E
Notation #
F⟮α⟯: adjoin a single elementαtoF.
def
intermediate_field.adjoin
(F : Type u_1)
[field F]
{E : Type u_2}
[field E]
[algebra F E]
(S : set E) :
adjoin F S extends a field F by adjoining a set S ⊆ E.
Equations
- intermediate_field.adjoin F S = {to_subalgebra := {carrier := (subfield.closure (set.range ⇑(algebra_map F E) ∪ S)).carrier, mul_mem' := _, one_mem' := _, add_mem' := _, zero_mem' := _, algebra_map_mem' := _}, neg_mem' := _, inv_mem' := _}
@[simp]
theorem
intermediate_field.adjoin_le_iff
{F : Type u_1}
[field F]
{E : Type u_2}
[field E]
[algebra F E]
{S : set E}
{T : intermediate_field F E} :
intermediate_field.adjoin F S ≤ T ↔ S ≤ ↑T
Galois insertion between adjoin and coe.
Equations
- intermediate_field.gi = {choice := λ (s : set E) (hs : ↑(intermediate_field.adjoin F s) ≤ s), (intermediate_field.adjoin F s).copy s _, gc := _, le_l_u := _, choice_eq := _}
@[protected, instance]
def
intermediate_field.complete_lattice
{F : Type u_1}
[field F]
{E : Type u_2}
[field E]
[algebra F E] :
@[protected, instance]
def
intermediate_field.inhabited
{F : Type u_1}
[field F]
{E : Type u_2}
[field E]
[algebra F E] :
inhabited (intermediate_field F E)
Equations
@[simp]
theorem
intermediate_field.bot_to_subalgebra
{F : Type u_1}
[field F]
{E : Type u_2}
[field E]
[algebra F E] :
@[simp]
theorem
intermediate_field.top_to_subalgebra
{F : Type u_1}
[field F]
{E : Type u_2}
[field E]
[algebra F E] :
@[simp]
theorem
intermediate_field.top_to_subfield
{F : Type u_1}
[field F]
{E : Type u_2}
[field E]
[algebra F E] :
@[simp]
theorem
intermediate_field.inf_to_subalgebra
{F : Type u_1}
[field F]
{E : Type u_2}
[field E]
[algebra F E]
(S T : intermediate_field F E) :
(S ⊓ T).to_subalgebra = S.to_subalgebra ⊓ T.to_subalgebra
@[simp]
theorem
intermediate_field.inf_to_subfield
{F : Type u_1}
[field F]
{E : Type u_2}
[field E]
[algebra F E]
(S T : intermediate_field F E) :
(S ⊓ T).to_subfield = S.to_subfield ⊓ T.to_subfield
@[simp]
theorem
intermediate_field.Inf_to_subalgebra
{F : Type u_1}
[field F]
{E : Type u_2}
[field E]
[algebra F E]
(S : set (intermediate_field F E)) :
@[simp]
theorem
intermediate_field.Inf_to_subfield
{F : Type u_1}
[field F]
{E : Type u_2}
[field E]
[algebra F E]
(S : set (intermediate_field F E)) :
(Inf S).to_subfield = Inf (intermediate_field.to_subfield '' S)
@[simp, norm_cast]
theorem
intermediate_field.coe_infi
{F : Type u_1}
[field F]
{E : Type u_2}
[field E]
[algebra F E]
{ι : Sort u_3}
(S : ι → intermediate_field F E) :
@[simp]
theorem
intermediate_field.infi_to_subalgebra
{F : Type u_1}
[field F]
{E : Type u_2}
[field E]
[algebra F E]
{ι : Sort u_3}
(S : ι → intermediate_field F E) :
(infi S).to_subalgebra = ⨅ (i : ι), (S i).to_subalgebra
@[simp]
theorem
intermediate_field.infi_to_subfield
{F : Type u_1}
[field F]
{E : Type u_2}
[field E]
[algebra F E]
{ι : Sort u_3}
(S : ι → intermediate_field F E) :
(infi S).to_subfield = ⨅ (i : ι), (S i).to_subfield
@[simp]
theorem
intermediate_field.equiv_of_eq_apply
{F : Type u_1}
[field F]
{E : Type u_2}
[field E]
[algebra F E]
{S T : intermediate_field F E}
(h : S = T)
(x : ↥S) :
⇑(intermediate_field.equiv_of_eq h) x = ⟨↑x, _⟩
def
intermediate_field.equiv_of_eq
{F : Type u_1}
[field F]
{E : Type u_2}
[field E]
[algebra F E]
{S T : intermediate_field F E}
(h : S = T) :
Construct an algebra isomorphism from an equality of intermediate fields
@[simp]
theorem
intermediate_field.equiv_of_eq_symm
{F : Type u_1}
[field F]
{E : Type u_2}
[field E]
[algebra F E]
{S T : intermediate_field F E}
(h : S = T) :
@[simp]
theorem
intermediate_field.equiv_of_eq_rfl
{F : Type u_1}
[field F]
{E : Type u_2}
[field E]
[algebra F E]
(S : intermediate_field F E) :
@[simp]
theorem
intermediate_field.equiv_of_eq_trans
{F : Type u_1}
[field F]
{E : Type u_2}
[field E]
[algebra F E]
{S T U : intermediate_field F E}
(hST : S = T)
(hTU : T = U) :
noncomputable
def
intermediate_field.bot_equiv
(F : Type u_1)
[field F]
(E : Type u_2)
[field E]
[algebra F E] :
The bottom intermediate_field is isomorphic to the field.
Equations
@[simp]
theorem
intermediate_field.bot_equiv_def
{F : Type u_1}
[field F]
{E : Type u_2}
[field E]
[algebra F E]
(x : F) :
⇑(intermediate_field.bot_equiv F E) (⇑(algebra_map F ↥⊥) x) = x
@[protected, instance]
noncomputable
def
intermediate_field.algebra_over_bot
{F : Type u_1}
[field F]
{E : Type u_2}
[field E]
[algebra F E] :
@[protected, instance]
def
intermediate_field.is_scalar_tower_over_bot
{F : Type u_1}
[field F]
{E : Type u_2}
[field E]
[algebra F E] :
is_scalar_tower ↥⊥ F E
@[simp]
theorem
intermediate_field.top_equiv_apply
{F : Type u_1}
[field F]
{E : Type u_2}
[field E]
[algebra F E]
(ᾰ : ↥(⊤.to_subalgebra)) :
The top intermediate_field is isomorphic to the field.
This is the intermediate field version of subalgebra.top_equiv.
@[simp]
theorem
intermediate_field.top_equiv_symm_apply_coe
{F : Type u_1}
[field F]
{E : Type u_2}
[field E]
[algebra F E]
(a : E) :
↑(⇑(intermediate_field.top_equiv.symm) a) = a
@[simp]
theorem
intermediate_field.coe_bot_eq_self
{F : Type u_1}
[field F]
{E : Type u_2}
[field E]
[algebra F E]
(K : intermediate_field F E) :
@[simp]
theorem
intermediate_field.coe_top_eq_top
{F : Type u_1}
[field F]
{E : Type u_2}
[field E]
[algebra F E]
(K : intermediate_field F E) :
theorem
intermediate_field.adjoin_eq_range_algebra_map_adjoin
(F : Type u_1)
[field F]
{E : Type u_2}
[field E]
[algebra F E]
(S : set E) :
↑(intermediate_field.adjoin F S) = set.range ⇑(algebra_map ↥(intermediate_field.adjoin F S) E)
theorem
intermediate_field.adjoin.algebra_map_mem
(F : Type u_1)
[field F]
{E : Type u_2}
[field E]
[algebra F E]
(S : set E)
(x : F) :
⇑(algebra_map F E) x ∈ intermediate_field.adjoin F S
theorem
intermediate_field.adjoin.range_algebra_map_subset
(F : Type u_1)
[field F]
{E : Type u_2}
[field E]
[algebra F E]
(S : set E) :
set.range ⇑(algebra_map F E) ⊆ ↑(intermediate_field.adjoin F S)
@[protected, instance]
def
intermediate_field.adjoin.field_coe
(F : Type u_1)
[field F]
{E : Type u_2}
[field E]
[algebra F E]
(S : set E) :
has_coe_t F ↥(intermediate_field.adjoin F S)
Equations
- intermediate_field.adjoin.field_coe F S = {coe := λ (x : F), ⟨⇑(algebra_map F E) x, _⟩}
theorem
intermediate_field.subset_adjoin
(F : Type u_1)
[field F]
{E : Type u_2}
[field E]
[algebra F E]
(S : set E) :
S ⊆ ↑(intermediate_field.adjoin F S)
theorem
intermediate_field.adjoin_contains_field_as_subfield
{E : Type u_2}
[field E]
(S : set E)
(F : subfield E) :
↑F ⊆ ↑(intermediate_field.adjoin ↥F S)
@[simp]
theorem
intermediate_field.adjoin_empty
(F : Type u_1)
(E : Type u_2)
[field F]
[field E]
[algebra F E] :
@[simp]
theorem
intermediate_field.adjoin_univ
(F : Type u_1)
(E : Type u_2)
[field F]
[field E]
[algebra F E] :
theorem
intermediate_field.adjoin_le_subfield
(F : Type u_1)
[field F]
{E : Type u_2}
[field E]
[algebra F E]
(S : set E)
{K : subfield E}
(HF : set.range ⇑(algebra_map F E) ⊆ ↑K)
(HS : S ⊆ ↑K) :
(intermediate_field.adjoin F S).to_subfield ≤ K
If K is a field with F ⊆ K and S ⊆ K then adjoin F S ≤ K.
theorem
intermediate_field.adjoin_subset_adjoin_iff
(F : Type u_1)
[field F]
{E : Type u_2}
[field E]
[algebra F E]
{F' : Type u_3}
[field F']
[algebra F' E]
{S S' : set E} :
↑(intermediate_field.adjoin F S) ⊆ ↑(intermediate_field.adjoin F' S') ↔ set.range ⇑(algebra_map F E) ⊆ ↑(intermediate_field.adjoin F' S') ∧ S ⊆ ↑(intermediate_field.adjoin F' S')
theorem
intermediate_field.adjoin_adjoin_left
(F : Type u_1)
[field F]
{E : Type u_2}
[field E]
[algebra F E]
(S T : set E) :
↑(intermediate_field.adjoin ↥(intermediate_field.adjoin F S) T) = intermediate_field.adjoin F (S ∪ T)
F[S][T] = F[S ∪ T]
@[simp]
theorem
intermediate_field.adjoin_insert_adjoin
(F : Type u_1)
[field F]
{E : Type u_2}
[field E]
[algebra F E]
(S : set E)
(x : E) :
intermediate_field.adjoin F (insert x ↑(intermediate_field.adjoin F S)) = intermediate_field.adjoin F (insert x S)
theorem
intermediate_field.adjoin_adjoin_comm
(F : Type u_1)
[field F]
{E : Type u_2}
[field E]
[algebra F E]
(S T : set E) :
F[S][T] = F[T][S]
theorem
intermediate_field.algebra_adjoin_le_adjoin
(F : Type u_1)
[field F]
{E : Type u_2}
[field E]
[algebra F E]
(S : set E) :
theorem
intermediate_field.adjoin_eq_algebra_adjoin
(F : Type u_1)
[field F]
{E : Type u_2}
[field E]
[algebra F E]
(S : set E)
(inv_mem : ∀ (x : E), x ∈ algebra.adjoin F S → x⁻¹ ∈ algebra.adjoin F S) :
theorem
intermediate_field.eq_adjoin_of_eq_algebra_adjoin
(F : Type u_1)
[field F]
{E : Type u_2}
[field E]
[algebra F E]
(S : set E)
(K : intermediate_field F E)
(h : K.to_subalgebra = algebra.adjoin F S) :
K = intermediate_field.adjoin F S
theorem
intermediate_field.adjoin_induction
(F : Type u_1)
[field F]
{E : Type u_2}
[field E]
[algebra F E]
{s : set E}
{p : E → Prop}
{x : E}
(h : x ∈ intermediate_field.adjoin F s)
(Hs : ∀ (x : E), x ∈ s → p x)
(Hmap : ∀ (x : F), p (⇑(algebra_map F E) x))
(Hadd : ∀ (x y : E), p x → p y → p (x + y))
(Hneg : ∀ (x : E), p x → p (-x))
(Hinv : ∀ (x : E), p x → p x⁻¹)
(Hmul : ∀ (x y : E), p x → p y → p (x * y)) :
p x
@[class]
- insert : α → set α
Variation on set.insert to enable good notation for adjoining elements to fields.
Used to preferentially use singleton rather than insert when adjoining one element.
@[protected, instance]
Equations
- intermediate_field.insert_empty = {insert := λ (x : α), {x}}
@[protected, instance]
Equations
- intermediate_field.insert_nonempty s = {insert := λ (x : α), set.insert x s}
@[simp]
theorem
intermediate_field.adjoin_simple.algebra_map_gen
(F : Type u_1)
[field F]
{E : Type u_2}
[field E]
[algebra F E]
(α : E) :
⇑(algebra_map ↥F⟮α⟯ E) (intermediate_field.adjoin_simple.gen F α) = α
@[simp]
theorem
intermediate_field.adjoin_simple.is_integral_gen
(F : Type u_1)
[field F]
{E : Type u_2}
[field E]
[algebra F E]
(α : E) :
is_integral F (intermediate_field.adjoin_simple.gen F α) ↔ is_integral F α
theorem
intermediate_field.adjoin_simple_to_subalgebra_of_integral
(F : Type u_1)
[field F]
{E : Type u_2}
[field E]
[algebra F E]
(α : E)
(hα : is_integral F α) :
F⟮α⟯.to_subalgebra = algebra.adjoin F {α}
@[simp]
theorem
intermediate_field.dim_eq_one_iff
{F : Type u_1}
[field F]
{E : Type u_2}
[field E]
[algebra F E]
{K : intermediate_field F E} :
@[simp]
theorem
intermediate_field.finrank_eq_one_iff
{F : Type u_1}
[field F]
{E : Type u_2}
[field E]
[algebra F E]
{K : intermediate_field F E} :
@[simp]
theorem
intermediate_field.dim_bot
{F : Type u_1}
[field F]
{E : Type u_2}
[field E]
[algebra F E] :
module.rank F ↥⊥ = 1
@[simp]
theorem
intermediate_field.finrank_bot
{F : Type u_1}
[field F]
{E : Type u_2}
[field E]
[algebra F E] :
theorem
intermediate_field.dim_adjoin_eq_one_iff
{F : Type u_1}
[field F]
{E : Type u_2}
[field E]
[algebra F E]
{S : set E} :
module.rank F ↥(intermediate_field.adjoin F S) = 1 ↔ S ⊆ ↑⊥
theorem
intermediate_field.finrank_adjoin_eq_one_iff
{F : Type u_1}
[field F]
{E : Type u_2}
[field E]
[algebra F E]
{S : set E} :
finite_dimensional.finrank F ↥(intermediate_field.adjoin F S) = 1 ↔ S ⊆ ↑⊥
theorem
intermediate_field.subsingleton_of_dim_adjoin_eq_one
{F : Type u_1}
[field F]
{E : Type u_2}
[field E]
[algebra F E]
(h : ∀ (x : E), module.rank F ↥F⟮x⟯ = 1) :
theorem
intermediate_field.subsingleton_of_finrank_adjoin_eq_one
{F : Type u_1}
[field F]
{E : Type u_2}
[field E]
[algebra F E]
(h : ∀ (x : E), finite_dimensional.finrank F ↥F⟮x⟯ = 1) :
theorem
intermediate_field.bot_eq_top_of_finrank_adjoin_le_one
{F : Type u_1}
[field F]
{E : Type u_2}
[field E]
[algebra F E]
[finite_dimensional F E]
(h : ∀ (x : E), finite_dimensional.finrank F ↥F⟮x⟯ ≤ 1) :
If F⟮x⟯ has dimension ≤1 over F for every x ∈ E then F = E.
theorem
intermediate_field.subsingleton_of_finrank_adjoin_le_one
{F : Type u_1}
[field F]
{E : Type u_2}
[field E]
[algebra F E]
[finite_dimensional F E]
(h : ∀ (x : E), finite_dimensional.finrank F ↥F⟮x⟯ ≤ 1) :
theorem
intermediate_field.minpoly_gen
{F : Type u_1}
[field F]
{E : Type u_2}
[field E]
[algebra F E]
{α : E}
(h : is_integral F α) :
minpoly F (intermediate_field.adjoin_simple.gen F α) = minpoly F α
theorem
intermediate_field.aeval_gen_minpoly
(F : Type u_1)
[field F]
{E : Type u_2}
[field E]
[algebra F E]
(α : E) :
⇑(polynomial.aeval (intermediate_field.adjoin_simple.gen F α)) (minpoly F α) = 0
noncomputable
def
intermediate_field.adjoin_root_equiv_adjoin
(F : Type u_1)
[field F]
{E : Type u_2}
[field E]
[algebra F E]
{α : E}
(h : is_integral F α) :
algebra isomorphism between adjoin_root and F⟮α⟯
Equations
theorem
intermediate_field.adjoin_root_equiv_adjoin_apply_root
(F : Type u_1)
[field F]
{E : Type u_2}
[field E]
[algebra F E]
{α : E}
(h : is_integral F α) :
noncomputable
def
intermediate_field.power_basis_aux
{K : Type u_3}
[field K]
{L : Type u_4}
[field L]
[algebra K L]
{x : L}
(hx : is_integral K x) :
The elements 1, x, ..., x ^ (d - 1) form a basis for K⟮x⟯,
where d is the degree of the minimal polynomial of x.
@[simp]
theorem
intermediate_field.adjoin.power_basis_dim
{K : Type u_3}
[field K]
{L : Type u_4}
[field L]
[algebra K L]
{x : L}
(hx : is_integral K x) :
(intermediate_field.adjoin.power_basis hx).dim = (minpoly K x).nat_degree
noncomputable
def
intermediate_field.adjoin.power_basis
{K : Type u_3}
[field K]
{L : Type u_4}
[field L]
[algebra K L]
{x : L}
(hx : is_integral K x) :
power_basis K ↥K⟮x⟯
The power basis 1, x, ..., x ^ (d - 1) for K⟮x⟯,
where d is the degree of the minimal polynomial of x.
Equations
- intermediate_field.adjoin.power_basis hx = {gen := intermediate_field.adjoin_simple.gen K x, dim := (minpoly K x).nat_degree, basis := intermediate_field.power_basis_aux hx, basis_eq_pow := _}
@[simp]
theorem
intermediate_field.adjoin.power_basis_gen
{K : Type u_3}
[field K]
{L : Type u_4}
[field L]
[algebra K L]
{x : L}
(hx : is_integral K x) :
theorem
intermediate_field.adjoin.finite_dimensional
{K : Type u_3}
[field K]
{L : Type u_4}
[field L]
[algebra K L]
{x : L}
(hx : is_integral K x) :
theorem
intermediate_field.adjoin.finrank
{K : Type u_3}
[field K]
{L : Type u_4}
[field L]
[algebra K L]
{x : L}
(hx : is_integral K x) :
finite_dimensional.finrank K ↥K⟮x⟯ = (minpoly K x).nat_degree
noncomputable
def
intermediate_field.alg_hom_adjoin_integral_equiv
(F : Type u_1)
[field F]
{E : Type u_2}
[field E]
[algebra F E]
{α : E}
{K : Type u_3}
[field K]
[algebra F K]
(h : is_integral F α) :
Algebra homomorphism F⟮α⟯ →ₐ[F] K are in bijection with the set of roots
of minpoly α in K.
Equations
noncomputable
def
intermediate_field.fintype_of_alg_hom_adjoin_integral
(F : Type u_1)
[field F]
{E : Type u_2}
[field E]
[algebra F E]
{α : E}
{K : Type u_3}
[field K]
[algebra F K]
(h : is_integral F α) :
Fintype of algebra homomorphism F⟮α⟯ →ₐ[F] K
theorem
intermediate_field.card_alg_hom_adjoin_integral
(F : Type u_1)
[field F]
{E : Type u_2}
[field E]
[algebra F E]
{α : E}
{K : Type u_3}
[field K]
[algebra F K]
(h : is_integral F α)
(h_sep : (minpoly F α).separable)
(h_splits : polynomial.splits (algebra_map F K) (minpoly F α)) :
fintype.card (↥F⟮α⟯ →ₐ[F] K) = (minpoly F α).nat_degree
def
intermediate_field.fg
{F : Type u_1}
[field F]
{E : Type u_2}
[field E]
[algebra F E]
(S : intermediate_field F E) :
Prop
An intermediate field S is finitely generated if there exists t : finset E such that
intermediate_field.adjoin F t = S.
theorem
intermediate_field.fg_adjoin_finset
{F : Type u_1}
[field F]
{E : Type u_2}
[field E]
[algebra F E]
(t : finset E) :
(intermediate_field.adjoin F ↑t).fg
theorem
intermediate_field.fg_def
{F : Type u_1}
[field F]
{E : Type u_2}
[field E]
[algebra F E]
{S : intermediate_field F E} :
theorem
intermediate_field.fg_of_fg_to_subalgebra
{F : Type u_1}
[field F]
{E : Type u_2}
[field E]
[algebra F E]
(S : intermediate_field F E)
(h : S.to_subalgebra.fg) :
S.fg
theorem
intermediate_field.fg_of_noetherian
{F : Type u_1}
[field F]
{E : Type u_2}
[field E]
[algebra F E]
(S : intermediate_field F E)
[is_noetherian F E] :
S.fg
theorem
intermediate_field.induction_on_adjoin_finset
{F : Type u_1}
[field F]
{E : Type u_2}
[field E]
[algebra F E]
(S : finset E)
(P : intermediate_field F E → Prop)
(base : P ⊥)
(ih : ∀ (K : intermediate_field F E) (x : E), x ∈ S → P K → P ↑(↥K)⟮x⟯) :
P (intermediate_field.adjoin F ↑S)
theorem
intermediate_field.induction_on_adjoin_fg
{F : Type u_1}
[field F]
{E : Type u_2}
[field E]
[algebra F E]
(P : intermediate_field F E → Prop)
(base : P ⊥)
(ih : ∀ (K : intermediate_field F E) (x : E), P K → P ↑(↥K)⟮x⟯)
(K : intermediate_field F E)
(hK : K.fg) :
P K
theorem
intermediate_field.induction_on_adjoin
{F : Type u_1}
[field F]
{E : Type u_2}
[field E]
[algebra F E]
[fd : finite_dimensional F E]
(P : intermediate_field F E → Prop)
(base : P ⊥)
(ih : ∀ (K : intermediate_field F E) (x : E), P K → P ↑(↥K)⟮x⟯)
(K : intermediate_field F E) :
P K
def
intermediate_field.lifts
(F : Type u_1)
(E : Type u_2)
(K : Type u_3)
[field F]
[field E]
[field K]
[algebra F E]
[algebra F K] :
Type (max u_2 u_3)
Lifts L → K of F → K
Equations
- intermediate_field.lifts F E K = Σ (L : intermediate_field F E), ↥L →ₐ[F] K
@[protected, instance]
def
intermediate_field.lifts.partial_order
{F : Type u_1}
{E : Type u_2}
{K : Type u_3}
[field F]
[field E]
[field K]
[algebra F E]
[algebra F K] :
Equations
- intermediate_field.lifts.partial_order = {le := λ (x y : intermediate_field.lifts F E K), x.fst ≤ y.fst ∧ ∀ (s : ↥(x.fst)) (t : ↥(y.fst)), ↑s = ↑t → ⇑(x.snd) s = ⇑(y.snd) t, lt := preorder.lt._default (λ (x y : intermediate_field.lifts F E K), x.fst ≤ y.fst ∧ ∀ (s : ↥(x.fst)) (t : ↥(y.fst)), ↑s = ↑t → ⇑(x.snd) s = ⇑(y.snd) t), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _}
@[protected, instance]
noncomputable
def
intermediate_field.lifts.order_bot
{F : Type u_1}
{E : Type u_2}
{K : Type u_3}
[field F]
[field E]
[field K]
[algebra F E]
[algebra F K] :
order_bot (intermediate_field.lifts F E K)
Equations
- intermediate_field.lifts.order_bot = {bot := ⟨⊥, (algebra.of_id F K).comp (intermediate_field.bot_equiv F E).to_alg_hom⟩, bot_le := _}
@[protected, instance]
noncomputable
def
intermediate_field.lifts.inhabited
{F : Type u_1}
{E : Type u_2}
{K : Type u_3}
[field F]
[field E]
[field K]
[algebra F E]
[algebra F K] :
inhabited (intermediate_field.lifts F E K)
Equations
theorem
intermediate_field.lifts.exists_max_two
{F : Type u_1}
{E : Type u_2}
{K : Type u_3}
[field F]
[field E]
[field K]
[algebra F E]
[algebra F K]
{c : set (intermediate_field.lifts F E K)}
{x y : intermediate_field.lifts F E K}
(hc : is_chain has_le.le c)
(hx : x ∈ set.insert ⊥ c)
(hy : y ∈ set.insert ⊥ c) :
∃ (z : intermediate_field.lifts F E K), z ∈ set.insert ⊥ c ∧ x ≤ z ∧ y ≤ z
theorem
intermediate_field.lifts.exists_max_three
{F : Type u_1}
{E : Type u_2}
{K : Type u_3}
[field F]
[field E]
[field K]
[algebra F E]
[algebra F K]
{c : set (intermediate_field.lifts F E K)}
{x y z : intermediate_field.lifts F E K}
(hc : is_chain has_le.le c)
(hx : x ∈ set.insert ⊥ c)
(hy : y ∈ set.insert ⊥ c)
(hz : z ∈ set.insert ⊥ c) :
∃ (w : intermediate_field.lifts F E K), w ∈ set.insert ⊥ c ∧ x ≤ w ∧ y ≤ w ∧ z ≤ w
def
intermediate_field.lifts.upper_bound_intermediate_field
{F : Type u_1}
{E : Type u_2}
{K : Type u_3}
[field F]
[field E]
[field K]
[algebra F E]
[algebra F K]
{c : set (intermediate_field.lifts F E K)}
(hc : is_chain has_le.le c) :
An upper bound on a chain of lifts
Equations
- intermediate_field.lifts.upper_bound_intermediate_field hc = {to_subalgebra := {carrier := λ (s : E), ∃ (x : intermediate_field.lifts F E K), x ∈ set.insert ⊥ c ∧ s ∈ x.fst, mul_mem' := _, one_mem' := _, add_mem' := _, zero_mem' := _, algebra_map_mem' := _}, neg_mem' := _, inv_mem' := _}
noncomputable
def
intermediate_field.lifts.upper_bound_alg_hom
{F : Type u_1}
{E : Type u_2}
{K : Type u_3}
[field F]
[field E]
[field K]
[algebra F E]
[algebra F K]
{c : set (intermediate_field.lifts F E K)}
(hc : is_chain has_le.le c) :
The lift on the upper bound on a chain of lifts
noncomputable
def
intermediate_field.lifts.upper_bound
{F : Type u_1}
{E : Type u_2}
{K : Type u_3}
[field F]
[field E]
[field K]
[algebra F E]
[algebra F K]
{c : set (intermediate_field.lifts F E K)}
(hc : is_chain has_le.le c) :
intermediate_field.lifts F E K
An upper bound on a chain of lifts
theorem
intermediate_field.lifts.exists_upper_bound
{F : Type u_1}
{E : Type u_2}
{K : Type u_3}
[field F]
[field E]
[field K]
[algebra F E]
[algebra F K]
(c : set (intermediate_field.lifts F E K))
(hc : is_chain has_le.le c) :
∃ (ub : intermediate_field.lifts F E K), ∀ (a : intermediate_field.lifts F E K), a ∈ c → a ≤ ub
noncomputable
def
intermediate_field.lifts.lift_of_splits
{F : Type u_1}
{E : Type u_2}
{K : Type u_3}
[field F]
[field E]
[field K]
[algebra F E]
[algebra F K]
(x : intermediate_field.lifts F E K)
{s : E}
(h1 : is_integral F s)
(h2 : polynomial.splits (algebra_map F K) (minpoly F s)) :
intermediate_field.lifts F E K
Extend a lift x : lifts F E K to an element s : E whose conjugates are all in K
Equations
- x.lift_of_splits h1 h2 = let h3 : is_integral ↥(x.fst) s := _, key : polynomial.splits (alg_hom.to_ring_hom x.snd) (minpoly ↥(x.fst) s) := _ in ⟨↑(↥(x.fst))⟮s⟯, alg_hom_equiv_sigma.inv_fun ⟨x.snd, (intermediate_field.alg_hom_adjoin_integral_equiv ↥(x.fst) h3).inv_fun ⟨polynomial.root_of_splits (alg_hom.to_ring_hom x.snd) key _, _⟩⟩⟩
theorem
intermediate_field.lifts.le_lifts_of_splits
{F : Type u_1}
{E : Type u_2}
{K : Type u_3}
[field F]
[field E]
[field K]
[algebra F E]
[algebra F K]
(x : intermediate_field.lifts F E K)
{s : E}
(h1 : is_integral F s)
(h2 : polynomial.splits (algebra_map F K) (minpoly F s)) :
x ≤ x.lift_of_splits h1 h2
theorem
intermediate_field.lifts.mem_lifts_of_splits
{F : Type u_1}
{E : Type u_2}
{K : Type u_3}
[field F]
[field E]
[field K]
[algebra F E]
[algebra F K]
(x : intermediate_field.lifts F E K)
{s : E}
(h1 : is_integral F s)
(h2 : polynomial.splits (algebra_map F K) (minpoly F s)) :
s ∈ (x.lift_of_splits h1 h2).fst
theorem
intermediate_field.lifts.exists_lift_of_splits
{F : Type u_1}
{E : Type u_2}
{K : Type u_3}
[field F]
[field E]
[field K]
[algebra F E]
[algebra F K]
(x : intermediate_field.lifts F E K)
{s : E}
(h1 : is_integral F s)
(h2 : polynomial.splits (algebra_map F K) (minpoly F s)) :
∃ (y : intermediate_field.lifts F E K), x ≤ y ∧ s ∈ y.fst
theorem
intermediate_field.alg_hom_mk_adjoin_splits
{F : Type u_1}
{E : Type u_2}
{K : Type u_3}
[field F]
[field E]
[field K]
[algebra F E]
[algebra F K]
{S : set E}
(hK : ∀ (s : E), s ∈ S → is_integral F s ∧ polynomial.splits (algebra_map F K) (minpoly F s)) :
nonempty (↥(intermediate_field.adjoin F S) →ₐ[F] K)
theorem
intermediate_field.alg_hom_mk_adjoin_splits'
{F : Type u_1}
{E : Type u_2}
{K : Type u_3}
[field F]
[field E]
[field K]
[algebra F E]
[algebra F K]
{S : set E}
(hS : intermediate_field.adjoin F S = ⊤)
(hK : ∀ (x : E), x ∈ S → is_integral F x ∧ polynomial.splits (algebra_map F K) (minpoly F x)) :
theorem
intermediate_field.le_sup_to_subalgebra
{K : Type u_1}
{L : Type u_2}
[field K]
[field L]
[algebra K L]
(E1 E2 : intermediate_field K L) :
E1.to_subalgebra ⊔ E2.to_subalgebra ≤ (E1 ⊔ E2).to_subalgebra
theorem
intermediate_field.sup_to_subalgebra
{K : Type u_1}
{L : Type u_2}
[field K]
[field L]
[algebra K L]
(E1 E2 : intermediate_field K L)
[h1 : finite_dimensional K ↥E1]
[h2 : finite_dimensional K ↥E2] :
(E1 ⊔ E2).to_subalgebra = E1.to_subalgebra ⊔ E2.to_subalgebra
theorem
intermediate_field.finite_dimensional_sup
{K : Type u_1}
{L : Type u_2}
[field K]
[field L]
[algebra K L]
(E1 E2 : intermediate_field K L)
[h1 : finite_dimensional K ↥E1]
[h2 : finite_dimensional K ↥E2] :
finite_dimensional K ↥(E1 ⊔ E2)
noncomputable
def
power_basis.equiv_adjoin_simple
{K : Type u_1}
{L : Type u_2}
[field K]
[field L]
[algebra K L]
(pb : power_basis K L) :
pb.equiv_adjoin_simple is the equivalence between K⟮pb.gen⟯ and L itself.
Equations
@[simp]
theorem
power_basis.equiv_adjoin_simple_aeval
{K : Type u_1}
{L : Type u_2}
[field K]
[field L]
[algebra K L]
(pb : power_basis K L)
(f : K[X]) :
⇑(pb.equiv_adjoin_simple) (⇑(polynomial.aeval (intermediate_field.adjoin_simple.gen K pb.gen)) f) = ⇑(polynomial.aeval pb.gen) f
@[simp]
theorem
power_basis.equiv_adjoin_simple_gen
{K : Type u_1}
{L : Type u_2}
[field K]
[field L]
[algebra K L]
(pb : power_basis K L) :
⇑(pb.equiv_adjoin_simple) (intermediate_field.adjoin_simple.gen K pb.gen) = pb.gen
@[simp]
theorem
power_basis.equiv_adjoin_simple_symm_aeval
{K : Type u_1}
{L : Type u_2}
[field K]
[field L]
[algebra K L]
(pb : power_basis K L)
(f : K[X]) :
⇑(pb.equiv_adjoin_simple.symm) (⇑(polynomial.aeval pb.gen) f) = ⇑(polynomial.aeval (intermediate_field.adjoin_simple.gen K pb.gen)) f
@[simp]
theorem
power_basis.equiv_adjoin_simple_symm_gen
{K : Type u_1}
{L : Type u_2}
[field K]
[field L]
[algebra K L]
(pb : power_basis K L) :
⇑(pb.equiv_adjoin_simple.symm) pb.gen = intermediate_field.adjoin_simple.gen K pb.gen