mathlib3 documentation

field_theory.adjoin

Adjoining Elements to Fields #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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
Instances for intermediate_field.adjoin
@[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} :

Galois insertion between adjoin and coe.

Equations
@[protected, instance]
def intermediate_field.inhabited {F : Type u_1} [field F] {E : Type u_2} [field E] [algebra F E] :
Equations
theorem intermediate_field.coe_bot {F : Type u_1} [field F] {E : Type u_2} [field E] [algebra F E] :
theorem intermediate_field.mem_bot {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.coe_top {F : Type u_1} [field F] {E : Type u_2} [field E] [algebra F E] :
@[simp]
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.top_to_subalgebra {F : Type u_1} [field F] {E : Type u_2} [field E] [algebra F E] :
@[simp]
theorem intermediate_field.top_to_subfield {F : Type u_1} [field F] {E : Type u_2} [field E] [algebra F E] :
@[simp, norm_cast]
theorem intermediate_field.coe_inf {F : Type u_1} [field F] {E : Type u_2} [field E] [algebra F E] (S T : intermediate_field F E) :
(S T) = S T
@[simp]
theorem intermediate_field.mem_inf {F : Type u_1} [field F] {E : Type u_2} [field E] [algebra F E] {S T : intermediate_field F E} {x : E} :
x S T x S x T
@[simp]
@[simp]
theorem intermediate_field.inf_to_subfield {F : Type u_1} [field F] {E : Type u_2} [field E] [algebra F E] (S T : intermediate_field F E) :
@[simp, norm_cast]
theorem intermediate_field.coe_Inf {F : Type u_1} [field F] {E : Type u_2} [field E] [algebra F E] (S : set (intermediate_field F E)) :
@[simp, norm_cast]
theorem intermediate_field.coe_infi {F : Type u_1} [field F] {E : Type u_2} [field E] [algebra F E] {ι : Sort u_3} (S : ι intermediate_field F E) :
(infi S) = (i : ι), (S i)
@[simp]
theorem intermediate_field.infi_to_subalgebra {F : Type u_1} [field F] {E : Type u_2} [field E] [algebra F E] {ι : Sort u_3} (S : ι intermediate_field F E) :
@[simp]
theorem intermediate_field.infi_to_subfield {F : Type u_1} [field F] {E : Type u_2} [field E] [algebra F E] {ι : Sort u_3} (S : ι intermediate_field F E) :
(infi S).to_subfield = (i : ι), (S i).to_subfield
@[simp]
theorem intermediate_field.equiv_of_eq_apply {F : Type u_1} [field F] {E : Type u_2} [field E] [algebra F E] {S T : intermediate_field F E} (h : S = T) (x : S) :
def intermediate_field.equiv_of_eq {F : Type u_1} [field F] {E : Type u_2} [field E] [algebra F E] {S T : intermediate_field F E} (h : S = T) :

Construct an algebra isomorphism from an equality of intermediate fields

Equations
noncomputable 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) :
@[simp]
theorem intermediate_field.bot_equiv_symm {F : Type u_1} [field F] {E : Type u_2} [field E] [algebra F E] (x : F) :
@[protected, instance]
@[simp]
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.

This is the intermediate field version of subalgebra.top_equiv.

