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

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

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

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

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

@[implicit_reducible]

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, ⋯⟩ }

@[implicit_reducible]

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, ⋯⟩ }

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

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

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

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

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

@[implicit_reducible]

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, ⋯⟩ }

@[implicit_reducible]

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, ⋯⟩ }

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

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

@[implicit_reducible, 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.

@[implicit_reducible, 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.

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.

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

The underlying AddSubgroup of a subfield.

Equations

• s.toAddSubgroup = s.toAddSubgroup

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

instance Subfield.instPartialOrder {K : Type u} [DivisionRing K] : PartialOrder (Subfield K)

Equations

• Subfield.instPartialOrder = PartialOrder.ofSetLike (Subfield K) K

instance Subfield.instSubfieldClass {K : Type u} [DivisionRing K] : SubfieldClass (Subfield K) K

theorem Subfield.mem_carrier {K : Type u} [DivisionRing K] {s : Subfield K} {x : K} : x ∈ s.carrier ↔ x ∈ s

@[simp]

theorem Subfield.mem_mk {K : Type u} [DivisionRing K] {S : Subring K} {x : K} (h : ∀ (x : K), x ∈ S.carrier → x⁻¹ ∈ S.carrier) : x ∈ { toSubring := S, inv_mem' := h } ↔ x ∈ S

@[simp]

theorem Subfield.coe_set_mk {K : Type u} [DivisionRing K] (S : Subring K) (h : ∀ (x : K), x ∈ S.carrier → x⁻¹ ∈ S.carrier) : ↑{ toSubring := S, inv_mem' := h } = ↑S

@[simp]

theorem Subfield.mk_le_mk {K : Type u} [DivisionRing K] {S S' : Subring K} (h : ∀ (x : K), x ∈ S.carrier → x⁻¹ ∈ S.carrier) (h' : ∀ (x : K), x ∈ S'.carrier → x⁻¹ ∈ S'.carrier) : { toSubring := S, inv_mem' := h } ≤ { toSubring := S', inv_mem' := h' } ↔ S ≤ S'

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.

theorem Subfield.ext_iff {K : Type u} [DivisionRing K] {S T : Subfield K} : S = T ↔ ∀ (x : K), x ∈ S ↔ x ∈ T

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' := ⋯ }

@[simp]

theorem Subfield.coe_copy {K : Type u} [DivisionRing K] (S : Subfield K) (s : Set K) (hs : s = ↑S) : ↑(S.copy s hs) = s

theorem Subfield.copy_eq {K : Type u} [DivisionRing K] (S : Subfield K) (s : Set K) (hs : s = ↑S) : S.copy s hs = S

@[simp]

theorem Subfield.coe_toSubring {K : Type u} [DivisionRing K] (s : Subfield K) : ↑s.toSubring = ↑s

@[simp]

theorem Subfield.mem_toSubring {K : Type u} [DivisionRing K] (s : Subfield K) (x : K) : x ∈ s.toSubring ↔ x ∈ s

def Subring.toSubfield {K : Type u} [DivisionRing K] (s : Subring K) (hinv : ∀ (x : K), x ∈ s → x⁻¹ ∈ s) : Subfield K

A Subring containing inverses is a Subfield.

Equations

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

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

A subfield contains the field's 1.

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

A subfield contains the field's 0.

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.

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.

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

A subfield is closed under negation.

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.

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

A subfield is closed under inverses.

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.

theorem Subfield.pow_mem {K : Type u} [DivisionRing K] (s : Subfield K) {x : K} (hx : x ∈ s) (n : ℕ) : x ^ n ∈ s

theorem Subfield.zsmul_mem {K : Type u} [DivisionRing K] (s : Subfield K) {x : K} (hx : x ∈ s) (n : ℤ) : n • x ∈ s

theorem Subfield.intCast_mem {K : Type u} [DivisionRing K] (s : Subfield K) (n : ℤ) : ↑n ∈ s

theorem Subfield.zpow_mem {K : Type u} [DivisionRing K] (s : Subfield K) {x : K} (hx : x ∈ s) (n : ℤ) : x ^ n ∈ s

@[implicit_reducible]

instance Subfield.instRingSubtypeMem {K : Type u} [DivisionRing K] (s : Subfield K) : Ring ↥s

Equations

• s.instRingSubtypeMem = s.toRing

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[simp]

theorem Subfield.coe_add {K : Type u} [DivisionRing K] (s : Subfield K) (x y : ↥s) : ↑(x + y) = ↑x + ↑y

@[simp]

theorem Subfield.coe_sub {K : Type u} [DivisionRing K] (s : Subfield K) (x y : ↥s) : ↑(x - y) = ↑x - ↑y

@[simp]

theorem Subfield.coe_neg {K : Type u} [DivisionRing K] (s : Subfield K) (x : ↥s) : ↑(-x) = -↑x

@[simp]

theorem Subfield.coe_mul {K : Type u} [DivisionRing K] (s : Subfield K) (x y : ↥s) : ↑(x * y) = ↑x * ↑y

@[simp]

theorem Subfield.coe_div {K : Type u} [DivisionRing K] (s : Subfield K) (x y : ↥s) : ↑(x / y) = ↑x / ↑y

@[simp]

theorem Subfield.coe_inv {K : Type u} [DivisionRing K] (s : Subfield K) (x : ↥s) : ↑x⁻¹ = (↑x)⁻¹

@[simp]

theorem Subfield.coe_zero {K : Type u} [DivisionRing K] (s : Subfield K) : ↑0 = 0

@[simp]

theorem Subfield.coe_one {K : Type u} [DivisionRing K] (s : Subfield K) : ↑1 = 1

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' := ⋯ }

@[simp]

theorem Subfield.subtype_apply {K : Type u} [DivisionRing K] {s : Subfield K} (x : ↥s) : s.subtype x = ↑x

theorem Subfield.subtype_injective {K : Type u} [DivisionRing K] (s : Subfield K) : Function.Injective ⇑s.subtype

@[simp]

theorem Subfield.coe_subtype {K : Type u} [DivisionRing K] (s : Subfield K) : ⇑s.subtype = Subtype.val

theorem Subfield.toSubring_subtype_eq_subtype (K : Type u) [DivisionRing K] (S : Subfield K) : S.subtype = S.subtype

Partial order

theorem Subfield.mem_toSubmonoid {K : Type u} [DivisionRing K] {s : Subfield K} {x : K} : x ∈ s.toSubmonoid ↔ x ∈ s

@[simp]

theorem Subfield.coe_toSubmonoid {K : Type u} [DivisionRing K] (s : Subfield K) : ↑s.toSubmonoid = ↑s

@[simp]

theorem Subfield.mem_toAddSubgroup {K : Type u} [DivisionRing K] {s : Subfield K} {x : K} : x ∈ s.toAddSubgroup ↔ x ∈ s

@[simp]

theorem Subfield.coe_toAddSubgroup {K : Type u} [DivisionRing K] (s : Subfield K) : ↑s.toAddSubgroup = ↑s