# Subfields #

Let K be a division ring, for example a field. This file defines 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)

• Subfield K : the type of subfields of a division ring K.

• instance : CompleteLattice (Subfield K) : the complete lattice structure on the subfields.

• Subfield.closure : subfield closure of a set, i.e., the smallest subfield that includes the set.

• Subfield.gi : closure : Set M → Subfield M and coercion (↑) : Subfield M → Set M form a GaloisInsertion.

• comap f B : Subfield K : the preimage of a subfield B along the ring homomorphism f

• map f A : Subfield L : the image of a subfield A along the ring homomorphism f.

• f.fieldRange : Subfield L : the range of the ring homomorphism f.

• eqLocusField f g : Subfield K : given ring homomorphisms f g : K →+* R, the subfield of K where f x = g x

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

class SubfieldClass (S : Type u_1) (K : Type u_2) [] [SetLike S K] extends , :

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

Instances
@[instance 100]
instance SubfieldClass.toSubgroupClass {K : Type u} [] (S : Type u_1) [SetLike S K] [h : ] :

A subfield contains 1, products and inverses.

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

Equations
• =
theorem SubfieldClass.nnratCast_mem {K : Type u} [] {S : Type u_1} [SetLike S K] [h : ] (s : S) (q : ℚ≥0) :
q s
theorem SubfieldClass.ratCast_mem {K : Type u} [] {S : Type u_1} [SetLike S K] [h : ] (s : S) (q : ) :
q s
instance SubfieldClass.instNNRatCast {K : Type u} [] {S : Type u_1} [SetLike S K] [h : ] (s : S) :
NNRatCast { x : K // x s }
Equations
• = { nnratCast := fun (q : ℚ≥0) => q, }
instance SubfieldClass.instRatCast {K : Type u} [] {S : Type u_1} [SetLike S K] [h : ] (s : S) :
RatCast { x : K // x s }
Equations
• = { ratCast := fun (q : ) => q, }
@[simp]
theorem SubfieldClass.coe_nnratCast {K : Type u} [] {S : Type u_1} [SetLike S K] [h : ] (s : S) (q : ℚ≥0) :
q = q
@[simp]
theorem SubfieldClass.coe_ratCast {K : Type u} [] {S : Type u_1} [SetLike S K] [h : ] (s : S) (x : ) :
x = x
theorem SubfieldClass.nnqsmul_mem {K : Type u} [] {S : Type u_1} [SetLike S K] [h : ] {x : K} (s : S) (q : ℚ≥0) (hx : x s) :
q x s
theorem SubfieldClass.qsmul_mem {K : Type u} [] {S : Type u_1} [SetLike S K] [h : ] {x : K} (s : S) (q : ) (hx : x s) :
q x s
@[deprecated SubfieldClass.coe_ratCast]
theorem SubfieldClass.coe_rat_cast {K : Type u} [] {S : Type u_1} [SetLike S K] [h : ] (s : S) (x : ) :
x = x

Alias of SubfieldClass.coe_ratCast.

@[deprecated SubfieldClass.ratCast_mem]
theorem SubfieldClass.coe_rat_mem {K : Type u} [] {S : Type u_1} [SetLike S K] [h : ] (s : S) (q : ) :
q s

Alias of SubfieldClass.ratCast_mem.

@[deprecated SubfieldClass.qsmul_mem]
theorem SubfieldClass.rat_smul_mem {K : Type u} [] {S : Type u_1} [SetLike S K] [h : ] {x : K} (s : S) (q : ) (hx : x s) :
q x s

Alias of SubfieldClass.qsmul_mem.

theorem SubfieldClass.ofScientific_mem {K : Type u} [] {S : Type u_1} [SetLike S K] [h : ] (s : S) {b : Bool} {n : } {m : } :
s
instance SubfieldClass.instSMulNNRat {K : Type u} [] {S : Type u_1} [SetLike S K] [h : ] (s : S) :
SMul ℚ≥0 { x : K // x s }
Equations
• = { smul := fun (q : ℚ≥0) (x : { x : K // x s }) => q x, }
instance SubfieldClass.instSMulRat {K : Type u} [] {S : Type u_1} [SetLike S K] [h : ] (s : S) :
SMul { x : K // x s }
Equations
• = { smul := fun (q : ) (x : { x : K // x s }) => q x, }
@[simp]
theorem SubfieldClass.coe_nnqsmul {K : Type u} [] {S : Type u_1} [SetLike S K] [h : ] (s : S) (q : ℚ≥0) (x : { x : K // x s }) :
(q x) = q x
@[simp]
theorem SubfieldClass.coe_qsmul {K : Type u} [] {S : Type u_1} [SetLike S K] [h : ] (s : S) (q : ) (x : { x : K // x s }) :
(q x) = q x
@[instance 75]
instance SubfieldClass.toDivisionRing {K : Type u} [] (S : Type u_1) [SetLike S K] [h : ] (s : S) :
DivisionRing { x : K // x s }

A subfield inherits a division ring structure

Equations
@[instance 75]
instance SubfieldClass.toField (S : Type u_1) {K : Type u_2} [] [SetLike S K] [] (s : S) :
Field { x : K // x s }

A subfield of a field inherits a field structure

Equations
structure Subfield (K : Type u) [] extends :

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.

• carrier : Set K
• mul_mem' : ∀ {a b : K}, a self.carrierb self.carriera * b self.carrier
• one_mem' : 1 self.carrier
• add_mem' : ∀ {a b : K}, a self.carrierb self.carriera + b self.carrier
• zero_mem' : 0 self.carrier
• neg_mem' : ∀ {x : K}, x self.carrier-x self.carrier
• inv_mem' : xself.carrier, x⁻¹ self.carrier

A subfield is closed under multiplicative inverses.

Instances For
theorem Subfield.inv_mem' {K : Type u} [] (self : ) (x : K) :
x self.carrierx⁻¹ self.carrier

A subfield is closed under multiplicative inverses.

def Subfield.toAddSubgroup {K : Type u} [] (s : ) :

The underlying AddSubgroup of a subfield.

Equations
Instances For
instance Subfield.instSetLike {K : Type u} [] :
Equations
• Subfield.instSetLike = { coe := fun (s : ) => s.carrier, coe_injective' := }
instance Subfield.instSubfieldClass {K : Type u} [] :
Equations
• =
theorem Subfield.mem_carrier {K : Type u} [] {s : } {x : K} :
x s.carrier x s
@[simp]
theorem Subfield.mem_mk {K : Type u} [] {S : } {x : K} (h : xS.carrier, x⁻¹ S.carrier) :
x { toSubring := S, inv_mem' := h } x S
@[simp]
theorem Subfield.coe_set_mk {K : Type u} [] (S : ) (h : xS.carrier, x⁻¹ S.carrier) :
{ toSubring := S, inv_mem' := h } = S
@[simp]
theorem Subfield.mk_le_mk {K : Type u} [] {S : } {S' : } (h : xS.carrier, x⁻¹ S.carrier) (h' : xS'.carrier, x⁻¹ S'.carrier) :
{ toSubring := S, inv_mem' := h } { toSubring := S', inv_mem' := h' } S S'
theorem Subfield.ext_iff {K : Type u} [] {S : } {T : } :
S = T ∀ (x : K), x S x T
theorem Subfield.ext {K : Type u} [] {S : } {T : } (h : ∀ (x : K), x S x T) :
S = T

Two subfields are equal if they have the same elements.

def Subfield.copy {K : Type u} [] (S : ) (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
• S.copy s hs = { carrier := s, mul_mem' := , one_mem' := , add_mem' := , zero_mem' := , neg_mem' := , inv_mem' := }
Instances For
@[simp]
theorem Subfield.coe_copy {K : Type u} [] (S : ) (s : Set K) (hs : s = S) :
(S.copy s hs) = s
theorem Subfield.copy_eq {K : Type u} [] (S : ) (s : Set K) (hs : s = S) :
S.copy s hs = S
@[simp]
theorem Subfield.coe_toSubring {K : Type u} [] (s : ) :
s.toSubring = s
@[simp]
theorem Subfield.mem_toSubring {K : Type u} [] (s : ) (x : K) :
x s.toSubring x s
def Subring.toSubfield {K : Type u} [] (s : ) (hinv : xs, x⁻¹ s) :

A Subring containing inverses is a Subfield.

Equations
• s.toSubfield hinv = { toSubring := s, inv_mem' := hinv }
Instances For
theorem Subfield.one_mem {K : Type u} [] (s : ) :
1 s

A subfield contains the field's 1.

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

A subfield contains the field's 0.

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

A subfield is closed under multiplication.

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

A subfield is closed under addition.

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

A subfield is closed under negation.

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

A subfield is closed under subtraction.

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

A subfield is closed under inverses.

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

A subfield is closed under division.

theorem Subfield.list_prod_mem {K : Type u} [] (s : ) {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} [] (s : ) {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} [] (s : ) (m : ) :
(∀ 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} [] (s : ) {ι : Type u_1} {t : } {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.

theorem Subfield.pow_mem {K : Type u} [] (s : ) {x : K} (hx : x s) (n : ) :
x ^ n s
theorem Subfield.zsmul_mem {K : Type u} [] (s : ) {x : K} (hx : x s) (n : ) :
n x s
theorem Subfield.intCast_mem {K : Type u} [] (s : ) (n : ) :
n s
@[deprecated intCast_mem]
theorem Subfield.coe_int_mem {R : Type u} {S : Type v} [Ring R] [SetLike S R] [hSR : ] (s : S) (n : ) :
n s

Alias of intCast_mem.

theorem Subfield.zpow_mem {K : Type u} [] (s : ) {x : K} (hx : x s) (n : ) :
x ^ n s
instance Subfield.instRingSubtypeMem {K : Type u} [] (s : ) :
Ring { x : K // x s }
Equations
• s.instRingSubtypeMem = s.toRing
instance Subfield.instDivSubtypeMem {K : Type u} [] (s : ) :
Div { x : K // x s }
Equations
• s.instDivSubtypeMem = { div := fun (x y : { x : K // x s }) => x / y, }
instance Subfield.instInvSubtypeMem {K : Type u} [] (s : ) :
Inv { x : K // x s }
Equations
• s.instInvSubtypeMem = { inv := fun (x : { x : K // x s }) => (↑x)⁻¹, }
instance Subfield.instPowSubtypeMemInt {K : Type u} [] (s : ) :
Pow { x : K // x s }
Equations
• s.instPowSubtypeMemInt = { pow := fun (x : { x : K // x s }) (z : ) => x ^ z, }
instance Subfield.toDivisionRing {K : Type u} [] (s : ) :
DivisionRing { x : K // x s }
Equations
instance Subfield.toField {K : Type u_1} [] (s : ) :
Field { x : K // x s }

A subfield inherits a field structure

Equations
@[simp]
theorem Subfield.coe_add {K : Type u} [] (s : ) (x : { x : K // x s }) (y : { x : K // x s }) :
(x + y) = x + y
@[simp]
theorem Subfield.coe_sub {K : Type u} [] (s : ) (x : { x : K // x s }) (y : { x : K // x s }) :
(x - y) = x - y
@[simp]
theorem Subfield.coe_neg {K : Type u} [] (s : ) (x : { x : K // x s }) :
(-x) = -x
@[simp]
theorem Subfield.coe_mul {K : Type u} [] (s : ) (x : { x : K // x s }) (y : { x : K // x s }) :
(x * y) = x * y
@[simp]
theorem Subfield.coe_div {K : Type u} [] (s : ) (x : { x : K // x s }) (y : { x : K // x s }) :
(x / y) = x / y
@[simp]
theorem Subfield.coe_inv {K : Type u} [] (s : ) (x : { x : K // x s }) :
x⁻¹ = (↑x)⁻¹
@[simp]
theorem Subfield.coe_zero {K : Type u} [] (s : ) :
0 = 0
@[simp]
theorem Subfield.coe_one {K : Type u} [] (s : ) :
1 = 1
def Subfield.subtype {K : Type u} [] (s : ) :
{ x : K // x s } →+* K

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

Equations
• s.subtype = { toFun := Subtype.val, map_one' := , map_mul' := , map_zero' := , map_add' := }
Instances For
@[simp]
theorem Subfield.coe_subtype {K : Type u} [] (s : ) :
s.subtype = Subtype.val
theorem Subfield.toSubring_subtype_eq_subtype (K : Type u) [] (S : ) :
S.subtype = S.subtype

# Partial order #

theorem Subfield.mem_toSubmonoid {K : Type u} [] {s : } {x : K} :
x s.toSubmonoid x s
@[simp]
theorem Subfield.coe_toSubmonoid {K : Type u} [] (s : ) :
s.toSubmonoid = s
@[simp]
theorem Subfield.mem_toAddSubgroup {K : Type u} [] {s : } {x : K} :
@[simp]
theorem Subfield.coe_toAddSubgroup {K : Type u} [] (s : ) :

# top #

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

The subfield of K containing all elements of K.

Equations
• Subfield.instTop = { top := let __src := ; { toSubring := __src, inv_mem' := } }
instance Subfield.instInhabited {K : Type u} [] :
Equations
• Subfield.instInhabited = { default := }
@[simp]
theorem Subfield.mem_top {K : Type u} [] (x : K) :
@[simp]
theorem Subfield.coe_top {K : Type u} [] :
= Set.univ
def Subfield.topEquiv {K : Type u} [] :
{ x : K // x } ≃+* K

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

Equations
• Subfield.topEquiv = Subsemiring.topEquiv
Instances For

# comap #

def Subfield.comap {K : Type u} {L : Type v} [] [] (f : K →+* L) (s : ) :

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

Equations
Instances For
@[simp]
theorem Subfield.coe_comap {K : Type u} {L : Type v} [] [] (f : K →+* L) (s : ) :
(Subfield.comap f s) = f ⁻¹' s
@[simp]
theorem Subfield.mem_comap {K : Type u} {L : Type v} [] [] {s : } {f : K →+* L} {x : K} :
x f x s
theorem Subfield.comap_comap {K : Type u} {L : Type v} {M : Type w} [] [] [] (s : ) (g : L →+* M) (f : K →+* L) :

# map #

def Subfield.map {K : Type u} {L : Type v} [] [] (f : K →+* L) (s : ) :

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

Equations
• = { toSubring := Subring.map f s.toSubring, inv_mem' := }
Instances For
@[simp]
theorem Subfield.coe_map {K : Type u} {L : Type v} [] [] (s : ) (f : K →+* L) :
(Subfield.map f s) = f '' s
@[simp]
theorem Subfield.mem_map {K : Type u} {L : Type v} [] [] {f : K →+* L} {s : } {y : L} :
y xs, f x = y
theorem Subfield.map_map {K : Type u} {L : Type v} {M : Type w} [] [] [] (s : ) (g : L →+* M) (f : K →+* L) :
theorem Subfield.map_le_iff_le_comap {K : Type u} {L : Type v} [] [] {f : K →+* L} {s : } {t : } :
t s
theorem Subfield.gc_map_comap {K : Type u} {L : Type v} [] [] (f : K →+* L) :

# range #

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

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

Equations
Instances For
@[simp]
theorem RingHom.coe_fieldRange {K : Type u} {L : Type v} [] [] (f : K →+* L) :
f.fieldRange =
@[simp]
theorem RingHom.mem_fieldRange {K : Type u} {L : Type v} [] [] {f : K →+* L} {y : L} :
y f.fieldRange ∃ (x : K), f x = y
theorem RingHom.fieldRange_eq_map {K : Type u} {L : Type v} [] [] (f : K →+* L) :
f.fieldRange =
theorem RingHom.map_fieldRange {K : Type u} {L : Type v} {M : Type w} [] [] [] (g : L →+* M) (f : K →+* L) :
Subfield.map g f.fieldRange = (g.comp f).fieldRange
instance RingHom.fintypeFieldRange {K : Type u} {L : Type v} [] [] [] [] (f : K →+* L) :
Fintype { x : L // x f.fieldRange }

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
• f.fintypeFieldRange =

# inf #

instance Subfield.instInf {K : Type u} [] :

The inf of two subfields is their intersection.

Equations
• Subfield.instInf = { inf := fun (s t : ) => let __src := s.toSubring t.toSubring; { toSubring := __src, inv_mem' := } }
@[simp]
theorem Subfield.coe_inf {K : Type u} [] (p : ) (p' : ) :
(p p') = p.carrier p'.carrier
@[simp]
theorem Subfield.mem_inf {K : Type u} [] {p : } {p' : } {x : K} :
x p p' x p x p'
instance Subfield.instInfSet {K : Type u} [] :
Equations
• Subfield.instInfSet = { sInf := fun (S : Set (Subfield K)) => let __src := sInf (Subfield.toSubring '' S); { toSubring := __src, inv_mem' := } }
@[simp]
theorem Subfield.coe_sInf {K : Type u} [] (S : Set (Subfield K)) :
(sInf S) = sS, s
theorem Subfield.mem_sInf {K : Type u} [] {S : Set (Subfield K)} {x : K} :
x sInf S pS, x p
@[simp]
theorem Subfield.sInf_toSubring {K : Type u} [] (s : Set (Subfield K)) :
(sInf s).toSubring = ts, t.toSubring
theorem Subfield.isGLB_sInf {K : Type u} [] (S : Set (Subfield K)) :
IsGLB S (sInf S)
instance Subfield.instCompleteLattice {K : Type u} [] :

Subfields of a ring form a complete lattice.

Equations

# subfield closure of a subset #

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

The Subfield generated by a set.

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

The subfield generated by a set includes the set.

theorem Subfield.subring_closure_le {K : Type u} [] (s : Set K) :
.toSubring
theorem Subfield.not_mem_of_not_mem_closure {K : Type u} [] {s : Set K} {P : K} (hP : P) :
Ps
@[simp]
theorem Subfield.closure_le {K : Type u} [] {s : Set K} {t : } :
s t

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

theorem Subfield.closure_mono {K : Type u} [] ⦃s : Set K ⦃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} [] {s : Set K} {t : } (h₁ : s t) (h₂ : ) :
theorem Subfield.closure_induction {K : Type u} [] {s : Set K} {p : KProp} {x : K} (h : ) (mem : xs, p x) (one : p 1) (add : ∀ (x y : K), p xp yp (x + y)) (neg : ∀ (x : K), p xp (-x)) (inv : ∀ (x : K), p xp x⁻¹) (mul : ∀ (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.

def Subfield.gi (K : Type u) [] :
GaloisInsertion Subfield.closure SetLike.coe

closure forms a Galois insertion with the coercion to set.

Equations
• = { choice := fun (s : Set K) (x : s) => , gc := , le_l_u := , choice_eq := }
Instances For
theorem Subfield.closure_eq {K : Type u} [] (s : ) :

Closure of a subfield S equals S.

@[simp]
theorem Subfield.closure_empty {K : Type u} [] :
@[simp]
theorem Subfield.closure_univ {K : Type u} [] :
theorem Subfield.closure_union {K : Type u} [] (s : Set K) (t : Set K) :
theorem Subfield.closure_iUnion {K : Type u} [] {ι : Sort u_1} (s : ιSet K) :
Subfield.closure (⋃ (i : ι), s i) = ⨆ (i : ι), Subfield.closure (s i)
theorem Subfield.closure_sUnion {K : Type u} [] (s : Set (Set K)) :
= ts,
theorem Subfield.map_sup {K : Type u} {L : Type v} [] [] (s : ) (t : ) (f : K →+* L) :
theorem Subfield.map_iSup {K : Type u} {L : Type v} [] [] {ι : Sort u_1} (f : K →+* L) (s : ι) :
Subfield.map f (iSup s) = ⨆ (i : ι), Subfield.map f (s i)
theorem Subfield.comap_inf {K : Type u} {L : Type v} [] [] (s : ) (t : ) (f : K →+* L) :
theorem Subfield.comap_iInf {K : Type u} {L : Type v} [] [] {ι : Sort u_1} (f : K →+* L) (s : ι) :
Subfield.comap f (iInf s) = ⨅ (i : ι), Subfield.comap f (s i)
@[simp]
theorem Subfield.map_bot {K : Type u} {L : Type v} [] [] (f : K →+* L) :
@[simp]
theorem Subfield.comap_top {K : Type u} {L : Type v} [] [] (f : K →+* L) :
theorem Subfield.mem_iSup_of_directed {K : Type u} [] {ι : Sort u_1} [hι : ] {S : ι} (hS : Directed (fun (x1 x2 : ) => 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} [] {ι : Sort u_1} [hι : ] {S : ι} (hS : Directed (fun (x1 x2 : ) => x1 x2) S) :
(⨆ (i : ι), S i) = ⋃ (i : ι), (S i)
theorem Subfield.mem_sSup_of_directedOn {K : Type u} [] {S : Set (Subfield K)} (Sne : S.Nonempty) (hS : DirectedOn (fun (x1 x2 : ) => x1 x2) S) {x : K} :
x sSup S sS, x s
theorem Subfield.coe_sSup_of_directedOn {K : Type u} [] {S : Set (Subfield K)} (Sne : S.Nonempty) (hS : DirectedOn (fun (x1 x2 : ) => x1 x2) S) :
(sSup S) = sS, s
def RingHom.rangeRestrictField {K : Type u} {L : Type v} [] [] (f : K →+* L) :
K →+* { x : L // x f.fieldRange }

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

Equations
• f.rangeRestrictField = f.rangeSRestrict
Instances For
@[simp]
theorem RingHom.coe_rangeRestrictField {K : Type u} {L : Type v} [] [] (f : K →+* L) (x : K) :
(f.rangeRestrictField x) = f x
def RingHom.eqLocusField {K : Type u} [] {L : Type v} [] (f : K →+* L) (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' := }
Instances For
theorem RingHom.eqOn_field_closure {K : Type u} [] {L : Type v} [] {f : K →+* L} {g : K →+* L} {s : Set K} (h : Set.EqOn (⇑f) (⇑g) s) :
Set.EqOn f g

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

The ring homomorphism associated to an inclusion of subfields.

Equations
• = S.subtype.codRestrict T
Instances For
@[simp]
theorem Subfield.fieldRange_subtype {K : Type u} [] (s : ) :
s.subtype.fieldRange = s
def RingEquiv.subfieldCongr {K : Type u} [] {s : } {t : } (h : s = t) :
{ x : K // x s } ≃+* { x : K // x t }

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

Equations
• = { toEquiv := , map_mul' := , map_add' := }
Instances For
theorem Subfield.closure_preimage_le {K : Type u} {L : Type v} [] [] (f : K →+* L) (s : Set L) :
theorem Subfield.multiset_prod_mem {K : Type u} [] (s : ) (m : ) :
(∀ 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} [] (s : ) {ι : Type u_1} {t : } {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} [] (s : ) :
Algebra { x : K // x s } K
Equations
• s.toAlgebra = s.subtype.toAlgebra
theorem Subfield.mem_closure_iff {K : Type u} [] {s : Set K} {x : K} :
y, z, y / z = x
theorem Subfield.map_comap_eq {K : Type u} {L : Type v} [] [] (f : K →+* L) (s : ) :
Subfield.map f (Subfield.comap f s) = s f.fieldRange
theorem Subfield.map_comap_eq_self {K : Type u} {L : Type v} [] [] {f : K →+* L} {s : } (h : s f.fieldRange) :
theorem Subfield.map_comap_eq_self_of_surjective {K : Type u} {L : Type v} [] [] {f : K →+* L} (hf : ) (s : ) :
theorem Subfield.comap_map {K : Type u} {L : Type v} [] [] (f : K →+* L) (s : ) :