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

• IntermediateField K L : the type of intermediate fields between K and L.
• Subalgebra.to_intermediateField: turns a subalgebra closed under ⁻¹ into an intermediate field
• Subfield.to_intermediateField: turns a subfield containing the image of K into an intermediate field
• IntermediateField.map: map an intermediate field along an AlgHom
• IntermediateField.restrict_scalars: restrict the scalars of an intermediate field to a smaller field in a tower of fields.

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

• carrier : Set L
• mul_mem' : ∀ {a b : L}, a ∈ s.carrier → b ∈ s.carrier → a * b ∈ s.carrier
• one_mem' : 1 ∈ s.carrier
• add_mem' : ∀ {a b : L}, a ∈ s.carrier → b ∈ s.carrier → a + b ∈ s.carrier
• zero_mem' : 0 ∈ s.carrier
• algebraMap_mem' : ∀ (r : K), ↑(algebraMap K L) r ∈ s.carrier
• inv_mem' : ∀ (x : L), x ∈ s.carrier → x⁻¹ ∈ s.carrier

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

instance IntermediateField.instSetLikeIntermediateField {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] : SetLike (IntermediateField K L) L

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) : Subfield L

Reinterpret an IntermediateField as a Subfield.

instance IntermediateField.instSubfieldClassIntermediateFieldInstSetLikeIntermediateField {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] : SubfieldClass (IntermediateField K L) L

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) : ↑(IntermediateField.toSubfield S) = ↑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 : L), x ∈ { toSubsemiring := s, algebraMap_mem' := hK }.toSubsemiring.toSubmonoid.toSubsemigroup.carrier → x⁻¹ ∈ { toSubsemiring := s, algebraMap_mem' := hK }.toSubsemiring.toSubmonoid.toSubsemigroup.carrier) (x : L) : x ∈ { toSubalgebra := { 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 ∈ IntermediateField.toSubfield s ↔ 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) : IntermediateField K L

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

@[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) : ↑(IntermediateField.copy S 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) : IntermediateField.copy S 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 ∈ S → y ∈ S → x * 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 ∈ S → y ∈ S → x + 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 ∈ S → y ∈ S → x - 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 ∈ S → x⁻¹ ∈ 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 ∈ S → y ∈ S → x / 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} : (∀ (x : L), x ∈ l → x ∈ S) → List.prod l ∈ 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} : (∀ (x : L), x ∈ l → x ∈ S) → List.sum l ∈ 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) : (∀ (a : L), a ∈ m → a ∈ S) → Multiset.prod m ∈ 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) : (∀ (a : L), a ∈ m → a ∈ S) → Multiset.sum m ∈ 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 : ∀ (c : ι), c ∈ t → f c ∈ S) : (Finset.prod t 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 : ∀ (c : ι), c ∈ t → f c ∈ S) : (Finset.sum t 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.coe_int_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 : { x // x ∈ S }) (y : { x // x ∈ 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 : { x // 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 : { x // x ∈ S }) (y : { x // x ∈ 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 : { x // 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 : { x // x ∈ S }) (n : ℕ) : ↑(x ^ n) = ↑x ^ n

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

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

Turn a subalgebra closed under inverses into an intermediate field

@[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 : ∀ (x : L), x ∈ S → x⁻¹ ∈ S) : (Subalgebra.toIntermediateField S 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) : Subalgebra.toIntermediateField S.toSubalgebra (_ : ∀ (x : L), x ∈ S → x⁻¹ ∈ S) = 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 { x // x ∈ S }) : IntermediateField K L

Turn a subalgebra satisfying IsField into an intermediate_field

@[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 { x // x ∈ S }) : (Subalgebra.toIntermediateField' S 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) : Subalgebra.toIntermediateField' S.toSubalgebra (_ : IsField { x // x ∈ S }) = 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) : IntermediateField K L

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

instance IntermediateField.toField {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (S : IntermediateField K L) : Field { x // x ∈ S }

An intermediate field inherits a field structure

@[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 : ι → { x // x ∈ S }) : ↑(Finset.sum Finset.univ fun i => f i) = Finset.sum Finset.univ 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 : ι → { x // x ∈ S }) : ↑(Finset.prod Finset.univ fun i => f i) = Finset.prod Finset.univ 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 { x // x ∈ S }

instance IntermediateField.module {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (S : IntermediateField K L) : Module K { x // x ∈ S }

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 { x // x ∈ S }

@[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 : { x // 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) {K' : Type u_4} [CommSemiring K'] [SMul K' K] [Algebra K' L] [IsScalarTower K' K L] : Algebra K' { x // x ∈ S }

instance IntermediateField.algebra {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (S : IntermediateField K L) : Algebra K { x // x ∈ S }

instance IntermediateField.toAlgebra {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 { x // x ∈ S } R

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 { x // x ∈ S } L R

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 { x // x ∈ S } R

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 { x // x ∈ S } L

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

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) : IntermediateField K L'

If f : L →+* L' fixes K, S.map f is the intermediate field between L' and K such that x ∈ S ↔ f x ∈ S.map f.

@[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

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₃) : IntermediateField.map g (IntermediateField.map f E) = IntermediateField.map (AlgHom.comp g f) E

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) : IntermediateField.map f S ≤ IntermediateField.map f T

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) : { x // x ∈ E } ≃ₐ[K] { x // x ∈ IntermediateField.map (↑e) E }

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

@[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 : { x // x ∈ E }) : ↑(↑(IntermediateField.intermediateFieldMap e E) a) = ↑e ↑a

@[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 : { x // x ∈ IntermediateField.map (↑e) E }) : ↑(↑(AlgEquiv.symm (IntermediateField.intermediateFieldMap e E)) a) = ↑(AlgEquiv.symm e) ↑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') : (AlgHom.fieldRange f).toSubalgebra = AlgHom.range f

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') : IntermediateField K L'

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

@[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') : ↑(AlgHom.fieldRange f) = 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') : IntermediateField.toSubfield (AlgHom.fieldRange f) = RingHom.fieldRange ↑f

@[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 ∈ AlgHom.fieldRange f ↔ ∃ x, ↑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) : { x // x ∈ S } →ₐ[K] L

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

@[simp]

theorem IntermediateField.coe_val {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (S : IntermediateField K L) : ↑(IntermediateField.val S) = 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) : ↑(IntermediateField.val S) { val := x, property := 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) : AlgHom.range (IntermediateField.val S) = 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) : AlgHom.fieldRange (IntermediateField.val S) = S

instance IntermediateField.AlgHom.inhabited {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (S : IntermediateField K L) : Inhabited ({ x // x ∈ S } →ₐ[K] L)

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 : { x // 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 : { x // x ∈ S }} : IsIntegral R ↑x ↔ IsIntegral R x

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) : { x // x ∈ E } →ₐ[K] { x // x ∈ 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.

theorem IntermediateField.inclusion_injective {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) : Function.Injective ↑(IntermediateField.inclusion hEF)

@[simp]

theorem IntermediateField.inclusion_self {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {E : IntermediateField K L} : IntermediateField.inclusion (_ : E ≤ E) = AlgHom.id K { x // x ∈ E }

@[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 : { x // x ∈ E }) : ↑(IntermediateField.inclusion hFG) (↑(IntermediateField.inclusion hEF) x) = ↑(IntermediateField.inclusion (_ : E ≤ G)) x

@[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 : { x // x ∈ 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] {S : IntermediateField K L} {S' : IntermediateField K L} (h : S.toSubalgebra = S'.toSubalgebra) : S = S'

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) : RingHom.fieldRange (algebraMap K L) ≤ IntermediateField.toSubfield S

@[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 { x // x ∈ F }) : IntermediateField K L

Lift an intermediate_field of an intermediate_field

instance IntermediateField.hasLift {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {F : IntermediateField K L} : CoeOut (IntermediateField K { x // x ∈ F }) (IntermediateField K L)

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) : IntermediateField K 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.

@[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} : ↑(IntermediateField.restrictScalars K E) = ↑E

@[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} : (IntermediateField.restrictScalars K E).toSubalgebra = Subalgebra.restrictScalars K E.toSubalgebra

@[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.toSubfield (IntermediateField.restrictScalars K E) = IntermediateField.toSubfield E

@[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} : x ∈ IntermediateField.restrictScalars K E ↔ x ∈ E

theorem IntermediateField.restrictScalars_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'] [Algebra L' L] [IsScalarTower K L' L] : Function.Injective (IntermediateField.restrictScalars K)

instance IntermediateField.finiteDimensional_left {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (F : IntermediateField K L) [FiniteDimensional K L] : FiniteDimensional K { x // x ∈ F }

instance IntermediateField.finiteDimensional_right {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (F : IntermediateField K L) [FiniteDimensional K L] : FiniteDimensional { x // x ∈ F } L

@[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 { x // x ∈ F.toSubalgebra } = Module.rank K { x // x ∈ F }

@[simp]

theorem IntermediateField.finrank_eq_finrank_subalgebra {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (F : IntermediateField K L) : FiniteDimensional.finrank K { x // x ∈ F.toSubalgebra } = FiniteDimensional.finrank K { x // x ∈ 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} [FiniteDimensional K L] (h_le : F ≤ E) (h_finrank : FiniteDimensional.finrank K { x // x ∈ E } ≤ FiniteDimensional.finrank K { x // x ∈ F }) : 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 L] (h_le : F ≤ E) (h_finrank : FiniteDimensional.finrank K { x // x ∈ F } = FiniteDimensional.finrank K { x // x ∈ E }) : 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 K L] (h_le : F ≤ E) (h_finrank : FiniteDimensional.finrank { x // x ∈ F } L ≤ FiniteDimensional.finrank { x // x ∈ E } L) : 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 L] (h_le : F ≤ E) (h_finrank : FiniteDimensional.finrank { x // x ∈ F } L = FiniteDimensional.finrank { x // x ∈ E } L) : 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 : { x // x ∈ S }} : IsAlgebraic K x ↔ IsAlgebraic K ↑x

theorem IntermediateField.isIntegral_iff {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {S : IntermediateField K L} {x : { x // x ∈ S }} : IsIntegral K x ↔ IsIntegral K ↑x

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

def subalgebraEquivIntermediateField {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (alg : Algebra.IsAlgebraic K L) : Subalgebra K L ≃o IntermediateField K L

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

@[simp]

theorem mem_subalgebraEquivIntermediateField {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (alg : Algebra.IsAlgebraic K L) {S : Subalgebra K L} {x : L} : x ∈ ↑(subalgebraEquivIntermediateField alg) S ↔ x ∈ S

@[simp]

theorem mem_subalgebraEquivIntermediateField_symm {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (alg : Algebra.IsAlgebraic K L) {S : IntermediateField K L} {x : L} : x ∈ ↑(OrderIso.symm (subalgebraEquivIntermediateField alg)) S ↔ x ∈ S