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 dimension1
overF
for everyx
inE
thenF = E
Notation
F⟮α⟯
: adjoin a single elementα
toF
.
adjoin F S
extends a field F
by adjoining a set S ⊆ E
.
Equations
- intermediate_field.adjoin F S = {carrier := (subfield.closure (set.range ⇑(algebra_map F E) ∪ S)).carrier, one_mem' := _, mul_mem' := _, zero_mem' := _, add_mem' := _, algebra_map_mem' := _, neg_mem' := _, inv_mem' := _}
Galois insertion between adjoin
and coe
.
Equations
- intermediate_field.gi = {choice := λ (S : set E) (_x : ↑(intermediate_field.adjoin F S) ≤ S), intermediate_field.adjoin F S, gc := _, le_l_u := _, choice_eq := _}
Equations
Construct an algebra isomorphism from an equality of subalgebras
The bottom intermediate_field is isomorphic to the field.
The top intermediate_field is isomorphic to the field.
Equations
- intermediate_field.adjoin.field_coe F S = {coe := λ (x : F), ⟨⇑(algebra_map F E) x, _⟩}
If K
is a field with F ⊆ K
and S ⊆ K
then adjoin F S ≤ K
.
F[S][T] = F[S ∪ T]
F[S][T] = F[T][S]
- 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.
Equations
- intermediate_field.insert_empty = {insert := λ (x : α), {x}}
Equations
- intermediate_field.insert_nonempty s = {insert := λ (x : α), set.insert x s}
If F⟮x⟯
has dimension ≤1
over F
for every x ∈ E
then F = E
.
algebra isomorphism between adjoin_root
and F⟮α⟯
Equations
- intermediate_field.adjoin_root_equiv_adjoin F h = alg_equiv.of_bijective {to_fun := ⇑(adjoin_root.lift (algebra_map F ↥F⟮α⟯) (intermediate_field.adjoin_simple.gen F α) _), map_one' := _, map_mul' := _, map_zero' := _, map_add' := _, commutes' := _} _
Algebra homomorphism F⟮α⟯ →ₐ[F] K
are in bijection with the set of roots
of minpoly α
in K
.
Equations
- intermediate_field.alg_hom_adjoin_integral_equiv F h = let ϕ : adjoin_root (minpoly F α) ≃ₐ[F] ↥F⟮α⟯ := intermediate_field.adjoin_root_equiv_adjoin F h, swap1 : (↥F⟮α⟯ →ₐ[F] K) ≃ (adjoin_root (minpoly F α) →ₐ[F] K) := {to_fun := λ (f : ↥F⟮α⟯ →ₐ[F] K), f.comp ϕ.to_alg_hom, inv_fun := λ (f : adjoin_root (minpoly F α) →ₐ[F] K), f.comp ϕ.symm.to_alg_hom, left_inv := _, right_inv := _}, swap2 : (adjoin_root (minpoly F α) →ₐ[F] K) ≃ {x // x ∈ (polynomial.map (algebra_map F K) (minpoly F α)).roots} := adjoin_root.equiv F K (minpoly F α) _ in swap1.trans swap2
Fintype of algebra homomorphism F⟮α⟯ →ₐ[F] K
Equations
- intermediate_field.fintype_of_alg_hom_adjoin_integral F h = fintype.of_equiv {x // x ∈ (polynomial.map (algebra_map F K) (minpoly F α)).roots} (intermediate_field.alg_hom_adjoin_integral_equiv F h).symm
An intermediate field S
is finitely generated if there exists t : finset E
such that
intermediate_field.adjoin F t = S
.
Lifts L → K
of F → K
Equations
- intermediate_field.lifts F E K = Σ (L : intermediate_field F E), ↥L →ₐ[F] K
Equations
- intermediate_field.lifts.order_bot = {bot := ⟨⊥, (algebra.of_id F K).comp intermediate_field.bot_equiv.to_alg_hom⟩, 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 := partial_order.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 := _, bot_le := _}
Equations
An upper bound on a chain of lifts
Equations
- intermediate_field.lifts.upper_bound_intermediate_field hc = {carrier := λ (s : E), ∃ (x : intermediate_field.lifts F E K), x ∈ set.insert ⊥ c ∧ s ∈ x.fst, one_mem' := _, mul_mem' := _, zero_mem' := _, add_mem' := _, algebra_map_mem' := _, neg_mem' := _, inv_mem' := _}
The lift on the upper bound on a chain of lifts
An upper bound on a chain of lifts
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 _, _⟩⟩⟩