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

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

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

Equations
source
@[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

source
theorem intermediate_field.gc {F : Type u_1} [field F] {E : Type u_2} [field E] [algebra F E] :
galois_connection (intermediate_field.adjoin F) coe

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

Galois insertion between adjoin and coe.

Equations
source
@[instance]
def intermediate_field.complete_lattice {F : Type u_1} [field F] {E : Type u_2} [field E] [algebra F E] :
complete_lattice (intermediate_field F E)

Equations
source
@[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
source
theorem intermediate_field.mem_bot {F : Type u_1} [field F] {E : Type u_2} [field E] [algebra F E] {x : E} :
x ∈ ⊥ ↔ x ∈ set.range ⇑(algebra_map F E)

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

source
@[simp]
theorem intermediate_field.bot_to_subalgebra {F : Type u_1} [field F] {E : Type u_2} [field E] [algebra F E] :
⊥.to_subalgebra = ⊥

source
@[simp]
theorem intermediate_field.top_to_subalgebra {F : Type u_1} [field F] {E : Type u_2} [field E] [algebra F E] :
⊤.to_subalgebra = ⊤

source
@[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) :
↑⊥ = K

source
@[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) :
↑⊤ = ⊤

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

source
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

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

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

source
@[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) :
has_coe_t ↥S ↥(intermediate_field.adjoin F S)

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

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

source
theorem intermediate_field.subset_adjoin_of_subset_left {E : Type u_2} [field E] (S : set E) {F : subfield E} {T : set E} :
T ⊆ ↑F → T ⊆ ↑(intermediate_field.adjoin ↥F S)

source
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} :
T ⊆ S → T ⊆ ↑(intermediate_field.adjoin F S)

source
@[simp]
theorem intermediate_field.adjoin_empty (F : Type u_1) (E : Type u_2) [field F] [field E] [algebra F E] :
intermediate_field.adjoin F ∅ = ⊥

source
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} :
set.range ⇑(algebra_map F E) ⊆ ↑K → 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.

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

source
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]

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

source
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) :
↑(intermediate_field.adjoin ↥(intermediate_field.adjoin F S) T) = ↑(intermediate_field.adjoin ↥(intermediate_field.adjoin F T) S)

F[S][T] = F[T][S]

source
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.adjoin F S).map f = intermediate_field.adjoin F (⇑f '' S)

source
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) :
algebra.adjoin F S ≤ (intermediate_field.adjoin F S).to_subalgebra

source
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) :
(∀ (x : E), x ∈ algebra.adjoin F S → x⁻¹ ∈ algebra.adjoin F S) → (intermediate_field.adjoin F S).to_subalgebra = algebra.adjoin F S

source
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) :
K.to_subalgebra = algebra.adjoin F S → K = intermediate_field.adjoin F S

source
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 ∈ s → p x) → (∀ (x : F), p (⇑(algebra_map F E) x)) → (∀ (x y : E), p x → p y → p (x + y)) → (∀ (x : E), p x → p (-x)) → (∀ (x : E), p x → p x⁻¹) → (∀ (x y : E), p x → p y → p (x * y)) → p x

source
@[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
source
@[instance]
def intermediate_field.insert_empty {α : Type u_1} :
intermediate_field.insert ∅

Equations
source
@[instance]
def intermediate_field.insert_nonempty {α : Type u_1} (s : set α) :
intermediate_field.insert s

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

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

generator of F⟮α⟯

Equations
source
@[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 α) = α

source
theorem intermediate_field.adjoin_simple_adjoin_simple (F : Type u_1) [field F] {E : Type u_2} [field E] [algebra F E] (α β : E) :
↑(↥F⟮α⟯)⟮β⟯ = F⟮α, β⟯

source
theorem intermediate_field.adjoin_simple_comm (F : Type u_1) [field F] {E : Type u_2} [field E] [algebra F E] (α β : E) :
↑(↥F⟮α⟯)⟮β⟯ = ↑(↥F⟮β⟯)⟮α⟯

source
@[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} :
intermediate_field.adjoin F S = ⊥ ↔ S ⊆ ↑⊥

source
@[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} :
F⟮α⟯ = ⊥ ↔ α ∈ ⊥

source
@[simp]
theorem intermediate_field.adjoin_zero {F : Type u_1} [field F] {E : Type u_2} [field E] [algebra F E] :
F⟮0⟯ = ⊥

source
@[simp]
theorem intermediate_field.adjoin_one {F : Type u_1} [field F] {E : Type u_2} [field E] [algebra F E] :
F⟮1⟯ = ⊥

source
@[simp]
theorem intermediate_field.adjoin_int {F : Type u_1} [field F] {E : Type u_2} [field E] [algebra F E] (n : ℤ) :
F⟮↑n⟯ = ⊥

source
@[simp]
theorem intermediate_field.adjoin_nat {F : Type u_1} [field F] {E : Type u_2} [field E] [algebra F E] (n : ℕ) :
F⟮↑n⟯ = ⊥

source
@[simp]
theorem intermediate_field.dim_intermediate_field_eq_dim_subalgebra {F : Type u_1} [field F] {E : Type u_2} [field E] [algebra F E] {S : set E} :
vector_space.dim F ↥((intermediate_field.adjoin F S).to_subalgebra) = vector_space.dim F ↥(intermediate_field.adjoin F S)

source
@[simp]
theorem intermediate_field.findim_intermediate_field_eq_findim_subalgebra {F : Type u_1} [field F] {E : Type u_2} [field E] [algebra F E] {S : set E} :
finite_dimensional.findim F ↥((intermediate_field.adjoin F S).to_subalgebra) = finite_dimensional.findim F ↥(intermediate_field.adjoin F S)

source
@[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} :
K.to_subalgebra = L.to_subalgebra ↔ K = L

source
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} :
vector_space.dim F ↥(intermediate_field.adjoin F S) = 1 ↔ S ⊆ ↑⊥

source
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} :
vector_space.dim F ↥F⟮α⟯ = 1 ↔ α ∈ ⊥

source
theorem intermediate_field.findim_adjoin_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 ↥(intermediate_field.adjoin F S) = 1 ↔ S ⊆ ↑⊥

source
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} :
finite_dimensional.findim F ↥F⟮α⟯ = 1 ↔ α ∈ ⊥

source
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 ↥F⟮x⟯ = 1) → ⊥ = ⊤

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

source
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 ↥F⟮x⟯ = 1) → ⊥ = ⊤

source
theorem intermediate_field.subsingleton_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 ↥F⟮x⟯ = 1) → subsingleton (intermediate_field F E)

source
theorem intermediate_field.subsingleton_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 ↥F⟮x⟯ = 1) → subsingleton (intermediate_field F E)

source
@[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) :
finite_dimensional F ↥K

source
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 ↥F⟮x⟯ ≤ 1) → ⊥ = ⊤

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

source
theorem intermediate_field.subsingleton_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 ↥F⟮x⟯ ≤ 1) → subsingleton (intermediate_field F E)

source
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
source
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

source
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

source
theorem intermediate_field.fg_bot {F : Type u_1} [field F] {E : Type u_2} [field E] [algebra F E] :
⊥.fg

source
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) :
S.to_subalgebra.fg → S.fg

source
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

source
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