Documentation

Mathlib.FieldTheory.IntermediateField

Intermediate fields #

Let L / K be a field extension, given as an instance Algebra K L. This file defines the type of fields in between K and L, IntermediateField K L. An IntermediateField K L is a subfield of L which contains (the image of) K, i.e. it is a Subfield L and a Subalgebra K L.

Main definitions #

Implementation notes #

Intermediate fields are defined with a structure extending Subfield and Subalgebra. A Subalgebra is closed under all operations except ⁻¹,

Tags #

intermediate field, field extension

structure IntermediateField (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra K L] extends Subalgebra :
Type u_2

S : IntermediateField K L is a subset of L such that there is a field tower L / S / K.

  • carrier : Set L
  • mul_mem' : ∀ {a b : L}, a self.carrierb self.carriera * b self.carrier
  • one_mem' : 1 self.carrier
  • add_mem' : ∀ {a b : L}, a self.carrierb self.carriera + b self.carrier
  • zero_mem' : 0 self.carrier
  • algebraMap_mem' : ∀ (r : K), (algebraMap K L) r self.carrier
  • inv_mem' : xself.carrier, x⁻¹ self.carrier
Instances For
    theorem IntermediateField.inv_mem' {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (self : IntermediateField K L) (x : L) :
    x self.carrierx⁻¹ self.carrier
    instance IntermediateField.instSetLike {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] :
    Equations
    • IntermediateField.instSetLike = { coe := fun (S : IntermediateField K L) => S.carrier, coe_injective' := }
    theorem IntermediateField.neg_mem {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (S : IntermediateField K L) {x : L} (hx : x S) :
    -x S
    def IntermediateField.toSubfield {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (S : IntermediateField K L) :

    Reinterpret an IntermediateField as a Subfield.

    Equations
    • S.toSubfield = let __src := S.toSubalgebra; { toSubsemiring := __src.toSubsemiring, neg_mem' := , inv_mem' := }
    Instances For
      Equations
      • =
      theorem IntermediateField.mem_carrier {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {s : IntermediateField K L} {x : L} :
      x s.carrier x s
      theorem IntermediateField.ext {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {S : IntermediateField K L} {T : IntermediateField K L} (h : ∀ (x : L), x S x T) :
      S = T

      Two intermediate fields are equal if they have the same elements.

      @[simp]
      theorem IntermediateField.coe_toSubalgebra {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (S : IntermediateField K L) :
      S.toSubalgebra = S
      @[simp]
      theorem IntermediateField.coe_toSubfield {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (S : IntermediateField K L) :
      S.toSubfield = S
      @[simp]
      theorem IntermediateField.mem_mk {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (s : Subsemiring L) (hK : ∀ (x : K), (algebraMap K L) x s) (hi : x{ toSubsemiring := s, algebraMap_mem' := hK }.carrier, x⁻¹ { toSubsemiring := s, algebraMap_mem' := hK }.carrier) (x : L) :
      x { toSubsemiring := s, algebraMap_mem' := hK, inv_mem' := hi } x s
      @[simp]
      theorem IntermediateField.mem_toSubalgebra {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (s : IntermediateField K L) (x : L) :
      x s.toSubalgebra x s
      @[simp]
      theorem IntermediateField.mem_toSubfield {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (s : IntermediateField K L) (x : L) :
      x s.toSubfield x s
      def IntermediateField.copy {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (S : IntermediateField K L) (s : Set L) (hs : s = S) :

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

      Equations
      • S.copy s hs = { toSubalgebra := S.copy s hs, inv_mem' := }
      Instances For
        @[simp]
        theorem IntermediateField.coe_copy {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (S : IntermediateField K L) (s : Set L) (hs : s = S) :
        (S.copy s hs) = s
        theorem IntermediateField.copy_eq {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (S : IntermediateField K L) (s : Set L) (hs : s = S) :
        S.copy s hs = S

        Lemmas inherited from more general structures #

        The declarations in this section derive from the fact that an IntermediateField is also a subalgebra or subfield. Their use should be replaceable with the corresponding lemma from a subobject class.

        theorem IntermediateField.algebraMap_mem {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (S : IntermediateField K L) (x : K) :
        (algebraMap K L) x S

        An intermediate field contains the image of the smaller field.

        theorem IntermediateField.smul_mem {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (S : IntermediateField K L) {y : L} :
        y S∀ {x : K}, x y S

        An intermediate field is closed under scalar multiplication.

        theorem IntermediateField.one_mem {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (S : IntermediateField K L) :
        1 S

        An intermediate field contains the ring's 1.

        theorem IntermediateField.zero_mem {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (S : IntermediateField K L) :
        0 S

        An intermediate field contains the ring's 0.

        theorem IntermediateField.mul_mem {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (S : IntermediateField K L) {x : L} {y : L} :
        x Sy Sx * y S

        An intermediate field is closed under multiplication.

        theorem IntermediateField.add_mem {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (S : IntermediateField K L) {x : L} {y : L} :
        x Sy Sx + y S

        An intermediate field is closed under addition.

        theorem IntermediateField.sub_mem {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (S : IntermediateField K L) {x : L} {y : L} :
        x Sy Sx - y S

        An intermediate field is closed under subtraction

        theorem IntermediateField.inv_mem {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (S : IntermediateField K L) {x : L} :
        x Sx⁻¹ S

        An intermediate field is closed under inverses.

        theorem IntermediateField.div_mem {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (S : IntermediateField K L) {x : L} {y : L} :
        x Sy Sx / y S

        An intermediate field is closed under division.

        theorem IntermediateField.list_prod_mem {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (S : IntermediateField K L) {l : List L} :
        (xl, x S)l.prod S

        Product of a list of elements in an intermediate_field is in the intermediate_field.

        theorem IntermediateField.list_sum_mem {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (S : IntermediateField K L) {l : List L} :
        (xl, x S)l.sum S

        Sum of a list of elements in an intermediate field is in the intermediate_field.

        theorem IntermediateField.multiset_prod_mem {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (S : IntermediateField K L) (m : Multiset L) :
        (am, a S)m.prod S

        Product of a multiset of elements in an intermediate field is in the intermediate_field.

        theorem IntermediateField.multiset_sum_mem {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (S : IntermediateField K L) (m : Multiset L) :
        (am, a S)m.sum S

        Sum of a multiset of elements in an IntermediateField is in the IntermediateField.

        theorem IntermediateField.prod_mem {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (S : IntermediateField K L) {ι : Type u_4} {t : Finset ι} {f : ιL} (h : ct, f c S) :
        (t.prod fun (i : ι) => f i) S

        Product of elements of an intermediate field indexed by a Finset is in the intermediate_field.

        theorem IntermediateField.sum_mem {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (S : IntermediateField K L) {ι : Type u_4} {t : Finset ι} {f : ιL} (h : ct, f c S) :
        (t.sum fun (i : ι) => f i) S

        Sum of elements in an IntermediateField indexed by a Finset is in the IntermediateField.

        theorem IntermediateField.pow_mem {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (S : IntermediateField K L) {x : L} (hx : x S) (n : ) :
        x ^ n S
        theorem IntermediateField.zsmul_mem {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (S : IntermediateField K L) {x : L} (hx : x S) (n : ) :
        n x S
        theorem IntermediateField.intCast_mem {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (S : IntermediateField K L) (n : ) :
        n S
        theorem IntermediateField.coe_add {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (S : IntermediateField K L) (x : S) (y : S) :
        (x + y) = x + y
        theorem IntermediateField.coe_neg {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (S : IntermediateField K L) (x : S) :
        (-x) = -x
        theorem IntermediateField.coe_mul {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (S : IntermediateField K L) (x : S) (y : S) :
        (x * y) = x * y
        theorem IntermediateField.coe_inv {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (S : IntermediateField K L) (x : S) :
        x⁻¹ = (x)⁻¹
        theorem IntermediateField.coe_zero {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (S : IntermediateField K L) :
        0 = 0
        theorem IntermediateField.coe_one {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (S : IntermediateField K L) :
        1 = 1
        theorem IntermediateField.coe_pow {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (S : IntermediateField K L) (x : S) (n : ) :
        (x ^ n) = x ^ n
        theorem IntermediateField.natCast_mem {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (S : IntermediateField K L) (n : ) :
        n S
        @[deprecated natCast_mem]
        theorem IntermediateField.coe_nat_mem {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (S : IntermediateField K L) (n : ) :
        n S

        Alias of IntermediateField.natCast_mem.

        @[deprecated intCast_mem]
        theorem IntermediateField.coe_int_mem {R : Type u} {S : Type v} [Ring R] [SetLike S R] [hSR : SubringClass S R] (s : S) (n : ) :
        n s

        Alias of intCast_mem.

        def Subalgebra.toIntermediateField {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (S : Subalgebra K L) (inv_mem : xS, x⁻¹ S) :

        Turn a subalgebra closed under inverses into an intermediate field

        Equations
        • S.toIntermediateField inv_mem = { toSubalgebra := S, inv_mem' := inv_mem }
        Instances For
          @[simp]
          theorem toSubalgebra_toIntermediateField {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (S : Subalgebra K L) (inv_mem : xS, x⁻¹ S) :
          (S.toIntermediateField inv_mem).toSubalgebra = S
          @[simp]
          theorem toIntermediateField_toSubalgebra {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (S : IntermediateField K L) :
          S.toIntermediateField = S
          def Subalgebra.toIntermediateField' {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (S : Subalgebra K L) (hS : IsField S) :

          Turn a subalgebra satisfying IsField into an intermediate_field

          Equations
          • S.toIntermediateField' hS = S.toIntermediateField
          Instances For
            @[simp]
            theorem toSubalgebra_toIntermediateField' {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (S : Subalgebra K L) (hS : IsField S) :
            (S.toIntermediateField' hS).toSubalgebra = S
            @[simp]
            theorem toIntermediateField'_toSubalgebra {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (S : IntermediateField K L) :
            S.toIntermediateField' = S
            def Subfield.toIntermediateField {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (S : Subfield L) (algebra_map_mem : ∀ (x : K), (algebraMap K L) x S) :

            Turn a subfield of L containing the image of K into an intermediate field

            Equations
            • S.toIntermediateField algebra_map_mem = { toSubsemiring := S.toSubsemiring, algebraMap_mem' := algebra_map_mem, inv_mem' := }
            Instances For
              instance IntermediateField.toField {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (S : IntermediateField K L) :
              Field S

              An intermediate field inherits a field structure

              Equations
              • S.toField = S.toSubfield.toField
              @[simp]
              theorem IntermediateField.coe_sum {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (S : IntermediateField K L) {ι : Type u_4} [Fintype ι] (f : ιS) :
              (Finset.univ.sum fun (i : ι) => f i) = Finset.univ.sum fun (i : ι) => (f i)
              theorem IntermediateField.coe_prod {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (S : IntermediateField K L) {ι : Type u_4} [Fintype ι] (f : ιS) :
              (Finset.univ.prod fun (i : ι) => f i) = Finset.univ.prod fun (i : ι) => (f i)

              IntermediateFields inherit structure from their Subalgebra coercions.

              instance IntermediateField.module' {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (S : IntermediateField K L) {R : Type u_4} [Semiring R] [SMul R K] [Module R L] [IsScalarTower R K L] :
              Module R S
              Equations
              • S.module' = S.module'
              instance IntermediateField.module {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (S : IntermediateField K L) :
              Module K S
              Equations
              instance IntermediateField.isScalarTower {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (S : IntermediateField K L) {R : Type u_4} [Semiring R] [SMul R K] [Module R L] [IsScalarTower R K L] :
              IsScalarTower R K S
              Equations
              • =
              @[simp]
              theorem IntermediateField.coe_smul {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (S : IntermediateField K L) {R : Type u_4} [Semiring R] [SMul R K] [Module R L] [IsScalarTower R K L] (r : R) (x : S) :
              (r x) = r x
              instance IntermediateField.algebra {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (S : IntermediateField K L) :
              Algebra K S
              Equations
              @[simp]
              theorem IntermediateField.algebraMap_apply {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (S : IntermediateField K L) (x : S) :
              (algebraMap (S) L) x = x
              @[simp]
              theorem IntermediateField.coe_algebraMap_apply {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (S : IntermediateField K L) (x : K) :
              ((algebraMap K S) x) = (algebraMap K L) x
              instance IntermediateField.isScalarTower_bot {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (S : IntermediateField K L) {R : Type u_4} [Semiring R] [Algebra L R] :
              IsScalarTower (S) L R
              Equations
              • =
              instance IntermediateField.isScalarTower_mid {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (S : IntermediateField K L) {R : Type u_4} [Semiring R] [Algebra L R] [Algebra K R] [IsScalarTower K L R] :
              IsScalarTower K (S) R
              Equations
              • =
              instance IntermediateField.isScalarTower_mid' {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (S : IntermediateField K L) :
              IsScalarTower K (S) L

              Specialize is_scalar_tower_mid to the common case where the top field is L

              Equations
              • =
              instance IntermediateField.instAlgebraSubtypeMem {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {S : IntermediateField K L} {E : Type u_4} [Field E] [Algebra L E] (T : IntermediateField (S) E) :
              Algebra S T
              Equations
              instance IntermediateField.instModuleSubtypeMem {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {S : IntermediateField K L} {E : Type u_4} [Field E] [Algebra L E] (T : IntermediateField (S) E) :
              Module S T
              Equations
              instance IntermediateField.instSMulSubtypeMem {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {S : IntermediateField K L} {E : Type u_4} [Field E] [Algebra L E] (T : IntermediateField (S) E) :
              SMul S T
              Equations
              instance IntermediateField.instIsScalarTowerSubtypeMem {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {S : IntermediateField K L} {E : Type u_4} [Field E] [Algebra L E] (T : IntermediateField (S) E) [Algebra K E] [IsScalarTower K L E] :
              IsScalarTower K S T
              Equations
              • =
              def IntermediateField.comap {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') :

              Given f : L →ₐ[K] L', S.comap f is the intermediate field between K and L such that f x ∈ S ↔ x ∈ S.comap f.

              Equations
              Instances For
                def IntermediateField.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) :

                Given f : L →ₐ[K] L', S.map f is the intermediate field between K and L' such that x ∈ S ↔ f x ∈ S.map f.

                Equations
                Instances For
                  @[simp]
                  theorem IntermediateField.coe_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'] (S : IntermediateField K L) (f : L →ₐ[K] L') :
                  (IntermediateField.map f S) = f '' S
                  @[simp]
                  theorem IntermediateField.toSubalgebra_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'] (S : IntermediateField K L) (f : L →ₐ[K] L') :
                  (IntermediateField.map f S).toSubalgebra = Subalgebra.map f S.toSubalgebra
                  @[simp]
                  theorem IntermediateField.toSubfield_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'] (S : IntermediateField K L) (f : L →ₐ[K] L') :
                  (IntermediateField.map f S).toSubfield = Subfield.map (f) S.toSubfield
                  theorem IntermediateField.map_map {K : Type u_4} {L₁ : Type u_5} {L₂ : Type u_6} {L₃ : Type u_7} [Field K] [Field L₁] [Algebra K L₁] [Field L₂] [Algebra K L₂] [Field L₃] [Algebra K L₃] (E : IntermediateField K L₁) (f : L₁ →ₐ[K] L₂) (g : L₂ →ₐ[K] L₃) :
                  theorem IntermediateField.map_mono {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} {T : IntermediateField K L} (h : S T) :
                  theorem IntermediateField.map_le_iff_le_comap {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} {t : IntermediateField K L'} :
                  theorem IntermediateField.gc_map_comap {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') :
                  def IntermediateField.intermediateFieldMap {K : Type u_1} {L : Type u_2} {L' : Type u_3} [Field K] [Field L] [Field L'] [Algebra K L] [Algebra K L'] (e : L ≃ₐ[K] L') (E : IntermediateField K L) :
                  E ≃ₐ[K] (IntermediateField.map (e) E)

                  Given an equivalence e : L ≃ₐ[K] L' of K-field extensions and an intermediate field E of L/K, intermediateFieldMap e E is the induced equivalence between E and E.map e

                  Equations
                  Instances For
                    @[simp]
                    theorem IntermediateField.intermediateFieldMap_apply_coe {K : Type u_1} {L : Type u_2} {L' : Type u_3} [Field K] [Field L] [Field L'] [Algebra K L] [Algebra K L'] (e : L ≃ₐ[K] L') (E : IntermediateField K L) (a : E) :
                    @[simp]
                    theorem IntermediateField.intermediateFieldMap_symm_apply_coe {K : Type u_1} {L : Type u_2} {L' : Type u_3} [Field K] [Field L] [Field L'] [Algebra K L] [Algebra K L'] (e : L ≃ₐ[K] L') (E : IntermediateField K L) (a : (IntermediateField.map (e) E)) :
                    ((IntermediateField.intermediateFieldMap e E).symm a) = e.symm a
                    @[simp]
                    theorem AlgHom.fieldRange_toSubalgebra {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') :
                    f.fieldRange.toSubalgebra = f.range
                    def AlgHom.fieldRange {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') :

                    The range of an algebra homomorphism, as an intermediate field.

                    Equations
                    • f.fieldRange = let __src := f.range; let __src_1 := (f).fieldRange; { toSubalgebra := __src, inv_mem' := }
                    Instances For
                      @[simp]
                      theorem AlgHom.coe_fieldRange {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') :
                      f.fieldRange = Set.range f
                      @[simp]
                      theorem AlgHom.fieldRange_toSubfield {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') :
                      f.fieldRange.toSubfield = (f).fieldRange
                      @[simp]
                      theorem AlgHom.mem_fieldRange {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'} {y : L'} :
                      y f.fieldRange ∃ (x : L), f x = y
                      def IntermediateField.val {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (S : IntermediateField K L) :
                      S →ₐ[K] L

                      The embedding from an intermediate field of L / K to L.

                      Equations
                      • S.val = S.val
                      Instances For
                        @[simp]
                        theorem IntermediateField.coe_val {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (S : IntermediateField K L) :
                        S.val = Subtype.val
                        @[simp]
                        theorem IntermediateField.val_mk {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (S : IntermediateField K L) {x : L} (hx : x S) :
                        S.val x, hx = x
                        theorem IntermediateField.range_val {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (S : IntermediateField K L) :
                        S.val.range = S.toSubalgebra
                        @[simp]
                        theorem IntermediateField.fieldRange_val {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (S : IntermediateField K L) :
                        S.val.fieldRange = S
                        instance IntermediateField.AlgHom.inhabited {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (S : IntermediateField K L) :
                        Equations
                        theorem IntermediateField.aeval_coe {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (S : IntermediateField K L) {R : Type u_4} [CommRing R] [Algebra R K] [Algebra R L] [IsScalarTower R K L] (x : S) (P : Polynomial R) :
                        (Polynomial.aeval x) P = ((Polynomial.aeval x) P)
                        theorem IntermediateField.coe_isIntegral_iff {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (S : IntermediateField K L) {R : Type u_4} [CommRing R] [Algebra R K] [Algebra R L] [IsScalarTower R K L] {x : S} :
                        def IntermediateField.inclusion {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {E : IntermediateField K L} {F : IntermediateField K L} (hEF : E F) :
                        E →ₐ[K] F

                        The map E → F when E is an intermediate field contained in the intermediate field F.

                        This is the intermediate field version of Subalgebra.inclusion.

                        Equations
                        Instances For
                          @[simp]
                          @[simp]
                          theorem IntermediateField.inclusion_inclusion {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {E : IntermediateField K L} {F : IntermediateField K L} {G : IntermediateField K L} (hEF : E F) (hFG : F G) (x : E) :
                          @[simp]
                          theorem IntermediateField.coe_inclusion {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {E : IntermediateField K L} {F : IntermediateField K L} (hEF : E F) (e : E) :
                          ((IntermediateField.inclusion hEF) e) = e
                          theorem IntermediateField.toSubalgebra_injective {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] :
                          Function.Injective IntermediateField.toSubalgebra
                          theorem IntermediateField.map_injective {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') :
                          theorem IntermediateField.set_range_subset {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (S : IntermediateField K L) :
                          Set.range (algebraMap K L) S
                          theorem IntermediateField.fieldRange_le {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (S : IntermediateField K L) :
                          (algebraMap K L).fieldRange S.toSubfield
                          @[simp]
                          theorem IntermediateField.toSubalgebra_le_toSubalgebra {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {S : IntermediateField K L} {S' : IntermediateField K L} :
                          S.toSubalgebra S'.toSubalgebra S S'
                          @[simp]
                          theorem IntermediateField.toSubalgebra_lt_toSubalgebra {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {S : IntermediateField K L} {S' : IntermediateField K L} :
                          S.toSubalgebra < S'.toSubalgebra S < S'
                          def IntermediateField.lift {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {F : IntermediateField K L} (E : IntermediateField K F) :

                          Lift an intermediate_field of an intermediate_field

                          Equations
                          Instances For
                            instance IntermediateField.hasLift {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {F : IntermediateField K L} :
                            Equations
                            • IntermediateField.hasLift = { coe := IntermediateField.lift }
                            theorem IntermediateField.lift_injective {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (F : IntermediateField K L) :
                            Function.Injective IntermediateField.lift
                            def IntermediateField.restrictScalars (K : Type u_1) {L : Type u_2} {L' : Type u_3} [Field K] [Field L] [Field L'] [Algebra K L] [Algebra K L'] [Algebra L' L] [IsScalarTower K L' L] (E : IntermediateField L' L) :

                            Given a tower L / ↥E / L' / K of field extensions, where E is an L'-intermediate field of L, reinterpret E as a K-intermediate field of L.

                            Equations
                            • One or more equations did not get rendered due to their size.
                            Instances For
                              @[simp]
                              theorem IntermediateField.coe_restrictScalars (K : Type u_1) {L : Type u_2} {L' : Type u_3} [Field K] [Field L] [Field L'] [Algebra K L] [Algebra K L'] [Algebra L' L] [IsScalarTower K L' L] {E : IntermediateField L' L} :
                              @[simp]
                              theorem IntermediateField.restrictScalars_toSubalgebra (K : Type u_1) {L : Type u_2} {L' : Type u_3} [Field K] [Field L] [Field L'] [Algebra K L] [Algebra K L'] [Algebra L' L] [IsScalarTower K L' L] {E : IntermediateField L' L} :
                              @[simp]
                              theorem IntermediateField.restrictScalars_toSubfield (K : Type u_1) {L : Type u_2} {L' : Type u_3} [Field K] [Field L] [Field L'] [Algebra K L] [Algebra K L'] [Algebra L' L] [IsScalarTower K L' L] {E : IntermediateField L' L} :
                              (IntermediateField.restrictScalars K E).toSubfield = E.toSubfield
                              @[simp]
                              theorem IntermediateField.mem_restrictScalars (K : Type u_1) {L : Type u_2} {L' : Type u_3} [Field K] [Field L] [Field L'] [Algebra K L] [Algebra K L'] [Algebra L' L] [IsScalarTower K L' L] {E : IntermediateField L' L} {x : L} :
                              def IntermediateField.extendScalars {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {F : IntermediateField K L} {E : IntermediateField K L} (h : F E) :

                              If F ≤ E are two intermediate fields of L / K, then E is also an intermediate field of L / F. It can be viewed as an inverse to IntermediateField.restrictScalars.

                              Equations
                              Instances For
                                @[simp]
                                theorem IntermediateField.coe_extendScalars {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {F : IntermediateField K L} {E : IntermediateField K L} (h : F E) :
                                @[simp]
                                theorem IntermediateField.extendScalars_toSubfield {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {F : IntermediateField K L} {E : IntermediateField K L} (h : F E) :
                                (IntermediateField.extendScalars h).toSubfield = E.toSubfield
                                @[simp]
                                theorem IntermediateField.mem_extendScalars {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {F : IntermediateField K L} {E : IntermediateField K L} (h : F E) {x : L} :
                                def IntermediateField.extendScalars.orderIso {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (F : IntermediateField K L) :
                                { E : IntermediateField K L // F E } ≃o IntermediateField (F) L

                                IntermediateField.extendScalars is an order isomorphism from { E : IntermediateField K L // F ≤ E } to IntermediateField F L. Its inverse is IntermediateField.restrictScalars.

                                Equations
                                • One or more equations did not get rendered due to their size.
                                Instances For
                                  Equations
                                  • =
                                  Equations
                                  • =
                                  @[simp]
                                  theorem IntermediateField.rank_eq_rank_subalgebra {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (F : IntermediateField K L) :
                                  Module.rank K F.toSubalgebra = Module.rank K F
                                  @[simp]
                                  theorem IntermediateField.toSubalgebra_eq_iff {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {F : IntermediateField K L} {E : IntermediateField K L} :
                                  F.toSubalgebra = E.toSubalgebra F = E
                                  theorem IntermediateField.eq_of_le_of_finrank_le {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {F : IntermediateField K L} {E : IntermediateField K L} [hfin : FiniteDimensional K E] (h_le : F E) (h_finrank : FiniteDimensional.finrank K E FiniteDimensional.finrank K F) :
                                  F = E

                                  If F ≤ E are two intermediate fields of L / K such that [E : K] ≤ [F : K] are finite, then F = E.

                                  theorem IntermediateField.eq_of_le_of_finrank_eq {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {F : IntermediateField K L} {E : IntermediateField K L} [FiniteDimensional K E] (h_le : F E) (h_finrank : FiniteDimensional.finrank K F = FiniteDimensional.finrank K E) :
                                  F = E

                                  If F ≤ E are two intermediate fields of L / K such that [F : K] = [E : K] are finite, then F = E.

                                  theorem IntermediateField.eq_of_le_of_finrank_le' {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {F : IntermediateField K L} {E : IntermediateField K L} [FiniteDimensional (F) L] (h_le : F E) (h_finrank : FiniteDimensional.finrank (F) L FiniteDimensional.finrank (E) L) :
                                  F = E

                                  If F ≤ E are two intermediate fields of L / K such that [L : F] ≤ [L : E] are finite, then F = E.

                                  theorem IntermediateField.eq_of_le_of_finrank_eq' {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {F : IntermediateField K L} {E : IntermediateField K L} [FiniteDimensional (F) L] (h_le : F E) (h_finrank : FiniteDimensional.finrank (F) L = FiniteDimensional.finrank (E) L) :
                                  F = E

                                  If F ≤ E are two intermediate fields of L / K such that [L : F] = [L : E] are finite, then F = E.

                                  theorem IntermediateField.isAlgebraic_iff {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {S : IntermediateField K L} {x : S} :
                                  theorem IntermediateField.isIntegral_iff {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {S : IntermediateField K L} {x : S} :
                                  theorem IntermediateField.minpoly_eq {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {S : IntermediateField K L} (x : S) :
                                  minpoly K x = minpoly K x

                                  If L/K is algebraic, the K-subalgebras of L are all fields.

                                  Equations
                                  • One or more equations did not get rendered due to their size.
                                  Instances For
                                    @[simp]
                                    theorem mem_subalgebraEquivIntermediateField {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] [Algebra.IsAlgebraic K L] {S : Subalgebra K L} {x : L} :
                                    x subalgebraEquivIntermediateField S x S
                                    @[simp]
                                    theorem mem_subalgebraEquivIntermediateField_symm {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] [Algebra.IsAlgebraic K L] {S : IntermediateField K L} {x : L} :
                                    x subalgebraEquivIntermediateField.symm S x S