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

@[class]
structure subfield_class (S : Type u_1) (K : out_param (Type u_2)) [field K] [set_like S K] :
Type

subfield_class S K states S is a type of subsets s ⊆ K closed under field operations.

Instances
@[protected, instance]
def subfield_class.subfield_class.to_subgroup_class {K : Type u} [field K] (S : Type u_1) [set_like S K] [h : subfield_class S K] :

A subfield contains 1, products and inverses.

Be assured that we're not actually proving that subfields are subgroups: subgroup_class is really an abbreviation of subgroup_with_or_without_zero_class.

Equations
@[protected, instance]
def subfield_class.to_field {K : Type u} [field K] (S : Type u_1) [set_like S K] [h : subfield_class S K] (s : S) :

A subfield inherits a field structure

Equations
@[protected, instance]
def subfield_class.to_linear_ordered_field (S : Type u_1) {K : Type u_2} [linear_ordered_field K] [set_like S K] [subfield_class S K] (s : S) :

A subfield of a linear_ordered_field is a linear_ordered_field.

Equations
def subfield.to_subring {K : Type u} [field K] (self : subfield 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] (s : subfield K) :

The underlying add_subgroup of a subfield.

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

The underlying submonoid of a subfield.

Equations
@[protected, instance]
def subfield.set_like {K : Type u} [field K] :
Equations
@[protected, instance]
def subfield.subfield_class {K : Type u} [field K] :
Equations
@[simp]
theorem subfield.mem_carrier {K : Type u} [field K] {s : subfield K} {x : K} :
x s.carrier x s
@[simp]
theorem subfield.mem_mk {K : Type u} [field K] {S : set K} {x : K} (h₁ : ∀ {a b : K}, a Sb Sa * b S) (h₂ : 1 S) (h₃ : ∀ {a b : K}, a Sb Sa + b S) (h₄ : 0 S) (h₅ : ∀ {x : K}, x S-x S) (h₆ : ∀ (x : K), x Sx⁻¹ S) :
x {carrier := S, mul_mem' := h₁, one_mem' := h₂, add_mem' := h₃, zero_mem' := h₄, neg_mem' := h₅, inv_mem' := h₆} x S
@[simp]
theorem subfield.coe_set_mk {K : Type u} [field K] (S : set K) (h₁ : ∀ {a b : K}, a Sb Sa * b S) (h₂ : 1 S) (h₃ : ∀ {a b : K}, a Sb Sa + b S) (h₄ : 0 S) (h₅ : ∀ {x : K}, x S-x S) (h₆ : ∀ (x : K), x Sx⁻¹ S) :
{carrier := S, mul_mem' := h₁, one_mem' := h₂, add_mem' := h₃, zero_mem' := h₄, neg_mem' := h₅, inv_mem' := h₆} = S
@[simp]
theorem subfield.mk_le_mk {K : Type u} [field K] {S S' : set K} (h₁ : ∀ {a b : K}, a Sb Sa * b S) (h₂ : 1 S) (h₃ : ∀ {a b : K}, a Sb Sa + b S) (h₄ : 0 S) (h₅ : ∀ {x : K}, x S-x S) (h₆ : ∀ (x : K), x Sx⁻¹ S) (h₁' : ∀ {a b : K}, a S'b S'a * b S') (h₂' : 1 S') (h₃' : ∀ {a b : K}, a S'b S'a + b S') (h₄' : 0 S') (h₅' : ∀ {x : K}, x S'-x S') (h₆' : ∀ (x : K), x S'x⁻¹ S') :
{carrier := S, mul_mem' := h₁, one_mem' := h₂, add_mem' := h₃, zero_mem' := h₄, neg_mem' := h₅, inv_mem' := h₆} {carrier := S', mul_mem' := h₁', one_mem' := h₂', add_mem' := h₃', zero_mem' := h₄', neg_mem' := h₅', inv_mem' := h₆'} S S'
@[ext]
theorem subfield.ext {K : Type u} [field K] {S T : subfield K} (h : ∀ (x : K), x S x T) :
S = T

Two subfields are equal if they have the same elements.

@[protected]
def subfield.copy {K : Type u} [field K] (S : subfield K) (s : set K) (hs : s = S) :

Copy of a subfield with a new carrier equal to the old one. Useful to fix definitional equalities.

Equations
@[simp]
theorem subfield.coe_copy {K : Type u} [field K] (S : subfield K) (s : set K) (hs : s = S) :
(S.copy s hs) = s
theorem subfield.copy_eq {K : Type u} [field K] (S : subfield K) (s : set K) (hs : s = S) :
S.copy s hs = S
@[simp]
theorem subfield.coe_to_subring {K : Type u} [field K] (s : subfield K) :
@[simp]
theorem subfield.mem_to_subring {K : Type u} [field K] (s : subfield K) (x : K) :
def subring.to_subfield {K : Type u} [field K] (s : subring K) (hinv : ∀ (x : K), x sx⁻¹ s) :

A subring containing inverses is a subfield.

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

A subfield contains the field's 1.

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

A subfield contains the field's 0.

@[protected]
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.

@[protected]
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.

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

A subfield is closed under negation.

@[protected]
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.

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

A subfield is closed under inverses.

@[protected]
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.

@[protected]
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.

@[protected]
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.

@[protected]
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.

@[protected]
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.

@[protected]
theorem subfield.prod_mem {K : Type u} [field K] (s : subfield K) {ι : Type u_1} {t : finset ι} {f : ι → K} (h : ∀ (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.

@[protected]
theorem subfield.sum_mem {K : Type u} [field K] (s : subfield K) {ι : Type u_1} {t : finset ι} {f : ι → K} (h : ∀ (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.

@[protected]
theorem subfield.pow_mem {K : Type u} [field K] (s : subfield K) {x : K} (hx : x s) (n : ) :
x ^ n s
@[protected]
theorem subfield.zsmul_mem {K : Type u} [field K] (s : subfield K) {x : K} (hx : x s) (n : ) :
n x s
@[protected]
theorem subfield.coe_int_mem {K : Type u} [field K] (s : subfield K) (n : ) :
n s
theorem subfield.zpow_mem {K : Type u} [field K] (s : subfield K) {x : K} (hx : x s) (n : ) :
x ^ n s
@[protected, instance]
def subfield.ring {K : Type u} [field K] (s : subfield K) :
Equations
@[protected, instance]
def subfield.has_div {K : Type u} [field K] (s : subfield K) :
Equations
@[protected, instance]
def subfield.has_inv {K : Type u} [field K] (s : subfield K) :
Equations
@[protected, instance]
def subfield.int.has_pow {K : Type u} [field K] (s : subfield K) :
Equations
@[protected, instance]
def subfield.to_field {K : Type u} [field K] (s : subfield K) :

A subfield inherits a field structure

Equations
@[protected, instance]

A subfield of a linear_ordered_field is a linear_ordered_field.

Equations
@[simp, norm_cast]
theorem subfield.coe_add {K : Type u} [field K] (s : subfield K) (x y : s) :
(x + y) = x + y
@[simp, norm_cast]
theorem subfield.coe_sub {K : Type u} [field K] (s : subfield K) (x y : s) :
(x - y) = x - y
@[simp, norm_cast]
theorem subfield.coe_neg {K : Type u} [field K] (s : subfield K) (x : s) :
@[simp, norm_cast]
theorem subfield.coe_mul {K : Type u} [field K] (s : subfield K) (x y : s) :
x * y = (x) * y
@[simp, norm_cast]
theorem subfield.coe_div {K : Type u} [field K] (s : subfield K) (x y : s) :
(x / y) = x / y
@[simp, norm_cast]
theorem subfield.coe_inv {K : Type u} [field K] (s : subfield K) (x : s) :
@[simp, norm_cast]
theorem subfield.coe_zero {K : Type u} [field K] (s : subfield K) :
0 = 0
@[simp, norm_cast]
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
@[protected, 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 #

@[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 #

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

The subfield of K containing all elements of K.

Equations
@[protected, 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] (f : K →+* L) (s : subfield L) :

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] (f : K →+* L) (s : subfield K) :

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] (f : K →+* L) :

The range of a ring homomorphism, as a subfield of the target. See Note [range copy pattern].

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.field_range ∃ (x : K), f x = y
theorem ring_hom.field_range_eq_map {K : Type u} {L : Type v} [field K] [field L] (f : K →+* L) :
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) :
@[protected, instance]
def ring_hom.fintype_field_range {K : Type u} {L : Type v} [field K] [field L] [fintype K] [decidable_eq L] (f : K →+* L) :

The range of a morphism of fields is a fintype, if the domain is a fintype.

Note that this instance can cause a diamond with subtype.fintype if L is also a fintype.

Equations

inf #

@[protected, 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'
@[protected, instance]
def subfield.has_Inf {K : Type u} [field K] :
Equations
@[simp, norm_cast]
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] (s : set 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.not_mem_of_not_mem_closure {K : Type u} [field K] {s : set K} {P : K} (hP : P subfield.closure s) :
P s
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⦄ (h : s t) :

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} (h₁ : s t) (h₂ : t subfield.closure s) :
theorem subfield.closure_induction {K : Type u} [field K] {s : set K} {p : K → Prop} {x : K} (h : x subfield.closure s) (Hs : ∀ (x : K), x sp x) (H1 : p 1) (Hadd : ∀ (x y : K), p xp yp (x + y)) (Hneg : ∀ (x : K), p xp (-x)) (Hinv : ∀ (x : K), p xp x⁻¹) (Hmul : ∀ (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.

@[protected]

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} (hS : 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)} (Sne : S.nonempty) (hS : directed_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) (h : ∀ (x : K), f x 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] (f g : K →+* L) :

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} (h : set.eq_on f g s) :

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} (h : set.eq_on f g ) :
f = g
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} (h : set.eq_on f g s) :
f = 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} (h : S 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} (h : s = 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) :