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
  • Subfield.instTop = { top := let __src := ; { toSubring := __src, inv_mem' := } }
Equations
  • Subfield.instInhabited = { default := }
@[simp]
theorem Subfield.mem_top {K : Type u} [DivisionRing K] (x : K) :
@[simp]
theorem Subfield.coe_top {K : Type u} [DivisionRing K] :
= Set.univ

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} [DivisionRing K] [DivisionRing L] (f : K →+* L) (s : Subfield L) :

    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} [DivisionRing K] [DivisionRing L] (f : K →+* L) (s : Subfield L) :
      (Subfield.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} :
      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) :

      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
      Instances For
        @[simp]
        theorem Subfield.coe_map {K : Type u} {L : Type v} [DivisionRing K] [DivisionRing L] (s : Subfield K) (f : K →+* L) :
        (Subfield.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 Subfield.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) :
        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} :

        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
        Instances For
          @[simp]
          theorem RingHom.coe_fieldRange {K : Type u} {L : Type v} [DivisionRing K] [DivisionRing L] (f : K →+* L) :
          f.fieldRange = Set.range f
          @[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.fieldRange_eq_map {K : Type u} {L : Type v} [DivisionRing K] [DivisionRing L] (f : K →+* L) :
          f.fieldRange = Subfield.map f
          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) :
          Subfield.map g f.fieldRange = (g.comp f).fieldRange
          theorem RingHom.mem_fieldRange_self {K : Type u} {L : Type v} [DivisionRing K] [DivisionRing L] (f : K →+* L) (x : K) :
          f x f.fieldRange
          theorem RingHom.fieldRange_eq_top_iff {K : Type u} {L : Type v} [DivisionRing K] [DivisionRing L] {f : K →+* L} :
          f.fieldRange = Function.Surjective f
          instance RingHom.fintypeFieldRange {K : Type u} {L : Type v} [DivisionRing K] [DivisionRing L] [Fintype K] [DecidableEq L] (f : K →+* L) :
          Fintype 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

          inf #

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

          The inf of two subfields is their intersection.

          Equations
          • Subfield.instMin = { min := fun (s t : Subfield K) => let __src := s.toSubring t.toSubring; { toSubring := __src, inv_mem' := } }
          @[simp]
          theorem Subfield.coe_inf {K : Type u} [DivisionRing K] (p p' : Subfield K) :
          (p p') = p.carrier p'.carrier
          @[simp]
          theorem Subfield.mem_inf {K : Type u} [DivisionRing K] {p p' : Subfield K} {x : K} :
          x p p' x p x p'
          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} [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

          subfield closure of a subset #

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

          The Subfield generated by a set.

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

            The subfield generated by a set includes the set.

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

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

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

            closure forms a Galois insertion with the coercion to set.

            Equations
            Instances For
              theorem Subfield.closure_eq {K : Type u} [DivisionRing K] (s : Subfield K) :

              Closure of a subfield S equals S.

              @[simp]
              theorem Subfield.closure_iUnion {K : Type u} [DivisionRing K] {ι : Sort u_1} (s : ιSet K) :
              Subfield.closure (⋃ (i : ι), s i) = ⨆ (i : ι), Subfield.closure (s i)
              theorem Subfield.map_sup {K : Type u} {L : Type v} [DivisionRing K] [DivisionRing L] (s t : Subfield K) (f : K →+* L) :
              theorem Subfield.map_iSup {K : Type u} {L : Type v} [DivisionRing K] [DivisionRing L] {ι : Sort u_1} (f : K →+* L) (s : ιSubfield K) :
              Subfield.map f (iSup s) = ⨆ (i : ι), Subfield.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) :
              theorem Subfield.map_iInf {K : Type u} {L : Type v} [DivisionRing K] [DivisionRing L] {ι : Sort u_1} [Nonempty ι] (f : K →+* L) (s : ιSubfield K) :
              Subfield.map f (iInf s) = ⨅ (i : ι), Subfield.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) :
              theorem Subfield.comap_iInf {K : Type u} {L : Type v} [DivisionRing K] [DivisionRing L] {ι : Sort u_1} (f : K →+* L) (s : ιSubfield L) :
              Subfield.comap f (iInf s) = ⨅ (i : ι), Subfield.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} [hι : 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} [hι : 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) :
              K →+* 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} [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' := }
                Instances For
                  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
                  Instances For
                    @[simp]
                    theorem Subfield.fieldRange_subtype {K : Type u} [DivisionRing K] (s : Subfield K) :
                    s.subtype.fieldRange = s
                    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
                    Instances For
                      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
                      • s.toAlgebra = s.subtype.toAlgebra
                      theorem Subfield.mem_closure_iff {K : Type u} [Field K] {s : Set K} {x : K} :
                      x Subfield.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) :
                      Subfield.map f (Subfield.comap f s) = s f.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) :
                      theorem Subfield.comap_map {K : Type u} {L : Type v} [DivisionRing K] [DivisionRing L] (f : K →+* L) (s : Subfield K) :

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

                      theorem 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