Documentation

Mathlib.Algebra.Field.Subfield.Basic

Subfields #

Let K be a division ring, for example a field. This file concerns the "bundled" subfield type Subfield K, a type whose terms correspond to subfields of K. Note we do not require the "subfields" to be commutative, so they are really sub-division rings / skew fields. This is the preferred way to talk about subfields in mathlib. Unbundled subfields (s : Set K and IsSubfield 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 K to Subfield K, sending a subset of K to the subfield it generates, and prove that it is a Galois insertion.

Main definitions #

Notation used here:

(K : Type u) [DivisionRing K] (L : Type u) [DivisionRing 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 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

theorem Subfield.list_prod_mem {K : Type u} [DivisionRing K] (s : Subfield K) {l : List K} :
(∀ xl, x 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} [DivisionRing K] (s : Subfield K) {l : List K} :
(∀ xl, x s)l.sum s

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

theorem Subfield.multiset_sum_mem {K : Type u} [DivisionRing K] (s : Subfield K) (m : Multiset K) :
(∀ am, a s)m.sum s

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

theorem Subfield.sum_mem {K : Type u} [DivisionRing K] (s : Subfield K) {ι : Type u_1} {t : Finset ι} {f : ιK} (h : ct, f c s) :
it, f i s

Sum of elements in a Subfield indexed by a Finset is in the Subfield.

top #

instance Subfield.instTop {K : Type u} [DivisionRing K] :

The subfield of K containing all elements of K.

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

The ring equiv between the top element of Subfield K and K.

Equations

comap #

def Subfield.comap {K : Type u} {L : Type v} [DivisionRing K] [DivisionRing 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} [DivisionRing K] [DivisionRing L] (f : K →+* L) (s : Subfield L) :
(comap f s) = f ⁻¹' s
@[simp]
theorem Subfield.mem_comap {K : Type u} {L : Type v} [DivisionRing K] [DivisionRing L] {s : Subfield L} {f : K →+* L} {x : K} :
x comap f s f x s
theorem Subfield.comap_comap {K : Type u} {L : Type v} {M : Type w} [DivisionRing K] [DivisionRing L] [DivisionRing M] (s : Subfield M) (g : L →+* M) (f : K →+* L) :
comap f (comap g s) = comap (g.comp f) s

map #

def Subfield.map {K : Type u} {L : Type v} [DivisionRing K] [DivisionRing 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} [DivisionRing K] [DivisionRing L] (s : Subfield K) (f : K →+* L) :
(map f s) = f '' s
@[simp]
theorem Subfield.mem_map {K : Type u} {L : Type v} [DivisionRing K] [DivisionRing L] {f : K →+* L} {s : Subfield K} {y : L} :
y map f s xs, f x = y
theorem Subfield.map_map {K : Type u} {L : Type v} {M : Type w} [DivisionRing K] [DivisionRing L] [DivisionRing M] (s : Subfield K) (g : L →+* M) (f : K →+* L) :
map g (map f s) = map (g.comp f) s
theorem Subfield.map_le_iff_le_comap {K : Type u} {L : Type v} [DivisionRing K] [DivisionRing L] {f : K →+* L} {s : Subfield K} {t : Subfield L} :
map f s t s comap f t
theorem Subfield.gc_map_comap {K : Type u} {L : Type v} [DivisionRing K] [DivisionRing L] (f : K →+* L) :

range #

def RingHom.fieldRange {K : Type u} {L : Type v} [DivisionRing K] [DivisionRing L] (f : K →+* L) :

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

Equations
@[simp]
theorem RingHom.coe_fieldRange {K : Type u} {L : Type v} [DivisionRing K] [DivisionRing L] (f : K →+* L) :
@[simp]
theorem RingHom.mem_fieldRange {K : Type u} {L : Type v} [DivisionRing K] [DivisionRing L] {f : K →+* L} {y : L} :
y f.fieldRange ∃ (x : K), f x = y
theorem RingHom.map_fieldRange {K : Type u} {L : Type v} {M : Type w} [DivisionRing K] [DivisionRing L] [DivisionRing M] (g : L →+* M) (f : K →+* L) :
theorem RingHom.mem_fieldRange_self {K : Type u} {L : Type v} [DivisionRing K] [DivisionRing L] (f : K →+* L) (x : K) :
instance RingHom.fintypeFieldRange {K : Type u} {L : Type v} [DivisionRing K] [DivisionRing L] [Fintype K] [DecidableEq 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 #

instance Subfield.instMin {K : Type u} [DivisionRing K] :

The inf of two subfields is their intersection.

Equations
@[simp]
theorem Subfield.coe_inf {K : Type u} [DivisionRing K] (p p' : Subfield K) :
(pp') = p.carrier p'.carrier
@[simp]
theorem Subfield.mem_inf {K : Type u} [DivisionRing K] {p p' : Subfield K} {x : K} :
x pp' x p x p'
Equations
@[simp]
theorem Subfield.coe_sInf {K : Type u} [DivisionRing K] (S : Set (Subfield K)) :
(sInf S) = sS, s
theorem Subfield.mem_sInf {K : Type u} [DivisionRing K] {S : Set (Subfield K)} {x : K} :
x sInf S pS, x p
@[simp]
theorem Subfield.coe_iInf {K : Type u} [DivisionRing K] {ι : Sort u_1} {S : ιSubfield K} :
(⨅ (i : ι), S i) = ⋂ (i : ι), (S i)
theorem Subfield.mem_iInf {K : Type u} [DivisionRing K] {ι : Sort u_1} {S : ιSubfield K} {x : K} :
x ⨅ (i : ι), S i ∀ (i : ι), x S i
@[simp]
theorem Subfield.sInf_toSubring {K : Type u} [DivisionRing K] (s : Set (Subfield K)) :
(sInf s).toSubring = ts, t.toSubring
theorem Subfield.isGLB_sInf {K : Type u} [DivisionRing K] (S : Set (Subfield K)) :
IsGLB S (sInf S)

Subfields of a ring form a complete lattice.

Equations
  • One or more equations did not get rendered due to their size.

subfield closure of a subset #

def Subfield.closure {K : Type u} [DivisionRing K] (s : Set K) :

The Subfield generated by a set.

Equations
theorem Subfield.mem_closure {K : Type u} [DivisionRing K] {x : K} {s : Set K} :
x closure s ∀ (S : Subfield K), s Sx S
@[simp]
theorem Subfield.subset_closure {K : Type u} [DivisionRing K] {s : Set K} :
s (closure s)

The subfield generated by a set includes the set.

theorem Subfield.notMem_of_notMem_closure {K : Type u} [DivisionRing K] {s : Set K} {P : K} (hP : Pclosure s) :
Ps
@[deprecated Subfield.notMem_of_notMem_closure (since := "2025-05-23")]
theorem Subfield.not_mem_of_not_mem_closure {K : Type u} [DivisionRing K] {s : Set K} {P : K} (hP : Pclosure s) :
Ps

Alias of Subfield.notMem_of_notMem_closure.

@[simp]
theorem Subfield.closure_le {K : Type u} [DivisionRing K] {s : Set K} {t : Subfield K} :
closure s t s t

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

theorem Subfield.closure_mono {K : Type u} [DivisionRing 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} [DivisionRing K] {s : Set K} {t : Subfield K} (h₁ : s t) (h₂ : t closure s) :
theorem Subfield.closure_induction {K : Type u} [DivisionRing K] {s : Set K} {p : (x : K) → x closure sProp} (mem : ∀ (x : K) (hx : x s), p x ) (one : p 1 ) (add : ∀ (x y : K) (hx : x closure s) (hy : y closure s), p x hxp y hyp (x + y) ) (neg : ∀ (x : K) (hx : x closure s), p x hxp (-x) ) (inv : ∀ (x : K) (hx : x closure s), p x hxp x⁻¹ ) (mul : ∀ (x y : K) (hx : x closure s) (hy : y closure s), p x hxp y hyp (x * y) ) {x : K} (h : x closure s) :
p x h

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
@[simp]
theorem Subfield.closure_eq {K : Type u} [DivisionRing K] (s : Subfield K) :
closure s = s

Closure of a subfield S equals S.

theorem Subfield.closure_union {K : Type u} [DivisionRing K] (s t : Set K) :
closure (s t) = closure sclosure t
theorem Subfield.closure_iUnion {K : Type u} [DivisionRing K] {ι : Sort u_1} (s : ιSet K) :
closure (⋃ (i : ι), s i) = ⨆ (i : ι), closure (s i)
theorem Subfield.closure_sUnion {K : Type u} [DivisionRing K] (s : Set (Set K)) :
closure (⋃₀ s) = ts, closure t
theorem Subfield.map_sup {K : Type u} {L : Type v} [DivisionRing K] [DivisionRing L] (s t : Subfield K) (f : K →+* L) :
map f (st) = map f smap f t
theorem Subfield.map_iSup {K : Type u} {L : Type v} [DivisionRing K] [DivisionRing L] {ι : Sort u_1} (f : K →+* L) (s : ιSubfield K) :
map f (iSup s) = ⨆ (i : ι), map f (s i)
theorem Subfield.map_inf {K : Type u} {L : Type v} [DivisionRing K] [DivisionRing L] (s t : Subfield K) (f : K →+* L) :
map f (st) = map f smap f t
theorem Subfield.map_iInf {K : Type u} {L : Type v} [DivisionRing K] [DivisionRing L] {ι : Sort u_1} [Nonempty ι] (f : K →+* L) (s : ιSubfield K) :
map f (iInf s) = ⨅ (i : ι), map f (s i)
theorem Subfield.comap_inf {K : Type u} {L : Type v} [DivisionRing K] [DivisionRing L] (s t : Subfield L) (f : K →+* L) :
comap f (st) = comap f scomap f t
theorem Subfield.comap_iInf {K : Type u} {L : Type v} [DivisionRing K] [DivisionRing L] {ι : Sort u_1} (f : K →+* L) (s : ιSubfield L) :
comap f (iInf s) = ⨅ (i : ι), comap f (s i)
@[simp]
theorem Subfield.map_bot {K : Type u} {L : Type v} [DivisionRing K] [DivisionRing L] (f : K →+* L) :
@[simp]
theorem Subfield.comap_top {K : Type u} {L : Type v} [DivisionRing K] [DivisionRing L] (f : K →+* L) :
theorem Subfield.mem_iSup_of_directed {K : Type u} [DivisionRing K] {ι : Sort u_1} [ : Nonempty ι] {S : ιSubfield K} (hS : Directed (fun (x1 x2 : Subfield K) => x1 x2) S) {x : K} :
x ⨆ (i : ι), S i ∃ (i : ι), x S i

The underlying set of a non-empty directed sSup 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_iSup_of_directed {K : Type u} [DivisionRing K] {ι : Sort u_1} [ : Nonempty ι] {S : ιSubfield K} (hS : Directed (fun (x1 x2 : Subfield K) => x1 x2) S) :
(⨆ (i : ι), S i) = ⋃ (i : ι), (S i)
theorem Subfield.mem_sSup_of_directedOn {K : Type u} [DivisionRing K] {S : Set (Subfield K)} (Sne : S.Nonempty) (hS : DirectedOn (fun (x1 x2 : Subfield K) => x1 x2) S) {x : K} :
x sSup S sS, x s
theorem Subfield.coe_sSup_of_directedOn {K : Type u} [DivisionRing K] {S : Set (Subfield K)} (Sne : S.Nonempty) (hS : DirectedOn (fun (x1 x2 : Subfield K) => x1 x2) S) :
(sSup S) = sS, s
def RingHom.rangeRestrictField {K : Type u} {L : Type v} [DivisionRing K] [DivisionRing L] (f : K →+* L) :

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

Equations
@[simp]
theorem RingHom.coe_rangeRestrictField {K : Type u} {L : Type v} [DivisionRing K] [DivisionRing L] (f : K →+* L) (x : K) :
(f.rangeRestrictField x) = f x
def RingHom.eqLocusField {K : Type u} [DivisionRing K] {L : Type v} [Semiring 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
  • f.eqLocusField g = { carrier := {x : K | f x = g x}, mul_mem' := , one_mem' := , add_mem' := , zero_mem' := , neg_mem' := , inv_mem' := }
theorem RingHom.eqOn_field_closure {K : Type u} [DivisionRing K] {L : Type v} [Semiring L] {f g : K →+* L} {s : Set K} (h : Set.EqOn (⇑f) (⇑g) s) :
Set.EqOn f g (Subfield.closure s)

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

theorem RingHom.eq_of_eqOn_subfield_top {K : Type u} [DivisionRing K] {L : Type v} [Semiring L] {f g : K →+* L} (h : Set.EqOn f g ) :
f = g
theorem RingHom.eq_of_eqOn_of_field_closure_eq_top {K : Type u} [DivisionRing K] {L : Type v} [Semiring L] {s : Set K} (hs : Subfield.closure s = ) {f g : K →+* L} (h : Set.EqOn (⇑f) (⇑g) s) :
f = g
theorem RingHom.map_field_closure {K : Type u} {L : Type v} [DivisionRing K] [DivisionRing 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} [DivisionRing K] {S T : Subfield K} (h : S T) :
S →+* T

The ring homomorphism associated to an inclusion of subfields.

Equations
def RingEquiv.subfieldCongr {K : Type u} [DivisionRing K] {s t : Subfield K} (h : s = t) :
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} [DivisionRing K] [DivisionRing L] (f : K →+* L) (s : Set L) :
closure (f ⁻¹' s) comap f (closure s)
theorem Subfield.multiset_prod_mem {K : Type u} [Field K] (s : Subfield K) (m : Multiset K) :
(∀ am, a s)m.prod s

Product 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} (h : ct, f c s) :
it, f i s

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

instance Subfield.toAlgebra {K : Type u} [Field K] (s : Subfield K) :
Algebra (↥s) K
Equations
theorem Subfield.mem_closure_iff {K : Type u} [Field K] {s : Set K} {x : K} :
x closure s ySubring.closure s, zSubring.closure s, y / z = x
theorem Subfield.map_comap_eq {K : Type u} {L : Type v} [DivisionRing K] [DivisionRing L] (f : K →+* L) (s : Subfield L) :
map f (comap f s) = sf.fieldRange
theorem Subfield.map_comap_eq_self {K : Type u} {L : Type v} [DivisionRing K] [DivisionRing L] {f : K →+* L} {s : Subfield L} (h : s f.fieldRange) :
map f (comap f s) = s
theorem Subfield.map_comap_eq_self_of_surjective {K : Type u} {L : Type v} [DivisionRing K] [DivisionRing L] {f : K →+* L} (hf : Function.Surjective f) (s : Subfield L) :
map f (comap f s) = s
theorem Subfield.comap_map {K : Type u} {L : Type v} [DivisionRing K] [DivisionRing L] (f : K →+* L) (s : Subfield K) :
comap f (map f s) = s

Actions by Subfields #

These are just copies of the definitions about Subsemiring starting from Subsemiring.MulAction.

instance Subfield.instSMulSubtypeMem {K : Type u} [DivisionRing K] {X : Type u_1} [SMul K X] (F : Subfield K) :
SMul (↥F) X

The action by a subfield is the action by the underlying field.

Equations
theorem Subfield.smul_def {K : Type u} [DivisionRing K] {X : Type u_1} [SMul K X] {F : Subfield K} (g : F) (m : X) :
g m = g m
instance Subfield.smulCommClass_left {K : Type u} [DivisionRing K] {X : Type u_2} {Y : Type u_1} [SMul K Y] [SMul X Y] [SMulCommClass K X Y] (F : Subfield K) :
SMulCommClass (↥F) X Y
instance Subfield.smulCommClass_right {K : Type u} [DivisionRing K] {X : Type u_1} {Y : Type u_2} [SMul X Y] [SMul K Y] [SMulCommClass X K Y] (F : Subfield K) :
SMulCommClass X (↥F) Y
instance Subfield.instIsScalarTowerSubtypeMem {K : Type u} [DivisionRing K] {X : Type u_1} {Y : Type u_2} [SMul X Y] [SMul K X] [SMul K Y] [IsScalarTower K X Y] (F : Subfield K) :
IsScalarTower (↥F) X Y

Note that this provides IsScalarTower F K K which is needed by smul_mul_assoc.

instance Subfield.instFaithfulSMulSubtypeMem {K : Type u} [DivisionRing K] {X : Type u_1} [SMul K X] [FaithfulSMul K X] (F : Subfield K) :
FaithfulSMul (↥F) X
instance Subfield.instMulActionSubtypeMem {K : Type u} [DivisionRing K] {X : Type u_1} [MulAction K X] (F : Subfield K) :
MulAction (↥F) X

The action by a subfield is the action by the underlying field.

Equations

The action by a subfield is the action by the underlying field.

Equations

The action by a subfield is the action by the underlying field.

Equations
instance Subfield.instSMulWithZeroSubtypeMem {K : Type u} [DivisionRing K] {X : Type u_1} [Zero X] [SMulWithZero K X] (F : Subfield K) :
SMulWithZero (↥F) X

The action by a subfield is the action by the underlying field.

Equations

The action by a subfield is the action by the underlying field.

Equations
instance Subfield.instModuleSubtypeMem {K : Type u} [DivisionRing K] {X : Type u_1} [AddCommMonoid X] [Module K X] (F : Subfield K) :
Module (↥F) X

The action by a subfield is the action by the underlying field.

Equations

The action by a subfield is the action by the underlying field.

Equations