# mathlibdocumentation

field_theory.intermediate_field

# Intermediate fields

Let L / K be a field extension, given as an instance algebra K L. This file defines the type of fields in between K and L, intermediate_field K L. An intermediate_field K L is a subfield of L which contains (the image of) K, i.e. it is a subfield L and a subalgebra K L.

## Main definitions

• intermediate_field K L : the type of intermediate fields between K and L.

• subalgebra.to_intermediate_field: turns a subalgebra closed under ⁻¹ into an intermediate field

• subfield.to_intermediate_field: turns a subfield containing the image of K into an intermediate field

• intermediate_field.map: map an intermediate field along an alg_hom

## Implementation notes

Intermediate fields are defined with a structure extending subfield and subalgebra. A subalgebra is closed under all operations except ⁻¹,

## Tags

intermediate field, field extension

def intermediate_field.to_subalgebra {K : Type u_1} {L : Type u_2} [field K] [field L] [ L] (s : L) :
L

Reinterpret an intermediate_field as a subalgebra.

structure intermediate_field (K : Type u_1) (L : Type u_2) [field K] [field L] [ L] :
Type u_2

S : intermediate_field K L is a subset of L such that there is a field tower L / S / K.

def intermediate_field.to_subfield {K : Type u_1} {L : Type u_2} [field K] [field L] [ L] (s : L) :

Reinterpret an intermediate_field as a subfield.

@[instance]
def intermediate_field.set.has_coe {K : Type u_1} {L : Type u_2} [field K] [field L] [ L] :
(set L)

Equations
@[simp]
theorem intermediate_field.coe_to_subalgebra {K : Type u_1} {L : Type u_2} [field K] [field L] [ L] (S : L) :

@[simp]
theorem intermediate_field.coe_to_subfield {K : Type u_1} {L : Type u_2} [field K] [field L] [ L] (S : L) :

@[instance]
def intermediate_field.has_coe_to_sort {K : Type u_1} {L : Type u_2} [field K] [field L] [ L] :

Equations
@[instance]
def intermediate_field.has_mem {K : Type u_1} {L : Type u_2} [field K] [field L] [ L] :
L)

Equations
@[simp]
theorem intermediate_field.mem_mk {K : Type u_1} {L : Type u_2} [field K] [field L] [ L] (s : set L) (hK : ∀ (x : K), L) x s) (ho : 1 s) (hm : ∀ {a b : L}, a sb sa * b s) (hz : 0 s) (ha : ∀ {a b : L}, a sb sa + b s) (hn : ∀ {x : L}, x s-x s) (hi : ∀ (x : L), x sx⁻¹ s) (x : L) :
x {carrier := s, one_mem' := ho, mul_mem' := hm, zero_mem' := hz, add_mem' := ha, algebra_map_mem' := hK, neg_mem' := hn, inv_mem' := hi} x s

@[simp]
theorem intermediate_field.mem_coe {K : Type u_1} {L : Type u_2} [field K] [field L] [ L] (S : L) (x : L) :
x S x S

@[simp]
theorem intermediate_field.mem_to_subalgebra {K : Type u_1} {L : Type u_2} [field K] [field L] [ L] (s : L) (x : L) :
x s

@[simp]
theorem intermediate_field.mem_to_subfield {K : Type u_1} {L : Type u_2} [field K] [field L] [ L] (s : L) (x : L) :

theorem intermediate_field.ext' {K : Type u_1} {L : Type u_2} [field K] [field L] [ L] ⦃s t : L⦄ (h : s = t) :
s = t

Two intermediate fields are equal if the underlying subsets are equal.

theorem intermediate_field.ext'_iff {K : Type u_1} {L : Type u_2} [field K] [field L] [ L] {s t : L} :
s = t s = t

Two intermediate fields are equal if and only if the underlying subsets are equal.

@[ext]
theorem intermediate_field.ext {K : Type u_1} {L : Type u_2} [field K] [field L] [ L] {S T : L} (h : ∀ (x : L), x S x T) :
S = T

Two intermediate fields are equal if they have the same elements.

theorem intermediate_field.algebra_map_mem {K : Type u_1} {L : Type u_2} [field K] [field L] [ L] (S : L) (x : K) :
L) x S

