mathlib3 documentation

field_theory.intermediate_field

Intermediate fields #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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, intermediate_field K L. An intermediate_field 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

source
structure intermediate_field (K : Type u_1) (L : Type u_2) [field K] [field L] [algebra K L] :
Type u_2

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

Instances for intermediate_field
source
def intermediate_field.to_subfield {K : Type u_1} {L : Type u_2} [field K] [field L] [algebra K L] (S : intermediate_field K L) :
subfield L

Reinterpret an intermediate_field as a subfield.

Equations
source
@[protected, instance]
def intermediate_field.set_like {K : Type u_1} {L : Type u_2} [field K] [field L] [algebra K L] :
set_like (intermediate_field K L) L
Equations
source
@[protected, instance]
def intermediate_field.subfield_class {K : Type u_1} {L : Type u_2} [field K] [field L] [algebra K L] :
subfield_class (intermediate_field K L) L
source
@[simp]
theorem intermediate_field.mem_carrier {K : Type u_1} {L : Type u_2} [field K] [field L] [algebra K L] {s : intermediate_field K L} {x : L} :
x ∈ s.to_subalgebra.carrier ↔ x ∈ s
source
@[ext]
theorem intermediate_field.ext {K : Type u_1} {L : Type u_2} [field K] [field L] [algebra K L] {S T : intermediate_field K L} (h : ∀ (x : L), x ∈ S ↔ x ∈ T) :
S = T

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

