mathlib documentation

field_theory.subfield

Subfields

Let K be a field. This file defines the "bundled" subfield type subfield K, a type whose terms correspond to subfields of K. This is the preferred way to talk about subfields in mathlib. Unbundled subfields (s : set K and is_subfield s) are not in this file, and they will ultimately be deprecated.

We prove that subfields are a complete lattice, and that you can map (pushforward) and comap (pull back) them along ring homomorphisms.

We define the closure construction from set R to subfield R, sending a subset of R to the subfield it generates, and prove that it is a Galois insertion.

Main definitions

Notation used here:

(K : Type u) [field K] (L : Type u) [field L] (f g : K →+* L) (A : subfield K) (B : subfield L) (s : set K)

Implementation notes

A subfield is implemented as a subring which is is closed under ⁻¹.

Lattice inclusion (e.g. and ) is used rather than set notation ( and ), although is defined as membership of a subfield's underlying set.

Tags

subfield, subfields

def subfield.to_subring {K : Type u} [field K] :

Reinterpret a subfield as a subring.

structure subfield (K : Type u) [field K] :
Type u

subfield R is the type of subfields of R. A subfield of R is a subset s that is a multiplicative submonoid and an additive subgroup. Note in particular that it shares the same 0 and 1 as R.

def subfield.to_add_subgroup {K : Type u} [field K] :

The underlying add_subgroup of a subfield.

Equations
def subfield.to_submonoid {K : Type u} [field K] :

The underlying submonoid of a subfield.

Equations
@[instance]
def subfield.has_coe {K : Type u} [field K] :

Equations
@[simp]
theorem subfield.coe_to_subring {K : Type u} [field K] (s : subfield K) :

@[instance]

Equations
@[instance]
def subfield.has_mem {K : Type u} [field K] :

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

@[simp]
theorem subfield.mem_to_subring {K : Type u} [field K] (s : subfield K) (x : K) :

theorem subfield.exists {K : Type u} [field K] {s : subfield K} {p : s → Prop} :
(∃ (x : s), p x) ∃ (x : K) (H : x s), p x, H⟩

theorem subfield.forall {K : Type u} [field K] {s : subfield K} {p : s → Prop} :
(∀ (x : s), p x) ∀ (x : K) (H : x s), p x, H⟩

def subring.to_subfield {K : Type u} [field K] (s : subring K) :
(∀ (x : K), x sx⁻¹ s)subfield K

A subring containing inverses is a subfield.

Equations
theorem subfield.ext' {K : Type u} [field K] ⦃s t : subfield K⦄ :
s = ts = t

Two subfields are equal if the underlying subsets are equal.

theorem subfield.ext'_iff {K : Type u} [field K] {s t : subfield K} :
s = t s = t

Two subfields are equal if and only if the underlying subsets are equal.

@[ext]
theorem subfield.ext {K : Type u} [field K] {S T : subfield K} :
(∀ (x : K), x S x T)S = T

Two subfields are equal if they have the same elements.

theorem subfield.one_mem {K : Type u} [field K] (s : subfield K) :
1 s

A subfield contains the ring's 1.

theorem subfield.zero_mem {K : Type u} [field K] (s : subfield K) :
0 s

A subfield contains the ring's 0.

theorem subfield.mul_mem {K : Type u} [field K] (s : subfield K) {x y : K} :
x sy sx * y s

A subfield is closed under multiplication.

theorem subfield.add_mem {K : Type u} [field K] (s : subfield K) {x y : K} :
x sy sx + y s

A subfield is closed under addition.

theorem subfield.neg_mem {K : Type u} [field K] (s : subfield K) {x : K} :
x s-x s

A subfield is closed under negation.

theorem subfield.sub_mem {K : Type u} [field K] (s : subfield K) {x y : K} :
x sy sx - y s

A subfield is closed under subtraction.