An intermediate field contains the image of the smaller field.

theorem intermediate_field.one_mem {K : Type u_1} {L : Type u_2} [field K] [field L] [ L] (S : L) :
1 S

An intermediate field contains the ring's 1.

theorem intermediate_field.zero_mem {K : Type u_1} {L : Type u_2} [field K] [field L] [ L] (S : L) :
0 S

An intermediate field contains the ring's 0.

theorem intermediate_field.mul_mem {K : Type u_1} {L : Type u_2} [field K] [field L] [ L] (S : L) {x y : L} :
x Sy Sx * y S

An intermediate field is closed under multiplication.

theorem intermediate_field.smul_mem {K : Type u_1} {L : Type u_2} [field K] [field L] [ L] (S : L) {y : L} :
y S∀ {x : K}, x y S

An intermediate field is closed under scalar multiplication.

theorem intermediate_field.add_mem {K : Type u_1} {L : Type u_2} [field K] [field L] [ L] (S : L) {x y : L} :
x Sy Sx + y S

An intermediate field is closed under addition.

theorem intermediate_field.sub_mem {K : Type u_1} {L : Type u_2} [field K] [field L] [ L] (S : L) {x y : L} (hx : x S) (hy : y S) :
x - y S

An intermediate field is closed under subtraction

theorem intermediate_field.neg_mem {K : Type u_1} {L : Type u_2} [field K] [field L] [ L] (S : L) {x : L} :
x S-x S

An intermediate field is closed under negation.

theorem intermediate_field.inv_mem {K : Type u_1} {L : Type u_2} [field K] [field L] [ L] (S : L) {x : L} :
x Sx⁻¹ S

An intermediate field is closed under inverses.

theorem intermediate_field.div_mem {K : Type u_1} {L : Type u_2} [field K] [field L] [ L] (S : L) {x y : L} (hx : x S) (hy : y S) :
x / y S

An intermediate field is closed under division.

theorem intermediate_field.list_prod_mem {K : Type u_1} {L : Type u_2} [field K] [field L] [ L] (S : L) {l : list L} :
(∀ (x : L), x lx S)l.prod S

Product of a list of elements in an intermediate_field is in the intermediate_field.

theorem intermediate_field.list_sum_mem {K : Type u_1} {L : Type u_2} [field K] [field L] [ L] (S : L) {l : list L} :
(∀ (x : L), x lx S)l.sum S

Sum of a list of elements in an intermediate field is in the intermediate_field.

theorem intermediate_field.multiset_prod_mem {K : Type u_1} {L : Type u_2} [field K] [field L] [ L] (S : L) (m : multiset L) :
(∀ (a : L), a ma S)m.prod S

Product of a multiset of elements in an intermediate field is in the intermediate_field.

theorem intermediate_field.multiset_sum_mem {K : Type u_1} {L : Type u_2} [field K] [field L] [ L] (S : L) (m : multiset L) :
(∀ (a : L), a ma S)m.sum S

Sum of a multiset of elements in a intermediate_field is in the intermediate_field.

theorem intermediate_field.prod_mem {K : Type u_1} {L : Type u_2} [field K] [field L] [ L] (S : L) {ι : Type u_3} {t : finset ι} {f : ι → L} (h : ∀ (c : ι), c tf c S) :
∏ (i : ι) in t, f i S

Product of elements of an intermediate field indexed by a finset is in the intermediate_field.

theorem intermediate_field.sum_mem {K : Type u_1} {L : Type u_2} [field K] [field L] [ L] (S : L) {ι : Type u_3} {t : finset ι} {f : ι → L} (h : ∀ (c : ι), c tf c S) :
∑ (i : ι) in t, f i S