Equations
@[simp]
@[simp]
theorem intermediate_field.restrict_scalars_top {F : Type u_1} [field F] {E : Type u_2} [field E] [algebra F E] {K : Type u_3} [field K] [algebra K E] [algebra K F] [is_scalar_tower K F E] :
theorem alg_hom.field_range_eq_map {F : Type u_1} [field F] {E : Type u_2} [field E] [algebra F E] {K : Type u_3} [field K] [algebra F K] (f : E →ₐ[F] K) :
theorem alg_hom.map_field_range {F : Type u_1} [field F] {E : Type u_2} [field E] [algebra F E] {K : Type u_3} {L : Type u_4} [field K] [field L] [algebra F K] [algebra F L] (f : E →ₐ[F] K) (g : K →ₐ[F] L) :
theorem alg_hom.field_range_eq_top {F : Type u_1} [field F] {E : Type u_2} [field E] [algebra F E] {K : Type u_3} [field K] [algebra F K] {f : E →ₐ[F] K} :
@[simp]
theorem alg_equiv.field_range_eq_top {F : Type u_1} [field F] {E : Type u_2} [field E] [algebra F E] {K : Type u_3} [field K] [algebra F K] (f : E ≃ₐ[F] K) :
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) :
@[protected, 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) :
@[protected, instance]
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]
@[simp]
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.

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.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 s p x) (Hmap : (x : F), p ((algebra_map F E) x)) (Hadd : (x y : E), p x p y p (x + y)) (Hneg : (x : E), p x p (-x)) (Hinv : (x : E), p x p x⁻¹) (Hmul : (x y : E), p x p y p (x * y)) :
p x
@[class]
structure intermediate_field.insert {α : Type u_3} (s : set α) :
Type u_3

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 of this typeclass
Instances of other typeclasses for intermediate_field.insert
  • intermediate_field.insert.has_sizeof_inst
@[protected, instance]
Equations
@[protected, 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
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 α) :
theorem intermediate_field.is_splitting_field_supr {F : Type u_1} [field F] {E : Type u_2} [field E] [algebra F E] {ι : Type u_3} {t : ι intermediate_field F E} {p : ι polynomial F} {s : finset ι} (h0 : s.prod (λ (i : ι), p i) 0) (h : (i : ι), i s polynomial.is_splitting_field F (t i) (p i)) :
polynomial.is_splitting_field F ( (i : ι) (H : i s), t i) (s.prod (λ (i : ι), p i))

A compositum of splitting fields is a splitting field

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

Adjoining a single element is compact in the lattice of intermediate fields.

Adjoining a finite subset is compact in the lattice of intermediate fields.

Adjoining a finite subset is compact in the lattice of intermediate fields.

@[protected, instance]

The lattice of intermediate fields is compactly generated.

