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

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

source
class SubfieldClass (S : Type u_1) (K : Type u_2) [DivisionRing K] [SetLike S K] extends SubringClass S K, InvMemClass S K :
Prop

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

- mul_mem {s : S} {a b : K} : a ∈ s → b ∈ s → a * b ∈ s
- one_mem (s : S) : 1 ∈ s
- add_mem {s : S} {a b : K} : a ∈ s → b ∈ s → a + b ∈ s
- zero_mem (s : S) : 0 ∈ s
- neg_mem {s : S} {x : K} : x ∈ s → -x ∈ s
- inv_mem {s : S} {x : K} : x ∈ s → x⁻¹ ∈ s

Instances

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

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`.

source
@[simp]
theorem SubfieldClass.nnratCast_mem {K : Type u} [DivisionRing K] {S : Type u_1} [SetLike S K] [h : SubfieldClass S K] (s : S) (q : ℚ≥0) :
↑q ∈ s
source
@[simp]
theorem SubfieldClass.ratCast_mem {K : Type u} [DivisionRing K] {S : Type u_1} [SetLike S K] [h : SubfieldClass S K] (s : S) (q : ℚ) :
↑q ∈ s
source
instance SubfieldClass.instNNRatCast {K : Type u} [DivisionRing K] {S : Type u_1} [SetLike S K] [h : SubfieldClass S K] (s : S) :
NNRatCast ↥s
Equations

- SubfieldClass.instNNRatCast s = { nnratCast := fun (q : ℚ≥0) => ⟨↑q, ⋯⟩ }

source
instance SubfieldClass.instRatCast {K : Type u} [DivisionRing K] {S : Type u_1} [SetLike S K] [h : SubfieldClass S K] (s : S) :
RatCast ↥s
Equations

- SubfieldClass.instRatCast s = { ratCast := fun (q : ℚ) => ⟨↑q, ⋯⟩ }

source
@[simp]
theorem SubfieldClass.coe_nnratCast {K : Type u} [DivisionRing K] {S : Type u_1} [SetLike S K] [h : SubfieldClass S K] (s : S) (q : ℚ≥0) :
↑↑q = ↑q
source
@[simp]
theorem SubfieldClass.coe_ratCast {K : Type u} [DivisionRing K] {S : Type u_1} [SetLike S K] [h : SubfieldClass S K] (s : S) (x : ℚ) :
↑↑x = ↑x
source
theorem SubfieldClass.nnqsmul_mem {K : Type u} [DivisionRing K] {S : Type u_1} [SetLike S K] [h : SubfieldClass S K] {x : K} (s : S) (q : ℚ≥0) (hx : x ∈ s) :
q • x ∈ s
source
theorem SubfieldClass.qsmul_mem {K : Type u} [DivisionRing K] {S : Type u_1} [SetLike S K] [h : SubfieldClass S K] {x : K} (s : S) (q : ℚ) (hx : x ∈ s) :
q • x ∈ s
source
@[simp]
theorem SubfieldClass.ofScientific_mem {K : Type u} [DivisionRing K] {S : Type u_1} [SetLike S K] [h : SubfieldClass S K] (s : S) {b : Bool} {n m : ℕ} :
OfScientific.ofScientific n b m ∈ s
source
instance SubfieldClass.instSMulNNRat {K : Type u} [DivisionRing K] {S : Type u_1} [SetLike S K] [h : SubfieldClass S K] (s : S) :
SMul ℚ≥0 ↥s
Equations

- SubfieldClass.instSMulNNRat s = { smul := fun (q : ℚ≥0) (x : ↥s) => ⟨q • ↑x, ⋯⟩ }

source
instance SubfieldClass.instSMulRat {K : Type u} [DivisionRing K] {S : Type u_1} [SetLike S K] [h : SubfieldClass S K] (s : S) :
SMul ℚ ↥s
Equations

- SubfieldClass.instSMulRat s = { smul := fun (q : ℚ) (x : ↥s) => ⟨q • ↑x, ⋯⟩ }

source
@[simp]
theorem SubfieldClass.coe_nnqsmul {K : Type u} [DivisionRing K] {S : Type u_1} [SetLike S K] [h : SubfieldClass S K] (s : S) (q : ℚ≥0) (x : ↥s) :
↑(q • x) = q • ↑x
source
@[simp]
theorem SubfieldClass.coe_qsmul {K : Type u} [DivisionRing K] {S : Type u_1} [SetLike S K] [h : SubfieldClass S K] (s : S) (q : ℚ) (x : ↥s) :
↑(q • x) = q • ↑x
source
@[instance 75]
instance SubfieldClass.toDivisionRing {K : Type u} [DivisionRing K] (S : Type u_1) [SetLike S K] [h : SubfieldClass S K] (s : S) :
DivisionRing ↥s

A subfield inherits a division ring structure

Equations

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

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

A subfield of a field inherits a field structure

Equations

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

source
structure Subfield (K : Type u) [DivisionRing K] extends Subring 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.

- carrier : Set K
- mul_mem' {a b : K} : a ∈ self.carrier → b ∈ self.carrier → a * b ∈ self.carrier
- one_mem' : 1 ∈ self.carrier
- add_mem' {a b : K} : a ∈ self.carrier → b ∈ self.carrier → a + b ∈ self.carrier
- zero_mem' : 0 ∈ self.carrier
- neg_mem' {x : K} : x ∈ self.carrier → -x ∈ self.carrier
- inv_mem' (x : K) : x ∈ self.carrier → x⁻¹ ∈ self.carrier

  A subfield is closed under multiplicative inverses.

Instances For

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

The underlying `AddSubgroup` of a subfield.

Equations

- s.toAddSubgroup = s.toAddSubgroup

Instances For

source
instance Subfield.instSetLike {K : Type u} [DivisionRing K] :
SetLike (Subfield K) K
Equations

- Subfield.instSetLike = { coe := fun (s : Subfield K) => s.carrier, coe_injective' := ⋯ }

source
instance Subfield.instSubfieldClass {K : Type u} [DivisionRing K] :
SubfieldClass (Subfield K) K
source
theorem Subfield.mem_carrier {K : Type u} [DivisionRing K] {s : Subfield K} {x : K} :
x ∈ s.carrier ↔ x ∈ s
source
@[simp]
theorem Subfield.mem_mk {K : Type u} [DivisionRing K] {S : Subring K} {x : K} (h : ∀ x ∈ S.carrier, x⁻¹ ∈ S.carrier) :
x ∈ { toSubring := S, inv_mem' := h } ↔ x ∈ S
source
@[simp]
theorem Subfield.coe_set_mk {K : Type u} [DivisionRing K] (S : Subring K) (h : ∀ x ∈ S.carrier, x⁻¹ ∈ S.carrier) :
↑{ toSubring := S, inv_mem' := h } = ↑S
source
@[simp]
theorem Subfield.mk_le_mk {K : Type u} [DivisionRing K] {S S' : Subring K} (h : ∀ x ∈ S.carrier, x⁻¹ ∈ S.carrier) (h' : ∀ x ∈ S'.carrier, x⁻¹ ∈ S'.carrier) :
{ toSubring := S, inv_mem' := h } ≤ { toSubring := S', inv_mem' := h' } ↔ S ≤ S'
source
theorem Subfield.ext {K : Type u} [DivisionRing K] {S T : Subfield K} (h : ∀ (x : K), x ∈ S ↔ x ∈ T) :
S = T

Two subfields are equal if they have the same elements.

source
theorem Subfield.ext_iff {K : Type u} [DivisionRing K] {S T : Subfield K} :
S = T ↔ ∀ (x : K), x ∈ S ↔ x ∈ T
source
def Subfield.copy {K : Type u} [DivisionRing K] (S : Subfield K) (s : Set K) (hs : s = ↑S) :
Subfield K

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

source
@[simp]
theorem Subfield.coe_copy {K : Type u} [DivisionRing K] (S : Subfield K) (s : Set K) (hs : s = ↑S) :
↑(S.copy s hs) = s
source
theorem Subfield.copy_eq {K : Type u} [DivisionRing K] (S : Subfield K) (s : Set K) (hs : s = ↑S) :
S.copy s hs = S
source
@[simp]
theorem Subfield.coe_toSubring {K : Type u} [DivisionRing K] (s : Subfield K) :
↑s.toSubring = ↑s
source
@[simp]
theorem Subfield.mem_toSubring {K : Type u} [DivisionRing K] (s : Subfield K) (x : K) :
x ∈ s.toSubring ↔ x ∈ s
source
def Subring.toSubfield {K : Type u} [DivisionRing K] (s : Subring K) (hinv : ∀ x ∈ s, x⁻¹ ∈ s) :
Subfield K

A `Subring` containing inverses is a `Subfield`.

Equations

- s.toSubfield hinv = { toSubring := s, inv_mem' := hinv }

Instances For

source
theorem Subfield.one_mem {K : Type u} [DivisionRing K] (s : Subfield K) :
1 ∈ s

A subfield contains the field's 1.

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

A subfield contains the field's 0.

source
theorem Subfield.mul_mem {K : Type u} [DivisionRing K] (s : Subfield K) {x y : K} :
x ∈ s → y ∈ s → x * y ∈ s

A subfield is closed under multiplication.

source
theorem Subfield.add_mem {K : Type u} [DivisionRing K] (s : Subfield K) {x y : K} :
x ∈ s → y ∈ s → x + y ∈ s

A subfield is closed under addition.

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

A subfield is closed under negation.

source
theorem Subfield.sub_mem {K : Type u} [DivisionRing K] (s : Subfield K) {x y : K} :
x ∈ s → y ∈ s → x - y ∈ s

A subfield is closed under subtraction.

source
theorem Subfield.inv_mem {K : Type u} [DivisionRing K] (s : Subfield K) {x : K} :
x ∈ s → x⁻¹ ∈ s

A subfield is closed under inverses.

source
theorem Subfield.div_mem {K : Type u} [DivisionRing K] (s : Subfield K) {x y : K} :
x ∈ s → y ∈ s → x / y ∈ s

A subfield is closed under division.

source
theorem Subfield.pow_mem {K : Type u} [DivisionRing K] (s : Subfield K) {x : K} (hx : x ∈ s) (n : ℕ) :
x ^ n ∈ s
source
theorem Subfield.zsmul_mem {K : Type u} [DivisionRing K] (s : Subfield K) {x : K} (hx : x ∈ s) (n : ℤ) :
n • x ∈ s
source
theorem Subfield.intCast_mem {K : Type u} [DivisionRing K] (s : Subfield K) (n : ℤ) :
↑n ∈ s
source
theorem Subfield.zpow_mem {K : Type u} [DivisionRing K] (s : Subfield K) {x : K} (hx : x ∈ s) (n : ℤ) :
x ^ n ∈ s
source
instance Subfield.instRingSubtypeMem {K : Type u} [DivisionRing K] (s : Subfield K) :
Ring ↥s
Equations

- s.instRingSubtypeMem = s.toRing

source
instance Subfield.instDivSubtypeMem {K : Type u} [DivisionRing K] (s : Subfield K) :
Div ↥s
Equations

- s.instDivSubtypeMem = { div := fun (x y : ↥s) => ⟨↑x / ↑y, ⋯⟩ }

source
instance Subfield.instInvSubtypeMem {K : Type u} [DivisionRing K] (s : Subfield K) :
Inv ↥s
Equations

- s.instInvSubtypeMem = { inv := fun (x : ↥s) => ⟨(↑x)⁻¹, ⋯⟩ }

source
instance Subfield.instPowSubtypeMemInt {K : Type u} [DivisionRing K] (s : Subfield K) :
Pow ↥s ℤ
Equations

- s.instPowSubtypeMemInt = { pow := fun (x : ↥s) (z : ℤ) => ⟨↑x ^ z, ⋯⟩ }

source
instance Subfield.toDivisionRing {K : Type u} [DivisionRing K] (s : Subfield K) :
DivisionRing ↥s
Equations

- s.toDivisionRing = SubfieldClass.toDivisionRing (Subfield K) s

source
instance Subfield.toField {K : Type u_1} [Field K] (s : Subfield K) :
Field ↥s

A subfield inherits a field structure

Equations

- s.toField = SubfieldClass.toField (Subfield K) s

source
@[simp]
theorem Subfield.coe_add {K : Type u} [DivisionRing K] (s : Subfield K) (x y : ↥s) :
↑(x + y) = ↑x + ↑y
source
@[simp]
theorem Subfield.coe_sub {K : Type u} [DivisionRing K] (s : Subfield K) (x y : ↥s) :
↑(x - y) = ↑x - ↑y
source
@[simp]
theorem Subfield.coe_neg {K : Type u} [DivisionRing K] (s : Subfield K) (x : ↥s) :
↑(-x) = -↑x
source
@[simp]
theorem Subfield.coe_mul {K : Type u} [DivisionRing K] (s : Subfield K) (x y : ↥s) :
↑(x * y) = ↑x * ↑y
source
@[simp]
theorem Subfield.coe_div {K : Type u} [DivisionRing K] (s : Subfield K) (x y : ↥s) :
↑(x / y) = ↑x / ↑y
source
@[simp]
theorem Subfield.coe_inv {K : Type u} [DivisionRing K] (s : Subfield K) (x : ↥s) :
↑x⁻¹ = (↑x)⁻¹
source
@[simp]
theorem Subfield.coe_zero {K : Type u} [DivisionRing K] (s : Subfield K) :
↑0 = 0
source
@[simp]
theorem Subfield.coe_one {K : Type u} [DivisionRing K] (s : Subfield K) :
↑1 = 1
source
def Subfield.subtype {K : Type u} [DivisionRing K] (s : Subfield K) :
↥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

source
@[simp]
theorem Subfield.subtype_apply {K : Type u} [DivisionRing K] {s : Subfield K} (x : ↥s) :
s.subtype x = ↑x
source
theorem Subfield.subtype_injective {K : Type u} [DivisionRing K] (s : Subfield K) :
Function.Injective ⇑s.subtype
source
@[simp]
theorem Subfield.coe_subtype {K : Type u} [DivisionRing K] (s : Subfield K) :
⇑s.subtype = Subtype.val
source
theorem Subfield.toSubring_subtype_eq_subtype (K : Type u) [DivisionRing K] (S : Subfield K) :
S.subtype = S.subtype

### Partial order #

source
theorem Subfield.mem_toSubmonoid {K : Type u} [DivisionRing K] {s : Subfield K} {x : K} :
x ∈ s.toSubmonoid ↔ x ∈ s
source
@[simp]
theorem Subfield.coe_toSubmonoid {K : Type u} [DivisionRing K] (s : Subfield K) :
↑s.toSubmonoid = ↑s
source
@[simp]
theorem Subfield.mem_toAddSubgroup {K : Type u} [DivisionRing K] {s : Subfield K} {x : K} :
x ∈ s.toAddSubgroup ↔ x ∈ s
source
@[simp]
theorem Subfield.coe_toAddSubgroup {K : Type u} [DivisionRing K] (s : Subfield K) :
↑s.toAddSubgroup = ↑s