field_theory.intermediate_field

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

Type u_2

to_subalgebra : subalgebra K L
neg_mem' : ∀ (x : L), x ∈ self.to_subalgebra.carrier → -x ∈ self.to_subalgebra.carrier
inv_mem' : ∀ (x : L), x ∈ self.to_subalgebra.carrier → x⁻¹ ∈ self.to_subalgebra.carrier

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

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

S.to_subfield = {carrier := S.to_subalgebra.carrier, one_mem' := _, mul_mem' := _, zero_mem' := _, add_mem' := _, neg_mem' := _, inv_mem' := _}

source

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

intermediate_field.set_like = {coe := λ (S : intermediate_field K L), S.to_subalgebra.carrier, coe_injective' := _}

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 : 1 ∈ s) (hm : ∀ {a b : L}, a ∈ s → b ∈ s → a * b ∈ s) (hz : 0 ∈ s) (ha : ∀ {a b : L}, a ∈ s → b ∈ s → a + b ∈ s) (hn : ∀ (x : L), x ∈ {carrier := s, one_mem' := ho, mul_mem' := hm, zero_mem' := hz, add_mem' := ha, algebra_map_mem' := hK}.carrier → -x ∈ {carrier := s, one_mem' := ho, mul_mem' := hm, zero_mem' := hz, add_mem' := ha, algebra_map_mem' := hK}.carrier) (hi : ∀ (x : L), x ∈ {carrier := s, one_mem' := ho, mul_mem' := hm, zero_mem' := hz, add_mem' := ha, algebra_map_mem' := hK}.carrier → x⁻¹ ∈ {carrier := s, one_mem' := ho, mul_mem' := hm, zero_mem' := hz, add_mem' := ha, algebra_map_mem' := hK}.carrier) (x : L) :

x ∈ {to_subalgebra := {carrier := s, one_mem' := ho, mul_mem' := hm, zero_mem' := hz, add_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

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.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

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

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

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

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

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} (hx : x ∈ S) (hy : y ∈ S) :

x - y ∈ S

An intermediate field is closed under subtraction

source

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

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

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} (hx : x ∈ S) (hy : y ∈ S) :

x / y ∈ S

An intermediate field is closed under division.

source

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

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

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

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

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

∏ (i : ι) in t, f i ∈ S

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

source

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

∑ (i : ι) in t, f i ∈ S

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

source

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

theorem intermediate_field.gsmul_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

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

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

S.to_intermediate_field inv_mem = {to_subalgebra := {carrier := S.carrier, one_mem' := _, mul_mem' := _, zero_mem' := _, add_mem' := _, algebra_map_mem' := _}, neg_mem' := _, inv_mem' := inv_mem}

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) (inv_mem : ∀ (x : L), x ∈ S.to_subalgebra → x⁻¹ ∈ S) :

S.to_subalgebra.to_intermediate_field inv_mem = 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

S.to_intermediate_field algebra_map_mem = {to_subalgebra := {carrier := S.carrier, one_mem' := _, mul_mem' := _, zero_mem' := _, add_mem' := _, algebra_map_mem' := algebra_map_mem}, neg_mem' := _, inv_mem' := _}

source

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

S.to_field = S.to_subfield.to_field

source

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

S.algebra = S.to_subalgebra.algebra

source

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

S.to_algebra = S.to_subalgebra.to_algebra

source

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

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

@[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} [field K] [field L] [algebra K L] (S : intermediate_field K L) {L' : Type u_3} [field L'] [algebra K L'] (f : L →ₐ[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

S.map f = {to_subalgebra := {carrier := (S.to_subalgebra.map f).carrier, one_mem' := _, mul_mem' := _, zero_mem' := _, add_mem' := _, algebra_map_mem' := _}, neg_mem' := _, inv_mem' := _}

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

S.val = S.to_subalgebra.val

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.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.lift1 {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

E.lift1 = E.map F.val

source

def intermediate_field.lift2 {K : Type u_1} {L : Type u_2} [field K] [field L] [algebra K L] {F : intermediate_field K L} (E : intermediate_field ↥F L) :

intermediate_field K L

Lift an intermediate_field of an intermediate_field

Equations

E.lift2 = {to_subalgebra := {carrier := E.to_subalgebra.carrier, one_mem' := _, mul_mem' := _, zero_mem' := _, add_mem' := _, algebra_map_mem' := _}, neg_mem' := _, inv_mem' := _}

source

@[instance]

def intermediate_field.has_lift1 {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

intermediate_field.has_lift1 = {lift := intermediate_field.lift1 F}

source

@[instance]

def intermediate_field.has_lift2 {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 ↥F L) (intermediate_field K L)

Equations

intermediate_field.has_lift2 = {lift := intermediate_field.lift2 F}

source

@[simp]

theorem intermediate_field.mem_lift2 {K : Type u_1} {L : Type u_2} [field K] [field L] [algebra K L] {F : intermediate_field K L} {E : intermediate_field ↥F L} {x : L} :

x ∈ ↑E ↔ x ∈ E

source

@[instance]

def intermediate_field.lift2_alg {K : Type u_1} {L : Type u_2} [field K] [field L] [algebra K L] {F : intermediate_field K L} {E : intermediate_field ↥F L} :

algebra K ↥E

Equations

intermediate_field.lift2_alg = {to_has_scalar := {smul := λ (a : K) (b : ↥E), (⇑((algebra_map ↥F ↥E).comp (algebra_map K ↥F)) a) * b}, to_ring_hom := {to_fun := ⇑((algebra_map ↥F ↥E).comp (algebra_map K ↥F)), map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}, commutes' := _, smul_def' := _}

source

@[instance]

def intermediate_field.lift2_tower {K : Type u_1} {L : Type u_2} [field K] [field L] [algebra K L] {F : intermediate_field K L} {E : intermediate_field ↥F L} :

is_scalar_tower K ↥F ↥E

source

def intermediate_field.lift2_alg_equiv {K : Type u_1} {L : Type u_2} [field K] [field L] [algebra K L] {F : intermediate_field K L} (E : intermediate_field ↥F L) :

↥↑E ≃ₐ[K] ↥E

lift2 is isomorphic to the original intermediate_field.

Equations

E.lift2_alg_equiv = {to_fun := λ (x : ↥↑E), x, inv_fun := λ (x : ↥E), x, left_inv := _, right_inv := _, map_mul' := _, map_add' := _, commutes' := _}

source

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

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

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

subalgebra_equiv_intermediate_field alg = {to_equiv := {to_fun := λ (S : subalgebra K L), S.to_intermediate_field _, inv_fun := λ (S : intermediate_field K L), S.to_subalgebra, left_inv := _, right_inv := _}, map_rel_iff' := _}

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

mathlib documentation

Intermediate fields #

Main definitions #

Implementation notes #

Tags #