Documentation

Mathlib.FieldTheory.Adjoin

Adjoining Elements to Fields #

In this file we introduce the notion of adjoining elements to fields. This isn't quite the same as adjoining elements to rings. For example, Algebra.adjoin K {x} might not include x⁻¹.

Main results #

Notation #

def IntermediateField.adjoin (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] (S : Set E) :

adjoin F S extends a field F by adjoining a set S ⊆ E.

Equations
Instances For
    theorem IntermediateField.mem_adjoin_iff (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] {S : Set E} (x : E) :
    x IntermediateField.adjoin F S ∃ (r : MvPolynomial (S) F) (s : MvPolynomial (S) F), x = (MvPolynomial.aeval Subtype.val) r / (MvPolynomial.aeval Subtype.val) s
    theorem IntermediateField.mem_adjoin_simple_iff (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] {α : E} (x : E) :
    x Fα ∃ (r : Polynomial F) (s : Polynomial F), x = (Polynomial.aeval α) r / (Polynomial.aeval α) s
    @[simp]
    theorem IntermediateField.adjoin_le_iff {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {S : Set E} {T : IntermediateField F E} :
    theorem IntermediateField.gc {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] :
    def IntermediateField.gi {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] :

    Galois insertion between adjoin and coe.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      Equations
      Equations
      • IntermediateField.instInhabitedIntermediateField = { default := }
      Equations
      theorem IntermediateField.coe_bot {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] :
      theorem IntermediateField.mem_bot {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {x : E} :
      @[simp]
      theorem IntermediateField.bot_toSubalgebra {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] :
      .toSubalgebra =
      @[simp]
      theorem IntermediateField.coe_top {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] :
      = Set.univ
      @[simp]
      theorem IntermediateField.mem_top {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {x : E} :
      @[simp]
      theorem IntermediateField.top_toSubalgebra {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] :
      .toSubalgebra =
      @[simp]
      theorem IntermediateField.coe_inf {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] (S : IntermediateField F E) (T : IntermediateField F E) :
      (S T) = S T
      @[simp]
      theorem IntermediateField.mem_inf {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {S : IntermediateField F E} {T : IntermediateField F E} {x : E} :
      x S T x S x T
      @[simp]
      theorem IntermediateField.inf_toSubalgebra {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] (S : IntermediateField F E) (T : IntermediateField F E) :
      (S T).toSubalgebra = S.toSubalgebra T.toSubalgebra
      @[simp]
      theorem IntermediateField.coe_sInf {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] (S : Set (IntermediateField F E)) :
      (sInf S) = sInf ((fun (x : IntermediateField F E) => x) '' S)
      @[simp]
      theorem IntermediateField.sInf_toSubalgebra {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] (S : Set (IntermediateField F E)) :
      (sInf S).toSubalgebra = sInf (IntermediateField.toSubalgebra '' S)
      @[simp]
      theorem IntermediateField.sInf_toSubfield {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] (S : Set (IntermediateField F E)) :
      IntermediateField.toSubfield (sInf S) = sInf (IntermediateField.toSubfield '' S)
      @[simp]
      theorem IntermediateField.coe_iInf {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {ι : Sort u_3} (S : ιIntermediateField F E) :
      (iInf S) = ⋂ (i : ι), (S i)
      @[simp]
      theorem IntermediateField.iInf_toSubalgebra {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {ι : Sort u_3} (S : ιIntermediateField F E) :
      (iInf S).toSubalgebra = ⨅ (i : ι), (S i).toSubalgebra
      @[simp]
      theorem IntermediateField.iInf_toSubfield {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {ι : Sort u_3} (S : ιIntermediateField F E) :
      @[simp]
      theorem IntermediateField.equivOfEq_apply {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {S : IntermediateField F E} {T : IntermediateField F E} (h : S = T) (x : S.toSubalgebra) :
      (IntermediateField.equivOfEq h) x = { val := x, property := }
      def IntermediateField.equivOfEq {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {S : IntermediateField F E} {T : IntermediateField F E} (h : S = T) :
      S ≃ₐ[F] T

      Construct an algebra isomorphism from an equality of intermediate fields

      Equations
      Instances For
        @[simp]
        theorem IntermediateField.equivOfEq_rfl {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] (S : IntermediateField F E) :
        IntermediateField.equivOfEq = AlgEquiv.refl
        noncomputable def IntermediateField.botEquiv (F : Type u_1) [Field F] (E : Type u_2) [Field E] [Algebra F E] :

        The bottom intermediate_field is isomorphic to the field.

        Equations
        Instances For
          theorem IntermediateField.botEquiv_def {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] (x : F) :
          @[simp]
          theorem IntermediateField.botEquiv_symm {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] (x : F) :
          noncomputable instance IntermediateField.algebraOverBot {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] :
          Algebra () F
          Equations
          instance IntermediateField.isScalarTower_over_bot {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] :
          Equations
          • =
          @[simp]
          theorem IntermediateField.topEquiv_apply {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] :
          ∀ (a : .toSubalgebra), IntermediateField.topEquiv a = a
          @[simp]
          theorem IntermediateField.topEquiv_symm_apply_coe {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] :
          ∀ (a : E), ((AlgEquiv.symm IntermediateField.topEquiv) a) = ((MulEquiv.symm Subalgebra.topEquiv) a)
          def IntermediateField.topEquiv {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] :

          The top IntermediateField is isomorphic to the field.

          This is the intermediate field version of Subalgebra.topEquiv.

          Equations
          Instances For
            @[simp]
            theorem IntermediateField.restrictScalars_top {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {K : Type u_3} [Field K] [Algebra K E] [Algebra K F] [IsScalarTower K F E] :
            @[simp]
            theorem IntermediateField.map_bot {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {K : Type u_3} [Field K] [Algebra F K] (f : E →ₐ[F] K) :
            theorem IntermediateField.map_sup {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {K : Type u_3} [Field K] [Algebra F K] (s : IntermediateField F E) (t : IntermediateField F E) (f : E →ₐ[F] K) :
            theorem IntermediateField.map_iSup {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {K : Type u_3} [Field K] [Algebra F K] {ι : Sort u_4} (f : E →ₐ[F] K) (s : ιIntermediateField F E) :
            theorem AlgHom.fieldRange_eq_map {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {K : Type u_3} [Field K] [Algebra F K] (f : E →ₐ[F] K) :
            theorem AlgHom.map_fieldRange {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {K : Type u_3} [Field K] [Algebra F K] {L : Type u_4} [Field L] [Algebra F L] (f : E →ₐ[F] K) (g : K →ₐ[F] L) :
            theorem AlgHom.fieldRange_eq_top {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {K : Type u_3} [Field K] [Algebra F K] {f : E →ₐ[F] K} :
            @[simp]
            theorem AlgEquiv.fieldRange_eq_top {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {K : Type u_3} [Field K] [Algebra F K] (f : E ≃ₐ[F] K) :
            noncomputable def IntermediateField.equivMap {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {K : Type u_3} [Field K] [Algebra F K] (L : IntermediateField F E) (f : E →ₐ[F] K) :

            An intermediate field is isomorphic to its image under an AlgHom (which is automatically injective)

            Equations
            Instances For
              @[simp]
              theorem IntermediateField.coe_equivMap_apply {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {K : Type u_3} [Field K] [Algebra F K] (L : IntermediateField F E) (f : E →ₐ[F] K) (x : L) :
              ((IntermediateField.equivMap L f) x) = f x
              theorem IntermediateField.adjoin.algebraMap_mem (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] (S : Set E) (x : F) :
              instance IntermediateField.adjoin.fieldCoe (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] (S : Set E) :
              Equations
              theorem IntermediateField.subset_adjoin (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] (S : Set E) :
              instance IntermediateField.adjoin.setCoe (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] (S : Set E) :
              Equations
              theorem IntermediateField.adjoin.mono (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] (S : Set E) (T : Set E) (h : S T) :
              theorem IntermediateField.subset_adjoin_of_subset_left {E : Type u_2} [Field E] (S : Set E) {F : Subfield E} {T : Set E} (HT : T F) :
              theorem IntermediateField.subset_adjoin_of_subset_right (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] (S : Set E) {T : Set E} (H : T S) :
              @[simp]
              theorem IntermediateField.adjoin_empty (F : Type u_3) (E : Type u_4) [Field F] [Field E] [Algebra F E] :
              F⟮⟯ =
              @[simp]
              theorem IntermediateField.adjoin_univ (F : Type u_3) (E : Type u_4) [Field F] [Field E] [Algebra F E] :
              theorem IntermediateField.adjoin_le_subfield (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] (S : Set E) {K : Subfield E} (HF : Set.range (algebraMap F E) K) (HS : S K) :

              If K is a field with F ⊆ K and S ⊆ K then adjoin F S ≤ K.

              theorem IntermediateField.adjoin_subset_adjoin_iff (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] {F' : Type u_3} [Field F'] [Algebra F' E] {S : Set E} {S' : Set E} :
              theorem IntermediateField.adjoin_map (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] (S : Set E) {E' : Type u_3} [Field E'] [Algebra F E'] (f : E →ₐ[F] E') :
              @[simp]
              theorem IntermediateField.lift_adjoin (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] (K : IntermediateField F E) (S : Set K) :
              theorem IntermediateField.lift_adjoin_simple (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] (K : IntermediateField F E) (α : K) :
              IntermediateField.lift Fα = Fα
              @[simp]
              @[simp]
              theorem IntermediateField.lift_top (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] (K : IntermediateField F E) :
              @[simp]
              theorem IntermediateField.adjoin_self (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] (K : IntermediateField F E) :
              theorem IntermediateField.restrictScalars_adjoin_of_algEquiv {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {L : Type u_3} {L' : Type u_4} [Field L] [Field L'] [Algebra F L] [Algebra L E] [Algebra F L'] [Algebra L' E] [IsScalarTower F L E] [IsScalarTower F L' E] (i : L ≃ₐ[F] L') (hi : (algebraMap L E) = (algebraMap L' E) i) (S : Set E) :

              If E / L / F and E / L' / F are two field extension towers, L ≃ₐ[F] L' is an isomorphism compatible with E / L and E / L', then for any subset S of E, L(S) and L'(S) are equal as intermediate fields of E / F.

              theorem IntermediateField.algebra_adjoin_le_adjoin (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] (S : Set E) :
              theorem IntermediateField.adjoin_eq_algebra_adjoin (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] (S : Set E) (inv_mem : xAlgebra.adjoin F S, x⁻¹ Algebra.adjoin F S) :
              theorem IntermediateField.eq_adjoin_of_eq_algebra_adjoin (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] (S : Set E) (K : IntermediateField F E) (h : K.toSubalgebra = Algebra.adjoin F S) :
              theorem IntermediateField.adjoin_induction (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] {s : Set E} {p : EProp} {x : E} (h : x IntermediateField.adjoin F s) (mem : xs, p x) (algebraMap : ∀ (x : F), p ((_root_.algebraMap F E) x)) (add : ∀ (x y : E), p xp yp (x + y)) (neg : ∀ (x : E), p xp (-x)) (inv : ∀ (x : E), p xp x⁻¹) (mul : ∀ (x y : E), p xp yp (x * y)) :
              p x

              If x₁ x₂ ... xₙ : E then F⟮x₁,x₂,...,xₙ⟯ is the IntermediateField F E generated by these elements.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  theorem IntermediateField.mem_adjoin_simple_self (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] (α : E) :
                  α Fα
                  def IntermediateField.AdjoinSimple.gen (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] (α : E) :
                  Fα

                  generator of F⟮α⟯

                  Equations
                  Instances For
                    @[simp]
                    theorem IntermediateField.AdjoinSimple.coe_gen (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] (α : E) :
                    theorem IntermediateField.AdjoinSimple.algebraMap_gen (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] (α : E) :
                    (algebraMap (Fα) E) (IntermediateField.AdjoinSimple.gen F α) = α
                    theorem IntermediateField.adjoin_simple_adjoin_simple (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] (α : E) (β : E) :
                    IntermediateField.restrictScalars F (Fα)β = Fα, β
                    theorem IntermediateField.adjoin_simple_comm (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] (α : E) (β : E) :
                    IntermediateField.restrictScalars F (Fα)β = IntermediateField.restrictScalars F (Fβ)α
                    theorem IntermediateField.adjoin_algebraic_toSubalgebra {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {S : Set E} (hS : xS, IsAlgebraic F x) :
                    theorem IntermediateField.adjoin_simple_toSubalgebra_of_integral {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {α : E} (hα : IsIntegral F α) :
                    Fα.toSubalgebra = Algebra.adjoin F {α}
                    theorem IntermediateField.le_sup_toSubalgebra {K : Type u_3} {L : Type u_4} [Field K] [Field L] [Algebra K L] (E1 : IntermediateField K L) (E2 : IntermediateField K L) :
                    E1.toSubalgebra E2.toSubalgebra (E1 E2).toSubalgebra
                    theorem IntermediateField.sup_toSubalgebra_of_isAlgebraic_right {K : Type u_3} {L : Type u_4} [Field K] [Field L] [Algebra K L] (E1 : IntermediateField K L) (E2 : IntermediateField K L) (halg : Algebra.IsAlgebraic K E2) :
                    (E1 E2).toSubalgebra = E1.toSubalgebra E2.toSubalgebra
                    theorem IntermediateField.sup_toSubalgebra_of_isAlgebraic_left {K : Type u_3} {L : Type u_4} [Field K] [Field L] [Algebra K L] (E1 : IntermediateField K L) (E2 : IntermediateField K L) (halg : Algebra.IsAlgebraic K E1) :
                    (E1 E2).toSubalgebra = E1.toSubalgebra E2.toSubalgebra
                    theorem IntermediateField.sup_toSubalgebra_of_isAlgebraic {K : Type u_3} {L : Type u_4} [Field K] [Field L] [Algebra K L] (E1 : IntermediateField K L) (E2 : IntermediateField K L) (halg : Algebra.IsAlgebraic K E1 Algebra.IsAlgebraic K E2) :
                    (E1 E2).toSubalgebra = E1.toSubalgebra E2.toSubalgebra

                    The compositum of two intermediate fields is equal to the compositum of them as subalgebras, if one of them is algebraic over the base field.

                    theorem IntermediateField.sup_toSubalgebra_of_left {K : Type u_3} {L : Type u_4} [Field K] [Field L] [Algebra K L] (E1 : IntermediateField K L) (E2 : IntermediateField K L) [FiniteDimensional K E1] :
                    (E1 E2).toSubalgebra = E1.toSubalgebra E2.toSubalgebra
                    @[deprecated IntermediateField.sup_toSubalgebra_of_left]
                    theorem IntermediateField.sup_toSubalgebra {K : Type u_3} {L : Type u_4} [Field K] [Field L] [Algebra K L] (E1 : IntermediateField K L) (E2 : IntermediateField K L) [FiniteDimensional K E1] :
                    (E1 E2).toSubalgebra = E1.toSubalgebra E2.toSubalgebra

                    Alias of IntermediateField.sup_toSubalgebra_of_left.

                    theorem IntermediateField.sup_toSubalgebra_of_right {K : Type u_3} {L : Type u_4} [Field K] [Field L] [Algebra K L] (E1 : IntermediateField K L) (E2 : IntermediateField K L) [FiniteDimensional K E2] :
                    (E1 E2).toSubalgebra = E1.toSubalgebra E2.toSubalgebra
                    instance IntermediateField.finiteDimensional_sup {K : Type u_3} {L : Type u_4} [Field K] [Field L] [Algebra K L] (E1 : IntermediateField K L) (E2 : IntermediateField K L) [FiniteDimensional K E1] [FiniteDimensional K E2] :
                    FiniteDimensional K (E1 E2)
                    Equations
                    • =
                    theorem IntermediateField.coe_iSup_of_directed {K : Type u_3} {L : Type u_4} [Field K] [Field L] [Algebra K L] {ι : Type u_5} {t : ιIntermediateField K L} [Nonempty ι] (dir : Directed (fun (x x_1 : IntermediateField K L) => x x_1) t) :
                    (iSup t) = ⋃ (i : ι), (t i)
                    theorem IntermediateField.toSubalgebra_iSup_of_directed {K : Type u_3} {L : Type u_4} [Field K] [Field L] [Algebra K L] {ι : Type u_5} {t : ιIntermediateField K L} (dir : Directed (fun (x x_1 : IntermediateField K L) => x x_1) t) :
                    (iSup t).toSubalgebra = ⨆ (i : ι), (t i).toSubalgebra
                    instance IntermediateField.finiteDimensional_iSup_of_finite {K : Type u_3} {L : Type u_4} [Field K] [Field L] [Algebra K L] {ι : Type u_5} {t : ιIntermediateField K L} [h : Finite ι] [∀ (i : ι), FiniteDimensional K (t i)] :
                    FiniteDimensional K (⨆ (i : ι), t i)
                    Equations
                    • =
                    instance IntermediateField.finiteDimensional_iSup_of_finset {K : Type u_3} {L : Type u_4} [Field K] [Field L] [Algebra K L] {ι : Type u_5} {t : ιIntermediateField K L} {s : Finset ι} [∀ (i : ι), FiniteDimensional K (t i)] :
                    FiniteDimensional K (⨆ i ∈ s, t i)
                    Equations
                    • =
                    theorem IntermediateField.finiteDimensional_iSup_of_finset' {K : Type u_3} {L : Type u_4} [Field K] [Field L] [Algebra K L] {ι : Type u_5} {t : ιIntermediateField K L} {s : Finset ι} (h : is, FiniteDimensional K (t i)) :
                    FiniteDimensional K (⨆ i ∈ s, t i)
                    theorem IntermediateField.isSplittingField_iSup {K : Type u_3} {L : Type u_4} [Field K] [Field L] [Algebra K L] {ι : Type u_5} {t : ιIntermediateField K L} {p : ιPolynomial K} {s : Finset ι} (h0 : (Finset.prod s fun (i : ι) => p i) 0) (h : is, Polynomial.IsSplittingField K ((t i)) (p i)) :
                    Polynomial.IsSplittingField K ((⨆ i ∈ s, t i)) (Finset.prod s fun (i : ι) => p i)

                    A compositum of splitting fields is a splitting field

                    theorem IntermediateField.adjoin_toSubalgebra_of_isAlgebraic {F : Type u_1} [Field F] (E : Type u_2) [Field E] [Algebra F E] {K : Type u_3} [Field K] [Algebra F K] [Algebra E K] [IsScalarTower F E K] (L : IntermediateField F K) (halg : Algebra.IsAlgebraic F E Algebra.IsAlgebraic F L) :
                    (IntermediateField.adjoin E L).toSubalgebra = Algebra.adjoin E L

                    If K / E / F is a field extension tower, L is an intermediate field of K / F, such that either E / F or L / F is algebraic, then E(L) = E[L].

                    theorem IntermediateField.adjoin_toSubalgebra_of_isAlgebraic_left {F : Type u_1} [Field F] (E : Type u_2) [Field E] [Algebra F E] {K : Type u_3} [Field K] [Algebra F K] [Algebra E K] [IsScalarTower F E K] (L : IntermediateField F K) (halg : Algebra.IsAlgebraic F E) :
                    (IntermediateField.adjoin E L).toSubalgebra = Algebra.adjoin E L
                    theorem IntermediateField.adjoin_toSubalgebra_of_isAlgebraic_right {F : Type u_1} [Field F] (E : Type u_2) [Field E] [Algebra F E] {K : Type u_3} [Field K] [Algebra F K] [Algebra E K] [IsScalarTower F E K] (L : IntermediateField F K) (halg : Algebra.IsAlgebraic F L) :
                    (IntermediateField.adjoin E L).toSubalgebra = Algebra.adjoin E L
                    theorem IntermediateField.adjoin_rank_le_of_isAlgebraic {F : Type u_1} [Field F] (E : Type u_2) [Field E] [Algebra F E] {K : Type u_3} [Field K] [Algebra F K] [Algebra E K] [IsScalarTower F E K] (L : IntermediateField F K) (halg : Algebra.IsAlgebraic F E Algebra.IsAlgebraic F L) :

                    If K / E / F is a field extension tower, L is an intermediate field of K / F, such that either E / F or L / F is algebraic, then [E(L) : E] ≤ [L : F]. A corollary of Subalgebra.adjoin_rank_le since in this case E(L) = E[L].

                    theorem IntermediateField.adjoin_rank_le_of_isAlgebraic_left {F : Type u_1} [Field F] (E : Type u_2) [Field E] [Algebra F E] {K : Type u_3} [Field K] [Algebra F K] [Algebra E K] [IsScalarTower F E K] (L : IntermediateField F K) (halg : Algebra.IsAlgebraic F E) :
                    theorem IntermediateField.adjoin_rank_le_of_isAlgebraic_right {F : Type u_1} [Field F] (E : Type u_2) [Field E] [Algebra F E] {K : Type u_3} [Field K] [Algebra F K] [Algebra E K] [IsScalarTower F E K] (L : IntermediateField F K) (halg : Algebra.IsAlgebraic F L) :
                    theorem IntermediateField.adjoin_simple_le_iff {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {α : E} {K : IntermediateField F E} :
                    Fα K α K
                    theorem IntermediateField.biSup_adjoin_simple {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] (S : Set E) :
                    ⨆ x ∈ S, Fx = IntermediateField.adjoin F S

                    Adjoining a single element is compact in the lattice of intermediate fields.

                    Adjoining a finite subset is compact in the lattice of intermediate fields.

                    Adjoining a finite subset is compact in the lattice of intermediate fields.

                    The lattice of intermediate fields is compactly generated.

                    Equations
                    • =
                    theorem IntermediateField.exists_finset_of_mem_iSup {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {ι : Type u_3} {f : ιIntermediateField F E} {x : E} (hx : x ⨆ (i : ι), f i) :
                    ∃ (s : Finset ι), x ⨆ i ∈ s, f i
                    theorem IntermediateField.exists_finset_of_mem_supr' {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {ι : Type u_3} {f : ιIntermediateField F E} {x : E} (hx : x ⨆ (i : ι), f i) :
                    ∃ (s : Finset ((i : ι) × (f i))), x ⨆ i ∈ s, Fi.snd
                    theorem IntermediateField.exists_finset_of_mem_supr'' {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {ι : Type u_3} {f : ιIntermediateField F E} (h : ∀ (i : ι), Algebra.IsAlgebraic F (f i)) {x : E} (hx : x ⨆ (i : ι), f i) :
                    ∃ (s : Finset ((i : ι) × (f i))), x ⨆ i ∈ s, IntermediateField.adjoin F (Polynomial.rootSet (minpoly F i.snd) E)
                    theorem IntermediateField.exists_finset_of_mem_adjoin {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {S : Set E} {x : E} (hx : x IntermediateField.adjoin F S) :
                    ∃ (T : Finset E), T S x IntermediateField.adjoin F T
                    @[simp]
                    theorem IntermediateField.adjoin_eq_bot_iff {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {S : Set E} :
                    theorem IntermediateField.adjoin_simple_eq_bot_iff {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {α : E} :
                    Fα = α
                    @[simp]
                    theorem IntermediateField.adjoin_zero {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] :
                    F0 =
                    @[simp]
                    theorem IntermediateField.adjoin_one {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] :
                    F1 =
                    @[simp]
                    theorem IntermediateField.adjoin_int {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] (n : ) :
                    Fn =
                    @[simp]
                    theorem IntermediateField.adjoin_nat {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] (n : ) :
                    Fn =
                    @[simp]
                    theorem IntermediateField.rank_eq_one_iff {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {K : IntermediateField F E} :
                    Module.rank F K = 1 K =
                    @[simp]
                    theorem IntermediateField.finrank_eq_one_iff {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {K : IntermediateField F E} :
                    @[simp]
                    theorem IntermediateField.rank_bot {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] :
                    @[simp]
                    theorem IntermediateField.finrank_bot {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] :
                    @[simp]
                    theorem IntermediateField.rank_bot' {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] :
                    @[simp]
                    theorem IntermediateField.rank_top {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] :
                    Module.rank () E = 1
                    @[simp]
                    theorem IntermediateField.finrank_top {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] :
                    @[simp]
                    theorem IntermediateField.rank_top' {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] :
                    theorem IntermediateField.rank_adjoin_eq_one_iff {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {S : Set E} :
                    theorem IntermediateField.rank_adjoin_simple_eq_one_iff {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {α : E} :
                    Module.rank F Fα = 1 α
                    theorem IntermediateField.finrank_adjoin_simple_eq_one_iff {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {α : E} :
                    FiniteDimensional.finrank F Fα = 1 α
                    theorem IntermediateField.bot_eq_top_of_rank_adjoin_eq_one {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] (h : ∀ (x : E), Module.rank F Fx = 1) :

                    If F⟮x⟯ has dimension 1 over F for every x ∈ E then F = E.

                    theorem IntermediateField.bot_eq_top_of_finrank_adjoin_eq_one {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] (h : ∀ (x : E), FiniteDimensional.finrank F Fx = 1) :
                    theorem IntermediateField.subsingleton_of_rank_adjoin_eq_one {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] (h : ∀ (x : E), Module.rank F Fx = 1) :
                    theorem IntermediateField.bot_eq_top_of_finrank_adjoin_le_one {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] [FiniteDimensional F E] (h : ∀ (x : E), FiniteDimensional.finrank F Fx 1) :

                    If F⟮x⟯ has dimension ≤1 over F for every x ∈ E then F = E.

                    theorem IntermediateField.minpoly_gen (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] (α : E) :
                    noncomputable def IntermediateField.adjoinRootEquivAdjoin (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] {α : E} (h : IsIntegral F α) :
                    AdjoinRoot (minpoly F α) ≃ₐ[F] Fα

                    algebra isomorphism between AdjoinRoot and F⟮α⟯

                    Equations
                    Instances For
                      noncomputable def IntermediateField.powerBasisAux {K : Type u} [Field K] {L : Type u_3} [Field L] [Algebra K L] {x : L} (hx : IsIntegral K x) :
                      Basis (Fin (Polynomial.natDegree (minpoly K x))) K Kx

                      The elements 1, x, ..., x ^ (d - 1) form a basis for K⟮x⟯, where d is the degree of the minimal polynomial of x.

                      Equations
                      Instances For
                        noncomputable def IntermediateField.adjoin.powerBasis {K : Type u} [Field K] {L : Type u_3} [Field L] [Algebra K L] {x : L} (hx : IsIntegral K x) :
                        PowerBasis K Kx

                        The power basis 1, x, ..., x ^ (d - 1) for K⟮x⟯, where d is the degree of the minimal polynomial of x.

                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          theorem IntermediateField.adjoin.finiteDimensional {K : Type u} [Field K] {L : Type u_3} [Field L] [Algebra K L] {x : L} (hx : IsIntegral K x) :
                          FiniteDimensional K Kx
                          theorem IntermediateField.isAlgebraic_adjoin_simple {K : Type u} [Field K] {L : Type u_3} [Field L] [Algebra K L] {x : L} (hx : IsIntegral K x) :
                          Algebra.IsAlgebraic K Kx
                          theorem IntermediateField.adjoin.finrank {K : Type u} [Field K] {L : Type u_3} [Field L] [Algebra K L] {x : L} (hx : IsIntegral K x) :
                          theorem IntermediateField.adjoin_eq_top_of_adjoin_eq_top (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] {K : Type u} [Field K] [Algebra F K] [Algebra E K] [IsScalarTower F E K] {S : Set K} (hprim : IntermediateField.adjoin F S = ) :

                          If K / E / F is a field extension tower, S ⊂ K is such that F(S) = K, then E(S) = K.

                          theorem IntermediateField.adjoin_minpoly_coeff_of_exists_primitive_element (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] {α : E} [FiniteDimensional F E] (hprim : Fα = ) (K : IntermediateField F E) :

                          If E / F is a finite extension such that E = F(α), then for any intermediate field K, the F adjoin the coefficients of minpoly K α is equal to K itself.

                          If E / F is an infinite algebraic extension, then there exists an intermediate field L / F with arbitrarily large finite extension degree.

                          theorem minpoly.degree_le {K : Type u} [Field K] {L : Type u_3} [Field L] [Algebra K L] (x : L) [FiniteDimensional K L] :
                          theorem IntermediateField.isAlgebraic_iSup {K : Type u} [Field K] {L : Type u_3} [Field L] [Algebra K L] {ι : Type u_4} {t : ιIntermediateField K L} (h : ∀ (i : ι), Algebra.IsAlgebraic K (t i)) :
                          Algebra.IsAlgebraic K (⨆ (i : ι), t i)

                          A compositum of algebraic extensions is algebraic

                          theorem IntermediateField.isAlgebraic_adjoin {K : Type u} [Field K] {L : Type u_3} [Field L] [Algebra K L] {S : Set L} (hS : xS, IsIntegral K x) :
                          theorem IntermediateField.finiteDimensional_adjoin {K : Type u} [Field K] {L : Type u_3} [Field L] [Algebra K L] {S : Set L} [Finite S] (hS : xS, IsIntegral K x) :

                          If L / K is a field extension, S is a finite subset of L, such that every element of S is integral (= algebraic) over K, then K(S) / K is a finite extension. A direct corollary of finiteDimensional_iSup_of_finite.

                          noncomputable def IntermediateField.algHomAdjoinIntegralEquiv (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] {α : E} {K : Type u} [Field K] [Algebra F K] (h : IsIntegral F α) :
                          (Fα →ₐ[F] K) { x : K // x Polynomial.aroots (minpoly F α) K }

                          Algebra homomorphism F⟮α⟯ →ₐ[F] K are in bijection with the set of roots of minpoly α in K.

                          Equations
                          Instances For
                            theorem IntermediateField.algHomAdjoinIntegralEquiv_symm_apply_gen (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] {α : E} {K : Type u} [Field K] [Algebra F K] (h : IsIntegral F α) (x : { x : K // x Polynomial.aroots (minpoly F α) K }) :
                            noncomputable def IntermediateField.fintypeOfAlgHomAdjoinIntegral (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] {α : E} {K : Type u} [Field K] [Algebra F K] (h : IsIntegral F α) :
                            Fintype (Fα →ₐ[F] K)

                            Fintype of algebra homomorphism F⟮α⟯ →ₐ[F] K

                            Equations
                            Instances For
                              theorem IntermediateField.card_algHom_adjoin_integral (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] {α : E} {K : Type u} [Field K] [Algebra F K] (h : IsIntegral F α) (h_sep : Polynomial.Separable (minpoly F α)) (h_splits : Polynomial.Splits (algebraMap F K) (minpoly F α)) :
                              theorem Polynomial.irreducible_comp {K : Type u} [Field K] {f : Polynomial K} {g : Polynomial K} (hfm : Polynomial.Monic f) (hgm : Polynomial.Monic g) (hf : Irreducible f) (hg : ∀ (E : Type u) [inst : Field E] [inst_1 : Algebra K E] (x : E), minpoly K x = fIrreducible (Polynomial.map (algebraMap K Kx) g - Polynomial.C (IntermediateField.AdjoinSimple.gen K x))) :

                              Let f, g be monic polynomials over K. If f is irreducible, and g(x) - α is irreducible in K⟮α⟯ with α a root of f, then f(g(x)) is irreducible.

                              def IntermediateField.FG {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] (S : IntermediateField F E) :

                              An intermediate field S is finitely generated if there exists t : Finset E such that IntermediateField.adjoin F t = S.

                              Equations
                              Instances For
                                theorem IntermediateField.fG_of_fG_toSubalgebra {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] (S : IntermediateField F E) (h : Subalgebra.FG S.toSubalgebra) :
                                theorem IntermediateField.induction_on_adjoin_finset {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] (S : Finset E) (P : IntermediateField F EProp) (base : P ) (ih : ∀ (K : IntermediateField F E), xS, P KP (IntermediateField.restrictScalars F (K)x)) :
                                theorem IntermediateField.induction_on_adjoin_fg {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] (P : IntermediateField F EProp) (base : P ) (ih : ∀ (K : IntermediateField F E) (x : E), P KP (IntermediateField.restrictScalars F (K)x)) (K : IntermediateField F E) (hK : IntermediateField.FG K) :
                                P K
                                theorem IntermediateField.induction_on_adjoin {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] [FiniteDimensional F E] (P : IntermediateField F EProp) (base : P ) (ih : ∀ (K : IntermediateField F E) (x : E), P KP (IntermediateField.restrictScalars F (K)x)) (K : IntermediateField F E) :
                                P K
                                noncomputable def PowerBasis.equivAdjoinSimple {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (pb : PowerBasis K L) :
                                Kpb.gen ≃ₐ[K] L

                                pb.equivAdjoinSimple is the equivalence between K⟮pb.gen⟯ and L itself.

                                Equations
                                Instances For
                                  @[simp]