theorem intermediate_field.exists_finset_of_mem_supr {F : Type u_1} [field F] {E : Type u_2} [field E] [algebra F E] {ι : Type u_3} {f : ι intermediate_field F E} {x : E} (hx : x (i : ι), f i) :
(s : finset ι), x (i : ι) (H : i s), f i
theorem intermediate_field.exists_finset_of_mem_supr' {F : Type u_1} [field F] {E : Type u_2} [field E] [algebra F E] {ι : Type u_3} {f : ι intermediate_field F E} {x : E} (hx : x (i : ι), f i) :
(s : finset (Σ (i : ι), (f i))), x (i : Σ (i : ι), (f i)) (H : i s), F(i.snd)
theorem intermediate_field.exists_finset_of_mem_supr'' {F : Type u_1} [field F] {E : Type u_2} [field E] [algebra F E] {ι : Type u_3} {f : ι intermediate_field F E} (h : (i : ι), algebra.is_algebraic F (f i)) {x : E} (hx : x (i : ι), f i) :
(s : finset (Σ (i : ι), (f i))), x (i : Σ (i : ι), (f i)) (H : i s), intermediate_field.adjoin F ((minpoly F i.snd).root_set 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.rank_eq_one_iff {F : Type u_1} [field F] {E : Type u_2} [field E] [algebra F E] {K : intermediate_field F E} :
@[simp]
@[simp]
theorem intermediate_field.rank_bot {F : Type u_1} [field F] {E : Type u_2} [field E] [algebra F E] :
@[simp]
theorem intermediate_field.finrank_bot {F : Type u_1} [field F] {E : Type u_2} [field E] [algebra F E] :
theorem intermediate_field.rank_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_rank_adjoin_eq_one {F : Type u_1} [field F] {E : Type u_2} [field E] [algebra F E] (h : (x : E), module.rank F Fx = 1) :

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

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

theorem intermediate_field.minpoly_gen {F : Type u_1} [field F] {E : Type u_2} [field E] [algebra F E] {α : E} (h : is_integral F α) :
noncomputable 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
noncomputable def intermediate_field.power_basis_aux {K : Type u_3} [field K] {L : Type u_4} [field L] [algebra K L] {x : L} (hx : is_integral K x) :

The elements 1, x, ..., x ^ (d - 1) form a basis for K⟮x⟯, where d is the degree of the minimal polynomial of x.

Equations
@[simp]
noncomputable def intermediate_field.adjoin.power_basis {K : Type u_3} [field K] {L : Type u_4} [field L] [algebra K L] {x : L} (hx : is_integral K x) :

The power basis 1, x, ..., x ^ (d - 1) for K⟮x⟯, where d is the degree of the minimal polynomial of x.

Equations
theorem intermediate_field.adjoin.finite_dimensional {K : Type u_3} [field K] {L : Type u_4} [field L] [algebra K L] {x : L} (hx : is_integral K x) :
theorem intermediate_field.adjoin.finrank {K : Type u_3} [field K] {L : Type u_4} [field L] [algebra K L] {x : L} (hx : is_integral K x) :
theorem minpoly.nat_degree_le {K : Type u_3} [field K] {L : Type u_4} [field L] [algebra K L] {x : L} [finite_dimensional K L] (hx : is_integral K x) :
theorem minpoly.degree_le {K : Type u_3} [field K] {L : Type u_4} [field L] [algebra K L] {x : L} [finite_dimensional K L] (hx : is_integral K x) :
noncomputable 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
noncomputable 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} :
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 S P K P (intermediate_field.restrict_scalars F (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 K P (intermediate_field.restrict_scalars F (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 K P (intermediate_field.restrict_scalars F (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
Instances for intermediate_field.lifts
@[protected, instance]
def intermediate_field.lifts.partial_order {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
@[protected, instance]
noncomputable 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
@[protected, instance]
noncomputable 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 : is_chain has_le.le c) (hx : x has_insert.insert c) (hy : y has_insert.insert c) :
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 : is_chain has_le.le c) (hx : x has_insert.insert c) (hy : y has_insert.insert c) (hz : z has_insert.insert 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 : is_chain has_le.le c) :
noncomputable 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)) :
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 S is_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 S is_integral F x polynomial.splits (algebra_map F K) (minpoly F x)) :
@[protected, instance]
def intermediate_field.finite_dimensional_sup {K : Type u_1} {L : Type u_2} [field K] [field L] [algebra K L] (E1 E2 : intermediate_field K L) [h1 : finite_dimensional K E1] [h2 : finite_dimensional K E2] :
@[protected, instance]
def intermediate_field.finite_dimensional_supr_of_finite {K : Type u_1} {L : Type u_2} [field K] [field L] [algebra K L] {ι : Type u_3} {t : ι intermediate_field K L} [h : finite ι] [ (i : ι), finite_dimensional K (t i)] :
finite_dimensional K ( (i : ι), t i)
@[protected, instance]
def intermediate_field.finite_dimensional_supr_of_finset {K : Type u_1} {L : Type u_2} [field K] [field L] [algebra K L] {ι : Type u_3} {f : ι intermediate_field K L} {s : finset ι} [h : (i : ι), i s finite_dimensional K (f i)] :
finite_dimensional K ( (i : ι) (H : i s), f i)
theorem intermediate_field.is_algebraic_supr {K : Type u_1} {L : Type u_2} [field K] [field L] [algebra K L] {ι : Type u_3} {f : ι intermediate_field K L} (h : (i : ι), algebra.is_algebraic K (f i)) :
algebra.is_algebraic K ( (i : ι), f i)

A compositum of algebraic extensions is algebraic

noncomputable def power_basis.equiv_adjoin_simple {K : Type u_1} {L : Type u_2} [field K] [field L] [algebra K L] (pb : power_basis K L) :

pb.equiv_adjoin_simple is the equivalence between K⟮pb.gen⟯ and L itself.

Equations