mathlib documentation

field_theory.adjoin

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

Notation

def intermediate_field.adjoin (F : Type u_1) [field F] {E : Type u_2} [field E] [algebra F E] :

adjoin F S extends a field F by adjoining a set S ⊆ E.

Equations
@[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} :

theorem intermediate_field.gc {F : Type u_1} [field F] {E : Type u_2} [field E] [algebra F E] :

def intermediate_field.gi {F : Type u_1} [field F] {E : Type u_2} [field E] [algebra F E] :

Galois insertion between adjoin and coe.

Equations
@[instance]
def intermediate_field.inhabited {F : Type u_1} [field F] {E : Type u_2} [field E] [algebra F E] :

Equations
theorem intermediate_field.mem_bot {F : Type u_1} [field F] {E : Type u_2} [field E] [algebra F E] {x : E} :

theorem intermediate_field.mem_top {F : Type u_1} [field F] {E : Type u_2} [field E] [algebra F E] {x : E} :

@[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.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.algebra_map_mem (F : Type u_1) [field F] {E : Type u_2} [field E] [algebra F E] (S : set E) (x : F) :

@[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) :

Equations
theorem intermediate_field.subset_adjoin (F : Type u_1) [field F] {E : Type u_2} [field E] [algebra F E] (S : set E) :

@[instance]
def intermediate_field.adjoin.set_coe (F : Type u_1) [field F] {E : Type u_2} [field E] [algebra F E] (S : set E) :

Equations
theorem intermediate_field.adjoin.mono (F : Type u_1) [field F] {E : Type u_2} [field E] [algebra F E] (S T : set E) :

theorem intermediate_field.subset_adjoin_of_subset_left {E : Type u_2} [field E] (S : set E) {F : subfield E} {T : set E} :

theorem intermediate_field.subset_adjoin_of_subset_right (F : Type u_1) [field F] {E : Type u_2} [field E] [algebra F E] (S : set E) {T : set E} :

@[simp]
theorem intermediate_field.adjoin_empty (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} :

If K is a field with F ⊆ K and S ⊆ K then adjoin F S ≤ K.

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) :

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') :

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) :

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) :

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} :
x intermediate_field.adjoin F s(∀ (x : E), x sp x)(∀ (x : F), p ((algebra_map F E) x))(∀ (x y : E), p xp yp (x + y))(∀ (x : E), p xp (-x))(∀ (x : E), p xp x⁻¹)(∀ (x y : E), p xp yp (x * y))p x

@[class]
structure intermediate_field.insert {α : Type u_3} :
set αType u_3
  • 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
@[instance]

Equations
theorem intermediate_field.mem_adjoin_simple_self (F : Type u_1) [field F] {E : Type u_2} [field E] [algebra F E] (α : E) :
α Fα

def intermediate_field.adjoin_simple.gen (F : Type u_1) [field F] {E : Type u_2} [field E] [algebra F E] (α : E) :

generator of F⟮α⟯

Equations
@[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) :

theorem intermediate_field.adjoin_simple_adjoin_simple (F : Type u_1) [field F] {E : Type u_2} [field E] [algebra F E] (α β : E) :

theorem intermediate_field.adjoin_simple_comm (F : Type u_1) [field F] {E : Type u_2} [field E] [algebra F E] (α β : E) :

@[simp]
theorem intermediate_field.adjoin_eq_bot_iff {F : Type u_1} [field F] {E : Type u_2} [field E] [algebra F E] {S : set E} :

@[simp]
theorem intermediate_field.adjoin_simple_eq_bot_iff {F : Type u_1} [field F] {E : Type u_2} [field E] [algebra F E] {α : E} :

@[simp]
theorem intermediate_field.adjoin_zero {F : Type u_1} [field F] {E : Type u_2} [field E] [algebra F E] :

@[simp]
theorem intermediate_field.adjoin_one {F : Type u_1} [field F] {E : Type u_2} [field E] [algebra F E] :

@[simp]
theorem intermediate_field.adjoin_int {F : Type u_1} [field F] {E : Type u_2} [field E] [algebra F E] (n : ) :

@[simp]
theorem intermediate_field.adjoin_nat {F : Type u_1} [field F] {E : Type u_2} [field E] [algebra F E] (n : ) :

@[simp]
theorem intermediate_field.to_subalgebra_eq_iff {F : Type u_1} [field F] {E : Type u_2} [field E] [algebra F E] {K L : intermediate_field 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} :

theorem intermediate_field.dim_adjoin_simple_eq_one_iff {F : Type u_1} [field F] {E : Type u_2} [field E] [algebra F E] {α : E} :

theorem intermediate_field.findim_adjoin_simple_eq_one_iff {F : Type u_1} [field F] {E : Type u_2} [field E] [algebra F E] {α : E} :

theorem intermediate_field.bot_eq_top_of_dim_adjoin_eq_one {F : Type u_1} [field F] {E : Type u_2} [field E] [algebra F E] :
(∀ (x : E), vector_space.dim F Fx = 1) =

If F⟮x⟯ has dimension 1 over F for every x ∈ E then F = E.

theorem intermediate_field.bot_eq_top_of_findim_adjoin_eq_one {F : Type u_1} [field F] {E : Type u_2} [field E] [algebra F E] :
(∀ (x : E), finite_dimensional.findim F Fx = 1) =

theorem intermediate_field.subsingleton_of_dim_adjoin_eq_one {F : Type u_1} [field F] {E : Type u_2} [field E] [algebra F E] :

theorem intermediate_field.subsingleton_of_findim_adjoin_eq_one {F : Type u_1} [field F] {E : Type u_2} [field E] [algebra F E] :

@[instance]
def intermediate_field.finite_dimensional {F : Type u_1} [field F] {E : Type u_2} [field E] [algebra F E] [finite_dimensional F E] (K : intermediate_field F E) :

theorem intermediate_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] :
(∀ (x : E), finite_dimensional.findim F Fx 1) =

If F⟮x⟯ has dimension ≤1 over F for every x ∈ E then F = E.

def intermediate_field.fg {F : Type u_1} [field F] {E : Type u_2} [field E] [algebra F E] :
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.

Equations
theorem intermediate_field.fg_adjoin_finset {F : Type u_1} [field F] {E : Type u_2} [field E] [algebra F E] (t : finset E) :

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} :
S.fg ∃ (t : set E), t.finite intermediate_field.adjoin F t = S

theorem intermediate_field.fg_bot {F : Type u_1} [field F] {E : Type u_2} [field E] [algebra 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) :

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 {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 KP (K)x) (K : intermediate_field F E) :
P K