mathlib documentation

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 ⁻¹,

TODO

field.adjoin currently returns a subalgebra, this should become an intermediate_field. The lattice structure on intermediate_field will follow from the adjunction given by field.adjoin.

Tags

intermediate field, field extension

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

Reinterpret an intermediate_field as a subalgebra.

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

Type u_2

carrier : set L
one_mem' : 1 ∈ c.carrier
mul_mem' : ∀ {a b : L}, a ∈ c.carrier → b ∈ c.carrier → a * b ∈ c.carrier
zero_mem' : 0 ∈ c.carrier
add_mem' : ∀ {a b : L}, a ∈ c.carrier → b ∈ c.carrier → a + b ∈ c.carrier
algebra_map_mem' : ∀ (r : K), ⇑(algebra_map K L) r ∈ c.carrier
neg_mem' : ∀ {x : L}, x ∈ c.carrier → -x ∈ c.carrier
inv_mem' : ∀ (x : L), x ∈ c.carrier → x⁻¹ ∈ c.carrier

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] [algebra K L] (s : intermediate_field K L) :

Reinterpret an intermediate_field as a subfield.

@[instance]

def intermediate_field.has_coe {K : Type u_1} {L : Type u_2} [field K] [field L] [algebra K L] :

has_coe (intermediate_field K L) (set L)

Equations

intermediate_field.has_coe = {coe := intermediate_field.carrier _inst_3}

@[simp]

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

↑(S.to_subalgebra) = ↑S

@[simp]

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

↑(S.to_subfield) = ↑S

@[instance]

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

has_coe_to_sort (intermediate_field K L)

Equations

intermediate_field.has_coe_to_sort = {S := Type u_2, coe := λ (S : intermediate_field K L), ↥(S.carrier)}

@[instance]

def intermediate_field.has_mem {K : Type u_1} {L : Type u_2} [field K] [field L] [algebra K L] :

has_mem L (intermediate_field K L)

Equations

intermediate_field.has_mem = {mem := λ (m : L) (S : intermediate_field K L), m ∈ ↑S}

@[simp]

theorem intermediate_field.mem_mk {K : Type u_1} {L : Type u_2} [field K] [field L] [algebra K L] (s : set L) (hK : ∀ (x : K), ⇑(algebra_map K L) x ∈ s) (ho : 1 ∈ s) (hm : ∀ {a b : L}, a ∈ s → b ∈ s → a * b ∈ s) (hz : 0 ∈ s) (ha : ∀ {a b : L}, a ∈ s → b ∈ s → a + b ∈ s) (hn : ∀ {x : L}, x ∈ s → -x ∈ s) (hi : ∀ (x : L), x ∈ s → x⁻¹ ∈ 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] [algebra K L] (S : intermediate_field K 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] [algebra K L] (s : intermediate_field K L) (x : L) :

x ∈ s.to_subalgebra ↔ x ∈ s

@[simp]

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

x ∈ s.to_subfield ↔ x ∈ s

theorem intermediate_field.ext' {K : Type u_1} {L : Type u_2} [field K] [field L] [algebra K L] ⦃s t : intermediate_field K 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] [algebra K L] {s t : intermediate_field K 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] [algebra K L] {S T : intermediate_field K 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] [algebra K L] (S : intermediate_field K L) (x : K) :

⇑(algebra_map 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] [algebra K L] (S : intermediate_field K 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] [algebra K L] (S : intermediate_field K 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] [algebra K L] (S : intermediate_field K L) {x y : L} (a : x ∈ S) (a_1 : y ∈ S) :

x * 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] [algebra K L] (S : intermediate_field K L) {y : L} (a : 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] [algebra K L] (S : intermediate_field K L) {x y : L} (a : x ∈ S) (a_1 : y ∈ S) :