Sum of elements in a intermediate_field indexed by a finset is in the intermediate_field.

theorem intermediate_field.pow_mem {K : Type u_1} {L : Type u_2} [field K] [field L] [ L] (S : L) {x : L} (hx : x S) (n : ) :
x ^ n S

theorem intermediate_field.gsmul_mem {K : Type u_1} {L : Type u_2} [field K] [field L] [ L] (S : L) {x : L} (hx : x S) (n : ) :
n •ℤ x S

theorem intermediate_field.coe_int_mem {K : Type u_1} {L : Type u_2} [field K] [field L] [ L] (S : L) (n : ) :
n S

def subalgebra.to_intermediate_field {K : Type u_1} {L : Type u_2} [field K] [field L] [ L] (S : L) (inv_mem : ∀ (x : L), x Sx⁻¹ S) :

Turn a subalgebra closed under inverses into an intermediate field

Equations
@[simp]
theorem to_subalgebra_to_intermediate_field {K : Type u_1} {L : Type u_2} [field K] [field L] [ L] (S : L) (inv_mem : ∀ (x : L), x Sx⁻¹ S) :

@[simp]
theorem to_intermediate_field_to_subalgebra {K : Type u_1} {L : Type u_2} [field K] [field L] [ L] (S : L) (inv_mem : ∀ (x : L), x⁻¹ S) :

def subfield.to_intermediate_field {K : Type u_1} {L : Type u_2} [field K] [field L] [ L] (S : subfield L) (algebra_map_mem : ∀ (x : K), L) x S) :

Turn a subfield of L containing the image of K into an intermediate field

Equations
@[instance]
def intermediate_field.to_field {K : Type u_1} {L : Type u_2} [field K] [field L] [ L] (S : L) :

An intermediate field inherits a field structure

Equations
@[simp]
theorem intermediate_field.coe_add {K : Type u_1} {L : Type u_2} [field K] [field L] [ L] (S : L) (x y : S) :
(x + y) = x + y

@[simp]
theorem intermediate_field.coe_neg {K : Type u_1} {L : Type u_2} [field K] [field L] [ L] (S : L) (x : S) :

@[simp]
theorem intermediate_field.coe_mul {K : Type u_1} {L : Type u_2} [field K] [field L] [ L] (S : L) (x y : S) :
x * y = (x) * y

@[simp]
theorem intermediate_field.coe_inv {K : Type u_1} {L : Type u_2} [field K] [field L] [ L] (S : L) (x : S) :

@[simp]
theorem intermediate_field.coe_zero {K : Type u_1} {L : Type u_2} [field K] [field L] [ L] (S : L) :
0 = 0

@[simp]
theorem intermediate_field.coe_one {K : Type u_1} {L : Type u_2} [field K] [field L] [ L] (S : L) :
1 = 1

@[instance]
def intermediate_field.algebra {K : Type u_1} {L : Type u_2} [field K] [field L] [ L] (S : L) :
S

Equations
@[instance]
def intermediate_field.to_algebra {K : Type u_1} {L : Type u_2} [field K] [field L] [ L] (S : L) :
L

Equations
@[instance]
def intermediate_field.is_scalar_tower {K : Type u_1} {L : Type u_2} [field K] [field L] [ L] (S : L) :
L

def intermediate_field.map {K : Type u_1} {L : Type u_2} [field K] [field L] [ L] (S : L) {L' : Type u_3} [field L'] [ L'] (f : L →ₐ[K] L') :

If f : L →+* L' fixes K, S.map f is the intermediate field between L' and K such that x ∈ S ↔ f x ∈ S.map f.

Equations
def intermediate_field.val {K : Type u_1} {L : Type u_2} [field K] [field L] [ L] (S : L) :

The embedding from an intermediate field of L / K to L.

Equations
@[simp]
theorem intermediate_field.coe_val {K : Type u_1} {L : Type u_2} [field K] [field L] [ L] (S : L) :

