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 adjoining S ∪ T.bot_eq_top_of_dim_adjoin_eq_one: ifF⟮x⟯has dimension1overFfor everyxinEthenF = E
Notation
F⟮α⟯: adjoin a single elementαtoF.
def
field.adjoin
(F : Type u_1)
[field F]
{E : Type u_2}
[field E]
[algebra F E]
(S : set E) :
subalgebra F E
adjoin F S extends a field F by adjoining a set S ⊆ E.
Equations
- field.adjoin F S = {carrier := field.closure (set.range ⇑(algebra_map F E) ∪ S), one_mem' := _, mul_mem' := _, zero_mem' := _, add_mem' := _, algebra_map_mem' := _}
theorem
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) :
↑(field.adjoin F S) = set.range ⇑(algebra_map ↥(field.adjoin F S) E)
theorem
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 ∈ field.adjoin F S
theorem
field.subset_adjoin_of_subset_left
{E : Type u_2}
[field E]
(S : set E)
{F : set E}
{HF : is_subfield F}
{T : set E}
(HT : T ⊆ F) :
T ⊆ ↑(field.adjoin ↥F S)
theorem
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) ⊆ ↑(field.adjoin F S)
@[instance]
def
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 ↥(field.adjoin F S)
Equations
- field.adjoin.field_coe F S = {coe := λ (x : F), ⟨⇑(algebra_map F E) x, _⟩}
theorem
field.subset_adjoin
(F : Type u_1)
[field F]
{E : Type u_2}
[field E]
[algebra F E]
(S : set E) :
S ⊆ ↑(field.adjoin F S)
theorem
field.adjoin.mono
(F : Type u_1)
[field F]
{E : Type u_2}
[field E]
[algebra F E]
(S T : set E)
(h : S ⊆ T) :
↑(field.adjoin F S) ⊆ ↑(field.adjoin F T)
@[instance]
def
field.adjoin.is_subfield
(F : Type u_1)
[field F]
{E : Type u_2}
[field E]
[algebra F E]
(S : set E) :
is_subfield ↑(field.adjoin F S)
@[instance]
def
field.adjoin.is_field
(F : Type u_1)
[field F]
{E : Type u_2}
[field E]
[algebra F E]
(S : set E) :
field ↥(field.adjoin F S)
Equations
- field.adjoin.is_field F S = is_subfield.field ↑(field.adjoin F S)
theorem
field.adjoin_contains_field_as_subfield
{E : Type u_2}
[field E]
(S F : set E)
{HF : is_subfield F} :
F ⊆ ↑(field.adjoin ↥F S)
theorem
field.adjoin_subset_subfield
(F : Type u_1)
[field F]
{E : Type u_2}
[field E]
[algebra F E]
(S : set E)
{K : set E}
[is_subfield K]
(HF : set.range ⇑(algebra_map F E) ⊆ K)
(HS : S ⊆ K) :
↑(field.adjoin F S) ⊆ K
If K is a field with F ⊆ K and S ⊆ K then adjoin F S ⊆ K.
theorem
field.adjoin_subset_iff
(F : Type u_1)
[field F]
{E : Type u_2}
[field E]
[algebra F E]
(S : set E)
{T : set E} :
S ⊆ ↑(field.adjoin F T) ↔ ↑(field.adjoin F S) ⊆ ↑(field.adjoin F T)
S ⊆ adjoin F T if and only if adjoin F S ⊆ adjoin F T.
theorem
field.subfield_subset_adjoin_self
{E : Type u_2}
[field E]
(S : set E)
{F : set E}
{HF : is_subfield F}
{T : set E}
{HT : T ⊆ F} :
T ⊆ ↑(field.adjoin ↥F S)
theorem
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} :
↑(field.adjoin F S) ⊆ ↑(field.adjoin F' S') ↔ set.range ⇑(algebra_map F E) ⊆ ↑(field.adjoin F' S') ∧ S ⊆ ↑(field.adjoin F' S')
theorem
field.adjoin_adjoin_left
(F : Type u_1)
[field F]
{E : Type u_2}
[field E]
[algebra F E]
(S T : set E) :
↑(field.adjoin ↥↑(field.adjoin F S) T) = ↑(field.adjoin F (S ∪ T))
F[S][T] = F[S ∪ T]
theorem
field.adjoin_adjoin_comm
(F : Type u_1)
[field F]
{E : Type u_2}
[field E]
[algebra F E]
(S T : set E) :
↑(field.adjoin ↥↑(field.adjoin F S) T) = ↑(field.adjoin ↥↑(field.adjoin F T) S)
F[S][T] = F[T][S]
@[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.
Instances
@[instance]
Equations
- field.insert_empty = {insert := λ (x : α), {x}}
@[instance]
Equations
- field.insert_nonempty s = {insert := λ (x : α), set.insert x s}
@[simp]
theorem
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) (field.adjoin_simple.gen F α) = α
theorem
field.sub_bot_of_adjoin_dim_eq_one
{F : Type u_1}
[field F]
{E : Type u_2}
[field E]
[algebra F E]
{S : set E}
(h : vector_space.dim F ↥(field.adjoin F S) = 1) :
theorem
field.adjoin_dim_eq_one_of_sub_bot
{F : Type u_1}
[field F]
{E : Type u_2}
[field E]
[algebra F E]
{S : set E}
(h : S ⊆ ↑⊥) :
vector_space.dim F ↥(field.adjoin F S) = 1
theorem
field.adjoin_dim_eq_one_iff
{F : Type u_1}
[field F]
{E : Type u_2}
[field E]
[algebra F E]
{S : set E} :
vector_space.dim F ↥(field.adjoin F S) = 1 ↔ S ⊆ ↑⊥
theorem
field.adjoin_findim_eq_one_iff
{F : Type u_1}
[field F]
{E : Type u_2}
[field E]
[algebra F E]
{S : set E} :
finite_dimensional.findim F ↥(field.adjoin F S) = 1 ↔ S ⊆ ↑⊥
theorem
field.bot_eq_top_of_findim_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.findim F ↥F⟮x⟯ ≤ 1) :
If F⟮x⟯ has dimension ≤1 over F for every x ∈ E then F = E.