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.

Stacks Tag 09FZ (first part)

Equations
Instances For
    @[simp]
    theorem IntermediateField.adjoin_toSubfield (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] (S : Set E) :
    theorem IntermediateField.mem_adjoin_range_iff (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] {ι : Type u_3} (i : ιE) (x : E) :
    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
    Instances For
      Equations
      theorem IntermediateField.sup_def {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] (S T : IntermediateField F E) :
      S T = IntermediateField.adjoin F (S T)
      theorem IntermediateField.sSup_def {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] (S : Set (IntermediateField F E)) :
      sSup S = IntermediateField.adjoin F (⋃₀ (SetLike.coe '' S))
      instance IntermediateField.instInhabited {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] :
      Equations
      • IntermediateField.instInhabited = { 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 =
      theorem IntermediateField.bot_toSubfield {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] :
      .toSubfield = (algebraMap F E).fieldRange
      @[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.top_toSubfield {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] :
      .toSubfield =
      @[simp]
      theorem IntermediateField.coe_inf {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] (S 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 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 T : IntermediateField F E) :
      (S T).toSubalgebra = S.toSubalgebra T.toSubalgebra
      @[simp]
      theorem IntermediateField.inf_toSubfield {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] (S T : IntermediateField F E) :
      (S T).toSubfield = S.toSubfield T.toSubfield
      @[simp]
      theorem IntermediateField.sup_toSubfield {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] (S T : IntermediateField F E) :
      (S T).toSubfield = S.toSubfield T.toSubfield
      @[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)) :
      (sInf S).toSubfield = sInf (IntermediateField.toSubfield '' S)
      @[simp]
      theorem IntermediateField.sSup_toSubfield {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] (S : Set (IntermediateField F E)) (hS : S.Nonempty) :
      (sSup S).toSubfield = sSup (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) :
      (iInf S).toSubfield = ⨅ (i : ι), (S i).toSubfield
      @[simp]
      theorem IntermediateField.iSup_toSubfield {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {ι : Sort u_3} [Nonempty ι] (S : ιIntermediateField F E) :
      (iSup S).toSubfield = ⨆ (i : ι), (S i).toSubfield
      def IntermediateField.equivOfEq {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {S 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_apply {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {S T : IntermediateField F E} (h : S = T) (x : S.toSubalgebra) :
        (IntermediateField.equivOfEq h) x = x,
        @[simp]
        theorem IntermediateField.equivOfEq_symm {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {S T : IntermediateField F E} (h : S = T) :
        @[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
        @[simp]
        theorem IntermediateField.equivOfEq_trans {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {S T U : IntermediateField F E} (hST : S = T) (hTU : T = U) :
        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] :
          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
          • IntermediateField.topEquiv = Subalgebra.topEquiv
          Instances For
            @[simp]
            theorem IntermediateField.topEquiv_symm_apply_coe {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] (a : E) :
            (IntermediateField.topEquiv.symm a) = a
            @[simp]
            theorem IntermediateField.topEquiv_apply {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] (a : ) :
            IntermediateField.topEquiv a = a
            @[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 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 IntermediateField.map_inf {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 t : IntermediateField F E) (f : E →ₐ[F] K) :
            theorem IntermediateField.map_iInf {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} [Nonempty ι] (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) :
            f.fieldRange = IntermediateField.map f
            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) :
            IntermediateField.map g f.fieldRange = (g.comp f).fieldRange
            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} :
            f.fieldRange = Function.Surjective f
            @[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) :
            (↑f).fieldRange =
            theorem IntermediateField.fieldRange_comp_val {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) :
            (f.comp L.val).fieldRange = IntermediateField.map f L
            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) :
              ((L.equivMap 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 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) :
              (IntermediateField.adjoin F S).toSubfield 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 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.adjoin_iUnion (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] {ι : Sort u_3} (f : ιSet E) :
              IntermediateField.adjoin F (⋃ (i : ι), f i) = ⨆ (i : ι), IntermediateField.adjoin F (f i)
              theorem IntermediateField.iSup_eq_adjoin (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] {ι : Sort u_3} (f : ιIntermediateField F E) :
              ⨆ (i : ι), f i = IntermediateField.adjoin F (⋃ (i : ι), (f i))
              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 : (x : E) → x IntermediateField.adjoin F sProp} (mem : ∀ (x : E) (hx : x s), p x ) (algebraMap : ∀ (x : F), p ((algebraMap F E) x) ) (add : ∀ (x y : E) (hx : x IntermediateField.adjoin F s) (hy : y IntermediateField.adjoin F s), p x hxp y hyp (x + y) ) (inv : ∀ (x : E) (hx : x IntermediateField.adjoin F s), p x hxp x⁻¹ ) (mul : ∀ (x y : E) (hx : x IntermediateField.adjoin F s) (hy : y IntermediateField.adjoin F s), p x hxp y hyp (x * y) ) {x : E} (h : x IntermediateField.adjoin F s) :
              p x h
              theorem IntermediateField.adjoin_algHom_ext (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] {K : Type u_3} [Semiring K] [Algebra F K] {s : Set E} ⦃φ₁ φ₂ : (IntermediateField.adjoin F s) →ₐ[F] K (h : ∀ (x : E) (hx : x s), φ₁ x, = φ₂ x, ) :
              φ₁ = φ₂
              theorem IntermediateField.algHom_ext_of_eq_adjoin (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] {K : Type u_3} [Semiring K] [Algebra F K] {S : IntermediateField F E} {s : Set E} (hS : S = IntermediateField.adjoin F s) ⦃φ₁ φ₂ : S →ₐ[F] K (h : ∀ (x : E) (hx : x s), φ₁ x, = φ₂ 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) :
                    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) :
                    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 {α}

                    Characterize IsSplittingField with IntermediateField.adjoin instead of Algebra.adjoin.

                    theorem IntermediateField.le_sup_toSubalgebra {K : Type u_3} {L : Type u_4} [Field K] [Field L] [Algebra K L] (E1 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 E2 : IntermediateField K L) [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 E2 : IntermediateField K L) [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 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 E2 : IntermediateField K L) [FiniteDimensional K E1] :
                    (E1 E2).toSubalgebra = E1.toSubalgebra E2.toSubalgebra
                    theorem IntermediateField.sup_toSubalgebra_of_right {K : Type u_3} {L : Type u_4} [Field K] [Field L] [Algebra K L] (E1 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 E2 : IntermediateField K L) [FiniteDimensional K E1] [FiniteDimensional K E2] :
                    FiniteDimensional K (E1 E2)
                    theorem IntermediateField.rank_sup_le_of_isAlgebraic {K : Type u_3} {L : Type u_4} [Field K] [Field L] [Algebra K L] (E1 E2 : IntermediateField K L) (halg : Algebra.IsAlgebraic K E1 Algebra.IsAlgebraic K E2) :
                    Module.rank K (E1 E2) Module.rank K E1 * Module.rank K E2

                    If E1 and E2 are intermediate fields, and at least one them are algebraic, then the rank of the compositum of E1 and E2 is less than or equal to the product of that of E1 and E2. Note that this result is also true without algebraic assumption, but the proof becomes very complicated.

                    theorem IntermediateField.finrank_sup_le {K : Type u_3} {L : Type u_4} [Field K] [Field L] [Algebra K L] (E1 E2 : IntermediateField K L) :
                    Module.finrank K (E1 E2) Module.finrank K E1 * Module.finrank K E2

                    If E1 and E2 are intermediate fields, then the Module.finrank of the compositum of E1 and E2 is less than or equal to the product of that of E1 and E2.

                    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 (x1 x2 : IntermediateField K L) => x1 x2) 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 (x1 x2 : IntermediateField K L) => x1 x2) 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)
                    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 (⨆ is, t i)
                    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 (⨆ is, 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 : is, p i 0) (h : is, Polynomial.IsSplittingField K (↥(t i)) (p i)) :
                    Polynomial.IsSplittingField K (↥(⨆ is, t i)) (∏ is, 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) :
                    xS, 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.

                    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 is, 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 is, 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 is, IntermediateField.adjoin F ((minpoly F i.snd).rootSet 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_intCast {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] (n : ) :
                    Fn =
                    @[simp]
                    theorem IntermediateField.adjoin_natCast {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] (n : ) :
                    Fn =
                    @[deprecated IntermediateField.adjoin_intCast]
                    theorem IntermediateField.adjoin_int {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] (n : ) :
                    Fn =

                    Alias of IntermediateField.adjoin_intCast.

                    @[deprecated IntermediateField.adjoin_natCast]
                    theorem IntermediateField.adjoin_nat {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] (n : ) :
                    Fn =

                    Alias of IntermediateField.adjoin_natCast.

                    @[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} :
                    Module.finrank F K = 1 K =
                    @[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.finrank_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] :
                    @[simp]
                    theorem IntermediateField.finrank_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} :
                    Module.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), Module.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.subsingleton_of_finrank_adjoin_eq_one {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] (h : ∀ (x : E), Module.finrank 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), Module.finrank F Fx 1) :

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

                    theorem IntermediateField.subsingleton_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), Module.finrank F Fx 1) :
                    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⟮α⟯

                    Stacks Tag 09G1 (Algebraic case)

                    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 (minpoly K x).natDegree) 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
                        Instances For
                          @[simp]
                          theorem IntermediateField.adjoin.powerBasis_dim {K : Type u} [Field K] {L : Type u_3} [Field L] [Algebra K L] {x : L} (hx : IsIntegral K x) :
                          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) :
                          Module.finrank K Kx = (minpoly K x).natDegree

                          If x is an algebraic element of field K, then its minimal polynomial has degree [K(x) : K].

                          Stacks Tag 09GN

                          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) :
                          IntermediateField.adjoin F (Polynomial.map (algebraMap (↥K) E) (minpoly (↥K) α)).coeffs = K

                          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.natDegree_le {K : Type u} [Field K] {L : Type u_3} [Field L] [Algebra K L] (x : L) [FiniteDimensional K L] :
                          (minpoly K x).natDegree Module.finrank K L
                          theorem minpoly.degree_le {K : Type u} [Field K] {L : Type u_3} [Field L] [Algebra K L] (x : L) [FiniteDimensional K L] :
                          (minpoly K x).degree (Module.finrank K L)
                          theorem minpoly.degree_dvd {K : Type u} [Field K] {L : Type u_3} [Field L] [Algebra K L] {x : L} (hx : IsIntegral K x) :
                          (minpoly K x).natDegree Module.finrank K L

                          If x : L is an integral element in a field extension L over K, then the degree of the minimal polynomial of x over K divides [L : K].

                          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 (minpoly F α).aroots 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 (minpoly F α).aroots 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 : IsSeparable F α) (h_splits : Polynomial.Splits (algebraMap F K) (minpoly F α)) :
                              Fintype.card (Fα →ₐ[F] K) = (minpoly F α).natDegree
                              theorem Polynomial.irreducible_comp {K : Type u} [Field K] {f g : Polynomial K} (hfm : f.Monic) (hgm : g.Monic) (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))) :
                              Irreducible (f.comp g)

                              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.

                              Stacks Tag 09FZ (second part)

                              Equations
                              Instances For
                                theorem IntermediateField.fg_adjoin_finset {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] (t : Finset E) :
                                theorem IntermediateField.fg_def {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {S : IntermediateField F E} :
                                S.FG ∃ (t : Set E), t.Finite IntermediateField.adjoin F t = S
                                theorem IntermediateField.fg_adjoin_of_finite {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {t : Set E} (h : t.Finite) :
                                theorem IntermediateField.fg_bot {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] :
                                .FG
                                theorem IntermediateField.fg_sup {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {S T : IntermediateField F E} (hS : S.FG) (hT : T.FG) :
                                (S T).FG
                                theorem IntermediateField.fg_iSup {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {ι : Sort u_3} [Finite ι] {S : ιIntermediateField F E} (h : ∀ (i : ι), (S i).FG) :
                                (⨆ (i : ι), S i).FG
                                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 : S.FG) :
                                S.FG
                                @[deprecated IntermediateField.fg_of_fg_toSubalgebra]
                                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 : S.FG) :
                                S.FG

                                Alias of IntermediateField.fg_of_fg_toSubalgebra.

                                theorem IntermediateField.fg_of_noetherian {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] (S : IntermediateField F E) [IsNoetherian F E] :
                                S.FG
                                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 : K.FG) :
                                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 AdjoinRoot.algHomOfDvd {K : Type u_1} [Field K] {p q : Polynomial K} (hpq : q p) :

                                The canonical algebraic homomorphism from AdjoinRoot p to AdjoinRoot q, where the polynomial q : K[X] divides p.

                                Equations
                                Instances For
                                  theorem AdjoinRoot.coe_algHomOfDvd {K : Type u_1} [Field K] {p q : Polynomial K} (hpq : q p) :
                                  (↑(AdjoinRoot.algHomOfDvd hpq).toRingHom).toFun = (AdjoinRoot.liftHom p (AdjoinRoot.root q) )
                                  noncomputable def AdjoinRoot.algEquivOfEq {K : Type u_1} [Field K] {p q : Polynomial K} (hp : p 0) (h_eq : p = q) :

                                  The canonical algebraic equivalence between AdjoinRoot p and AdjoinRoot q, where the two polynomials p q : K[X] are equal.

                                  Equations
                                  Instances For
                                    theorem AdjoinRoot.coe_algEquivOfEq {K : Type u_1} [Field K] {p q : Polynomial K} (hp : p 0) (h_eq : p = q) :
                                    theorem AdjoinRoot.algEquivOfEq_toAlgHom {K : Type u_1} [Field K] {p q : Polynomial K} (hp : p 0) (h_eq : p = q) :
                                    noncomputable def AdjoinRoot.algEquivOfAssociated {K : Type u_1} [Field K] {p q : Polynomial K} (hp : p 0) (hpq : Associated p q) :

                                    The canonical algebraic equivalence between AdjoinRoot p and AdjoinRoot q, where the two polynomials p q : K[X] are associated.

                                    Equations
                                    Instances For
                                      theorem AdjoinRoot.coe_algEquivOfAssociated {K : Type u_1} [Field K] {p q : Polynomial K} (hp : p 0) (hpq : Associated p q) :
                                      theorem minpoly.eq_of_root {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {x y : L} (hx : IsAlgebraic K x) (h_ev : (Polynomial.aeval y) (minpoly K x) = 0) :
                                      minpoly K y = minpoly K x

                                      If y : L is a root of minpoly K x, then minpoly K y = minpoly K x.

                                      noncomputable def minpoly.algEquiv {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {x y : L} (hx : IsAlgebraic K x) (h_mp : minpoly K x = minpoly K y) :
                                      Kx ≃ₐ[K] Ky

                                      The canonical algEquiv between K⟮x⟯and K⟮y⟯, sending x to y, where x and y have the same minimal polynomial over K.

                                      Equations
                                      Instances For
                                        theorem minpoly.algEquiv_apply {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {x y : L} (hx : IsAlgebraic K x) (h_mp : minpoly K x = minpoly K y) :

                                        minpoly.algEquiv sends the generator of K⟮x⟯ to the generator of K⟮y⟯.

                                        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]
                                          theorem PowerBasis.equivAdjoinSimple_aeval {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (pb : PowerBasis K L) (f : Polynomial K) :
                                          pb.equivAdjoinSimple ((Polynomial.aeval (IntermediateField.AdjoinSimple.gen K pb.gen)) f) = (Polynomial.aeval pb.gen) f
                                          @[simp]
                                          theorem PowerBasis.equivAdjoinSimple_gen {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (pb : PowerBasis K L) :
                                          pb.equivAdjoinSimple (IntermediateField.AdjoinSimple.gen K pb.gen) = pb.gen
                                          @[simp]
                                          theorem PowerBasis.equivAdjoinSimple_symm_aeval {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (pb : PowerBasis K L) (f : Polynomial K) :
                                          pb.equivAdjoinSimple.symm ((Polynomial.aeval pb.gen) f) = (Polynomial.aeval (IntermediateField.AdjoinSimple.gen K pb.gen)) f
                                          @[simp]
                                          theorem PowerBasis.equivAdjoinSimple_symm_gen {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (pb : PowerBasis K L) :
                                          pb.equivAdjoinSimple.symm pb.gen = IntermediateField.AdjoinSimple.gen K pb.gen
                                          theorem IntermediateField.map_comap_eq {K : Type u_1} {L : Type u_2} {L' : Type u_3} [Field K] [Field L] [Field L'] [Algebra K L] [Algebra K L'] (f : L →ₐ[K] L') (S : IntermediateField K L') :
                                          theorem IntermediateField.map_comap_eq_self {K : Type u_1} {L : Type u_2} {L' : Type u_3} [Field K] [Field L] [Field L'] [Algebra K L] [Algebra K L'] {f : L →ₐ[K] L'} {S : IntermediateField K L'} (h : S f.fieldRange) :
                                          theorem IntermediateField.map_comap_eq_self_of_surjective {K : Type u_1} {L : Type u_2} {L' : Type u_3} [Field K] [Field L] [Field L'] [Algebra K L] [Algebra K L'] {f : L →ₐ[K] L'} (hf : Function.Surjective f) (S : IntermediateField K L') :
                                          theorem IntermediateField.comap_map {K : Type u_1} {L : Type u_2} {L' : Type u_3} [Field K] [Field L] [Field L'] [Algebra K L] [Algebra K L'] (f : L →ₐ[K] L') (S : IntermediateField K L) :
                                          theorem IsFractionRing.algHom_fieldRange_eq_of_comp_eq {F : Type u_1} {A : Type u_2} {K : Type u_3} {L : Type u_4} [Field F] [CommRing A] [Algebra F A] [Field K] [Algebra F K] [Algebra A K] [IsFractionRing A K] [Field L] [Algebra F L] {g : A →ₐ[F] L} {f : K →ₐ[F] L} (h : (↑f).comp (algebraMap A K) = g) :
                                          f.fieldRange = IntermediateField.adjoin F g.range

                                          If F is a field, A is an F-algebra with fraction field K, L is a field, g : A →ₐ[F] L lifts to f : K →ₐ[F] L, then the image of f is the field generated by the image of g. Note: this does not require IsScalarTower F A K.

                                          theorem IsFractionRing.algHom_fieldRange_eq_of_comp_eq_of_range_eq {F : Type u_1} {A : Type u_2} {K : Type u_3} {L : Type u_4} [Field F] [CommRing A] [Algebra F A] [Field K] [Algebra F K] [Algebra A K] [IsFractionRing A K] [Field L] [Algebra F L] {g : A →ₐ[F] L} {f : K →ₐ[F] L} (h : (↑f).comp (algebraMap A K) = g) {s : Set L} (hs : g.range = Algebra.adjoin F s) :
                                          f.fieldRange = IntermediateField.adjoin F s

                                          If F is a field, A is an F-algebra with fraction field K, L is a field, g : A →ₐ[F] L lifts to f : K →ₐ[F] L, s is a set such that the image of g is the subalgebra generated by s, then the image of f is the intermediate field generated by s. Note: this does not require IsScalarTower F A K.

                                          theorem IsFractionRing.liftAlgHom_fieldRange {F : Type u_1} {A : Type u_2} {K : Type u_3} {L : Type u_4} [Field F] [CommRing A] [Algebra F A] [Field K] [Algebra F K] [Algebra A K] [IsFractionRing A K] [Field L] [Algebra F L] {g : A →ₐ[F] L} [IsScalarTower F A K] (hg : Function.Injective g) :

                                          The image of IsFractionRing.liftAlgHom is the intermediate field generated by the image of the algebra hom.

                                          theorem IsFractionRing.liftAlgHom_fieldRange_eq_of_range_eq {F : Type u_1} {A : Type u_2} {K : Type u_3} {L : Type u_4} [Field F] [CommRing A] [Algebra F A] [Field K] [Algebra F K] [Algebra A K] [IsFractionRing A K] [Field L] [Algebra F L] {g : A →ₐ[F] L} [IsScalarTower F A K] (hg : Function.Injective g) {s : Set L} (hs : g.range = Algebra.adjoin F s) :

                                          The image of IsFractionRing.liftAlgHom is the intermediate field generated by s, if the image of the algebra hom is the subalgebra generated by s.