theorem subfield.inv_mem {K : Type u} [field K] (s : subfield K) {x : K} :
x sx⁻¹ s

A subfield is closed under inverses.

theorem subfield.div_mem {K : Type u} [field K] (s : subfield K) {x y : K} :
x sy sx / y s

A subfield is closed under division.

theorem subfield.list_prod_mem {K : Type u} [field K] (s : subfield K) {l : list K} :
(∀ (x : K), x lx s)l.prod s

Product of a list of elements in a subfield is in the subfield.

theorem subfield.list_sum_mem {K : Type u} [field K] (s : subfield K) {l : list K} :
(∀ (x : K), x lx s)l.sum s

Sum of a list of elements in a subfield is in the subfield.

theorem subfield.multiset_prod_mem {K : Type u} [field K] (s : subfield K) (m : multiset K) :
(∀ (a : K), a ma s)m.prod s

Product of a multiset of elements in a subfield is in the subfield.

theorem subfield.multiset_sum_mem {K : Type u} [field K] (s : subfield K) (m : multiset K) :
(∀ (a : K), a ma s)m.sum s

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

theorem subfield.prod_mem {K : Type u} [field K] (s : subfield K) {ι : Type u_1} {t : finset ι} {f : ι → K} :
(∀ (c : ι), c tf c s)∏ (i : ι) in t, f i s

Product of elements of a subfield indexed by a finset is in the subfield.

theorem subfield.sum_mem {K : Type u} [field K] (s : subfield K) {ι : Type u_1} {t : finset ι} {f : ι → K} :
(∀ (c : ι), c tf c s)∑ (i : ι) in t, f i s

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

theorem subfield.pow_mem {K : Type u} [field K] (s : subfield K) {x : K} (hx : x s) (n : ) :
x ^ n s

theorem subfield.gsmul_mem {K : Type u} [field K] (s : subfield K) {x : K} (hx : x s) (n : ) :
n •ℤ x s

theorem subfield.coe_int_mem {K : Type u} [field K] (s : subfield K) (n : ) :
n s

@[simp]
theorem subfield.coe_add {K : Type u} [field K] (s : subfield K) (x y : s) :
(x + y) = x + y

@[simp]
theorem subfield.coe_neg {K : Type u} [field K] (s : subfield K) (x : s) :

@[simp]
theorem subfield.coe_mul {K : Type u} [field K] (s : subfield K) (x y : s) :
x * y = (x) * y

@[simp]
theorem subfield.coe_inv {K : Type u} [field K] (s : subfield K) (x : s) :

@[simp]
theorem subfield.coe_zero {K : Type u} [field K] (s : subfield K) :
0 = 0

@[simp]
theorem subfield.coe_one {K : Type u} [field K] (s : subfield K) :
1 = 1

def subfield.subtype {K : Type u} [field K] (s : subfield K) :

The embedding from a subfield of the field K to K.

Equations
@[instance]
def subfield.to_algebra {K : Type u} [field K] (s : subfield K) :

Equations
@[simp]
theorem subfield.coe_subtype {K : Type u} [field K] (s : subfield K) :

Partial order

@[instance]
def subfield.partial_order {K : Type u} [field K] :

Equations
theorem subfield.le_def {K : Type u} [field K] {s t : subfield K} :
s t ∀ ⦃x : K⦄, x sx t

@[simp]
theorem subfield.coe_subset_coe {K : Type u} [field K] {s t : subfield K} :
s t s t

@[simp]
theorem subfield.coe_ssubset_coe {K : Type u} [field K] {s t : subfield K} :
s t s < t

@[simp]
theorem subfield.mem_coe {K : Type u} [field K] {s : subfield K} {m : K} :
m s m s

@[simp]
theorem subfield.coe_coe {K : Type u} [field K] (s : subfield K) :

@[simp]
theorem subfield.mem_to_submonoid {K : Type u} [field K] {s : subfield K} {x : K} :

