Skip to content

Commit

Permalink
Browse files Browse the repository at this point in the history
feat(field_theory/splitting_field): splitting field unique (#3654)
Main theorem:
```lean
polynomial.is_splitting_field.alg_equiv {α} (β) [field α] [field β] [algebra α β]
  (f : polynomial α) [is_splitting_field α β f] : β ≃ₐ[α] splitting_field f
````



Co-authored-by: Vierkantor <Vierkantor@users.noreply.github.com>
  • Loading branch information
kckennylau and Vierkantor committed Aug 6, 2020
1 parent bc2bcac commit e57fc3d
Show file tree
Hide file tree
Showing 15 changed files with 483 additions and 99 deletions.
8 changes: 2 additions & 6 deletions src/algebra/group/hom.lean
Expand Up @@ -321,12 +321,8 @@ theorem map_mul_inv {G H} [group G] [group H] (f : G →* H) (g h : G) :
@[to_additive]
lemma injective_iff {G H} [group G] [monoid H] (f : G →* H) :
function.injective f ↔ (∀ a, f a = 1 → a = 1) :=
begin
refine ⟨λ h a, (h.eq_iff' f.map_one).1, λ H x y hxy, _⟩,
rw [← mul_inv_eq_one],
apply H,
rw [map_mul, hxy, ← map_mul, mul_inv_self, map_one]
end
⟨λ h x hfx, h $ hfx.trans f.map_one.symm,
λ h x y hxy, mul_inv_eq_one.1 $ h _ $ by rw [f.map_mul, hxy, ← f.map_mul, mul_inv_self, f.map_one]⟩

include mM
/-- Makes a group homomomorphism from a proof that the map preserves multiplication. -/
Expand Down
26 changes: 19 additions & 7 deletions src/data/equiv/ring.lean
Expand Up @@ -115,7 +115,7 @@ lemma to_opposite_symm_apply (r : Rᵒᵖ) : (to_opposite R).symm r = unop r :=

end comm_semiring

section
section semiring

variables [semiring R] [semiring S] (f : R ≃+* S) (x y : R)

Expand All @@ -139,7 +139,11 @@ variable {x}
lemma map_ne_one_iff : f x ≠ 1 ↔ x ≠ 1 := (f : R ≃* S).map_ne_one_iff
lemma map_ne_zero_iff : f x ≠ 0 ↔ x ≠ 0 := (f : R ≃+ S).map_ne_zero_iff

end
/-- Produce a ring isomorphism from a bijective ring homomorphism. -/
noncomputable def of_bijective (f : R →+* S) (hf : function.bijective f) : R ≃+* S :=
{ .. equiv.of_bijective f hf, .. f }

end semiring

section

Expand All @@ -155,7 +159,7 @@ end

section semiring_hom

variables [semiring R] [semiring S]
variables [semiring R] [semiring S] [semiring S']

/-- Reinterpret a ring equivalence as a ring homomorphism. -/
def to_ring_hom (e : R ≃+* S) : R →+* S :=
Expand All @@ -182,15 +186,19 @@ lemma to_monoid_hom_refl : (ring_equiv.refl R).to_monoid_hom = monoid_hom.id R :
lemma to_add_monoid_hom_refl : (ring_equiv.refl R).to_add_monoid_hom = add_monoid_hom.id R := rfl

@[simp]
lemma to_ring_hom_apply_symm_to_ring_hom_apply {R S} [semiring R] [semiring S] (e : R ≃+* S) :
lemma to_ring_hom_apply_symm_to_ring_hom_apply (e : R ≃+* S) :
∀ (y : S), e.to_ring_hom (e.symm.to_ring_hom y) = y :=
e.to_equiv.apply_symm_apply

@[simp]
lemma symm_to_ring_hom_apply_to_ring_hom_apply {R S} [semiring R] [semiring S] (e : R ≃+* S) :
lemma symm_to_ring_hom_apply_to_ring_hom_apply (e : R ≃+* S) :
∀ (x : R), e.symm.to_ring_hom (e.to_ring_hom x) = x :=
equiv.symm_apply_apply (e.to_equiv)

@[simp]
lemma to_ring_hom_trans (e₁ : R ≃+* S) (e₂ : S ≃+* S') :
(e₁.trans e₂).to_ring_hom = e₂.to_ring_hom.comp e₁.to_ring_hom := rfl

end semiring_hom

end ring_equiv
Expand All @@ -206,17 +214,21 @@ end mul_equiv

namespace ring_equiv

variables [has_add R] [has_add S] [has_mul R] [has_mul S]

/-- Two ring isomorphisms agree if they are defined by the
same underlying function. -/
@[ext] lemma ext {R S : Type*} [has_mul R] [has_add R] [has_mul S] [has_add S]
{f g : R ≃+* S} (h : ∀ x, f x = g x) : f = g :=
@[ext] lemma ext {f g : R ≃+* S} (h : ∀ x, f x = g x) : f = g :=
begin
have h₁ : f.to_equiv = g.to_equiv := equiv.ext h,
cases f, cases g, congr,
{ exact (funext h) },
{ exact congr_arg equiv.inv_fun h₁ }
end

@[simp] theorem trans_symm (e : R ≃+* S) : e.trans e.symm = ring_equiv.refl R := ext e.3
@[simp] theorem symm_trans (e : R ≃+* S) : e.symm.trans e = ring_equiv.refl S := ext e.4

/-- If two rings are isomorphic, and the second is an integral domain, then so is the first. -/
protected lemma is_integral_domain {A : Type*} (B : Type*) [ring A] [ring B]
(hB : is_integral_domain B) (e : A ≃+* B) : is_integral_domain A :=
Expand Down
7 changes: 7 additions & 0 deletions src/data/finset/basic.lean
Expand Up @@ -1483,6 +1483,13 @@ begin
end

end image
end finset

theorem multiset.to_finset_map [decidable_eq α] [decidable_eq β] (f : α → β) (m : multiset α) :
(m.map f).to_finset = m.to_finset.image f :=
finset.val_inj.1 (multiset.erase_dup_map_erase_dup_eq _ _).symm

namespace finset

/-! ### card -/
section card
Expand Down
5 changes: 5 additions & 0 deletions src/data/list/basic.lean
Expand Up @@ -1807,6 +1807,11 @@ calc (l₁ ++ l₂).prod = foldl (*) (foldl (*) 1 l₁ * 1) l₂ : by simp [list
theorem prod_join {l : list (list α)} : l.join.prod = (l.map list.prod).prod :=
by induction l; [refl, simp only [*, list.join, map, prod_append, prod_cons]]

theorem prod_ne_zero {R : Type*} [domain R] {L : list R} :
(∀ x ∈ L, (x : _) ≠ 0) → L.prod ≠ 0 :=
list.rec_on L (λ _, one_ne_zero) $ λ hd tl ih H,
by { rw forall_mem_cons at H, rw prod_cons, exact mul_ne_zero H.1 (ih H.2) }

@[to_additive]
theorem prod_eq_foldr : l.prod = foldr (*) 1 l :=
list.rec_on l rfl $ λ a l ihl, by rw [prod_cons, foldr_cons, ihl]
Expand Down
13 changes: 13 additions & 0 deletions src/data/multiset/basic.lean
Expand Up @@ -153,6 +153,10 @@ mem_cons.2 $ or.inr h
@[simp] theorem mem_cons_self (a : α) (s : multiset α) : a ∈ a :: s :=
mem_cons.2 (or.inl rfl)

theorem forall_mem_cons {p : α → Prop} {a : α} {s : multiset α} :
(∀ x ∈ (a :: s), p x) ↔ p a ∧ ∀ x ∈ s, p x :=
quotient.induction_on' s $ λ L, list.forall_mem_cons

theorem exists_cons_of_mem {s : multiset α} {a : α} : a ∈ s → ∃ t, s = a :: t :=
quot.induction_on s $ λ l (h : a ∈ l),
let ⟨l₁, l₂, e⟩ := mem_split h in
Expand Down Expand Up @@ -590,6 +594,10 @@ def map (f : α → β) (s : multiset α) : multiset β :=
quot.lift_on s (λ l : list α, (l.map f : multiset β))
(λ l₁ l₂ p, quot.sound (p.map f))

theorem forall_mem_map_iff {f : α → β} {p : β → Prop} {s : multiset α} :
(∀ y ∈ s.map f, p y) ↔ (∀ x ∈ s, p (f x)) :=
quotient.induction_on' s $ λ L, list.forall_mem_map_iff

@[simp] theorem coe_map (f : α → β) (l : list α) : map f ↑l = l.map f := rfl

@[simp] theorem map_zero (f : α → β) : map f 0 = 0 := rfl
Expand Down Expand Up @@ -778,6 +786,11 @@ lemma sum_map_mul_right [semiring β] {b : β} {s : multiset α} {f : α → β}
sum (s.map (λa, f a * b)) = sum (s.map f) * b :=
multiset.induction_on s (by simp) (assume a s ih, by simp [ih, add_mul])

theorem prod_ne_zero {R : Type*} [integral_domain R] {m : multiset R} :
(∀ x ∈ m, (x : _) ≠ 0) → m.prod ≠ 0 :=
multiset.induction_on m (λ _, one_ne_zero) $ λ hd tl ih H,
by { rw forall_mem_cons at H, rw prod_cons, exact mul_ne_zero H.1 (ih H.2) }

@[to_additive]
lemma prod_hom [comm_monoid α] [comm_monoid β] (s : multiset α) (f : α → β) [is_monoid_hom f] :
(s.map f).prod = f s.prod :=
Expand Down
16 changes: 16 additions & 0 deletions src/data/polynomial/eval.lean
Expand Up @@ -343,6 +343,9 @@ instance map.is_semiring_hom : is_semiring_hom (map f) :=
map_add := λ _ _, eval₂_add _ _,
map_mul := λ _ _, map_mul f, }

lemma map_list_prod (L : list (polynomial R)) : L.prod.map f = (L.map $ map f).prod :=
eq.symm $ list.prod_hom _ _

@[simp] lemma map_pow (n : ℕ) : (p ^ n).map f = p.map f ^ n := is_monoid_hom.map_pow (map f) _ _

lemma mem_map_range {p : polynomial S} :
Expand Down Expand Up @@ -433,6 +436,19 @@ lemma root_mul_right_of_is_root {p : polynomial R} (q : polynomial R) :

end eval

section map

variables [comm_semiring R] [comm_semiring S] (f : R →+* S)

lemma map_multiset_prod (m : multiset (polynomial R)) : m.prod.map f = (m.map $ map f).prod :=
eq.symm $ multiset.prod_hom _ _

lemma map_prod {ι : Type*} (g : ι → polynomial R) (s : finset ι) :
(∏ i in s, g i).map f = ∏ i in s, (g i).map f :=
eq.symm $ prod_hom _ _

end map

end comm_semiring

section ring
Expand Down
3 changes: 3 additions & 0 deletions src/data/polynomial/field_division.lean
Expand Up @@ -207,6 +207,9 @@ by rw [← gcd_is_unit_iff, ← gcd_is_unit_iff, gcd_map, is_unit_map]
p.map f = 0 ↔ p = 0 :=
by simp [polynomial.ext_iff, f.map_eq_zero, coeff_map]

lemma map_ne_zero [field k] {f : R →+* k} (hp : p ≠ 0) : p.map f ≠ 0 :=
mt (map_eq_zero f).1 hp

lemma exists_root_of_degree_eq_one (h : degree p = 1) : ∃ x, is_root p x :=
⟨-(p.coeff 0 / p.coeff 1),
have p.coeff 10,
Expand Down
29 changes: 29 additions & 0 deletions src/data/polynomial/ring_division.lean
Expand Up @@ -129,6 +129,9 @@ using_well_founded {dec_tac := tactic.assumption}
noncomputable def roots (p : polynomial R) : finset R :=
if h : p = 0 thenelse classical.some (exists_finset_roots h)

@[simp] lemma roots_zero : (0 : polynomial R).roots = ∅ :=
dif_pos rfl

lemma card_roots (hp0 : p ≠ 0) : ((roots p).card : with_bot ℕ) ≤ degree p :=
begin
unfold roots,
Expand Down Expand Up @@ -166,6 +169,32 @@ finset.ext $ λ r, by rw [mem_union, mem_roots hpq, mem_roots (mul_ne_zero_iff.1
@[simp] lemma roots_X_sub_C (r : R) : roots (X - C r) = {r} :=
finset.ext $ λ s, by rw [mem_roots (X_sub_C_ne_zero r), root_X_sub_C, mem_singleton, eq_comm]

@[simp] lemma roots_C (x : R) : (C x).roots = ∅ :=
if H : x = 0 then by rw [H, C_0, roots_zero] else finset.ext $ λ r,
have h : C x ≠ 0, from λ h, H $ C_inj.1 $ h.symm ▸ C_0.symm,
by rw [mem_roots h, is_root.def, eval_C, eq_false_intro H, eq_false_intro (finset.not_mem_empty r)]

@[simp] lemma roots_one : (1 : polynomial R).roots = ∅ :=
roots_C 1

lemma roots_list_prod (L : list (polynomial R)) :
(∀ p ∈ L, (p : _) ≠ 0) → L.prod.roots = L.to_finset.bind roots :=
list.rec_on L (λ _, roots_one) $ λ hd tl ih H,
begin
rw list.forall_mem_cons at H,
rw [list.prod_cons, roots_mul (mul_ne_zero H.1 $ list.prod_ne_zero H.2),
list.to_finset_cons, finset.bind_insert, ih H.2]
end

lemma roots_multiset_prod (m : multiset (polynomial R)) :
(∀ p ∈ m, (p : _) ≠ 0) → m.prod.roots = m.to_finset.bind roots :=
multiset.induction_on m (λ _, roots_one) $ λ hd tl ih H,
begin
rw multiset.forall_mem_cons at H,
rw [multiset.prod_cons, roots_mul (mul_ne_zero H.1 $ multiset.prod_ne_zero H.2),
multiset.to_finset_cons, finset.bind_insert, ih H.2]
end

lemma card_roots_X_pow_sub_C {n : ℕ} (hn : 0 < n) (a : R) :
(roots ((X : polynomial R) ^ n - C a)).card ≤ n :=
with_bot.coe_le_coe.1 $
Expand Down

0 comments on commit e57fc3d

Please sign in to comment.