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_rank_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' := _}
Instances for ↥intermediate_field.adjoin
@[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.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.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, norm_cast]
theorem
intermediate_field.coe_Inf
{F : Type u_1}
[field F]
{E : Type u_2}
[field E]
[algebra F E]
(S : set (intermediate_field F E)) :
↑(has_Inf.Inf S) = has_Inf.Inf (coe '' S)
@[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)) :
@[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) :
@[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
@[simp]
theorem
intermediate_field.bot_equiv_symm
{F : Type u_1}
[field F]
{E : Type u_2}
[field E]
[algebra F E]
(x : F) :
⇑((intermediate_field.bot_equiv F E).symm) x = ⇑(algebra_map F ↥⊥) x
theorem
intermediate_field.coe_algebra_map_over_bot
{F : Type u_1}
[field F]
{E : Type u_2}
[field E]
[algebra F E] :
⇑(algebra_map ↥⊥ F) = ⇑(intermediate_field.bot_equiv 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.restrict_scalars_bot_eq_self
{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.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_map
(F : Type u_1)
[field F]
{E : Type u_2}
[field E]
[algebra F E]
(S : set E)
{E' : Type u_3}
[field E']
[algebra F E']
(f : E →ₐ[F] E') :
intermediate_field.map f (intermediate_field.adjoin F S) = intermediate_field.adjoin F (⇑f '' S)
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]
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.
Instances of this typeclass
Instances of other typeclasses for intermediate_field.insert
- intermediate_field.insert.has_sizeof_inst
@[protected, instance]
Equations
- intermediate_field.insert_empty = {insert := λ (x : α), {x}}
@[protected, instance]
Equations
- intermediate_field.insert_nonempty s = {insert := λ (x : α), has_insert.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 {α}
theorem
intermediate_field.is_splitting_field_iff
{F : Type u_1}
[field F]
{E : Type u_2}
[field E]
[algebra F E]
{p : polynomial F}
{K : intermediate_field F E} :
polynomial.is_splitting_field F ↥K p ↔ polynomial.splits (algebra_map F ↥K) p ∧ K = intermediate_field.adjoin F (p.root_set E)
theorem
intermediate_field.adjoin_root_set_is_splitting_field
{F : Type u_1}
[field F]
{E : Type u_2}
[field E]
[algebra F E]
{p : polynomial F}
(hp : polynomial.splits (algebra_map F E) p) :
polynomial.is_splitting_field F ↥(intermediate_field.adjoin F (p.root_set E)) p
theorem
intermediate_field.is_splitting_field_supr
{F : Type u_1}
[field F]
{E : Type u_2}
[field E]
[algebra F E]
{ι : Type u_3}
{t : ι → intermediate_field F E}
{p : ι → polynomial F}
{s : finset ι}
(h0 : s.prod (λ (i : ι), p i) ≠ 0)
(h : ∀ (i : ι), i ∈ s → polynomial.is_splitting_field F ↥(t i) (p i)) :
A compositum of splitting fields is a splitting field
theorem
intermediate_field.exists_finset_of_mem_supr''
{F : Type u_1}
[field F]
{E : Type u_2}
[field E]
[algebra F E]
{ι : Type u_3}
{f : ι → intermediate_field F E}
(h : ∀ (i : ι), algebra.is_algebraic F ↥(f i))
{x : E}
(hx : x ∈ ⨆ (i : ι), f i) :
@[simp]
theorem
intermediate_field.rank_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} :
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
theorem
minpoly.nat_degree_le
{K : Type u_3}
[field K]
{L : Type u_4}
[field L]
[algebra K L]
{x : L}
[finite_dimensional K L]
(hx : is_integral K x) :
(minpoly K x).nat_degree ≤ finite_dimensional.finrank K L
theorem
minpoly.degree_le
{K : Type u_3}
[field K]
{L : Type u_4}
[field L]
[algebra K L]
{x : L}
[finite_dimensional K L]
(hx : is_integral K x) :
(minpoly K x).degree ≤ ↑(finite_dimensional.finrank K L)
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_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 (intermediate_field.restrict_scalars F (↥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 (intermediate_field.restrict_scalars F (↥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 (intermediate_field.restrict_scalars F (↥K)⟮x⟯))
(K : intermediate_field F E) :
P 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 := _}
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 ∈ has_insert.insert ⊥ c)
(hy : y ∈ has_insert.insert ⊥ c) :
∃ (z : intermediate_field.lifts F E K), z ∈ has_insert.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 ∈ has_insert.insert ⊥ c)
(hy : y ∈ has_insert.insert ⊥ c)
(hz : z ∈ has_insert.insert ⊥ c) :
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 ∈ has_insert.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
{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 ⟨intermediate_field.restrict_scalars F (↥(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)) :
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
@[protected, instance]
def
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)
@[protected, instance]
def
intermediate_field.finite_dimensional_supr_of_finite
{K : Type u_1}
{L : Type u_2}
[field K]
[field L]
[algebra K L]
{ι : Type u_3}
{t : ι → intermediate_field K L}
[h : finite ι]
[∀ (i : ι), finite_dimensional K ↥(t i)] :
finite_dimensional K (↥⨆ (i : ι), t i)
@[protected, instance]
def
intermediate_field.finite_dimensional_supr_of_finset
{K : Type u_1}
{L : Type u_2}
[field K]
[field L]
[algebra K L]
{ι : Type u_3}
{f : ι → intermediate_field K L}
{s : finset ι}
[h : ∀ (i : ι), i ∈ s → finite_dimensional K ↥(f i)] :
finite_dimensional K (↥⨆ (i : ι) (H : i ∈ s), f i)
theorem
intermediate_field.is_algebraic_supr
{K : Type u_1}
{L : Type u_2}
[field K]
[field L]
[algebra K L]
{ι : Type u_3}
{f : ι → intermediate_field K L}
(h : ∀ (i : ι), algebra.is_algebraic K ↥(f i)) :
algebra.is_algebraic K (↥⨆ (i : ι), f i)
A compositum of algebraic extensions is algebraic
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 : polynomial K) :
⇑(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 : polynomial K) :
⇑(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