x + 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] [algebra K L] (S : intermediate_field K 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] [algebra K L] (S : intermediate_field K L) {x : L} (a : 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] [algebra K L] (S : intermediate_field K L) {x : L} (a : x ∈ 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] [algebra K L] (S : intermediate_field K 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] [algebra K L] (S : intermediate_field K L) {l : list L} (a : ∀ (x : L), x ∈ l → x ∈ 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] [algebra K L] (S : intermediate_field K L) {l : list L} (a : ∀ (x : L), x ∈ l → x ∈ 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] [algebra K L] (S : intermediate_field K L) (m : multiset L) (a : ∀ (a : L), a ∈ m → a ∈ 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] [algebra K L] (S : intermediate_field K L) (m : multiset L) (a : ∀ (a : L), a ∈ m → a ∈ 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] [algebra K L] (S : intermediate_field K L) {ι : Type u_3} {t : finset ι} {f : ι → L} (h : ∀ (c : ι), c ∈ t → f 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] [algebra K L] (S : intermediate_field K L) {ι : Type u_3} {t : finset ι} {f : ι → L} (h : ∀ (c : ι), c ∈ t → f 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] [algebra K L] (S : intermediate_field K 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] [algebra K L] (S : intermediate_field K 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] [algebra K L] (S : intermediate_field K L) (n : ℤ) :

@[instance]

def intermediate_field.inhabited {K : Type u_1} {L : Type u_2} [field K] [field L] [algebra K L] :

inhabited (intermediate_field K L)

Equations

intermediate_field.inhabited = {default := {carrier := ⊤.carrier, one_mem' := _, mul_mem' := _, zero_mem' := _, add_mem' := _, algebra_map_mem' := _, neg_mem' := _, inv_mem' := _}}

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

intermediate_field K L

Turn a subalgebra closed under inverses into an intermediate field

Equations

S.to_intermediate_field inv_mem = {carrier := S.carrier, one_mem' := _, mul_mem' := _, zero_mem' := _, add_mem' := _, algebra_map_mem' := _, neg_mem' := _, inv_mem' := inv_mem}

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

intermediate_field K L

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

Equations

S.to_intermediate_field algebra_map_mem = {carrier := S.carrier, one_mem' := _, mul_mem' := _, zero_mem' := _, add_mem' := _, algebra_map_mem' := algebra_map_mem, neg_mem' := _, inv_mem' := _}

@[instance]

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

An intermediate field inherits a field structure

Equations

S.to_field = S.to_subfield.to_field

@[simp]

theorem intermediate_field.coe_add {K : Type u_1} {L : Type u_2} [field K] [field L] [algebra K L] (S : intermediate_field K 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] [algebra K L] (S : intermediate_field K L) (x : ↥S) :

@[simp]

theorem intermediate_field.coe_mul {K : Type u_1} {L : Type u_2} [field K] [field L] [algebra K L] (S : intermediate_field K 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] [algebra K L] (S : intermediate_field K L) (x : ↥S) :

↑x⁻¹ = (↑x)⁻¹

@[simp]

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

↑0 = 0

@[simp]

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

↑1 = 1

@[instance]

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

Equations

S.algebra = S.to_subalgebra.algebra

@[instance]

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

Equations

S.to_algebra = S.to_subalgebra.to_algebra

@[instance]

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

is_scalar_tower K ↥S L

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

intermediate_field 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

S.map f = {carrier := (S.to_subalgebra.map f).carrier, one_mem' := _, mul_mem' := _, zero_mem' := _, add_mem' := _, algebra_map_mem' := _, neg_mem' := _, inv_mem' := _}

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

↥S →ₐ[K] L

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

Equations

S.val = S.to_subalgebra.val

@[simp]

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

⇑(S.val) = coe

@[simp]

theorem intermediate_field.val_mk {K : Type u_1} {L : Type u_2} [field K] [field L] [algebra K L] (S : intermediate_field K 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] [algebra K L] {S S' : intermediate_field K 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] [algebra K L] :

partial_order (intermediate_field K L)

Equations

intermediate_field.partial_order = {le := λ (S T : intermediate_field K L), ↑S ⊆ ↑T, lt := preorder.lt._default (λ (S T : intermediate_field K L), ↑S ⊆ ↑T), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _}

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

set.range ⇑(algebra_map K L) ⊆ ↑S

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

(algebra_map K L).field_range ≤ S.to_subfield