From b1d56ff4da2d0076f02c83e4110c8db9a111c63c Mon Sep 17 00:00:00 2001 From: Thomas Browning Date: Sat, 22 Aug 2020 16:29:38 -0700 Subject: [PATCH 01/32] feat(field_theory/adjoin): new file Defines adjoining elements to fields --- src/field_theory/adjoin.lean | 202 +++++++++++++++++++++++++++++++++++ 1 file changed, 202 insertions(+) create mode 100644 src/field_theory/adjoin.lean diff --git a/src/field_theory/adjoin.lean b/src/field_theory/adjoin.lean new file mode 100644 index 0000000000000..bcbc764bfd2a9 --- /dev/null +++ b/src/field_theory/adjoin.lean @@ -0,0 +1,202 @@ +/- +Copyright (c) 2020 Thomas Browning and Patrick Lutz. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Thomas Browning and Patrick Lutz +-/ + +import field_theory.subfield +import field_theory.separable +import field_theory.tower +import group_theory.subgroup +import field_theory.minimal_polynomial +import linear_algebra.dimension +import linear_algebra.finite_dimensional +import ring_theory.adjoin_root +import data.zmod.basic + +/-! +# Adjoining Elements to Fields + +In this file we introduce the notion of adjoining elements to fields. +This isn't quite the same as adjoining elements to rings, since the element might not be algebraic. + +## Main results + +(This is just a start, We've got more to add, including a proof of the Primitive Element Theorem) + +- `adjoin_twice`: adjoining S and then T is the same as adjoining S ∪ T. + +## Notation + + - `F[α]` : Adjoin α to F. +-/ + +variables (F : Type*) [field F] {E : Type*} [field E] [algebra F E] (S : set E) + +/-- +Adjoining a set S ⊆ E to a field F +-/ +def adjoin : set E := field.closure (set.range (algebra_map F E) ∪ S) + +lemma adjoin.field_mem (x : F) : algebra_map F E x ∈ adjoin F S := +field.mem_closure (or.inl (set.mem_range_self x)) + +lemma adjoin.field_subset : set.range (algebra_map F E) ⊆ adjoin F S := +begin + intros x hx, + cases hx with f hf, + rw ←hf, + exact adjoin.field_mem F S f, +end + +instance adjoin.field_coe : has_coe_t F (adjoin F S) := +{coe := λ x, ⟨algebra_map F E x, adjoin.field_mem F S x⟩} + +lemma adjoin.set_mem (x : S) : ↑x ∈ adjoin F S := +field.mem_closure (or.inr (subtype.mem x)) + +lemma adjoin.set_subset : S ⊆ adjoin F S := +λ x hx, adjoin.set_mem F S ⟨x,hx⟩ + +instance adjoin.set_coe : has_coe_t S (adjoin F S) := +{coe := λ x, ⟨↑x, adjoin.set_mem F S x⟩} + +lemma adjoin.mono (T : set E) (h : S ⊆ T) : adjoin F S ⊆ adjoin F T := +field.closure_mono (set.union_subset (set.subset_union_left _ _) (set.subset_union_of_subset_right h _)) + +instance adjoin.is_subfield : is_subfield (adjoin F S) := field.closure.is_subfield + +lemma adjoin_contains_field_as_subfield (F : set E) {HF : is_subfield F} : F ⊆ adjoin F S := +λ x hx, adjoin.field_mem F S ⟨x, hx⟩ + +lemma adjoin_contains_subset {T : set E} {H : T ⊆ S} : T ⊆ adjoin F S := +begin + intros x hx, + exact adjoin.set_mem F S ⟨x,H hx⟩, +end + +instance adjoin.is_algebra : algebra F (adjoin F S) := { + smul := λ x y, ⟨algebra_map F E x, adjoin.field_mem F S x⟩ * y, + to_fun := λ x, ⟨algebra_map F E x, adjoin.field_mem F S x⟩, + map_one' := by simp only [ring_hom.map_one];refl, + map_mul' := λ x y, by simp only [ring_hom.map_mul];refl, + map_zero' := by simp only [ring_hom.map_zero];refl, + map_add' := λ x y, by simp only [ring_hom.map_add];refl, + commutes' := λ x y, by rw mul_comm, + smul_def' := λ x y, rfl, +} + +def adjoin_as_submodule : submodule F E := { + carrier := adjoin F S, + zero_mem' := is_add_submonoid.zero_mem, + add_mem' := λ a b, is_add_submonoid.add_mem, + smul_mem' := + begin + intros a b hb, + rw algebra.smul_def, + exact is_submonoid.mul_mem (adjoin.field_mem F S a) hb, + end +} + +definition adjoin_as_submodule_equiv : (adjoin F S) ≃ₗ[F] (adjoin_as_submodule F S) := { + to_fun := λ x, x, + map_add' := λ x y, rfl, + map_smul' := + begin + intros x y, + ext1, + change _ = x • ↑y, + rw algebra.smul_def, + rw algebra.smul_def, + refl, + end, + inv_fun := λ x, x, + left_inv := λ x, rfl, + right_inv := λ x, rfl, +} + +/-- If F ⊆ T and S ⊆ T then F[S] ⊆ F[T] -/ +lemma adjoin_subset {T : set E} [is_subfield T] (HF : set.range (algebra_map F E) ⊆ T) +(HS : S ⊆ T) : adjoin F S ⊆ T := +begin + apply field.closure_subset, + rw set.union_subset_iff, + exact ⟨HF,HS⟩, +end + +/-- If S ⊆ F[T] then F[S] ⊆ F[T] -/ +lemma adjoin_subset' {T : set E} (HT : S ⊆ adjoin F T) : adjoin F S ⊆ adjoin F T := +adjoin_subset F S (adjoin.field_subset F T) HT + +lemma set_range_subset {T₁ T₂ : set E} [is_subfield T₁] [is_subfield T₂] {hyp : T₁ ⊆ T₂} : +set.range (algebra_map T₁ E) ⊆ T₂ := +begin + intros x hx, + cases hx with f hf, + rw ←hf, + cases f with t ht, + exact hyp ht, +end + +lemma adjoin_contains_field_subset {F : set E} {HF : is_subfield F} {T : set E} {HT : T ⊆ F} : +T ⊆ adjoin F S := +λ x hx, adjoin.field_mem F S ⟨x,HT hx⟩ + +/-- F[S][T] = F[S ∪ T] -/ +lemma adjoin_twice (T : set E) : adjoin (adjoin F S) T = adjoin F (S ∪ T) := +begin + apply set.eq_of_subset_of_subset, + apply adjoin_subset, + apply set_range_subset, + apply adjoin_subset, + apply adjoin.field_subset, + apply adjoin_contains_subset, + apply set.subset_union_left, + apply adjoin_contains_subset, + apply set.subset_union_right, + apply adjoin_subset, + transitivity adjoin F S, + apply adjoin.field_subset, + apply adjoin_subset, + apply adjoin_contains_field_subset, + apply adjoin.field_subset, + apply adjoin_contains_field_subset, + apply adjoin.set_subset, + apply set.union_subset, + apply adjoin_contains_field_subset, + apply adjoin.set_subset, + apply adjoin.set_subset, +end + +lemma adjoin.composition : +(algebra_map F E) = (algebra_map (adjoin F S) E).comp (algebra_map F (adjoin F S)) := by ext;refl + +instance adjoin_algebra_tower : is_scalar_tower F (adjoin F S) E := { + smul_assoc := + begin + intros x y z, + rw algebra.smul_def, + rw algebra.smul_def, + rw algebra.smul_def, + rw ring_hom.map_mul, + rw mul_assoc, + refl, + end +} + +variables (α : E) + +--we're working on automatically getting notation for K[α,β,γ], but haven't quite figured it out yet +notation K`[`:std.prec.max_plus β`]` := adjoin K (@singleton _ _ set.has_singleton β) +notation K`[`:std.prec.max_plus β `,` γ`]` := adjoin K {β,γ} + +lemma adjoin_simple.element_mem : α ∈ F[α] := +adjoin.set_mem F {α} (⟨α,set.mem_singleton α⟩ : ({α} : set E)) + +/-- generator of F(α) -/ +def adjoin_simple.gen : F[α] := ⟨α, adjoin_simple.element_mem F α⟩ + +lemma adjoin_simple.gen_eq_alpha : algebra_map F[α] E (adjoin_simple.gen F α) = α := rfl + +lemma adjoin_simple_twice (β : E) : F[α][β] = adjoin F {α,β} := +adjoin_twice _ _ _ From 113addede8bfc55bf294976993ac32d88b67bec6 Mon Sep 17 00:00:00 2001 From: Thomas Browning Date: Sat, 22 Aug 2020 17:17:24 -0700 Subject: [PATCH 02/32] doc(field_theory/adjoin): add docstrings --- src/field_theory/adjoin.lean | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/field_theory/adjoin.lean b/src/field_theory/adjoin.lean index bcbc764bfd2a9..ba67bcfe46c9d 100644 --- a/src/field_theory/adjoin.lean +++ b/src/field_theory/adjoin.lean @@ -86,6 +86,7 @@ instance adjoin.is_algebra : algebra F (adjoin F S) := { smul_def' := λ x y, rfl, } +/-- F[S] is an F-submodule of E -/ def adjoin_as_submodule : submodule F E := { carrier := adjoin F S, zero_mem' := is_add_submonoid.zero_mem, @@ -98,6 +99,7 @@ def adjoin_as_submodule : submodule F E := { end } +/-- proves an obvious linear equivalence (occasionally useful when working with dimension) -/ definition adjoin_as_submodule_equiv : (adjoin F S) ≃ₗ[F] (adjoin_as_submodule F S) := { to_fun := λ x, x, map_add' := λ x y, rfl, From 59e53711d488120eec3836990be9592fde238e78 Mon Sep 17 00:00:00 2001 From: Thomas Browning Date: Sat, 22 Aug 2020 17:58:09 -0700 Subject: [PATCH 03/32] refactor(field_theory/adjoin): remove assumption --- src/field_theory/adjoin.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/field_theory/adjoin.lean b/src/field_theory/adjoin.lean index ba67bcfe46c9d..a78decc2b127e 100644 --- a/src/field_theory/adjoin.lean +++ b/src/field_theory/adjoin.lean @@ -130,7 +130,7 @@ end lemma adjoin_subset' {T : set E} (HT : S ⊆ adjoin F T) : adjoin F S ⊆ adjoin F T := adjoin_subset F S (adjoin.field_subset F T) HT -lemma set_range_subset {T₁ T₂ : set E} [is_subfield T₁] [is_subfield T₂] {hyp : T₁ ⊆ T₂} : +lemma set_range_subset {T₁ T₂ : set E} [is_subfield T₁] {hyp : T₁ ⊆ T₂} : set.range (algebra_map T₁ E) ⊆ T₂ := begin intros x hx, From f9b010ebff63831315aebe184b2be30e7d2ba7ea Mon Sep 17 00:00:00 2001 From: tb65536 Date: Tue, 25 Aug 2020 21:10:51 -0700 Subject: [PATCH 04/32] Update src/field_theory/adjoin.lean Co-authored-by: Vierkantor --- src/field_theory/adjoin.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/field_theory/adjoin.lean b/src/field_theory/adjoin.lean index a78decc2b127e..477bf9d8fadca 100644 --- a/src/field_theory/adjoin.lean +++ b/src/field_theory/adjoin.lean @@ -28,7 +28,7 @@ This isn't quite the same as adjoining elements to rings, since the element migh ## Notation - - `F[α]` : Adjoin α to F. + - `F[α]` : Adjoin a single element α to F. -/ variables (F : Type*) [field F] {E : Type*} [field E] [algebra F E] (S : set E) From c6d4e4bdb71ad246103c101fbdbd5e6cd006d956 Mon Sep 17 00:00:00 2001 From: tb65536 Date: Tue, 25 Aug 2020 21:11:17 -0700 Subject: [PATCH 05/32] Update src/field_theory/adjoin.lean Co-authored-by: Vierkantor --- src/field_theory/adjoin.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/field_theory/adjoin.lean b/src/field_theory/adjoin.lean index 477bf9d8fadca..cc66f80a94a63 100644 --- a/src/field_theory/adjoin.lean +++ b/src/field_theory/adjoin.lean @@ -34,7 +34,7 @@ This isn't quite the same as adjoining elements to rings, since the element migh variables (F : Type*) [field F] {E : Type*} [field E] [algebra F E] (S : set E) /-- -Adjoining a set S ⊆ E to a field F +`adjoin F S` extends a field `F` by adjoining a set `S ⊆ E`. -/ def adjoin : set E := field.closure (set.range (algebra_map F E) ∪ S) From 0dc82992868d94ed926fdf46cc42b89f4c2d91a1 Mon Sep 17 00:00:00 2001 From: tb65536 Date: Tue, 25 Aug 2020 21:11:37 -0700 Subject: [PATCH 06/32] Update src/field_theory/adjoin.lean Co-authored-by: Vierkantor --- src/field_theory/adjoin.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/field_theory/adjoin.lean b/src/field_theory/adjoin.lean index cc66f80a94a63..c37d820f7ee63 100644 --- a/src/field_theory/adjoin.lean +++ b/src/field_theory/adjoin.lean @@ -198,7 +198,7 @@ adjoin.set_mem F {α} (⟨α,set.mem_singleton α⟩ : ({α} : set E)) /-- generator of F(α) -/ def adjoin_simple.gen : F[α] := ⟨α, adjoin_simple.element_mem F α⟩ -lemma adjoin_simple.gen_eq_alpha : algebra_map F[α] E (adjoin_simple.gen F α) = α := rfl +lemma adjoin_simple.algebra_map_gen : algebra_map F[α] E (adjoin_simple.gen F α) = α := rfl lemma adjoin_simple_twice (β : E) : F[α][β] = adjoin F {α,β} := adjoin_twice _ _ _ From 13b1503b2816b11a6b2ea3f029885da691de0bc9 Mon Sep 17 00:00:00 2001 From: tb65536 Date: Tue, 25 Aug 2020 21:11:49 -0700 Subject: [PATCH 07/32] Update src/field_theory/adjoin.lean Co-authored-by: Vierkantor --- src/field_theory/adjoin.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/field_theory/adjoin.lean b/src/field_theory/adjoin.lean index c37d820f7ee63..a8d14253a1d0c 100644 --- a/src/field_theory/adjoin.lean +++ b/src/field_theory/adjoin.lean @@ -192,7 +192,7 @@ variables (α : E) notation K`[`:std.prec.max_plus β`]` := adjoin K (@singleton _ _ set.has_singleton β) notation K`[`:std.prec.max_plus β `,` γ`]` := adjoin K {β,γ} -lemma adjoin_simple.element_mem : α ∈ F[α] := +lemma mem_adjoin_simple_self : α ∈ F[α] := adjoin.set_mem F {α} (⟨α,set.mem_singleton α⟩ : ({α} : set E)) /-- generator of F(α) -/ From 8b5b1f14ad478fea8f2873b8c5be59bfbec3116f Mon Sep 17 00:00:00 2001 From: tb65536 Date: Tue, 25 Aug 2020 21:12:04 -0700 Subject: [PATCH 08/32] Update src/field_theory/adjoin.lean Co-authored-by: Vierkantor --- src/field_theory/adjoin.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/field_theory/adjoin.lean b/src/field_theory/adjoin.lean index a8d14253a1d0c..56aa8d95ad604 100644 --- a/src/field_theory/adjoin.lean +++ b/src/field_theory/adjoin.lean @@ -200,5 +200,5 @@ def adjoin_simple.gen : F[α] := ⟨α, adjoin_simple.element_mem F α⟩ lemma adjoin_simple.algebra_map_gen : algebra_map F[α] E (adjoin_simple.gen F α) = α := rfl -lemma adjoin_simple_twice (β : E) : F[α][β] = adjoin F {α,β} := +lemma adjoin_simple_adjoin_simple (β : E) : F[α][β] = adjoin F {α,β} := adjoin_twice _ _ _ From 6a19cdca753486780af929112c8c95fabb5112dc Mon Sep 17 00:00:00 2001 From: Thomas Browning Date: Tue, 25 Aug 2020 21:14:52 -0700 Subject: [PATCH 09/32] fix(field_theory/adjoin.lean) change adjoin_simple.gen --- src/field_theory/adjoin.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/field_theory/adjoin.lean b/src/field_theory/adjoin.lean index 56aa8d95ad604..e66309dd1d6f9 100644 --- a/src/field_theory/adjoin.lean +++ b/src/field_theory/adjoin.lean @@ -196,7 +196,7 @@ lemma mem_adjoin_simple_self : α ∈ F[α] := adjoin.set_mem F {α} (⟨α,set.mem_singleton α⟩ : ({α} : set E)) /-- generator of F(α) -/ -def adjoin_simple.gen : F[α] := ⟨α, adjoin_simple.element_mem F α⟩ +def adjoin_simple.gen : F[α] := ⟨α, mem_adjoin_simple_self F α⟩ lemma adjoin_simple.algebra_map_gen : algebra_map F[α] E (adjoin_simple.gen F α) = α := rfl From 206f7eff76883cce11fdd0f866fe5d6a2e205b85 Mon Sep 17 00:00:00 2001 From: Thomas Browning Date: Tue, 25 Aug 2020 21:17:05 -0700 Subject: [PATCH 10/32] doc(field_theory/adjoin.lean): explained why field adjoin is not necessarily the same as algebra adjoin --- src/field_theory/adjoin.lean | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/field_theory/adjoin.lean b/src/field_theory/adjoin.lean index e66309dd1d6f9..609eb7d3fad11 100644 --- a/src/field_theory/adjoin.lean +++ b/src/field_theory/adjoin.lean @@ -18,7 +18,8 @@ import data.zmod.basic # Adjoining Elements to Fields In this file we introduce the notion of adjoining elements to fields. -This isn't quite the same as adjoining elements to rings, since the element might not be algebraic. +This isn't quite the same as adjoining elements to rings. +For example, algebra.adjoin K {x} might not include x⁻¹ ## Main results From 88a2562389382d61d76ee6f554b9779c85409b3a Mon Sep 17 00:00:00 2001 From: Thomas Browning Date: Tue, 25 Aug 2020 21:54:21 -0700 Subject: [PATCH 11/32] feat(field_theory/adjoin.lean): adjoin F S is now automatically a subalgebra --- src/field_theory/adjoin.lean | 53 +++++++++++++----------------------- 1 file changed, 19 insertions(+), 34 deletions(-) diff --git a/src/field_theory/adjoin.lean b/src/field_theory/adjoin.lean index 609eb7d3fad11..ce80e12bf2bf3 100644 --- a/src/field_theory/adjoin.lean +++ b/src/field_theory/adjoin.lean @@ -19,7 +19,7 @@ import data.zmod.basic In this file we introduce the notion of adjoining elements to fields. This isn't quite the same as adjoining elements to rings. -For example, algebra.adjoin K {x} might not include x⁻¹ +For example, algebra.adjoin K {x} might not include x⁻¹. ## Main results @@ -37,7 +37,16 @@ variables (F : Type*) [field F] {E : Type*} [field E] [algebra F E] (S : set E) /-- `adjoin F S` extends a field `F` by adjoining a set `S ⊆ E`. -/ -def adjoin : set E := field.closure (set.range (algebra_map F E) ∪ S) +def adjoin : subalgebra F E := { + carrier := { + carrier := field.closure (set.range (algebra_map F E) ∪ S), + one_mem' := is_submonoid.one_mem, + mul_mem' := λ x y, is_submonoid.mul_mem, + zero_mem' := is_add_submonoid.zero_mem, + add_mem' := λ x y, is_add_submonoid.add_mem, + }, + algebra_map_mem' := λ x, field.mem_closure (or.inl (set.mem_range.mpr ⟨x,rfl⟩)), +} lemma adjoin.field_mem (x : F) : algebra_map F E x ∈ adjoin F S := field.mem_closure (or.inl (set.mem_range_self x)) @@ -62,10 +71,10 @@ lemma adjoin.set_subset : S ⊆ adjoin F S := instance adjoin.set_coe : has_coe_t S (adjoin F S) := {coe := λ x, ⟨↑x, adjoin.set_mem F S x⟩} -lemma adjoin.mono (T : set E) (h : S ⊆ T) : adjoin F S ⊆ adjoin F T := +lemma adjoin.mono (T : set E) (h : S ⊆ T) : (adjoin F S : set E) ⊆ adjoin F T := field.closure_mono (set.union_subset (set.subset_union_left _ _) (set.subset_union_of_subset_right h _)) -instance adjoin.is_subfield : is_subfield (adjoin F S) := field.closure.is_subfield +instance adjoin.is_subfield : is_subfield (adjoin F S : set E) := field.closure.is_subfield lemma adjoin_contains_field_as_subfield (F : set E) {HF : is_subfield F} : F ⊆ adjoin F S := λ x hx, adjoin.field_mem F S ⟨x, hx⟩ @@ -76,32 +85,8 @@ begin exact adjoin.set_mem F S ⟨x,H hx⟩, end -instance adjoin.is_algebra : algebra F (adjoin F S) := { - smul := λ x y, ⟨algebra_map F E x, adjoin.field_mem F S x⟩ * y, - to_fun := λ x, ⟨algebra_map F E x, adjoin.field_mem F S x⟩, - map_one' := by simp only [ring_hom.map_one];refl, - map_mul' := λ x y, by simp only [ring_hom.map_mul];refl, - map_zero' := by simp only [ring_hom.map_zero];refl, - map_add' := λ x y, by simp only [ring_hom.map_add];refl, - commutes' := λ x y, by rw mul_comm, - smul_def' := λ x y, rfl, -} - -/-- F[S] is an F-submodule of E -/ -def adjoin_as_submodule : submodule F E := { - carrier := adjoin F S, - zero_mem' := is_add_submonoid.zero_mem, - add_mem' := λ a b, is_add_submonoid.add_mem, - smul_mem' := - begin - intros a b hb, - rw algebra.smul_def, - exact is_submonoid.mul_mem (adjoin.field_mem F S a) hb, - end -} - /-- proves an obvious linear equivalence (occasionally useful when working with dimension) -/ -definition adjoin_as_submodule_equiv : (adjoin F S) ≃ₗ[F] (adjoin_as_submodule F S) := { +definition adjoin_as_submodule_equiv : (adjoin F S) ≃ₗ[F] (adjoin F S) := { to_fun := λ x, x, map_add' := λ x y, rfl, map_smul' := @@ -120,7 +105,7 @@ definition adjoin_as_submodule_equiv : (adjoin F S) ≃ₗ[F] (adjoin_as_submodu /-- If F ⊆ T and S ⊆ T then F[S] ⊆ F[T] -/ lemma adjoin_subset {T : set E} [is_subfield T] (HF : set.range (algebra_map F E) ⊆ T) -(HS : S ⊆ T) : adjoin F S ⊆ T := +(HS : S ⊆ T) : (adjoin F S : set E) ⊆ T := begin apply field.closure_subset, rw set.union_subset_iff, @@ -128,7 +113,7 @@ begin end /-- If S ⊆ F[T] then F[S] ⊆ F[T] -/ -lemma adjoin_subset' {T : set E} (HT : S ⊆ adjoin F T) : adjoin F S ⊆ adjoin F T := +lemma adjoin_subset' {T : set E} (HT : S ⊆ adjoin F T) : (adjoin F S : set E) ⊆ adjoin F T := adjoin_subset F S (adjoin.field_subset F T) HT lemma set_range_subset {T₁ T₂ : set E} [is_subfield T₁] {hyp : T₁ ⊆ T₂} : @@ -146,7 +131,7 @@ T ⊆ adjoin F S := λ x hx, adjoin.field_mem F S ⟨x,HT hx⟩ /-- F[S][T] = F[S ∪ T] -/ -lemma adjoin_twice (T : set E) : adjoin (adjoin F S) T = adjoin F (S ∪ T) := +lemma adjoin_twice (T : set E) : (adjoin (adjoin F S : set E) T : set E) = adjoin F (S ∪ T) := begin apply set.eq_of_subset_of_subset, apply adjoin_subset, @@ -158,7 +143,7 @@ begin apply adjoin_contains_subset, apply set.subset_union_right, apply adjoin_subset, - transitivity adjoin F S, + transitivity (adjoin F S : set E), apply adjoin.field_subset, apply adjoin_subset, apply adjoin_contains_field_subset, @@ -201,5 +186,5 @@ def adjoin_simple.gen : F[α] := ⟨α, mem_adjoin_simple_self F α⟩ lemma adjoin_simple.algebra_map_gen : algebra_map F[α] E (adjoin_simple.gen F α) = α := rfl -lemma adjoin_simple_adjoin_simple (β : E) : F[α][β] = adjoin F {α,β} := +lemma adjoin_simple_adjoin_simple (β : E) : ((F[α] : set E)[β] : set E) = adjoin F ({α,β} : set E) := adjoin_twice _ _ _ From cdf5f3efbdefbd54dd695ac83bc033d48580a26a Mon Sep 17 00:00:00 2001 From: Thomas Browning Date: Tue, 25 Aug 2020 21:57:47 -0700 Subject: [PATCH 12/32] refactor(field_theory/adjoin.lean): algebra_tower no longer needed --- src/field_theory/adjoin.lean | 13 ------------- 1 file changed, 13 deletions(-) diff --git a/src/field_theory/adjoin.lean b/src/field_theory/adjoin.lean index ce80e12bf2bf3..66d6b8fba05e0 100644 --- a/src/field_theory/adjoin.lean +++ b/src/field_theory/adjoin.lean @@ -159,19 +159,6 @@ end lemma adjoin.composition : (algebra_map F E) = (algebra_map (adjoin F S) E).comp (algebra_map F (adjoin F S)) := by ext;refl -instance adjoin_algebra_tower : is_scalar_tower F (adjoin F S) E := { - smul_assoc := - begin - intros x y z, - rw algebra.smul_def, - rw algebra.smul_def, - rw algebra.smul_def, - rw ring_hom.map_mul, - rw mul_assoc, - refl, - end -} - variables (α : E) --we're working on automatically getting notation for K[α,β,γ], but haven't quite figured it out yet From ec1a1b7939f4bb671dd20ba1ef8054d0e4104ab4 Mon Sep 17 00:00:00 2001 From: Thomas Browning Date: Wed, 26 Aug 2020 11:38:38 -0700 Subject: [PATCH 13/32] refactor(field_theory/adjoin.lean): clean up --- src/field_theory/adjoin.lean | 31 ++++++++++++++++++------------- 1 file changed, 18 insertions(+), 13 deletions(-) diff --git a/src/field_theory/adjoin.lean b/src/field_theory/adjoin.lean index 66d6b8fba05e0..10e739506cfa7 100644 --- a/src/field_theory/adjoin.lean +++ b/src/field_theory/adjoin.lean @@ -5,14 +5,7 @@ Authors: Thomas Browning and Patrick Lutz -/ import field_theory.subfield -import field_theory.separable -import field_theory.tower -import group_theory.subgroup -import field_theory.minimal_polynomial -import linear_algebra.dimension import linear_algebra.finite_dimensional -import ring_theory.adjoin_root -import data.zmod.basic /-! # Adjoining Elements to Fields @@ -161,17 +154,29 @@ lemma adjoin.composition : variables (α : E) ---we're working on automatically getting notation for K[α,β,γ], but haven't quite figured it out yet -notation K`[`:std.prec.max_plus β`]` := adjoin K (@singleton _ _ set.has_singleton β) -notation K`[`:std.prec.max_plus β `,` γ`]` := adjoin K {β,γ} +notation K`[`:std.prec.max_plus l:(foldr `, ` (h t, set.insert h t) ∅) `]` := adjoin K l + +--unfortunately this lemma is not definitionally true +lemma adjoin_singleton : F[α] = adjoin F {α} := +begin + change adjoin F (insert α ∅) = adjoin F {α}, + rw insert_emptyc_eq α, + exact set.is_lawful_singleton, +end lemma mem_adjoin_simple_self : α ∈ F[α] := -adjoin.set_mem F {α} (⟨α,set.mem_singleton α⟩ : ({α} : set E)) +begin + rw adjoin_singleton, + exact adjoin.set_mem F {α} (⟨α,set.mem_singleton α⟩ : ({α} : set E)), +end /-- generator of F(α) -/ def adjoin_simple.gen : F[α] := ⟨α, mem_adjoin_simple_self F α⟩ lemma adjoin_simple.algebra_map_gen : algebra_map F[α] E (adjoin_simple.gen F α) = α := rfl -lemma adjoin_simple_adjoin_simple (β : E) : ((F[α] : set E)[β] : set E) = adjoin F ({α,β} : set E) := -adjoin_twice _ _ _ +lemma adjoin_simple_adjoin_simple (β : E) : F[α,β] = adjoin F {α,β} := +begin + change adjoin F (insert α (insert β ∅)) = adjoin F _, + simp only [insert_emptyc_eq], +end From 0d6cac863af0e1441614aaa24d36fdd1d0113068 Mon Sep 17 00:00:00 2001 From: Thomas Browning Date: Wed, 26 Aug 2020 11:50:12 -0700 Subject: [PATCH 14/32] refactor(field_theory/adjoin.lean): indent proof of adjoin_twice --- src/field_theory/adjoin.lean | 58 +++++++++++++----------------------- 1 file changed, 20 insertions(+), 38 deletions(-) diff --git a/src/field_theory/adjoin.lean b/src/field_theory/adjoin.lean index 10e739506cfa7..c1745b2a0392b 100644 --- a/src/field_theory/adjoin.lean +++ b/src/field_theory/adjoin.lean @@ -78,24 +78,6 @@ begin exact adjoin.set_mem F S ⟨x,H hx⟩, end -/-- proves an obvious linear equivalence (occasionally useful when working with dimension) -/ -definition adjoin_as_submodule_equiv : (adjoin F S) ≃ₗ[F] (adjoin F S) := { - to_fun := λ x, x, - map_add' := λ x y, rfl, - map_smul' := - begin - intros x y, - ext1, - change _ = x • ↑y, - rw algebra.smul_def, - rw algebra.smul_def, - refl, - end, - inv_fun := λ x, x, - left_inv := λ x, rfl, - right_inv := λ x, rfl, -} - /-- If F ⊆ T and S ⊆ T then F[S] ⊆ F[T] -/ lemma adjoin_subset {T : set E} [is_subfield T] (HF : set.range (algebra_map F E) ⊆ T) (HS : S ⊆ T) : (adjoin F S : set E) ⊆ T := @@ -127,26 +109,26 @@ T ⊆ adjoin F S := lemma adjoin_twice (T : set E) : (adjoin (adjoin F S : set E) T : set E) = adjoin F (S ∪ T) := begin apply set.eq_of_subset_of_subset, - apply adjoin_subset, - apply set_range_subset, - apply adjoin_subset, - apply adjoin.field_subset, - apply adjoin_contains_subset, - apply set.subset_union_left, - apply adjoin_contains_subset, - apply set.subset_union_right, - apply adjoin_subset, - transitivity (adjoin F S : set E), - apply adjoin.field_subset, - apply adjoin_subset, - apply adjoin_contains_field_subset, - apply adjoin.field_subset, - apply adjoin_contains_field_subset, - apply adjoin.set_subset, - apply set.union_subset, - apply adjoin_contains_field_subset, - apply adjoin.set_subset, - apply adjoin.set_subset, + { apply adjoin_subset, + { apply set_range_subset, + apply adjoin_subset, + { apply adjoin.field_subset }, + { apply adjoin_contains_subset, + apply set.subset_union_left} }, + { apply adjoin_contains_subset, + apply set.subset_union_right } }, + { apply adjoin_subset, + { transitivity (adjoin F S : set E), + { apply adjoin.field_subset}, + { apply adjoin_subset, + { apply adjoin_contains_field_subset, + apply adjoin.field_subset }, + { apply adjoin_contains_field_subset, + apply adjoin.set_subset} } }, + { apply set.union_subset, + { apply adjoin_contains_field_subset, + apply adjoin.set_subset }, + { apply adjoin.set_subset } } } end lemma adjoin.composition : From f4595a2c741502cbcddfaa646b90c782d081924a Mon Sep 17 00:00:00 2001 From: Patrick Lutz Date: Thu, 27 Aug 2020 20:09:34 -0700 Subject: [PATCH 15/32] making some of the requested changes --- src/field_theory/adjoin.lean | 86 ++++++++++++++++++------------------ 1 file changed, 43 insertions(+), 43 deletions(-) diff --git a/src/field_theory/adjoin.lean b/src/field_theory/adjoin.lean index c1745b2a0392b..e9f9460fa2b99 100644 --- a/src/field_theory/adjoin.lean +++ b/src/field_theory/adjoin.lean @@ -25,6 +25,7 @@ For example, algebra.adjoin K {x} might not include x⁻¹. - `F[α]` : Adjoin a single element α to F. -/ +namespace field variables (F : Type*) [field F] {E : Type*} [field E] [algebra F E] (S : set E) /-- @@ -41,25 +42,29 @@ def adjoin : subalgebra F E := { algebra_map_mem' := λ x, field.mem_closure (or.inl (set.mem_range.mpr ⟨x,rfl⟩)), } -lemma adjoin.field_mem (x : F) : algebra_map F E x ∈ adjoin F S := +lemma adjoin.algebra_map_mem (x : F) : algebra_map F E x ∈ adjoin F S := field.mem_closure (or.inl (set.mem_range_self x)) -lemma adjoin.field_subset : set.range (algebra_map F E) ⊆ adjoin F S := +lemma subset_adjoin_of_subset_left {F : set E} {HF : is_subfield F} {T : set E} (HT : T ⊆ F) : + T ⊆ adjoin F S := +λ x hx, adjoin.algebra_map_mem F S ⟨x, HT hx⟩ + +lemma adjoin.range_algebra_map_subset : set.range (algebra_map F E) ⊆ adjoin F S := begin intros x hx, cases hx with f hf, - rw ←hf, - exact adjoin.field_mem F S f, + rw ← hf, + exact adjoin.algebra_map_mem F S f, end instance adjoin.field_coe : has_coe_t F (adjoin F S) := -{coe := λ x, ⟨algebra_map F E x, adjoin.field_mem F S x⟩} +{coe := λ x, ⟨algebra_map F E x, adjoin.algebra_map_mem F S x⟩} lemma adjoin.set_mem (x : S) : ↑x ∈ adjoin F S := field.mem_closure (or.inr (subtype.mem x)) -lemma adjoin.set_subset : S ⊆ adjoin F S := -λ x hx, adjoin.set_mem F S ⟨x,hx⟩ +lemma subset_adjoin : S ⊆ adjoin F S := +λ x hx, adjoin.set_mem F S ⟨x, hx⟩ instance adjoin.set_coe : has_coe_t S (adjoin F S) := {coe := λ x, ⟨↑x, adjoin.set_mem F S x⟩} @@ -70,29 +75,30 @@ field.closure_mono (set.union_subset (set.subset_union_left _ _) (set.subset_uni instance adjoin.is_subfield : is_subfield (adjoin F S : set E) := field.closure.is_subfield lemma adjoin_contains_field_as_subfield (F : set E) {HF : is_subfield F} : F ⊆ adjoin F S := -λ x hx, adjoin.field_mem F S ⟨x, hx⟩ +λ x hx, adjoin.algebra_map_mem F S ⟨x, hx⟩ -lemma adjoin_contains_subset {T : set E} {H : T ⊆ S} : T ⊆ adjoin F S := +lemma subset_adjoin_of_subset_right {T : set E} (H : T ⊆ S) : T ⊆ adjoin F S := begin intros x hx, exact adjoin.set_mem F S ⟨x,H hx⟩, end -/-- If F ⊆ T and S ⊆ T then F[S] ⊆ F[T] -/ -lemma adjoin_subset {T : set E} [is_subfield T] (HF : set.range (algebra_map F E) ⊆ T) -(HS : S ⊆ T) : (adjoin F S : set E) ⊆ T := +/-- If `K` is a field with `F ⊆ K` and `S ⊆ K` then `adjoin F S ⊆ K`. -/ +lemma adjoin_subset_subfield {K : set E} [is_subfield K] (HF : set.range (algebra_map F E) ⊆ K) + (HS : S ⊆ K) : (adjoin F S : set E) ⊆ K := begin apply field.closure_subset, rw set.union_subset_iff, - exact ⟨HF,HS⟩, + exact ⟨HF, HS⟩, end -/-- If S ⊆ F[T] then F[S] ⊆ F[T] -/ -lemma adjoin_subset' {T : set E} (HT : S ⊆ adjoin F T) : (adjoin F S : set E) ⊆ adjoin F T := -adjoin_subset F S (adjoin.field_subset F T) HT +/-- `S ⊆ adjoin F T` if and only if `adjoin F S ⊆ adjoin F T` -/ +lemma adjoin_subset_iff {T : set E} : S ⊆ adjoin F T ↔ (adjoin F S : set E) ⊆ adjoin F T := +⟨λ h, adjoin_subset_subfield F S (adjoin.range_algebra_map_subset F T) h, + λ h, set.subset.trans (subset_adjoin F S) h⟩ -lemma set_range_subset {T₁ T₂ : set E} [is_subfield T₁] {hyp : T₁ ⊆ T₂} : -set.range (algebra_map T₁ E) ⊆ T₂ := +lemma set_range_subset {T₁ T₂ : set E} [is_subfield T₁] (hyp : T₁ ⊆ T₂) : + set.range (algebra_map T₁ E) ⊆ T₂ := begin intros x hx, cases hx with f hf, @@ -101,34 +107,26 @@ begin exact hyp ht, end -lemma adjoin_contains_field_subset {F : set E} {HF : is_subfield F} {T : set E} {HT : T ⊆ F} : -T ⊆ adjoin F S := -λ x hx, adjoin.field_mem F S ⟨x,HT hx⟩ +lemma subfield_subset_adjoin_self {F : set E} {HF : is_subfield F} {T : set E} {HT : T ⊆ F} : + T ⊆ adjoin F S := +λ x hx, adjoin.algebra_map_mem F S ⟨x,HT hx⟩ + +lemma adjoin_subset_adjoin_iff {F' : Type*} [field F'] [algebra F' E] + {S S' : set E} : (adjoin F S : set E) ⊆ adjoin F' S' ↔ + set.range (algebra_map F E) ⊆ adjoin F' S' ∧ S ⊆ adjoin F' S' := +⟨λ h, ⟨trans (adjoin.range_algebra_map_subset _ _) h, trans (subset_adjoin _ _) h⟩, + λ ⟨hF, hS⟩, field.closure_subset (set.union_subset hF hS)⟩ /-- F[S][T] = F[S ∪ T] -/ -lemma adjoin_twice (T : set E) : (adjoin (adjoin F S : set E) T : set E) = adjoin F (S ∪ T) := +lemma adjoin_adjoin_left (T : set E) : (adjoin (adjoin F S : set E) T : set E) = adjoin F (S ∪ T) := begin - apply set.eq_of_subset_of_subset, - { apply adjoin_subset, - { apply set_range_subset, - apply adjoin_subset, - { apply adjoin.field_subset }, - { apply adjoin_contains_subset, - apply set.subset_union_left} }, - { apply adjoin_contains_subset, - apply set.subset_union_right } }, - { apply adjoin_subset, - { transitivity (adjoin F S : set E), - { apply adjoin.field_subset}, - { apply adjoin_subset, - { apply adjoin_contains_field_subset, - apply adjoin.field_subset }, - { apply adjoin_contains_field_subset, - apply adjoin.set_subset} } }, - { apply set.union_subset, - { apply adjoin_contains_field_subset, - apply adjoin.set_subset }, - { apply adjoin.set_subset } } } + apply set.eq_of_subset_of_subset; rw adjoin_subset_adjoin_iff; split, + { exact set_range_subset (adjoin.mono _ _ _ (set.subset_union_left _ _)) }, + { exact subset_adjoin_of_subset_right _ _ (set.subset_union_right _ _) }, + { exact subset_adjoin_of_subset_left _ (adjoin.range_algebra_map_subset _ _) }, + { exact set.union_subset + (subset_adjoin_of_subset_left _ (subset_adjoin _ _)) + (subset_adjoin _ _) }, end lemma adjoin.composition : @@ -162,3 +160,5 @@ begin change adjoin F (insert α (insert β ∅)) = adjoin F _, simp only [insert_emptyc_eq], end + +end field From d736714485ac1673c207b86a08d892313a64b806 Mon Sep 17 00:00:00 2001 From: tb65536 Date: Thu, 27 Aug 2020 23:35:47 -0700 Subject: [PATCH 16/32] Update src/field_theory/adjoin.lean Co-authored-by: Johan Commelin --- src/field_theory/adjoin.lean | 12 +++++------- 1 file changed, 5 insertions(+), 7 deletions(-) diff --git a/src/field_theory/adjoin.lean b/src/field_theory/adjoin.lean index e9f9460fa2b99..4797caf3063d5 100644 --- a/src/field_theory/adjoin.lean +++ b/src/field_theory/adjoin.lean @@ -31,16 +31,14 @@ variables (F : Type*) [field F] {E : Type*} [field E] [algebra F E] (S : set E) /-- `adjoin F S` extends a field `F` by adjoining a set `S ⊆ E`. -/ -def adjoin : subalgebra F E := { - carrier := { - carrier := field.closure (set.range (algebra_map F E) ∪ S), +def adjoin : subalgebra F E := +{ carrier := + { carrier := field.closure (set.range (algebra_map F E) ∪ S), one_mem' := is_submonoid.one_mem, mul_mem' := λ x y, is_submonoid.mul_mem, zero_mem' := is_add_submonoid.zero_mem, - add_mem' := λ x y, is_add_submonoid.add_mem, - }, - algebra_map_mem' := λ x, field.mem_closure (or.inl (set.mem_range.mpr ⟨x,rfl⟩)), -} + add_mem' := λ x y, is_add_submonoid.add_mem }, + algebra_map_mem' := λ x, field.mem_closure (or.inl (set.mem_range.mpr ⟨x,rfl⟩)) } lemma adjoin.algebra_map_mem (x : F) : algebra_map F E x ∈ adjoin F S := field.mem_closure (or.inl (set.mem_range_self x)) From 0528cb7b0d331b85e557aad266a63c710dbc97f0 Mon Sep 17 00:00:00 2001 From: Thomas Browning Date: Thu, 27 Aug 2020 23:41:01 -0700 Subject: [PATCH 17/32] refactor(field_theory/adjoin): remove adjoin.composition --- src/field_theory/adjoin.lean | 3 --- 1 file changed, 3 deletions(-) diff --git a/src/field_theory/adjoin.lean b/src/field_theory/adjoin.lean index 4797caf3063d5..4a09880ca7d30 100644 --- a/src/field_theory/adjoin.lean +++ b/src/field_theory/adjoin.lean @@ -127,9 +127,6 @@ begin (subset_adjoin _ _) }, end -lemma adjoin.composition : -(algebra_map F E) = (algebra_map (adjoin F S) E).comp (algebra_map F (adjoin F S)) := by ext;refl - variables (α : E) notation K`[`:std.prec.max_plus l:(foldr `, ` (h t, set.insert h t) ∅) `]` := adjoin K l From 8573f9241a4b02d89b21c05b3e4c5a0325316857 Mon Sep 17 00:00:00 2001 From: Thomas Browning Date: Fri, 28 Aug 2020 00:17:24 -0700 Subject: [PATCH 18/32] refactor(field_theory/adjoin): remove adjoin.set_mem --- src/field_theory/adjoin.lean | 11 ++++------- 1 file changed, 4 insertions(+), 7 deletions(-) diff --git a/src/field_theory/adjoin.lean b/src/field_theory/adjoin.lean index 4a09880ca7d30..07c07bd883769 100644 --- a/src/field_theory/adjoin.lean +++ b/src/field_theory/adjoin.lean @@ -58,14 +58,11 @@ end instance adjoin.field_coe : has_coe_t F (adjoin F S) := {coe := λ x, ⟨algebra_map F E x, adjoin.algebra_map_mem F S x⟩} -lemma adjoin.set_mem (x : S) : ↑x ∈ adjoin F S := -field.mem_closure (or.inr (subtype.mem x)) - lemma subset_adjoin : S ⊆ adjoin F S := -λ x hx, adjoin.set_mem F S ⟨x, hx⟩ +λ x hx, field.mem_closure (or.inr hx) instance adjoin.set_coe : has_coe_t S (adjoin F S) := -{coe := λ x, ⟨↑x, adjoin.set_mem F S x⟩} +{coe := λ x, ⟨x,subset_adjoin F S (subtype.mem x)⟩} lemma adjoin.mono (T : set E) (h : S ⊆ T) : (adjoin F S : set E) ⊆ adjoin F T := field.closure_mono (set.union_subset (set.subset_union_left _ _) (set.subset_union_of_subset_right h _)) @@ -78,7 +75,7 @@ lemma adjoin_contains_field_as_subfield (F : set E) {HF : is_subfield F} : F ⊆ lemma subset_adjoin_of_subset_right {T : set E} (H : T ⊆ S) : T ⊆ adjoin F S := begin intros x hx, - exact adjoin.set_mem F S ⟨x,H hx⟩, + exact subset_adjoin F S (H hx), end /-- If `K` is a field with `F ⊆ K` and `S ⊆ K` then `adjoin F S ⊆ K`. -/ @@ -142,7 +139,7 @@ end lemma mem_adjoin_simple_self : α ∈ F[α] := begin rw adjoin_singleton, - exact adjoin.set_mem F {α} (⟨α,set.mem_singleton α⟩ : ({α} : set E)), + exact subset_adjoin F {α} (set.mem_singleton α), end /-- generator of F(α) -/ From a67b30140c8e7ab36c860a1655bfcd0efb9c4179 Mon Sep 17 00:00:00 2001 From: Thomas Browning Date: Fri, 28 Aug 2020 13:28:41 -0700 Subject: [PATCH 19/32] refactor(field_theory/adjoin): change notation --- src/field_theory/adjoin.lean | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/src/field_theory/adjoin.lean b/src/field_theory/adjoin.lean index 07c07bd883769..ebc6b35b09f3d 100644 --- a/src/field_theory/adjoin.lean +++ b/src/field_theory/adjoin.lean @@ -126,28 +126,28 @@ end variables (α : E) -notation K`[`:std.prec.max_plus l:(foldr `, ` (h t, set.insert h t) ∅) `]` := adjoin K l +notation K`[(`:std.prec.max_plus l:(foldr `, ` (h t, set.insert h t) ∅) `)]` := adjoin K l --unfortunately this lemma is not definitionally true -lemma adjoin_singleton : F[α] = adjoin F {α} := +lemma adjoin_singleton : F[(α)] = adjoin F {α} := begin change adjoin F (insert α ∅) = adjoin F {α}, rw insert_emptyc_eq α, exact set.is_lawful_singleton, end -lemma mem_adjoin_simple_self : α ∈ F[α] := +lemma mem_adjoin_simple_self : α ∈ F[(α)] := begin rw adjoin_singleton, exact subset_adjoin F {α} (set.mem_singleton α), end /-- generator of F(α) -/ -def adjoin_simple.gen : F[α] := ⟨α, mem_adjoin_simple_self F α⟩ +def adjoin_simple.gen : F[(α)] := ⟨α, mem_adjoin_simple_self F α⟩ -lemma adjoin_simple.algebra_map_gen : algebra_map F[α] E (adjoin_simple.gen F α) = α := rfl +lemma adjoin_simple.algebra_map_gen : algebra_map F[(α)] E (adjoin_simple.gen F α) = α := rfl -lemma adjoin_simple_adjoin_simple (β : E) : F[α,β] = adjoin F {α,β} := +lemma adjoin_simple_adjoin_simple (β : E) : F[(α,β)] = adjoin F {α,β} := begin change adjoin F (insert α (insert β ∅)) = adjoin F _, simp only [insert_emptyc_eq], From a53f38ef32ac89aaaa89dbd7ec42baf76667027a Mon Sep 17 00:00:00 2001 From: Patrick Lutz Date: Fri, 28 Aug 2020 13:32:23 -0700 Subject: [PATCH 20/32] new proof of set_range_subset --- src/field_theory/adjoin.lean | 7 ++----- 1 file changed, 2 insertions(+), 5 deletions(-) diff --git a/src/field_theory/adjoin.lean b/src/field_theory/adjoin.lean index ebc6b35b09f3d..bcdba3edfb037 100644 --- a/src/field_theory/adjoin.lean +++ b/src/field_theory/adjoin.lean @@ -92,13 +92,10 @@ lemma adjoin_subset_iff {T : set E} : S ⊆ adjoin F T ↔ (adjoin F S : set E) ⟨λ h, adjoin_subset_subfield F S (adjoin.range_algebra_map_subset F T) h, λ h, set.subset.trans (subset_adjoin F S) h⟩ -lemma set_range_subset {T₁ T₂ : set E} [is_subfield T₁] (hyp : T₁ ⊆ T₂) : +lemma set_range_subset {T₁ T₂ : set E} [is_subring T₁] (hyp : T₁ ⊆ T₂) : set.range (algebra_map T₁ E) ⊆ T₂ := begin - intros x hx, - cases hx with f hf, - rw ←hf, - cases f with t ht, + rintros x ⟨⟨t, ht⟩, rfl⟩, exact hyp ht, end From 1cff5e2d99fc519539a85eb555542b4371654b59 Mon Sep 17 00:00:00 2001 From: Patrick Lutz Date: Fri, 28 Aug 2020 13:47:35 -0700 Subject: [PATCH 21/32] moved lemma to ring_theory/algebra and changed comments to match new notation --- src/field_theory/adjoin.lean | 13 +++---------- src/ring_theory/algebra.lean | 7 +++++++ 2 files changed, 10 insertions(+), 10 deletions(-) diff --git a/src/field_theory/adjoin.lean b/src/field_theory/adjoin.lean index bcdba3edfb037..3e9d33b3660f6 100644 --- a/src/field_theory/adjoin.lean +++ b/src/field_theory/adjoin.lean @@ -22,7 +22,7 @@ For example, algebra.adjoin K {x} might not include x⁻¹. ## Notation - - `F[α]` : Adjoin a single element α to F. + - `F[(α)]` : Adjoin a single element α to F. -/ namespace field @@ -92,13 +92,6 @@ lemma adjoin_subset_iff {T : set E} : S ⊆ adjoin F T ↔ (adjoin F S : set E) ⟨λ h, adjoin_subset_subfield F S (adjoin.range_algebra_map_subset F T) h, λ h, set.subset.trans (subset_adjoin F S) h⟩ -lemma set_range_subset {T₁ T₂ : set E} [is_subring T₁] (hyp : T₁ ⊆ T₂) : - set.range (algebra_map T₁ E) ⊆ T₂ := -begin - rintros x ⟨⟨t, ht⟩, rfl⟩, - exact hyp ht, -end - lemma subfield_subset_adjoin_self {F : set E} {HF : is_subfield F} {T : set E} {HT : T ⊆ F} : T ⊆ adjoin F S := λ x hx, adjoin.algebra_map_mem F S ⟨x,HT hx⟩ @@ -113,7 +106,7 @@ lemma adjoin_subset_adjoin_iff {F' : Type*} [field F'] [algebra F' E] lemma adjoin_adjoin_left (T : set E) : (adjoin (adjoin F S : set E) T : set E) = adjoin F (S ∪ T) := begin apply set.eq_of_subset_of_subset; rw adjoin_subset_adjoin_iff; split, - { exact set_range_subset (adjoin.mono _ _ _ (set.subset_union_left _ _)) }, + { exact algebra.set_range_subset (adjoin.mono _ _ _ (set.subset_union_left _ _)) }, { exact subset_adjoin_of_subset_right _ _ (set.subset_union_right _ _) }, { exact subset_adjoin_of_subset_left _ (adjoin.range_algebra_map_subset _ _) }, { exact set.union_subset @@ -139,7 +132,7 @@ begin exact subset_adjoin F {α} (set.mem_singleton α), end -/-- generator of F(α) -/ +/-- generator of F[(α)] -/ def adjoin_simple.gen : F[(α)] := ⟨α, mem_adjoin_simple_self F α⟩ lemma adjoin_simple.algebra_map_gen : algebra_map F[(α)] E (adjoin_simple.gen F α) = α := rfl diff --git a/src/ring_theory/algebra.lean b/src/ring_theory/algebra.lean index 2978bb4241681..3b1e2b9932f83 100644 --- a/src/ring_theory/algebra.lean +++ b/src/ring_theory/algebra.lean @@ -186,6 +186,13 @@ lemma subring_coe_algebra_map {R : Type*} [comm_ring R] (S : set R) [is_subring lemma subring_algebra_map_apply {R : Type*} [comm_ring R] (S : set R) [is_subring S] (x : S) : algebra_map S R x = x := rfl +lemma set_range_subset {R : Type*} [comm_ring R] {T₁ T₂ : set R} [is_subring T₁] (hyp : T₁ ⊆ T₂) : + set.range (algebra_map T₁ R) ⊆ T₂ := +begin + rintros x ⟨⟨t, ht⟩, rfl⟩, + exact hyp ht, +end + variables (R A) /-- The multiplication in an algebra is a bilinear map. -/ def lmul : A →ₗ A →ₗ A := From 132b72b2d39684272d4b85efe7804a5c4f083975 Mon Sep 17 00:00:00 2001 From: Thomas Browning Date: Fri, 28 Aug 2020 17:38:25 -0700 Subject: [PATCH 22/32] refactor(field_theory/adjoin): prove adjoin is field --- src/field_theory/adjoin.lean | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/field_theory/adjoin.lean b/src/field_theory/adjoin.lean index 3e9d33b3660f6..40bf96087de5e 100644 --- a/src/field_theory/adjoin.lean +++ b/src/field_theory/adjoin.lean @@ -69,6 +69,9 @@ field.closure_mono (set.union_subset (set.subset_union_left _ _) (set.subset_uni instance adjoin.is_subfield : is_subfield (adjoin F S : set E) := field.closure.is_subfield +--Lean has trouble figuring this out on its own +instance adjoin.is_field : field (adjoin F S) := @is_subfield.field E _ ((adjoin F S) : set E) _ + lemma adjoin_contains_field_as_subfield (F : set E) {HF : is_subfield F} : F ⊆ adjoin F S := λ x hx, adjoin.algebra_map_mem F S ⟨x, hx⟩ From 067b0f3f9a37f88ae8673790cc3b1420bb2b653d Mon Sep 17 00:00:00 2001 From: tb65536 Date: Sat, 29 Aug 2020 11:04:03 -0700 Subject: [PATCH 23/32] Update src/field_theory/adjoin.lean Co-authored-by: Bryan Gin-ge Chen --- src/field_theory/adjoin.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/field_theory/adjoin.lean b/src/field_theory/adjoin.lean index 40bf96087de5e..a87f2b783d52b 100644 --- a/src/field_theory/adjoin.lean +++ b/src/field_theory/adjoin.lean @@ -105,7 +105,7 @@ lemma adjoin_subset_adjoin_iff {F' : Type*} [field F'] [algebra F' E] ⟨λ h, ⟨trans (adjoin.range_algebra_map_subset _ _) h, trans (subset_adjoin _ _) h⟩, λ ⟨hF, hS⟩, field.closure_subset (set.union_subset hF hS)⟩ -/-- F[S][T] = F[S ∪ T] -/ +/-- `F[S][T] = F[S ∪ T]` -/ lemma adjoin_adjoin_left (T : set E) : (adjoin (adjoin F S : set E) T : set E) = adjoin F (S ∪ T) := begin apply set.eq_of_subset_of_subset; rw adjoin_subset_adjoin_iff; split, From 01a97470b053bfca2252ed46a24441f1bdf5028f Mon Sep 17 00:00:00 2001 From: tb65536 Date: Sat, 29 Aug 2020 11:14:05 -0700 Subject: [PATCH 24/32] Update src/field_theory/adjoin.lean Co-authored-by: Bryan Gin-ge Chen --- src/field_theory/adjoin.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/field_theory/adjoin.lean b/src/field_theory/adjoin.lean index a87f2b783d52b..260545a8cc526 100644 --- a/src/field_theory/adjoin.lean +++ b/src/field_theory/adjoin.lean @@ -12,7 +12,7 @@ import linear_algebra.finite_dimensional In this file we introduce the notion of adjoining elements to fields. This isn't quite the same as adjoining elements to rings. -For example, algebra.adjoin K {x} might not include x⁻¹. +For example, `algebra.adjoin K {x}` might not include `x⁻¹`. ## Main results From 2c321b436cc1a55398f4c3deeba9b57a6329a71e Mon Sep 17 00:00:00 2001 From: tb65536 Date: Sat, 29 Aug 2020 11:35:24 -0700 Subject: [PATCH 25/32] Update src/field_theory/adjoin.lean Co-authored-by: Bryan Gin-ge Chen --- src/field_theory/adjoin.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/field_theory/adjoin.lean b/src/field_theory/adjoin.lean index 260545a8cc526..cf682055886a4 100644 --- a/src/field_theory/adjoin.lean +++ b/src/field_theory/adjoin.lean @@ -135,7 +135,7 @@ begin exact subset_adjoin F {α} (set.mem_singleton α), end -/-- generator of F[(α)] -/ +/-- generator of `F[(α)]` -/ def adjoin_simple.gen : F[(α)] := ⟨α, mem_adjoin_simple_self F α⟩ lemma adjoin_simple.algebra_map_gen : algebra_map F[(α)] E (adjoin_simple.gen F α) = α := rfl From 03401ae53efc884ecf54d143d63026ed2dae1675 Mon Sep 17 00:00:00 2001 From: tb65536 Date: Sat, 29 Aug 2020 11:35:34 -0700 Subject: [PATCH 26/32] Update src/field_theory/adjoin.lean Co-authored-by: Bryan Gin-ge Chen --- src/field_theory/adjoin.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/field_theory/adjoin.lean b/src/field_theory/adjoin.lean index cf682055886a4..f24d0edee94c6 100644 --- a/src/field_theory/adjoin.lean +++ b/src/field_theory/adjoin.lean @@ -16,7 +16,7 @@ For example, `algebra.adjoin K {x}` might not include `x⁻¹`. ## Main results -(This is just a start, We've got more to add, including a proof of the Primitive Element Theorem) +(This is just a start; we've got more to add, including a proof of the Primitive Element Theorem.) - `adjoin_twice`: adjoining S and then T is the same as adjoining S ∪ T. From 920a5949d2d8055ec4eba8e700670fe0012ea84a Mon Sep 17 00:00:00 2001 From: tb65536 Date: Sat, 29 Aug 2020 11:35:44 -0700 Subject: [PATCH 27/32] Update src/field_theory/adjoin.lean Co-authored-by: Bryan Gin-ge Chen --- src/field_theory/adjoin.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/field_theory/adjoin.lean b/src/field_theory/adjoin.lean index f24d0edee94c6..e453ee891fa3a 100644 --- a/src/field_theory/adjoin.lean +++ b/src/field_theory/adjoin.lean @@ -90,7 +90,7 @@ begin exact ⟨HF, HS⟩, end -/-- `S ⊆ adjoin F T` if and only if `adjoin F S ⊆ adjoin F T` -/ +/-- `S ⊆ adjoin F T` if and only if `adjoin F S ⊆ adjoin F T`. -/ lemma adjoin_subset_iff {T : set E} : S ⊆ adjoin F T ↔ (adjoin F S : set E) ⊆ adjoin F T := ⟨λ h, adjoin_subset_subfield F S (adjoin.range_algebra_map_subset F T) h, λ h, set.subset.trans (subset_adjoin F S) h⟩ From 10558a0a0acdadc281d54bfe330a681c6acd2473 Mon Sep 17 00:00:00 2001 From: tb65536 Date: Sat, 29 Aug 2020 11:35:58 -0700 Subject: [PATCH 28/32] Update src/field_theory/adjoin.lean Co-authored-by: Bryan Gin-ge Chen --- src/field_theory/adjoin.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/field_theory/adjoin.lean b/src/field_theory/adjoin.lean index e453ee891fa3a..8f3b7dc83c869 100644 --- a/src/field_theory/adjoin.lean +++ b/src/field_theory/adjoin.lean @@ -22,7 +22,7 @@ For example, `algebra.adjoin K {x}` might not include `x⁻¹`. ## Notation - - `F[(α)]` : Adjoin a single element α to F. + - `F[(α)]`: adjoin a single element `α` to `F`. -/ namespace field From 1279b643d6677a4b78b8eea94189ddaf9bd80dc2 Mon Sep 17 00:00:00 2001 From: Thomas Browning Date: Sun, 30 Aug 2020 08:52:02 -0700 Subject: [PATCH 29/32] doc(field_theory/adjoin.lean): rename theorem in doc --- src/field_theory/adjoin.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/field_theory/adjoin.lean b/src/field_theory/adjoin.lean index 8f3b7dc83c869..56276d76db37b 100644 --- a/src/field_theory/adjoin.lean +++ b/src/field_theory/adjoin.lean @@ -18,7 +18,7 @@ For example, `algebra.adjoin K {x}` might not include `x⁻¹`. (This is just a start; we've got more to add, including a proof of the Primitive Element Theorem.) -- `adjoin_twice`: adjoining S and then T is the same as adjoining S ∪ T. +- `adjoin_adjoin_left`: adjoining S and then T is the same as adjoining S ∪ T. ## Notation From 794dad1f9b23e237134121ab160246c860aa3f0c Mon Sep 17 00:00:00 2001 From: Thomas Browning Date: Sun, 30 Aug 2020 12:09:31 -0700 Subject: [PATCH 30/32] refactor(field_theory/adjoin.lean): new brackets --- src/field_theory/adjoin.lean | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/src/field_theory/adjoin.lean b/src/field_theory/adjoin.lean index 56276d76db37b..2724b27b3c54b 100644 --- a/src/field_theory/adjoin.lean +++ b/src/field_theory/adjoin.lean @@ -119,28 +119,28 @@ end variables (α : E) -notation K`[(`:std.prec.max_plus l:(foldr `, ` (h t, set.insert h t) ∅) `)]` := adjoin K l +notation K`⟮`:std.prec.max_plus l:(foldr `, ` (h t, set.insert h t) ∅) `⟯` := adjoin K l --unfortunately this lemma is not definitionally true -lemma adjoin_singleton : F[(α)] = adjoin F {α} := +lemma adjoin_singleton : F⟮α⟯ = adjoin F {α} := begin change adjoin F (insert α ∅) = adjoin F {α}, rw insert_emptyc_eq α, exact set.is_lawful_singleton, end -lemma mem_adjoin_simple_self : α ∈ F[(α)] := +lemma mem_adjoin_simple_self : α ∈ F⟮α⟯ := begin rw adjoin_singleton, exact subset_adjoin F {α} (set.mem_singleton α), end /-- generator of `F[(α)]` -/ -def adjoin_simple.gen : F[(α)] := ⟨α, mem_adjoin_simple_self F α⟩ +def adjoin_simple.gen : F⟮α⟯ := ⟨α, mem_adjoin_simple_self F α⟩ -lemma adjoin_simple.algebra_map_gen : algebra_map F[(α)] E (adjoin_simple.gen F α) = α := rfl +lemma adjoin_simple.algebra_map_gen : algebra_map F⟮α⟯ E (adjoin_simple.gen F α) = α := rfl -lemma adjoin_simple_adjoin_simple (β : E) : F[(α,β)] = adjoin F {α,β} := +lemma adjoin_simple_adjoin_simple (β : E) : F⟮α,β⟯ = adjoin F {α,β} := begin change adjoin F (insert α (insert β ∅)) = adjoin F _, simp only [insert_emptyc_eq], From ac725eba26a03a4d63b202de9eb94a500d6adeae Mon Sep 17 00:00:00 2001 From: tb65536 Date: Sun, 30 Aug 2020 14:42:32 -0700 Subject: [PATCH 31/32] Update src/field_theory/adjoin.lean Co-authored-by: Floris van Doorn --- src/field_theory/adjoin.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/field_theory/adjoin.lean b/src/field_theory/adjoin.lean index 2724b27b3c54b..7d850c188aae3 100644 --- a/src/field_theory/adjoin.lean +++ b/src/field_theory/adjoin.lean @@ -22,7 +22,7 @@ For example, `algebra.adjoin K {x}` might not include `x⁻¹`. ## Notation - - `F[(α)]`: adjoin a single element `α` to `F`. + - `F⟮α⟯`: adjoin a single element `α` to `F`. -/ namespace field From e0601e3fa4fe56747ab554fde5a78d6f1030dc7e Mon Sep 17 00:00:00 2001 From: Patrick Lutz Date: Sun, 30 Aug 2020 15:00:28 -0700 Subject: [PATCH 32/32] updated documentation to reflect new notation --- src/field_theory/adjoin.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/field_theory/adjoin.lean b/src/field_theory/adjoin.lean index 7d850c188aae3..4dd8edb153e2d 100644 --- a/src/field_theory/adjoin.lean +++ b/src/field_theory/adjoin.lean @@ -135,7 +135,7 @@ begin exact subset_adjoin F {α} (set.mem_singleton α), end -/-- generator of `F[(α)]` -/ +/-- generator of `F⟮α⟯` -/ def adjoin_simple.gen : F⟮α⟯ := ⟨α, mem_adjoin_simple_self F α⟩ lemma adjoin_simple.algebra_map_gen : algebra_map F⟮α⟯ E (adjoin_simple.gen F α) = α := rfl