From 7afd66abbf2ea4144f11d323ec6245dbc6603a79 Mon Sep 17 00:00:00 2001 From: tb65536 Date: Fri, 29 Jul 2022 14:31:26 +0000 Subject: [PATCH] feat(field_theory/intermediate_field): Produce an intermediate field from a subalgebra satisfying `is_field`. (#15659) This construction came up when proving that if `p` splits in `L/K`, then `p.is_splitting_field K (adjoin K (p.root_set L))`. --- src/field_theory/intermediate_field.lean | 27 ++++++++++++++++++++---- 1 file changed, 23 insertions(+), 4 deletions(-) diff --git a/src/field_theory/intermediate_field.lean b/src/field_theory/intermediate_field.lean index afa1a1ac2bf71..f2933d2f4e68f 100644 --- a/src/field_theory/intermediate_field.lean +++ b/src/field_theory/intermediate_field.lean @@ -190,11 +190,30 @@ def subalgebra.to_intermediate_field (S : subalgebra K L) (inv_mem : ∀ x ∈ S (S.to_intermediate_field inv_mem).to_subalgebra = S := by { ext, refl } -@[simp] lemma to_intermediate_field_to_subalgebra - (S : intermediate_field K L) (inv_mem : ∀ x ∈ S.to_subalgebra, x⁻¹ ∈ S) : - S.to_subalgebra.to_intermediate_field inv_mem = S := +@[simp] lemma to_intermediate_field_to_subalgebra (S : intermediate_field K L) : + S.to_subalgebra.to_intermediate_field (λ x, S.inv_mem) = S := by { ext, refl } +/-- Turn a subalgebra satisfying `is_field` into an intermediate_field -/ +def subalgebra.to_intermediate_field' (S : subalgebra K L) (hS : is_field S) : + intermediate_field K L := +S.to_intermediate_field $ λ x hx, begin + by_cases hx0 : x = 0, + { rw [hx0, inv_zero], + exact S.zero_mem }, + letI hS' := hS.to_field, + obtain ⟨y, hy⟩ := hS.mul_inv_cancel (show (⟨x, hx⟩ : S) ≠ 0, from subtype.ne_of_val_ne hx0), + rw [subtype.ext_iff, S.coe_mul, S.coe_one, subtype.coe_mk, mul_eq_one_iff_inv_eq₀ hx0] at hy, + exact hy.symm ▸ y.2, +end + +@[simp] lemma to_subalgebra_to_intermediate_field' (S : subalgebra K L) (hS : is_field S) : + (S.to_intermediate_field' hS).to_subalgebra = S := +by { ext, refl } + +@[simp] lemma to_intermediate_field'_to_subalgebra (S : intermediate_field K L) : + S.to_subalgebra.to_intermediate_field' (field.to_is_field S) = S := +by { ext, refl } /-- Turn a subfield of `L` containing the image of `K` into an intermediate field -/ def subfield.to_intermediate_field (S : subfield L) @@ -476,7 +495,7 @@ def subalgebra_equiv_intermediate_field (alg : algebra.is_algebraic K L) : { to_fun := λ S, S.to_intermediate_field (λ x hx, S.inv_mem_of_algebraic (alg (⟨x, hx⟩ : S))), inv_fun := λ S, S.to_subalgebra, left_inv := λ S, to_subalgebra_to_intermediate_field _ _, - right_inv := λ S, to_intermediate_field_to_subalgebra _ _, + right_inv := to_intermediate_field_to_subalgebra, map_rel_iff' := λ S S', iff.rfl } @[simp] lemma mem_subalgebra_equiv_intermediate_field (alg : algebra.is_algebraic K L)