@[simp]
theorem subfield.coe_to_submonoid {K : Type u} [field K] (s : subfield K) :

@[simp]
theorem subfield.mem_to_add_subgroup {K : Type u} [field K] {s : subfield K} {x : K} :

@[simp]
theorem subfield.coe_to_add_subgroup {K : Type u} [field K] (s : subfield K) :

top

@[instance]
def subfield.has_top {K : Type u} [field K] :

The subfield of K containing all elements of K.

Equations
@[instance]
def subfield.inhabited {K : Type u} [field K] :

Equations
@[simp]
theorem subfield.mem_top {K : Type u} [field K] (x : K) :

@[simp]
theorem subfield.coe_top {K : Type u} [field K] :

comap

def subfield.comap {K : Type u} {L : Type v} [field K] [field L] :
(K →+* L)subfield Lsubfield K

The preimage of a subfield along a ring homomorphism is a subfield.

Equations
@[simp]
theorem subfield.coe_comap {K : Type u} {L : Type v} [field K] [field L] (f : K →+* L) (s : subfield L) :

@[simp]
theorem subfield.mem_comap {K : Type u} {L : Type v} [field K] [field L] {s : subfield L} {f : K →+* L} {x : K} :

theorem subfield.comap_comap {K : Type u} {L : Type v} {M : Type w} [field K] [field L] [field M] (s : subfield M) (g : L →+* M) (f : K →+* L) :

map

def subfield.map {K : Type u} {L : Type v} [field K] [field L] :
(K →+* L)subfield Ksubfield L

The image of a subfield along a ring homomorphism is a subfield.

Equations
@[simp]
theorem subfield.coe_map {K : Type u} {L : Type v} [field K] [field L] (s : subfield K) (f : K →+* L) :

@[simp]
theorem subfield.mem_map {K : Type u} {L : Type v} [field K] [field L] {f : K →+* L} {s : subfield K} {y : L} :
y subfield.map f s ∃ (x : K) (H : x s), f x = y

theorem subfield.map_map {K : Type u} {L : Type v} {M : Type w} [field K] [field L] [field M] (s : subfield K) (g : L →+* M) (f : K →+* L) :

theorem subfield.map_le_iff_le_comap {K : Type u} {L : Type v} [field K] [field L] {f : K →+* L} {s : subfield K} {t : subfield L} :

theorem subfield.gc_map_comap {K : Type u} {L : Type v} [field K] [field L] (f : K →+* L) :

range

def ring_hom.field_range {K : Type u} {L : Type v} [field K] [field L] :
(K →+* L)subfield L

The range of a ring homomorphism, as a subfield of the target.

Equations
@[simp]
theorem ring_hom.coe_field_range {K : Type u} {L : Type v} [field K] [field L] (f : K →+* L) :

@[simp]
theorem ring_hom.mem_field_range {K : Type u} {L : Type v} [field K] [field L] {f : K →+* L} {y : L} :
y f.range ∃ (x : K), f x = y

theorem ring_hom.map_field_range {K : Type u} {L : Type v} {M : Type w} [field K] [field L] [field M] (g : L →+* M) (f : K →+* L) :

inf

@[instance]
def subfield.has_inf {K : Type u} [field K] :

The inf of two subfields is their intersection.

