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] (S : set 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] :

def intermediate_field.subalgebra.equiv_of_eq {F : Type u_1} [field F] {E : Type u_2} [field E] [algebra F E] {X Y : subalgebra F E} (h : X = Y) :

Construct an algebra isomorphism from an equality of subalgebras

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

The bottom intermediate_field is isomorphic to the field.

Equations
@[simp]
theorem intermediate_field.bot_equiv_def {F : Type u_1} [field F] {E : Type u_2} [field E] [algebra F E] (x : F) :

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

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

The top intermediate_field is isomorphic to the field.

Equations
@[simp]
theorem intermediate_field.top_equiv_def {F : Type u_1} [field F] {E : Type u_2} [field E] [algebra F E] (x : ) :

@[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) (h : S T) :

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

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} (H : T S) :

@[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} (HF : set.range (algebra_map F E) K) (HS : S K) :

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) (inv_mem : ∀ (x : E), x algebra.adjoin F Sx⁻¹ 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) :

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 sp x) (Hmap : ∀ (x : F), p ((algebra_map F E) x)) (Hadd : ∀ (x y : E), p xp yp (x + y)) (Hneg : ∀ (x : E), p xp (-x)) (Hinv : ∀ (x : E), p xp x⁻¹) (Hmul : ∀ (x y : E), p xp yp (x * y)) :
p x

@[class]
structure intermediate_field.insert {α : Type u_3} (s : 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) :

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

@[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.dim_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.findim_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.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] (h : ∀ (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] (h : ∀ (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] (h : ∀ (x : E), vector_space.dim F Fx = 1) :

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

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

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

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

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

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

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.

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) (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 SP KP (K)x) :

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

def intermediate_field.lifts (F : Type u_1) (E : Type u_2) (K : Type u_3) [field F] [field E] [field K] [algebra F E] [algebra F K] :
Type (max u_2 u_3)

Lifts L → K of F → K

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

Equations
@[instance]
def intermediate_field.lifts.inhabited {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
theorem intermediate_field.lifts.eq_of_le {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 y : intermediate_field.lifts F E K} (hxy : x y) (s : (x.fst)) :
(x.snd) s = (y.snd) s, _⟩

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 : zorn.chain has_le.le c) (hx : x set.insert c) (hy : y set.insert c) :
∃ (z : intermediate_field.lifts F E K), z set.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 : zorn.chain has_le.le c) (hx : x set.insert c) (hy : y set.insert c) (hz : z set.insert c) :
∃ (w : intermediate_field.lifts F E K), w set.insert c x w y w z w

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 : zorn.chain has_le.le c) :

An upper bound on a chain of lifts

Equations

The lift on the upper bound on a chain of lifts

Equations
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 : zorn.chain has_le.le c) :
∃ (ub : intermediate_field.lifts F E K), ∀ (a : intermediate_field.lifts F E K), a ca ub

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

Extend a lift x : lifts F E K to an element s : E whose conjugates are all in K

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

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)) :
∃ (y : intermediate_field.lifts F E K), x y s y.fst

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 Sis_integral F s 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} (hS : intermediate_field.adjoin F S = ) (hK : ∀ (x : E), x Sis_integral F x polynomial.splits (algebra_map F K) (minpoly F x)) :