source
@[simp]
theorem intermediate_field.coe_to_subalgebra {K : Type u_1} {L : Type u_2} [field K] [field L] [algebra K L] (S : intermediate_field K L) :
↑(S.to_subalgebra) = ↑S
source
@[simp]
theorem intermediate_field.coe_to_subfield {K : Type u_1} {L : Type u_2} [field K] [field L] [algebra K L] (S : intermediate_field K L) :
↑(S.to_subfield) = ↑S
source
@[simp]
theorem intermediate_field.mem_mk {K : Type u_1} {L : Type u_2} [field K] [field L] [algebra K L] (s : set L) (hK : ∀ (x : K), ⇑(algebra_map K L) x ∈ s) (ho : ∀ {a b : L}, a ∈ s → b ∈ s → a * b ∈ s) (hm : 1 ∈ s) (hz : ∀ {a b : L}, a ∈ s → b ∈ s → a + b ∈ s) (ha : 0 ∈ s) (hn : ∀ (x : L), x ∈ {carrier := s, mul_mem' := ho, one_mem' := hm, add_mem' := hz, zero_mem' := ha, algebra_map_mem' := hK}.carrier → -x ∈ {carrier := s, mul_mem' := ho, one_mem' := hm, add_mem' := hz, zero_mem' := ha, algebra_map_mem' := hK}.carrier) (hi : ∀ (x : L), x ∈ {carrier := s, mul_mem' := ho, one_mem' := hm, add_mem' := hz, zero_mem' := ha, algebra_map_mem' := hK}.carrier → x⁻¹ ∈ {carrier := s, mul_mem' := ho, one_mem' := hm, add_mem' := hz, zero_mem' := ha, algebra_map_mem' := hK}.carrier) (x : L) :
x ∈ {to_subalgebra := {carrier := s, mul_mem' := ho, one_mem' := hm, add_mem' := hz, zero_mem' := ha, algebra_map_mem' := hK}, neg_mem' := hn, inv_mem' := hi} ↔ x ∈ s
source
@[simp]
theorem intermediate_field.mem_to_subalgebra {K : Type u_1} {L : Type u_2} [field K] [field L] [algebra K L] (s : intermediate_field K L) (x : L) :
x ∈ s.to_subalgebra ↔ x ∈ s
source
@[simp]
theorem intermediate_field.mem_to_subfield {K : Type u_1} {L : Type u_2} [field K] [field L] [algebra K L] (s : intermediate_field K L) (x : L) :
x ∈ s.to_subfield ↔ x ∈ s
source
@[protected]
def intermediate_field.copy {K : Type u_1} {L : Type u_2} [field K] [field L] [algebra K L] (S : intermediate_field K L) (s : set L) (hs : s = ↑S) :
intermediate_field K L

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

Equations
source
@[simp]
theorem intermediate_field.coe_copy {K : Type u_1} {L : Type u_2} [field K] [field L] [algebra K L] (S : intermediate_field K L) (s : set L) (hs : s = ↑S) :
↑(S.copy s hs) = s
source
theorem intermediate_field.copy_eq {K : Type u_1} {L : Type u_2} [field K] [field L] [algebra K L] (S : intermediate_field 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 intermediate_field is also a subalgebra or subfield. Their use should be replaceable with the corresponding lemma from a subobject class.

source
theorem intermediate_field.algebra_map_mem {K : Type u_1} {L : Type u_2} [field K] [field L] [algebra K L] (S : intermediate_field K L) (x : K) :
⇑(algebra_map K L) x ∈ S

An intermediate field contains the image of the smaller field.

source
theorem intermediate_field.smul_mem {K : Type u_1} {L : Type u_2} [field K] [field L] [algebra K L] (S : intermediate_field K L) {y : L} :
y ∈ S → ∀ {x : K}, x • y ∈ S

An intermediate field is closed under scalar multiplication.

source
@[protected]
theorem intermediate_field.one_mem {K : Type u_1} {L : Type u_2} [field K] [field L] [algebra K L] (S : intermediate_field K L) :
1 ∈ S

An intermediate field contains the ring's 1.

source
@[protected]
theorem intermediate_field.zero_mem {K : Type u_1} {L : Type u_2} [field K] [field L] [algebra K L] (S : intermediate_field K L) :
0 ∈ S

An intermediate field contains the ring's 0.

source
@[protected]
theorem intermediate_field.mul_mem {K : Type u_1} {L : Type u_2} [field K] [field L] [algebra K L] (S : intermediate_field K L) {x y : L} :
x ∈ S → y ∈ S → x * y ∈ S

An intermediate field is closed under multiplication.

source
@[protected]
theorem intermediate_field.add_mem {K : Type u_1} {L : Type u_2} [field K] [field L] [algebra K L] (S : intermediate_field K L) {x y : L} :
x ∈ S → y ∈ S → x + y ∈ S

An intermediate field is closed under addition.

source
@[protected]
theorem intermediate_field.sub_mem {K : Type u_1} {L : Type u_2} [field K] [field L] [algebra K L] (S : intermediate_field K L) {x y : L} :
x ∈ S → y ∈ S → x - y ∈ S

An intermediate field is closed under subtraction

source
@[protected]
theorem intermediate_field.neg_mem {K : Type u_1} {L : Type u_2} [field K] [field L] [algebra K L] (S : intermediate_field K L) {x : L} :
x ∈ S → -x ∈ S

An intermediate field is closed under negation.

source
@[protected]
theorem intermediate_field.inv_mem {K : Type u_1} {L : Type u_2} [field K] [field L] [algebra K L] (S : intermediate_field K L) {x : L} :
x ∈ S → x⁻¹ ∈ S

An intermediate field is closed under inverses.

source
@[protected]
theorem intermediate_field.div_mem {K : Type u_1} {L : Type u_2} [field K] [field L] [algebra K L] (S : intermediate_field K L) {x y : L} :
x ∈ S → y ∈ S → x / y ∈ S

An intermediate field is closed under division.

source
@[protected]
theorem intermediate_field.list_prod_mem {K : Type u_1} {L : Type u_2} [field K] [field L] [algebra K L] (S : intermediate_field K L) {l : list L} :
(∀ (x : L), x ∈ l → x ∈ S) → l.prod ∈ S

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

source
@[protected]
theorem intermediate_field.list_sum_mem {K : Type u_1} {L : Type u_2} [field K] [field L] [algebra K L] (S : intermediate_field K L) {l : list L} :
(∀ (x : L), x ∈ l → x ∈ S) → l.sum ∈ S

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

source
@[protected]
theorem intermediate_field.multiset_prod_mem {K : Type u_1} {L : Type u_2} [field K] [field L] [algebra K L] (S : intermediate_field K L) (m : multiset L) :
(∀ (a : L), a ∈ m → a ∈ S) → m.prod ∈ S

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

source
@[protected]
theorem intermediate_field.multiset_sum_mem {K : Type u_1} {L : Type u_2} [field K] [field L] [algebra K L] (S : intermediate_field K L) (m : multiset L) :
(∀ (a : L), a ∈ m → a ∈ S) → m.sum ∈ S

Sum of a multiset of elements in a intermediate_field is in the intermediate_field.

source
@[protected]
theorem intermediate_field.prod_mem {K : Type u_1} {L : Type u_2} [field K] [field L] [algebra K L] (S : intermediate_field K L) {ι : Type u_3} {t : finset ι} {f : ι → L} (h : ∀ (c : ι), c ∈ t → f c ∈ S) :
t.prod (λ (i : ι), f i) ∈ S

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

source
@[protected]
theorem intermediate_field.sum_mem {K : Type u_1} {L : Type u_2} [field K] [field L] [algebra K L] (S : intermediate_field K L) {ι : Type u_3} {t : finset ι} {f : ι → L} (h : ∀ (c : ι), c ∈ t → f c ∈ S) :
t.sum (λ (i : ι), f i) ∈ S

Sum of elements in a intermediate_field indexed by a finset is in the intermediate_field.

source
@[protected]
theorem intermediate_field.pow_mem {K : Type u_1} {L : Type u_2} [field K] [field L] [algebra K L] (S : intermediate_field K L) {x : L} (hx : x ∈ S) (n : ℤ) :
x ^ n ∈ S
source
@[protected]
theorem intermediate_field.zsmul_mem {K : Type u_1} {L : Type u_2} [field K] [field L] [algebra K L] (S : intermediate_field K L) {x : L} (hx : x ∈ S) (n : ℤ) :
n • x ∈ S
source
@[protected]
theorem intermediate_field.coe_int_mem {K : Type u_1} {L : Type u_2} [field K] [field L] [algebra K L] (S : intermediate_field K L) (n : ℤ) :
↑n ∈ S
source
@[protected]
theorem intermediate_field.coe_add {K : Type u_1} {L : Type u_2} [field K] [field L] [algebra K L] (S : intermediate_field K L) (x y : ↥S) :
↑(x + y) = ↑x + ↑y
source
@[protected]
theorem intermediate_field.coe_neg {K : Type u_1} {L : Type u_2} [field K] [field L] [algebra K L] (S : intermediate_field K L) (x : ↥S) :
↑-x = -↑x
source
@[protected]
theorem intermediate_field.coe_mul {K : Type u_1} {L : Type u_2} [field K] [field L] [algebra K L] (S : intermediate_field K L) (x y : ↥S) :
↑(x * y) = ↑x * ↑y
source
@[protected]
theorem intermediate_field.coe_inv {K : Type u_1} {L : Type u_2} [field K] [field L] [algebra K L] (S : intermediate_field K L) (x : ↥S) :
↑x⁻¹ = (↑x)⁻¹
source
@[protected]
theorem intermediate_field.coe_zero {K : Type u_1} {L : Type u_2} [field K] [field L] [algebra K L] (S : intermediate_field K L) :
↑0 = 0
source
@[protected]
theorem intermediate_field.coe_one {K : Type u_1} {L : Type u_2} [field K] [field L] [algebra K L] (S : intermediate_field K L) :
↑1 = 1
source
@[protected]
theorem intermediate_field.coe_pow {K : Type u_1} {L : Type u_2} [field K] [field L] [algebra K L] (S : intermediate_field K L) (x : ↥S) (n : ℕ) :
↑(x ^ n) = ↑x ^ n
source
theorem intermediate_field.coe_nat_mem {K : Type u_1} {L : Type u_2} [field K] [field L] [algebra K L] (S : intermediate_field K L) (n : ℕ) :
↑n ∈ S
source
def subalgebra.to_intermediate_field {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) :
intermediate_field K L

Turn a subalgebra closed under inverses into an intermediate field

Equations
source
@[simp]
theorem to_subalgebra_to_intermediate_field {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) :
(S.to_intermediate_field inv_mem).to_subalgebra = S
source
@[simp]
theorem to_intermediate_field_to_subalgebra {K : Type u_1} {L : Type u_2} [field K] [field L] [algebra K L] (S : intermediate_field K L) :
S.to_subalgebra.to_intermediate_field _ = S
source
def subalgebra.to_intermediate_field' {K : Type u_1} {L : Type u_2} [field K] [field L] [algebra K L] (S : subalgebra K L) (hS : is_field ↥S) :
intermediate_field K L

Turn a subalgebra satisfying is_field into an intermediate_field

Equations
source
@[simp]
theorem to_subalgebra_to_intermediate_field' {K : Type u_1} {L : Type u_2} [field K] [field L] [algebra K L] (S : subalgebra K L) (hS : is_field ↥S) :
(S.to_intermediate_field' hS).to_subalgebra = S
source
@[simp]
theorem to_intermediate_field'_to_subalgebra {K : Type u_1} {L : Type u_2} [field K] [field L] [algebra K L] (S : intermediate_field K L) :
S.to_subalgebra.to_intermediate_field' _ = S
source
def subfield.to_intermediate_field {K : Type u_1} {L : Type u_2} [field K] [field L] [algebra K L] (S : subfield L) (algebra_map_mem : ∀ (x : K), ⇑(algebra_map K L) x ∈ S) :
intermediate_field K L

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

Equations
source
@[protected, instance]
def intermediate_field.to_field {K : Type u_1} {L : Type u_2} [field K] [field L] [algebra K L] (S : intermediate_field K L) :
field ↥S

An intermediate field inherits a field structure

Equations
source
@[simp, norm_cast]
theorem intermediate_field.coe_sum {K : Type u_1} {L : Type u_2} [field K] [field L] [algebra K L] (S : intermediate_field K L) {ι : Type u_3} [fintype ι] (f : ι → ↥S) :
↑(finset.univ.sum (λ (i : ι), f i)) = finset.univ.sum (λ (i : ι), ↑(f i))
source
@[simp, norm_cast]
theorem intermediate_field.coe_prod {K : Type u_1} {L : Type u_2} [field K] [field L] [algebra K L] (S : intermediate_field K L) {ι : Type u_3} [fintype ι] (f : ι → ↥S) :
↑(finset.univ.prod (λ (i : ι), f i)) = finset.univ.prod (λ (i : ι), ↑(f i))

intermediate_fields inherit structure from their subalgebra coercions.

source
@[protected, instance]
def intermediate_field.module' {K : Type u_1} {L : Type u_2} [field K] [field L] [algebra K L] (S : intermediate_field K L) {R : Type u_3} [semiring R] [has_smul R K] [module R L] [is_scalar_tower R K L] :
module R ↥S
Equations
source
@[protected, instance]
def intermediate_field.module {K : Type u_1} {L : Type u_2} [field K] [field L] [algebra K L] (S : intermediate_field K L) :
module K ↥S
Equations
source
@[protected, instance]
def intermediate_field.is_scalar_tower {K : Type u_1} {L : Type u_2} [field K] [field L] [algebra K L] (S : intermediate_field K L) {R : Type u_3} [semiring R] [has_smul R K] [module R L] [is_scalar_tower R K L] :
is_scalar_tower R K ↥S
source
@[simp]
theorem intermediate_field.coe_smul {K : Type u_1} {L : Type u_2} [field K] [field L] [algebra K L] (S : intermediate_field K L) {R : Type u_3} [semiring R] [has_smul R K] [module R L] [is_scalar_tower R K L] (r : R) (x : ↥S) :
↑(r • x) = r • ↑x
source
@[protected, instance]
def intermediate_field.algebra' {K : Type u_1} {L : Type u_2} [field K] [field L] [algebra K L] (S : intermediate_field K L) {K' : Type u_3} [comm_semiring K'] [has_smul K' K] [algebra K' L] [is_scalar_tower K' K L] :
algebra K' ↥S
Equations
source
@[protected, instance]
def intermediate_field.algebra {K : Type u_1} {L : Type u_2} [field K] [field L] [algebra K L] (S : intermediate_field K L) :
algebra K ↥S
Equations
source
@[protected, instance]
def intermediate_field.to_algebra {K : Type u_1} {L : Type u_2} [field K] [field L] [algebra K L] (S : intermediate_field K L) {R : Type u_3} [semiring R] [algebra L R] :
algebra ↥S R
Equations
source
@[protected, instance]
def intermediate_field.is_scalar_tower_bot {K : Type u_1} {L : Type u_2} [field K] [field L] [algebra K L] (S : intermediate_field K L) {R : Type u_3} [semiring R] [algebra L R] :
is_scalar_tower ↥S L R
source
@[protected, instance]
def intermediate_field.is_scalar_tower_mid {K : Type u_1} {L : Type u_2} [field K] [field L] [algebra K L] (S : intermediate_field K L) {R : Type u_3} [semiring R] [algebra L R] [algebra K R] [is_scalar_tower K L R] :
is_scalar_tower K ↥S R
source
@[protected, instance]
def intermediate_field.is_scalar_tower_mid' {K : Type u_1} {L : Type u_2} [field K] [field L] [algebra K L] (S : intermediate_field K L) :
is_scalar_tower K ↥S L

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

source
def intermediate_field.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 : intermediate_field K L) :
intermediate_field 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.

Equations
Instances for ↥intermediate_field.map
source
@[simp]
theorem intermediate_field.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 : intermediate_field K L) (f : L →ₐ[K] L') :
↑(intermediate_field.map f S) = ⇑f '' ↑S
source
theorem intermediate_field.map_map {K : Type u_1} {L₁ : Type u_2} {L₂ : Type u_3} {L₃ : Type u_4} [field K] [field L₁] [algebra K L₁] [field L₂] [algebra K L₂] [field L₃] [algebra K L₃] (E : intermediate_field K L₁) (f : L₁ →ₐ[K] L₂) (g : L₂ →ₐ[K] L₃) :
intermediate_field.map g (intermediate_field.map f E) = intermediate_field.map (g.comp f) E
source
def intermediate_field.intermediate_field_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'] (e : L ≃ₐ[K] L') (E : intermediate_field K L) :
↥E ≃ₐ[K] ↥(intermediate_field.map e.to_alg_hom 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

Equations
source
@[simp]
theorem intermediate_field.intermediate_field_map_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 : intermediate_field K L) (a : ↥E) :
↑(⇑(intermediate_field.intermediate_field_map e E) a) = ⇑e ↑a
source
@[simp]
theorem intermediate_field.intermediate_field_map_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 : intermediate_field K L) (a : ↥(intermediate_field.map e.to_alg_hom E)) :
↑(⇑((intermediate_field.intermediate_field_map e E).symm) a) = ⇑(e.symm) ↑a
source
def alg_hom.field_range {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') :
intermediate_field K L'

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

Equations
source
@[simp]
theorem alg_hom.field_range_to_subalgebra {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.field_range.to_subalgebra = f.range
source
@[simp]
theorem alg_hom.coe_field_range {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.field_range) = set.range ⇑f
source
@[simp]
theorem alg_hom.field_range_to_subfield {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.field_range.to_subfield = ↑f.field_range
source
@[simp]
theorem alg_hom.mem_field_range {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.field_range ↔ ∃ (x : L), ⇑f x = y
source
def intermediate_field.val {K : Type u_1} {L : Type u_2} [field K] [field L] [algebra K L] (S : intermediate_field K L) :
↥S →ₐ[K] L

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

Equations
source
@[simp]
theorem intermediate_field.coe_val {K : Type u_1} {L : Type u_2} [field K] [field L] [algebra K L] (S : intermediate_field K L) :
⇑(S.val) = coe
source
@[simp]
theorem intermediate_field.val_mk {K : Type u_1} {L : Type u_2} [field K] [field L] [algebra K L] (S : intermediate_field K L) {x : L} (hx : x ∈ S) :
⇑(S.val) ⟨x, hx⟩ = x
source
theorem intermediate_field.range_val {K : Type u_1} {L : Type u_2} [field K] [field L] [algebra K L] (S : intermediate_field K L) :
S.val.range = S.to_subalgebra
source
@[simp]
theorem intermediate_field.field_range_val {K : Type u_1} {L : Type u_2} [field K] [field L] [algebra K L] (S : intermediate_field K L) :
S.val.field_range = S
source
@[protected, instance]
def intermediate_field.alg_hom.inhabited {K : Type u_1} {L : Type u_2} [field K] [field L] [algebra K L] (S : intermediate_field K L) :
inhabited (↥S →ₐ[K] L)
Equations
source
theorem intermediate_field.aeval_coe {K : Type u_1} {L : Type u_2} [field K] [field L] [algebra K L] (S : intermediate_field K L) {R : Type u_3} [comm_ring R] [algebra R K] [algebra R L] [is_scalar_tower R K L] (x : ↥S) (P : polynomial R) :
⇑(polynomial.aeval ↑x) P = ↑(⇑(polynomial.aeval x) P)
source
theorem intermediate_field.coe_is_integral_iff {K : Type u_1} {L : Type u_2} [field K] [field L] [algebra K L] (S : intermediate_field K L) {R : Type u_3} [comm_ring R] [algebra R K] [algebra R L] [is_scalar_tower R K L] {x : ↥S} :
is_integral R ↑x ↔ is_integral R x
source
def intermediate_field.inclusion {K : Type u_1} {L : Type u_2} [field K] [field L] [algebra K L] {E F : intermediate_field 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
source
theorem intermediate_field.inclusion_injective {K : Type u_1} {L : Type u_2} [field K] [field L] [algebra K L] {E F : intermediate_field K L} (hEF : E ≤ F) :
function.injective ⇑(intermediate_field.inclusion hEF)
source
@[simp]
theorem intermediate_field.inclusion_self {K : Type u_1} {L : Type u_2} [field K] [field L] [algebra K L] {E : intermediate_field K L} :
intermediate_field.inclusion _ = alg_hom.id K ↥E
source
@[simp]
theorem intermediate_field.inclusion_inclusion {K : Type u_1} {L : Type u_2} [field K] [field L] [algebra K L] {E F G : intermediate_field K L} (hEF : E ≤ F) (hFG : F ≤ G) (x : ↥E) :
⇑(intermediate_field.inclusion hFG) (⇑(intermediate_field.inclusion hEF) x) = ⇑(intermediate_field.inclusion _) x
source
@[simp]
theorem intermediate_field.coe_inclusion {K : Type u_1} {L : Type u_2} [field K] [field L] [algebra K L] {E F : intermediate_field K L} (hEF : E ≤ F) (e : ↥E) :
↑(⇑(intermediate_field.inclusion hEF) e) = ↑e
source
theorem intermediate_field.to_subalgebra_injective {K : Type u_1} {L : Type u_2} [field K] [field L] [algebra K L] {S S' : intermediate_field K L} (h : S.to_subalgebra = S'.to_subalgebra) :
S = S'
source
theorem intermediate_field.set_range_subset {K : Type u_1} {L : Type u_2} [field K] [field L] [algebra K L] (S : intermediate_field K L) :
set.range ⇑(algebra_map K L) ⊆ ↑S
source
theorem intermediate_field.field_range_le {K : Type u_1} {L : Type u_2} [field K] [field L] [algebra K L] (S : intermediate_field K L) :
(algebra_map K L).field_range ≤ S.to_subfield
source
@[simp]
theorem intermediate_field.to_subalgebra_le_to_subalgebra {K : Type u_1} {L : Type u_2} [field K] [field L] [algebra K L] {S S' : intermediate_field K L} :
S.to_subalgebra ≤ S'.to_subalgebra ↔ S ≤ S'
source
@[simp]
theorem intermediate_field.to_subalgebra_lt_to_subalgebra {K : Type u_1} {L : Type u_2} [field K] [field L] [algebra K L] {S S' : intermediate_field K L} :
S.to_subalgebra < S'.to_subalgebra ↔ S < S'
source
def intermediate_field.lift {K : Type u_1} {L : Type u_2} [field K] [field L] [algebra K L] {F : intermediate_field K L} (E : intermediate_field K ↥F) :
intermediate_field K L

Lift an intermediate_field of an intermediate_field

Equations
source
@[protected, instance]
def intermediate_field.has_lift {K : Type u_1} {L : Type u_2} [field K] [field L] [algebra K L] {F : intermediate_field K L} :
has_lift_t (intermediate_field K ↥F) (intermediate_field K L)
Equations
source
def intermediate_field.restrict_scalars (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] [is_scalar_tower K L' L] (E : intermediate_field L' L) :
intermediate_field 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.

Equations
source
@[simp]
theorem intermediate_field.coe_restrict_scalars (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] [is_scalar_tower K L' L] {E : intermediate_field L' L} :
↑(intermediate_field.restrict_scalars K E) = ↑E
source
@[simp]
theorem intermediate_field.restrict_scalars_to_subalgebra (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] [is_scalar_tower K L' L] {E : intermediate_field L' L} :
(intermediate_field.restrict_scalars K E).to_subalgebra = subalgebra.restrict_scalars K E.to_subalgebra
source
@[simp]
theorem intermediate_field.restrict_scalars_to_subfield (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] [is_scalar_tower K L' L] {E : intermediate_field L' L} :
(intermediate_field.restrict_scalars K E).to_subfield = E.to_subfield
source
@[simp]
theorem intermediate_field.mem_restrict_scalars (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] [is_scalar_tower K L' L] {E : intermediate_field L' L} {x : L} :
x ∈ intermediate_field.restrict_scalars K E ↔ x ∈ E
source
theorem intermediate_field.restrict_scalars_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] [is_scalar_tower K L' L] :
function.injective (intermediate_field.restrict_scalars K)
source
@[protected, instance]
def intermediate_field.finite_dimensional_left {K : Type u_1} {L : Type u_2} [field K] [field L] [algebra K L] (F : intermediate_field K L) [finite_dimensional K L] :
finite_dimensional K ↥F
source
@[protected, instance]
def intermediate_field.finite_dimensional_right {K : Type u_1} {L : Type u_2} [field K] [field L] [algebra K L] (F : intermediate_field K L) [finite_dimensional K L] :
finite_dimensional ↥F L
source
@[simp]
theorem intermediate_field.rank_eq_rank_subalgebra {K : Type u_1} {L : Type u_2} [field K] [field L] [algebra K L] (F : intermediate_field K L) :
module.rank K ↥(F.to_subalgebra) = module.rank K ↥F
source
@[simp]
theorem intermediate_field.finrank_eq_finrank_subalgebra {K : Type u_1} {L : Type u_2} [field K] [field L] [algebra K L] (F : intermediate_field K L) :
finite_dimensional.finrank K ↥(F.to_subalgebra) = finite_dimensional.finrank K ↥F
source
@[simp]
theorem intermediate_field.to_subalgebra_eq_iff {K : Type u_1} {L : Type u_2} [field K] [field L] [algebra K L] {F E : intermediate_field K L} :
F.to_subalgebra = E.to_subalgebra ↔ F = E
source
theorem intermediate_field.eq_of_le_of_finrank_le {K : Type u_1} {L : Type u_2} [field K] [field L] [algebra K L] {F E : intermediate_field K L} [finite_dimensional K L] (h_le : F ≤ E) (h_finrank : finite_dimensional.finrank K ↥E ≤ finite_dimensional.finrank K ↥F) :
F = E
source
theorem intermediate_field.eq_of_le_of_finrank_eq {K : Type u_1} {L : Type u_2} [field K] [field L] [algebra K L] {F E : intermediate_field K L} [finite_dimensional K L] (h_le : F ≤ E) (h_finrank : finite_dimensional.finrank K ↥F = finite_dimensional.finrank K ↥E) :
F = E
source
theorem intermediate_field.eq_of_le_of_finrank_le' {K : Type u_1} {L : Type u_2} [field K] [field L] [algebra K L] {F E : intermediate_field K L} [finite_dimensional K L] (h_le : F ≤ E) (h_finrank : finite_dimensional.finrank ↥F L ≤ finite_dimensional.finrank ↥E L) :
F = E
source
theorem intermediate_field.eq_of_le_of_finrank_eq' {K : Type u_1} {L : Type u_2} [field K] [field L] [algebra K L] {F E : intermediate_field K L} [finite_dimensional K L] (h_le : F ≤ E) (h_finrank : finite_dimensional.finrank ↥F L = finite_dimensional.finrank ↥E L) :
F = E
source
theorem intermediate_field.is_algebraic_iff {K : Type u_1} {L : Type u_2} [field K] [field L] [algebra K L] {S : intermediate_field K L} {x : ↥S} :
is_algebraic K x ↔ is_algebraic K ↑x
source
theorem intermediate_field.is_integral_iff {K : Type u_1} {L : Type u_2} [field K] [field L] [algebra K L] {S : intermediate_field K L} {x : ↥S} :
is_integral K x ↔ is_integral K ↑x
source
theorem intermediate_field.minpoly_eq {K : Type u_1} {L : Type u_2} [field K] [field L] [algebra K L] {S : intermediate_field K L} (x : ↥S) :
minpoly K x = minpoly K ↑x
source
def subalgebra_equiv_intermediate_field {K : Type u_1} {L : Type u_2} [field K] [field L] [algebra K L] (alg : algebra.is_algebraic K L) :
subalgebra K L ≃o intermediate_field K L

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

Equations
source
@[simp]
theorem mem_subalgebra_equiv_intermediate_field {K : Type u_1} {L : Type u_2} [field K] [field L] [algebra K L] (alg : algebra.is_algebraic K L) {S : subalgebra K L} {x : L} :
x ∈ ⇑(subalgebra_equiv_intermediate_field alg) S ↔ x ∈ S
source
@[simp]
theorem mem_subalgebra_equiv_intermediate_field_symm {K : Type u_1} {L : Type u_2} [field K] [field L] [algebra K L] (alg : algebra.is_algebraic K L) {S : intermediate_field K L} {x : L} :
x ∈ ⇑((subalgebra_equiv_intermediate_field alg).symm) S ↔ x ∈ S