@[simp]
theorem intermediate_field.val_mk {K : Type u_1} {L : Type u_2} [field K] [field L] [ L] (S : L) {x : L} (hx : x S) :
(S.val) x, hx⟩ = x

theorem intermediate_field.to_subalgebra_injective {K : Type u_1} {L : Type u_2} [field K] [field L] [ L] {S S' : L} (h : S.to_subalgebra = S'.to_subalgebra) :
S = S'

@[instance]
def intermediate_field.partial_order {K : Type u_1} {L : Type u_2} [field K] [field L] [ L] :

Equations
theorem intermediate_field.set_range_subset {K : Type u_1} {L : Type u_2} [field K] [field L] [ L] (S : L) :

theorem intermediate_field.field_range_le {K : Type u_1} {L : Type u_2} [field K] [field L] [ L] (S : L) :

@[simp]
theorem intermediate_field.to_subalgebra_le_to_subalgebra {K : Type u_1} {L : Type u_2} [field K] [field L] [ L] {S S' : L} :
S S'

@[simp]
theorem intermediate_field.to_subalgebra_lt_to_subalgebra {K : Type u_1} {L : Type u_2} [field K] [field L] [ L] {S S' : L} :
S < S'

def intermediate_field.lift1 {K : Type u_1} {L : Type u_2} [field K] [field L] [ L] {F : L} (E : F) :

Lift an intermediate_field of an intermediate_field

Equations
def intermediate_field.lift2 {K : Type u_1} {L : Type u_2} [field K] [field L] [ L] {F : L} (E : L) :

Lift an intermediate_field of an intermediate_field

Equations
@[instance]
def intermediate_field.has_lift1 {K : Type u_1} {L : Type u_2} [field K] [field L] [ L] {F : L} :
L)

Equations
@[instance]
def intermediate_field.has_lift2 {K : Type u_1} {L : Type u_2} [field K] [field L] [ L] {F : L} :
L)

Equations
@[simp]
theorem intermediate_field.mem_lift2 {K : Type u_1} {L : Type u_2} [field K] [field L] [ L] {F : L} {E : L} {x : L} :
x E x E

@[instance]
def intermediate_field.finite_dimensional_left {K : Type u_1} {L : Type u_2} [field K] [field L] [ L] [ L] (F : L) :

@[instance]
def intermediate_field.finite_dimensional_right {K : Type u_1} {L : Type u_2} [field K] [field L] [ L] [ L] (F : L) :

theorem intermediate_field.eq_of_le_of_findim_le {K : Type u_1} {L : Type u_2} [field K] [field L] [ L] [ L] {F E : L} (h_le : F E) (h_findim : ) :
F = E

theorem intermediate_field.eq_of_le_of_findim_eq {K : Type u_1} {L : Type u_2} [field K] [field L] [ L] [ L] {F E : L} (h_le : F E) (h_findim : = ) :
F = E

theorem intermediate_field.eq_of_le_of_findim_le' {K : Type u_1} {L : Type u_2} [field K] [field L] [ L] [ L] {F E : L} (h_le : F E) (h_findim : ) :
F = E

theorem intermediate_field.eq_of_le_of_findim_eq' {K : Type u_1} {L : Type u_2} [field K] [field L] [ L] [ L] {F E : L} (h_le : F E) (h_findim : = ) :
F = E

def subalgebra_equiv_intermediate_field {K : Type u_1} {L : Type u_2} [field K] [field L] [ L] (alg : L) :
L ≃o

If L/K is algebraic, the K-subalgebras of L are all fields.

Equations
@[simp]
theorem mem_subalgebra_equiv_intermediate_field {K : Type u_1} {L : Type u_2} [field K] [field L] [ L] (alg : L) {S : L} {x : L} :
x S

@[simp]
theorem mem_subalgebra_equiv_intermediate_field_symm {K : Type u_1} {L : Type u_2} [field K] [field L] [ L] (alg : L) {S : L} {x : L} :
x S x S