Documentation

Mathlib.Algebra.Field.Subfield.Defs

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)

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 :

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} [DivisionRing K] (S : Type u_1) [SetLike S K] [h : SubfieldClass 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.

    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
    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
    instance SubfieldClass.instNNRatCast {K : Type u} [DivisionRing K] {S : Type u_1} [SetLike S K] [h : SubfieldClass S K] (s : S) :
    Equations
      instance SubfieldClass.instRatCast {K : Type u} [DivisionRing K] {S : Type u_1} [SetLike S K] [h : SubfieldClass S K] (s : S) :
      RatCast s
      Equations
        @[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
        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 : } :
        instance SubfieldClass.instSMulNNRat {K : Type u} [DivisionRing K] {S : Type u_1} [SetLike S K] [h : SubfieldClass S K] (s : S) :
        Equations
          instance SubfieldClass.instSMulRat {K : Type u} [DivisionRing K] {S : Type u_1} [SetLike S K] [h : SubfieldClass S K] (s : S) :
          SMul s
          Equations
            @[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
            @[instance 75]
            instance SubfieldClass.toDivisionRing {K : Type u} [DivisionRing K] (S : Type u_1) [SetLike S K] [h : SubfieldClass S K] (s : S) :

            A subfield inherits a division ring structure

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

                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.

                Instances For

                  The underlying AddSubgroup of a subfield.

                  Equations
                    Instances For
                      Equations
                        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 : xS.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 : xS.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 : 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 {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) :

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

                        Equations
                          Instances For
                            @[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) :
                            def Subring.toSubfield {K : Type u} [DivisionRing K] (s : Subring K) (hinv : xs, x⁻¹ s) :

                            A Subring containing inverses is a Subfield.

                            Equations
                              Instances For
                                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 sy sx * y s

                                A subfield is closed under multiplication.

                                theorem Subfield.add_mem {K : Type u} [DivisionRing K] (s : Subfield K) {x y : K} :
                                x sy sx + 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 sy sx - y s

                                A subfield is closed under subtraction.

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

                                A subfield is closed under inverses.

                                theorem Subfield.div_mem {K : Type u} [DivisionRing K] (s : Subfield K) {x y : K} :
                                x sy sx / 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
                                instance Subfield.instRingSubtypeMem {K : Type u} [DivisionRing K] (s : Subfield K) :
                                Ring s
                                Equations
                                  instance Subfield.instDivSubtypeMem {K : Type u} [DivisionRing K] (s : Subfield K) :
                                  Div s
                                  Equations
                                    instance Subfield.instInvSubtypeMem {K : Type u} [DivisionRing K] (s : Subfield K) :
                                    Inv s
                                    Equations
                                      instance Subfield.instPowSubtypeMemInt {K : Type u} [DivisionRing K] (s : Subfield K) :
                                      Pow s
                                      Equations
                                        Equations
                                          instance Subfield.toField {K : Type u_1} [Field K] (s : Subfield K) :
                                          Field s

                                          A subfield inherits a field structure

                                          Equations
                                            @[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
                                              Instances For
                                                @[simp]
                                                theorem Subfield.subtype_apply {K : Type u} [DivisionRing K] {s : Subfield K} (x : s) :
                                                s.subtype x = x
                                                @[simp]

                                                Partial order #

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