Equations
@[simp]
theorem subfield.coe_inf {K : Type u} [field K] (p p' : subfield K) :
(p p') = p p'

@[simp]
theorem subfield.mem_inf {K : Type u} [field K] {p p' : subfield K} {x : K} :
x p p' x p x p'

@[instance]
def subfield.has_Inf {K : Type u} [field K] :

Equations
@[simp]
theorem subfield.coe_Inf {K : Type u} [field K] (S : set (subfield K)) :
(Inf S) = ⋂ (s : subfield K) (H : s S), s

theorem subfield.mem_Inf {K : Type u} [field K] {S : set (subfield K)} {x : K} :
x Inf S ∀ (p : subfield K), p Sx p

@[simp]
theorem subfield.Inf_to_subring {K : Type u} [field K] (s : set (subfield K)) :
(Inf s).to_subring = ⨅ (t : subfield K) (H : t s), t.to_subring

theorem subfield.is_glb_Inf {K : Type u} [field K] (S : set (subfield K)) :
is_glb S (Inf S)

subfield closure of a subset

def subfield.closure {K : Type u} [field K] :
set Ksubfield K

The subfield generated by a set.

Equations
theorem subfield.mem_closure_iff {K : Type u} [field K] {s : set K} {x : K} :
x subfield.closure s ∃ (y : K) (H : y subring.closure s) (z : K) (H : z subring.closure s), y / z = x

@[simp]
theorem subfield.subset_closure {K : Type u} [field K] {s : set K} :

The subfield generated by a set includes the set.

theorem subfield.mem_closure {K : Type u} [field K] {x : K} {s : set K} :
x subfield.closure s ∀ (S : subfield K), s Sx S

@[simp]
theorem subfield.closure_le {K : Type u} [field K] {s : set K} {t : subfield K} :

A subfield t includes closure s if and only if it includes s.

theorem subfield.closure_mono {K : Type u} [field K] ⦃s t : set K⦄ :

Subfield closure of a set is monotone in its argument: if s ⊆ t, then closure s ≤ closure t.

theorem subfield.closure_eq_of_le {K : Type u} [field K] {s : set K} {t : subfield K} :

theorem subfield.closure_induction {K : Type u} [field K] {s : set K} {p : K → Prop} {x : K} :
x subfield.closure s(∀ (x : K), x sp x)p 1(∀ (x y : K), p xp yp (x + y))(∀ (x : K), p xp (-x))(∀ (x : K), p xp x⁻¹)(∀ (x y : K), p xp yp (x * y))p x

An induction principle for closure membership. If p holds for 1, and all elements of s, and is preserved under addition, negation, and multiplication, then p holds for all elements of the closure of s.

closure forms a Galois insertion with the coercion to set.

Equations
theorem subfield.closure_eq {K : Type u} [field K] (s : subfield K) :

Closure of a subfield S equals S.

@[simp]
theorem subfield.closure_empty {K : Type u} [field K] :

@[simp]

theorem subfield.closure_Union {K : Type u} [field K] {ι : Sort u_1} (s : ι → set K) :
subfield.closure (⋃ (i : ι), s i) = ⨆ (i : ι), subfield.closure (s i)

theorem subfield.closure_sUnion {K : Type u} [field K] (s : set (set K)) :
subfield.closure (⋃₀s) = ⨆ (t : set K) (H : t s), subfield.closure t

theorem subfield.map_sup {K : Type u} {L : Type v} [field K] [field L] (s t : subfield K) (f : K →+* L) :

theorem subfield.map_supr {K : Type u} {L : Type v} [field K] [field L] {ι : Sort u_1} (f : K →+* L) (s : ι → subfield K) :
subfield.map f (supr s) = ⨆ (i : ι), subfield.map f (s i)

theorem subfield.comap_inf {K : Type u} {L : Type v} [field K] [field L] (s t : subfield L) (f : K →+* L) :

theorem subfield.comap_infi {K : Type u} {L : Type v} [field K] [field L] {ι : Sort u_1} (f : K →+* L) (s : ι → subfield L) :
subfield.comap f (infi s) = ⨅ (i : ι), subfield.comap f (s i)

@[simp]
theorem subfield.map_bot {K : Type u} {L : Type v} [field K] [field L] (f : K →+* L) :

@[simp]
theorem subfield.comap_top {K : Type u} {L : Type v} [field K] [field L] (f : K →+* L) :

theorem subfield.mem_supr_of_directed {K : Type u} [field K] {ι : Sort u_1} [hι : nonempty ι] {S : ι → subfield K} (hS : directed has_le.le S) {x : K} :
(x ⨆ (i : ι), S i) ∃ (i : ι), x S i

The underlying set of a non-empty directed Sup of subfields is just a union of the subfields. Note that this fails without the directedness assumption (the union of two subfields is typically not a subfield)

theorem subfield.coe_supr_of_directed {K : Type u} [field K] {ι : Sort u_1} [hι : nonempty ι] {S : ι → subfield K} :
directed has_le.le S((⨆ (i : ι), S i) = ⋃ (i : ι), (S i))

theorem subfield.mem_Sup_of_directed_on {K : Type u} [field K] {S : set (subfield K)} (Sne : S.nonempty) (hS : directed_on has_le.le S) {x : K} :
x Sup S ∃ (s : subfield K) (H : s S), x s

theorem subfield.coe_Sup_of_directed_on {K : Type u} [field K] {S : set (subfield K)} :
S.nonemptydirected_on has_le.le S((Sup S) = ⋃ (s : subfield K) (H : s S), s)

def ring_hom.cod_restrict_field {K : Type u} {L : Type v} [field K] [field L] (f : K →+* L) (s : subfield L) :
(∀ (x : K), f x s)K →+* s

Restrict the codomain of a ring homomorphism to a subfield that includes the range.

Equations
def ring_hom.restrict_field {K : Type u} {L : Type v} [field K] [field L] (f : K →+* L) (s : subfield K) :

Restriction of a ring homomorphism to a subfield of the domain.

Equations
@[simp]
theorem ring_hom.restrict_field_apply {K : Type u} {L : Type v} [field K] [field L] {s : subfield K} (f : K →+* L) (x : s) :

def ring_hom.range_restrict_field {K : Type u} {L : Type v} [field K] [field L] (f : K →+* L) :

Restriction of a ring homomorphism to its range interpreted as a subfield.

Equations
@[simp]
theorem ring_hom.coe_range_restrict_field {K : Type u} {L : Type v} [field K] [field L] (f : K →+* L) (x : K) :

def ring_hom.eq_locus_field {K : Type u} {L : Type v} [field K] [field L] :
(K →+* L)(K →+* L)subfield K

The subfield of elements x : R such that f x = g x, i.e., the equalizer of f and g as a subfield of R

Equations
theorem ring_hom.eq_on_field_closure {K : Type u} {L : Type v} [field K] [field L] {f g : K →+* L} {s : set K} :

If two ring homomorphisms are equal on a set, then they are equal on its subfield closure.

theorem ring_hom.eq_of_eq_on_subfield_top {K : Type u} {L : Type v} [field K] [field L] {f g : K →+* L} :

theorem ring_hom.eq_of_eq_on_of_field_closure_eq_top {K : Type u} {L : Type v} [field K] [field L] {s : set K} (hs : subfield.closure s = ) {f g : K →+* L} :
set.eq_on f g sf = g

theorem ring_hom.field_closure_preimage_le {K : Type u} {L : Type v} [field K] [field L] (f : K →+* L) (s : set L) :

theorem ring_hom.map_field_closure {K : Type u} {L : Type v} [field K] [field L] (f : K →+* L) (s : set K) :

The image under a ring homomorphism of the subfield generated by a set equals the subfield generated by the image of the set.

def subfield.inclusion {K : Type u} [field K] {S T : subfield K} :
S TS →+* T

The ring homomorphism associated to an inclusion of subfields.

Equations
@[simp]
theorem subfield.field_range_subtype {K : Type u} [field K] (s : subfield K) :

def ring_equiv.subfield_congr {K : Type u} [field K] {s t : subfield K} :
s = ts ≃+* t

Makes the identity isomorphism from a proof two subfields of a multiplicative monoid are equal.

Equations
theorem subfield.closure_preimage_le {K : Type u} {L : Type v} [field K] [field L] (f : K →+* L) (s : set L) :