From a9232fb26708557c9ee2e72f65db4336592515b8 Mon Sep 17 00:00:00 2001 From: Johan Commelin Date: Tue, 8 Oct 2019 17:02:01 +0200 Subject: [PATCH 01/37] Valuation on power series --- src/examples/char_p.lean | 99 ++++++++++++++++++++++++++++++++++++++++ 1 file changed, 99 insertions(+) create mode 100644 src/examples/char_p.lean diff --git a/src/examples/char_p.lean b/src/examples/char_p.lean new file mode 100644 index 00000000..83ac2ac4 --- /dev/null +++ b/src/examples/char_p.lean @@ -0,0 +1,99 @@ +import ring_theory.power_series +import algebra.char_p + +import for_mathlib.nnreal + +import adic_space + +section + +open_locale classical + +noncomputable def nnreal_of_enat (b : nnreal) (n : enat) : nnreal := +if h : n.dom then (b^n.get h) else 0 + +@[simp] lemma nnreal_of_enat_top (b : nnreal) : + nnreal_of_enat b ⊤ = 0 := +begin + rw [nnreal_of_enat, dif_neg], exact not_false +end + +@[simp] lemma nnreal_of_enat_zero (b : nnreal) : + nnreal_of_enat b 0 = 1 := +begin + rw [nnreal_of_enat, dif_pos, enat.get_zero, pow_zero], + exact trivial, +end + +@[simp] lemma nnreal_of_enat_one (b : nnreal) : + nnreal_of_enat b 1 = b := +begin + rw [nnreal_of_enat, dif_pos, enat.get_one, pow_one], + exact trivial, +end + +@[simp] lemma nnreal_of_enat_add (b : nnreal) (m n : enat) : + nnreal_of_enat b (m + n) = nnreal_of_enat b m * nnreal_of_enat b n := +begin + delta nnreal_of_enat, + by_cases hm : m.dom, + { by_cases hn : n.dom, + { have hmn : (m + n).dom := ⟨hm, hn⟩, + rw [dif_pos hm, dif_pos hn, dif_pos, + subtype.coe_ext, nnreal.coe_mul, ← nnreal.coe_mul, ← pow_add, enat.get_add, add_comm], + exact hmn, }, + { rw [dif_pos hm, dif_neg hn, dif_neg, mul_zero], + contrapose! hn with H, exact H.2 } }, + { rw [dif_neg hm, dif_neg, zero_mul], + contrapose! hm with H, exact H.1 }, +end + +@[simp] lemma nnreal_of_enat_le (b : nnreal) (h₁ : b ≠ 0) (h₂ : b ≤ 1) (m n : enat) (h : m ≤ n) : + nnreal_of_enat b n ≤ nnreal_of_enat b m := +begin + delta nnreal_of_enat, + by_cases hn : n.dom, + { rw ← enat.coe_get hn at h, + have hm : m.dom := enat.dom_of_le_some h, + rw [← enat.coe_get hm, enat.coe_le_coe] at h, + rw [dif_pos hm, dif_pos hn], + rw [← linear_ordered_structure.inv_le_inv one_ne_zero h₁, inv_one'] at h₂, + have := pow_le_pow h₂ h, + -- We need lots of norm_cast lemmas + rwa [nnreal.coe_le, nnreal.coe_pow, nnreal.coe_pow, nnreal.coe_inv, ← pow_inv, ← pow_inv, + ← nnreal.coe_pow, ← nnreal.coe_pow, ← nnreal.coe_inv, ← nnreal.coe_inv, ← nnreal.coe_le, + linear_ordered_structure.inv_le_inv] at this, + all_goals { sorry } }, + { rw dif_neg hn, exact zero_le _ } +end + +end + +namespace power_series +variables {p : ℕ} [hp : p.prime] +variables {K : Type*} [discrete_field K] [char_p K p] +include hp + +open_locale classical + +noncomputable def valuation : valuation (power_series K) nnreal := +{ to_fun := λ φ, nnreal_of_enat (p⁻¹) φ.order, + map_zero' := by rw [order_zero, nnreal_of_enat_top], + map_one' := by rw [order_one, nnreal_of_enat_zero], + map_mul' := λ x y, by rw [order_mul, nnreal_of_enat_add], + map_add' := λ x y, + begin + have : _ ≤ _ := order_add_ge x y, + rw min_le_iff at this, + rw le_max_iff, + have inv_p_ne_zero : (p : nnreal)⁻¹ ≠ 0, + { assume H, rw [← inv_inj'', inv_inv'', inv_zero'] at H, + apply hp.ne_zero, exact_mod_cast H }, + cases this with h h; [left, right], + all_goals + { apply nnreal_of_enat_le _ inv_p_ne_zero _ _ _ h, + rw [← linear_ordered_structure.inv_le_inv one_ne_zero inv_p_ne_zero, inv_inv'', inv_one'], + exact_mod_cast le_of_lt hp.one_lt, }, + end } + +end power_series From 624afd758336c61e96c6d1e82e1e19a8d514b7d1 Mon Sep 17 00:00:00 2001 From: Johan Commelin Date: Wed, 9 Oct 2019 09:50:10 +0200 Subject: [PATCH 02/37] Remove sorries --- src/examples/char_p.lean | 4 +++- src/for_mathlib/group_with_zero.lean | 9 +++++++++ 2 files changed, 12 insertions(+), 1 deletion(-) diff --git a/src/examples/char_p.lean b/src/examples/char_p.lean index 83ac2ac4..4e8c0958 100644 --- a/src/examples/char_p.lean +++ b/src/examples/char_p.lean @@ -63,7 +63,9 @@ begin rwa [nnreal.coe_le, nnreal.coe_pow, nnreal.coe_pow, nnreal.coe_inv, ← pow_inv, ← pow_inv, ← nnreal.coe_pow, ← nnreal.coe_pow, ← nnreal.coe_inv, ← nnreal.coe_inv, ← nnreal.coe_le, linear_ordered_structure.inv_le_inv] at this, - all_goals { sorry } }, + all_goals { contrapose! h₁ }, + any_goals { exact subtype.val_injective h₁ }, + all_goals { apply group_with_zero.pow_eq_zero, assumption } }, { rw dif_neg hn, exact zero_le _ } end diff --git a/src/for_mathlib/group_with_zero.lean b/src/for_mathlib/group_with_zero.lean index 96beb2ed..f8cc4e66 100644 --- a/src/for_mathlib/group_with_zero.lean +++ b/src/for_mathlib/group_with_zero.lean @@ -159,6 +159,15 @@ begin symmetry, apply eq_inv_of_mul_left_eq_one', simp [_root_.mul_assoc, hx, hy], end +lemma pow_eq_zero (x : α) (n : ℕ) (h : x^n = 0) : x = 0 := +begin + induction n with n ih, { rw pow_zero at h, exfalso, exact one_ne_zero h }, + by_cases hx : x = 0, { exact hx }, + apply ih, + replace h := congr_arg ((*) x⁻¹) h, + rwa [pow_succ, mul_zero, inv_mul_cancel_assoc_right _ _ hx] at h, +end + /--Adjoining a zero element to the units of a group with zero is naturally equivalent to the group with zero.-/ noncomputable def with_zero_units_equiv : with_zero (units α) ≃ α := From 1fbe1257fe0cb7e0b5c538e67b16d817734b65a3 Mon Sep 17 00:00:00 2001 From: Johan Commelin Date: Wed, 9 Oct 2019 10:28:59 +0200 Subject: [PATCH 03/37] Valuation on Laurent series --- src/examples/char_p.lean | 86 ++++++++++++++++++++++++++++++++++++---- 1 file changed, 78 insertions(+), 8 deletions(-) diff --git a/src/examples/char_p.lean b/src/examples/char_p.lean index 4e8c0958..93ad003a 100644 --- a/src/examples/char_p.lean +++ b/src/examples/char_p.lean @@ -5,11 +5,12 @@ import for_mathlib.nnreal import adic_space -section - +noncomputable theory open_locale classical -noncomputable def nnreal_of_enat (b : nnreal) (n : enat) : nnreal := +section + +def nnreal_of_enat (b : nnreal) (n : enat) : nnreal := if h : n.dom then (b^n.get h) else 0 @[simp] lemma nnreal_of_enat_top (b : nnreal) : @@ -69,16 +70,54 @@ begin { rw dif_neg hn, exact zero_le _ } end +@[simp] lemma nnreal_of_enat_lt (b : nnreal) (h₁ : b ≠ 0) (h₂ : b < 1) (m n : enat) (h : m < n) : + nnreal_of_enat b n < nnreal_of_enat b m := +begin + delta nnreal_of_enat, + by_cases hn : n.dom, + { rw ← enat.coe_get hn at h, + have hm : m.dom := enat.dom_of_le_some (le_of_lt h), + rw [← enat.coe_get hm, enat.coe_lt_coe] at h, + rw [dif_pos hm, dif_pos hn], + rw [← linear_ordered_structure.inv_lt_inv one_ne_zero h₁, inv_one'] at h₂, + have := pow_lt_pow h₂ h, + -- We need lots of norm_cast lemmas + rwa [nnreal.coe_lt, nnreal.coe_pow, nnreal.coe_pow, nnreal.coe_inv, ← pow_inv, ← pow_inv, + ← nnreal.coe_pow, ← nnreal.coe_pow, ← nnreal.coe_inv, ← nnreal.coe_inv, ← nnreal.coe_lt, + linear_ordered_structure.inv_lt_inv] at this, + all_goals { contrapose! h₁ }, + any_goals { exact subtype.val_injective h₁ }, + all_goals { apply group_with_zero.pow_eq_zero, assumption } }, + { rw dif_neg hn, + have : n = ⊤ := roption.eq_none_iff'.mpr hn, subst this, + replace h := ne_of_lt h, + rw enat.ne_top_iff at h, rcases h with ⟨m, rfl⟩, + rw dif_pos, swap, {trivial}, + apply pow_pos, + exact lt_of_le_of_ne b.2 h₁.symm } +end + +open function + +@[simp] lemma nnreal_of_enat_inj (b : nnreal) (h₁ : b ≠ 0) (h₂ : b < 1) : + injective (nnreal_of_enat b) := +begin + intros m n h, + wlog H : m ≤ n, + rcases lt_or_eq_of_le H with H|rfl, + { have := nnreal_of_enat_lt b h₁ h₂ m n H, + exfalso, exact ne_of_lt this h.symm, }, + { refl }, +end + end namespace power_series -variables {p : ℕ} [hp : p.prime] -variables {K : Type*} [discrete_field K] [char_p K p] +variables (p : ℕ) [hp : p.prime] +variables (K : Type*) [discrete_field K] [char_p K p] include hp -open_locale classical - -noncomputable def valuation : valuation (power_series K) nnreal := +def valuation : valuation (power_series K) nnreal := { to_fun := λ φ, nnreal_of_enat (p⁻¹) φ.order, map_zero' := by rw [order_zero, nnreal_of_enat_top], map_one' := by rw [order_one, nnreal_of_enat_zero], @@ -99,3 +138,34 @@ noncomputable def valuation : valuation (power_series K) nnreal := end } end power_series + +/- The following definition is mathematically correct, +but probably not the version that we want to put into mathlib. +We make it for the sole purpose of constructing a perfectoid field.-/ +def laurent_series (K : Type*) [discrete_field K] := localization.fraction_ring (power_series K) + +namespace laurent_series +variables (K : Type*) [discrete_field K] + +instance : discrete_field (laurent_series K) := by delta laurent_series; apply_instance + +variables {p : ℕ} [hp : p.prime] [char_p K p] + +include hp + +def valuation : valuation (laurent_series K) nnreal := +valuation.localization (power_series.valuation p K) $ λ φ h, +begin + rw localization.fraction_ring.mem_non_zero_divisors_iff_ne_zero at h, + contrapose! h, + change nnreal_of_enat _ _ = 0 at h, + have inv_p_ne_zero : (p : nnreal)⁻¹ ≠ 0, + { assume H, rw [← inv_inj'', inv_inv'', inv_zero'] at H, + apply hp.ne_zero, exact_mod_cast H }, + rwa [← nnreal_of_enat_top, (nnreal_of_enat_inj _ inv_p_ne_zero _).eq_iff, + power_series.order_eq_top] at h, + rw [← linear_ordered_structure.inv_lt_inv one_ne_zero inv_p_ne_zero, inv_inv'', inv_one'], + exact_mod_cast hp.one_lt, +end + +end laurent_series From ce353977b5d58fd3a4554be9858ad9217cd7fe6d Mon Sep 17 00:00:00 2001 From: Johan Commelin Date: Wed, 9 Oct 2019 10:40:33 +0200 Subject: [PATCH 04/37] Almost have valuation on perfection of Laurent series --- src/examples/char_p.lean | 28 +++++++++++++++++++++++++++- 1 file changed, 27 insertions(+), 1 deletion(-) diff --git a/src/examples/char_p.lean b/src/examples/char_p.lean index 93ad003a..138fca12 100644 --- a/src/examples/char_p.lean +++ b/src/examples/char_p.lean @@ -4,6 +4,7 @@ import algebra.char_p import for_mathlib.nnreal import adic_space +import valuation.perfection noncomputable theory open_locale classical @@ -149,7 +150,7 @@ variables (K : Type*) [discrete_field K] instance : discrete_field (laurent_series K) := by delta laurent_series; apply_instance -variables {p : ℕ} [hp : p.prime] [char_p K p] +variables (p : ℕ) [hp : p.prime] [char_p K p] include hp @@ -168,4 +169,29 @@ begin exact_mod_cast hp.one_lt, end +instance : char_p (laurent_series K) p := +begin + constructor, + intro n, + -- We shouldn't prove this directly. + -- Rather: every nonzero algebra over a char_p is itself char_p + sorry +end + end laurent_series + +def laurent_series_perfection (K : Type*) [discrete_field K] (p : ℕ) := +perfect_closure (laurent_series K) p + +namespace laurent_series_perfection +variables (K : Type*) [discrete_field K] +variables (p : ℕ) [hp : p.prime] [char_p K p] +include hp + +instance : discrete_field (laurent_series_perfection K p) := +perfect_closure.discrete_field (laurent_series K) p + +def valuation : valuation (laurent_series_perfection K p) nnreal := +valuation.perfection (laurent_series.valuation K p) p + +end laurent_series_perfection From 2ec862fca135c4f0d784aa7d516c6d3794981a12 Mon Sep 17 00:00:00 2001 From: Johan Commelin Date: Wed, 9 Oct 2019 11:21:15 +0200 Subject: [PATCH 05/37] Valuation on perfection of Laurent series --- src/examples/char_p.lean | 16 +++++++++------- src/for_mathlib/char_p.lean | 33 +++++++++++++++++++++++++++++++++ 2 files changed, 42 insertions(+), 7 deletions(-) create mode 100644 src/for_mathlib/char_p.lean diff --git a/src/examples/char_p.lean b/src/examples/char_p.lean index 138fca12..ff5c758e 100644 --- a/src/examples/char_p.lean +++ b/src/examples/char_p.lean @@ -2,6 +2,7 @@ import ring_theory.power_series import algebra.char_p import for_mathlib.nnreal +import for_mathlib.char_p import adic_space import valuation.perfection @@ -150,6 +151,11 @@ variables (K : Type*) [discrete_field K] instance : discrete_field (laurent_series K) := by delta laurent_series; apply_instance +def algebra : algebra K (laurent_series K) := +algebra.of_ring_hom (localization.of ∘ power_series.C K) $ +@is_ring_hom.comp _ _ _ _ (power_series.C K) (ring_hom.is_ring_hom _) + _ _ localization.of localization.of.is_ring_hom + variables (p : ℕ) [hp : p.prime] [char_p K p] include hp @@ -169,14 +175,10 @@ begin exact_mod_cast hp.one_lt, end +local attribute [instance] algebra + instance : char_p (laurent_series K) p := -begin - constructor, - intro n, - -- We shouldn't prove this directly. - -- Rather: every nonzero algebra over a char_p is itself char_p - sorry -end +char_p_algebra K end laurent_series diff --git a/src/for_mathlib/char_p.lean b/src/for_mathlib/char_p.lean new file mode 100644 index 00000000..be947104 --- /dev/null +++ b/src/for_mathlib/char_p.lean @@ -0,0 +1,33 @@ +import algebra.char_p +import ring_theory.algebra +import ring_theory.ideal_operations + +lemma map_nat_cast {α : Type*} {β : Type*} [semiring α] [semiring β] + (f : α → β) [is_semiring_hom f] (n : ℕ) : + f n = n := +begin + induction n with n ih, { exact is_semiring_hom.map_zero f }, + rw [nat.cast_succ, nat.cast_succ, is_semiring_hom.map_add f, ih, is_semiring_hom.map_one f], +end + +open function +variables {K : Type*} {R : Type*} {p : ℕ} [discrete_field K] [nonzero_comm_ring R] [algebra K R] + +-- is_field_hom.injective is not general enough +lemma hom_injective (f : K → R) [is_ring_hom f] : injective f := +begin + apply (is_ring_hom.inj_iff_ker_eq_bot f).mpr, + apply classical.or_iff_not_imp_right.mp (ideal.eq_bot_or_top _), + rw ideal.eq_top_iff_one, + exact is_ring_hom.not_one_mem_ker f, +end + +variable (K) + +lemma char_p_algebra [char_p K p] : char_p R p := +{ cast_eq_zero_iff := λ n, + begin + have : injective (algebra_map R : K → R) := hom_injective _, + rw [← char_p.cast_eq_zero_iff K, ← this.eq_iff, algebra.map_zero, + map_nat_cast (algebra_map R : K → R)], + end } From 5a6da6c023c8b47403bb64ffd0a1b2c6f7e4723b Mon Sep 17 00:00:00 2001 From: Johan Commelin Date: Wed, 9 Oct 2019 12:50:35 +0200 Subject: [PATCH 06/37] Towards a perfectoid field --- src/examples/char_p.lean | 43 +++++++++++++++++++++++++++++++++++++++- 1 file changed, 42 insertions(+), 1 deletion(-) diff --git a/src/examples/char_p.lean b/src/examples/char_p.lean index ff5c758e..514735f3 100644 --- a/src/examples/char_p.lean +++ b/src/examples/char_p.lean @@ -4,8 +4,8 @@ import algebra.char_p import for_mathlib.nnreal import for_mathlib.char_p -import adic_space import valuation.perfection +import perfectoid_space noncomputable theory open_locale classical @@ -197,3 +197,44 @@ def valuation : valuation (laurent_series_perfection K p) nnreal := valuation.perfection (laurent_series.valuation K p) p end laurent_series_perfection + +namespace laurent_series_perfection +-- Now we take K in universe Type. For example `valued` requires this. +variables (K : Type) [discrete_field K] +variables (p : ℕ) [hp : p.prime] [char_p K p] +include hp + +instance : valued (laurent_series_perfection K p) := +{ Γ₀ := nnreal, v := valuation K p } + +end laurent_series_perfection + +section +open uniform_space +variables (K : Type) [discrete_field K] +variables (p : ℕ) [hp : p.prime] [char_p K p] + +include hp + +local attribute [instance] valued.subgroups_basis subgroups_basis.topology + ring_filter_basis.topological_ring valued.uniform_space + +/-- The completion of the perfection of the Laurent series over a field. -/ +def clsp := completion (laurent_series_perfection K p) + +end + +namespace clsp +variables (K : Type) [discrete_field K] +variables (p : ℕ) [hp : p.prime] [char_p K p] + +include hp + +local attribute [instance] valued.subgroups_basis subgroups_basis.topology + ring_filter_basis.topological_ring valued.uniform_space + +instance : discrete_field (clsp K p) := uniform_space.completion.discrete_field + +def valuation : valuation (clsp K p) nnreal := valued.extension_valuation + +end clsp From 5a98ff8a1269c8930c443d1c6e2172520087a713 Mon Sep 17 00:00:00 2001 From: Johan Commelin Date: Wed, 9 Oct 2019 16:44:21 +0200 Subject: [PATCH 07/37] More proof sketches --- src/Frobenius.lean | 23 ++++ src/examples/char_p.lean | 159 ++++++++++++++++++++------ src/for_mathlib/ideal_operations.lean | 5 +- src/for_mathlib/primes.lean | 28 ++++- src/valuation/perfection.lean | 31 ++++- 5 files changed, 205 insertions(+), 41 deletions(-) diff --git a/src/Frobenius.lean b/src/Frobenius.lean index 2342c6af..af502a55 100644 --- a/src/Frobenius.lean +++ b/src/Frobenius.lean @@ -1,5 +1,7 @@ import algebra.char_p import for_mathlib.primes +import for_mathlib.char_p +import for_mathlib.ideal_operations /-! The main purpose of this file is to introduce notation that @@ -12,3 +14,24 @@ noncomputable def Frobenius (α : Type*) [semiring α] : α → α := λ x, x^(r notation `Frob` R `∕` x := Frobenius (ideal.quotient (ideal.span ({x} : set R))) notation x `∣` y `in` R := (x : R) ∣ (y : R) + +section +open function + +variables (R : Type*) [comm_ring R] (p : nat.primes) +lemma Frob_mod_surjective_char_p (h : surjective (Frobenius R)) (hp : ring_char R = p) : + surjective (Frob R∕p) := +begin + rintro ⟨x⟩, + rcases h x with ⟨y, rfl⟩, + refine ⟨ideal.quotient.mk _ y, _⟩, + delta Frobenius, + rw ← ideal.quotient.mk_pow, + congr' 2, + haveI : char_p R p := by { rw ← hp, apply_instance }, + rw [show (p : R) = (p : ℕ), by rw coe_coe], + rw [char_p.cast_eq_zero, ideal.span_zero], + sorry +end + +end diff --git a/src/examples/char_p.lean b/src/examples/char_p.lean index 514735f3..d82de719 100644 --- a/src/examples/char_p.lean +++ b/src/examples/char_p.lean @@ -10,6 +10,8 @@ import perfectoid_space noncomputable theory open_locale classical +local postfix `ᵒ` : 66 := power_bounded_subring + section def nnreal_of_enat (b : nnreal) (n : enat) : nnreal := @@ -115,9 +117,8 @@ end end namespace power_series -variables (p : ℕ) [hp : p.prime] +variables (p : nat.primes) variables (K : Type*) [discrete_field K] [char_p K p] -include hp def valuation : valuation (power_series K) nnreal := { to_fun := λ φ, nnreal_of_enat (p⁻¹) φ.order, @@ -131,12 +132,14 @@ def valuation : valuation (power_series K) nnreal := rw le_max_iff, have inv_p_ne_zero : (p : nnreal)⁻¹ ≠ 0, { assume H, rw [← inv_inj'', inv_inv'', inv_zero'] at H, - apply hp.ne_zero, exact_mod_cast H }, + apply p.ne_zero, sorry + /- exact_mod_cast H -/ }, cases this with h h; [left, right], all_goals { apply nnreal_of_enat_le _ inv_p_ne_zero _ _ _ h, rw [← linear_ordered_structure.inv_le_inv one_ne_zero inv_p_ne_zero, inv_inv'', inv_one'], - exact_mod_cast le_of_lt hp.one_lt, }, + apply le_of_lt, sorry + /- exact_mod_cast p.one_lt, -/ }, end } end power_series @@ -147,7 +150,7 @@ We make it for the sole purpose of constructing a perfectoid field.-/ def laurent_series (K : Type*) [discrete_field K] := localization.fraction_ring (power_series K) namespace laurent_series -variables (K : Type*) [discrete_field K] +variables (p : nat.primes) (K : Type*) [discrete_field K] instance : discrete_field (laurent_series K) := by delta laurent_series; apply_instance @@ -156,9 +159,7 @@ algebra.of_ring_hom (localization.of ∘ power_series.C K) $ @is_ring_hom.comp _ _ _ _ (power_series.C K) (ring_hom.is_ring_hom _) _ _ localization.of localization.of.is_ring_hom -variables (p : ℕ) [hp : p.prime] [char_p K p] - -include hp +variables [char_p K p] def valuation : valuation (laurent_series K) nnreal := valuation.localization (power_series.valuation p K) $ λ φ h, @@ -168,73 +169,157 @@ begin change nnreal_of_enat _ _ = 0 at h, have inv_p_ne_zero : (p : nnreal)⁻¹ ≠ 0, { assume H, rw [← inv_inj'', inv_inv'', inv_zero'] at H, - apply hp.ne_zero, exact_mod_cast H }, + apply p.ne_zero, sorry, -- exact_mod_cast H + }, rwa [← nnreal_of_enat_top, (nnreal_of_enat_inj _ inv_p_ne_zero _).eq_iff, power_series.order_eq_top] at h, rw [← linear_ordered_structure.inv_lt_inv one_ne_zero inv_p_ne_zero, inv_inv'', inv_one'], - exact_mod_cast hp.one_lt, + sorry + -- exact_mod_cast p.one_lt, +end + +lemma non_trivial : ¬ (valuation p K).is_trivial := +begin + assume H, cases H (localization.of (power_series.X)) with h h; + erw valuation.localization_apply at h; change nnreal_of_enat _ _ = _ at h, + { apply p.ne_zero, + simp only [nnreal.inv_eq_zero, nnreal_of_enat_one, + nat.cast_eq_zero, power_series.order_X] at h, + sorry }, + { simp only [nnreal_of_enat_one, power_series.order_X] at h, + rw [← inv_inj'', inv_inv'', inv_one'] at h, + apply p.ne_one, sorry, -- exact_mod_cast h + } end local attribute [instance] algebra -instance : char_p (laurent_series K) p := -char_p_algebra K +instance : char_p (laurent_series K) (ring_char K) := +@char_p_algebra K _ _ _ _ _ (ring_char.char _) end laurent_series -def laurent_series_perfection (K : Type*) [discrete_field K] (p : ℕ) := -perfect_closure (laurent_series K) p +def laurent_series_perfection (K : Type*) [discrete_field K] := +perfect_closure (laurent_series K) (ring_char K) namespace laurent_series_perfection -variables (K : Type*) [discrete_field K] -variables (p : ℕ) [hp : p.prime] [char_p K p] -include hp +variables (p : nat.primes) (K : Type*) [discrete_field K] [char_p K p] +include p + +instance : discrete_field (laurent_series_perfection K) := +@perfect_closure.discrete_field (laurent_series K) _ _ (ring_char.prime p K) _ -instance : discrete_field (laurent_series_perfection K p) := -perfect_closure.discrete_field (laurent_series K) p +def valuation : valuation (laurent_series_perfection K) nnreal := +@valuation.perfection (laurent_series K) _ (laurent_series.valuation p K) +(ring_char K) (ring_char.prime p _) _ -def valuation : valuation (laurent_series_perfection K p) nnreal := -valuation.perfection (laurent_series.valuation K p) p +lemma non_discrete (ε : nnreal) (h : 0 < ε) : + ∃ x : laurent_series_perfection K, 1 < valuation p K x ∧ valuation p K x < 1 + ε := +@valuation.perfection.non_discrete _ _ _ (ring_char.prime p _) _ _ +(laurent_series.non_trivial p K) ε h + +lemma non_trivial : ¬ (valuation p K).is_trivial := +begin + rcases non_discrete p K 2 (by norm_num) with ⟨x, h₁, h₂⟩, + contrapose! h₁, cases h₁ x with h h; rw h, + exact zero_le _, +end end laurent_series_perfection namespace laurent_series_perfection -- Now we take K in universe Type. For example `valued` requires this. -variables (K : Type) [discrete_field K] -variables (p : ℕ) [hp : p.prime] [char_p K p] -include hp +variables (p : nat.primes) (K : Type) [discrete_field K] [char_p K p] +include p -instance : valued (laurent_series_perfection K p) := -{ Γ₀ := nnreal, v := valuation K p } +instance : valued (laurent_series_perfection K) := +{ Γ₀ := nnreal, v := valuation p K } end laurent_series_perfection -section -open uniform_space +namespace valuation +variables {R : Type*} [comm_ring R] +variables {Γ₀ : Type*} [linear_ordered_comm_group_with_zero Γ₀] + +local attribute [instance] classical.decidable_linear_order + +def le_one_subring (v : valuation R Γ₀) := {r : R // v r ≤ 1} + +instance le_one_subring.is_subring (v : valuation R Γ₀) : comm_ring v.le_one_subring := +@subtype.comm_ring R _ {r : R | v r ≤ 1} +{ zero_mem := show v 0 ≤ 1, by simp, + one_mem := show v 1 ≤ 1, by simp, + add_mem := λ r s (hr : v r ≤ 1) (hs : v s ≤ 1), show v (r+s) ≤ 1, + by calc v (r + s) ≤ max (v r) (v s) : v.map_add r s + ... ≤ 1 : max_le hr hs, + neg_mem := λ r (hr : v r ≤ 1), show v (-r) ≤ 1, by rwa [v.map_neg], + mul_mem := λ r s (hr : v r ≤ 1) (hs : v s ≤ 1), show v (r*s) ≤ 1, + begin + rw v.map_mul, + refine le_trans (actual_ordered_comm_monoid.mul_le_mul_right' hr) _, + rwa one_mul + end } + +end valuation + +section pfd_fld +open function +parameter (p : nat.primes) variables (K : Type) [discrete_field K] -variables (p : ℕ) [hp : p.prime] [char_p K p] -include hp +class perfectoid_field : Type := +[top : uniform_space K] +[top_fld : topological_division_ring K] +[complete : complete_space K] +[sep : separated K] +(v : valuation K nnreal) +(non_discrete : ∀ ε : nnreal, 0 < ε → ∃ x : K, 1 < v x ∧ v x < 1 + ε) +(Frobenius : surjective (Frob v.le_one_subring∕p)) + +end pfd_fld + +section +open uniform_space +variables (p : nat.primes) (K : Type) [discrete_field K] [char_p K p] +include p local attribute [instance] valued.subgroups_basis subgroups_basis.topology ring_filter_basis.topological_ring valued.uniform_space /-- The completion of the perfection of the Laurent series over a field. -/ -def clsp := completion (laurent_series_perfection K p) +def clsp := completion (laurent_series_perfection K) end namespace clsp -variables (K : Type) [discrete_field K] -variables (p : ℕ) [hp : p.prime] [char_p K p] - -include hp +open uniform_space +variables (p : nat.primes) (K : Type) [discrete_field K] [char_p K p] +include p local attribute [instance] valued.subgroups_basis subgroups_basis.topology ring_filter_basis.topological_ring valued.uniform_space -instance : discrete_field (clsp K p) := uniform_space.completion.discrete_field +instance : discrete_field (clsp p K) := completion.discrete_field +instance : uniform_space (clsp p K) := completion.uniform_space _ +instance : topological_division_ring (clsp p K) := completion.topological_division_ring +instance : complete_space (clsp p K) := completion.complete_space _ +instance : separated (clsp p K) := completion.separated _ + +def valuation : valuation (clsp p K) nnreal := valued.extension_valuation -def valuation : valuation (clsp K p) nnreal := valued.extension_valuation +instance : perfectoid_field p (clsp p K) := +{ v := valuation p K, + non_discrete := λ ε h, + begin + choose x hx using laurent_series_perfection.non_discrete p K ε h, + delta clsp, use x, + convert hx using 2; exact valued.extension_extends _ + end, + Frobenius := + begin + apply Frob_mod_surjective_char_p, + sorry, + sorry, + end } end clsp diff --git a/src/for_mathlib/ideal_operations.lean b/src/for_mathlib/ideal_operations.lean index d63a80a4..a96e8025 100644 --- a/src/for_mathlib/ideal_operations.lean +++ b/src/for_mathlib/ideal_operations.lean @@ -29,5 +29,8 @@ begin simp [h] }, end -lemma ideal.span_empty {R : Type*} [comm_ring R] : ideal.span (∅ : set R) = ⊥ := +@[simp] lemma ideal.span_empty {R : Type*} [comm_ring R] : ideal.span (∅ : set R) = ⊥ := ideal.span_eq_bot.mpr (λ x h, false.elim h) + +@[simp] lemma ideal.span_zero {R : Type*} [comm_ring R] : ideal.span ({0} : set R) = ⊥ := +ideal.span_eq_bot.mpr $ λ x, set.mem_singleton_iff.mp diff --git a/src/for_mathlib/primes.lean b/src/for_mathlib/primes.lean index daea8479..56e68824 100644 --- a/src/for_mathlib/primes.lean +++ b/src/for_mathlib/primes.lean @@ -1,7 +1,31 @@ import data.nat.prime import ring_theory.ideals -open nat +import for_mathlib.char_p + +namespace nat +namespace primes +variable (p : primes) instance : has_coe primes ℕ := ⟨subtype.val⟩ -instance monoid.prime_pow {α : Type*} [monoid α]: has_pow α primes := ⟨λ x p, x^p.val⟩ + +lemma ne_zero : (p : ℕ) ≠ 0 := p.2.ne_zero +lemma ne_one : (p : ℕ) ≠ 1 := p.2.ne_one +lemma one_lt : 1 < (p : ℕ) := p.2.one_lt + +end primes +end nat + +instance monoid.prime_pow {α : Type*} [monoid α]: has_pow α nat.primes := ⟨λ x p, x^p.val⟩ + +section +variables (p : nat.primes) (R : Type*) [semiring R] [char_p R p] +include p + +lemma ring_char.prime : nat.prime (ring_char R) := +by { rw ← ring_char.eq R ‹_›, exact p.2 } + +end + +instance ring_char.char (R : Type*) [semiring R] : char_p R (ring_char R) := +{ cast_eq_zero_iff := ring_char.spec R } diff --git a/src/valuation/perfection.lean b/src/valuation/perfection.lean index bc7617f7..46453aae 100644 --- a/src/valuation/perfection.lean +++ b/src/valuation/perfection.lean @@ -84,7 +84,9 @@ end end perfection section -variables (p : ℕ) [nat.prime p] [char_p R p] +variables (R) (p : ℕ) [hp : p.prime] [char_p R p] + +include hp def perfection : valuation (perfect_closure R p) nnreal := { to_fun := perfection.f v p, @@ -103,4 +105,31 @@ def perfection : valuation (perfect_closure R p) nnreal := end +namespace perfection +variables (K : Type*) [discrete_field K] (p : ℕ) [hp : p.prime] [char_p K p] +include hp + +lemma non_discrete (v : valuation K nnreal) (hv : ¬ v.is_trivial) (ε : nnreal) (h : 0 < ε) : + ∃ x : perfect_closure K p, 1 < v.perfection K p x ∧ v.perfection K p x < 1 + ε := +begin + obtain ⟨x, hx⟩ : ∃ x, 1 < v x, + { delta is_trivial at hv, push_neg at hv, rcases hv with ⟨x, h₁, h₂⟩, + by_cases hx : 1 < v x, { use [x,hx] }, + use x⁻¹, + rw [v.map_inv, ← linear_ordered_structure.inv_lt_inv _ one_ne_zero, inv_inv'', inv_one'], + { push_neg at hx, exact lt_of_le_of_ne hx h₂ }, + { contrapose! h₁, rwa nnreal.inv_eq_zero at h₁ } }, + suffices : ∃ n : ℕ, (v x)^(p^(-n : ℤ) : ℝ) < 1 + ε, + { rcases this with ⟨n, hn⟩, + refine ⟨quot.mk (perfect_closure.r K p) (n,x), _, hn⟩, + change 1 < (v x)^(p^(-n : ℤ) : ℝ), + rw nnreal.coe_lt, + apply real.one_lt_rpow hx, + apply fpow_pos_of_pos, + exact_mod_cast hp.pos, }, + sorry +end + +end perfection + end valuation From e5e53384bd6e7de008137a531f1477e54746b4ef Mon Sep 17 00:00:00 2001 From: Johan Commelin Date: Wed, 9 Oct 2019 16:58:46 +0200 Subject: [PATCH 08/37] Remove a bunch of trivial sorrys --- src/examples/char_p.lean | 29 ++++++++++++++++------------- 1 file changed, 16 insertions(+), 13 deletions(-) diff --git a/src/examples/char_p.lean b/src/examples/char_p.lean index d82de719..de4bec32 100644 --- a/src/examples/char_p.lean +++ b/src/examples/char_p.lean @@ -132,14 +132,15 @@ def valuation : valuation (power_series K) nnreal := rw le_max_iff, have inv_p_ne_zero : (p : nnreal)⁻¹ ≠ 0, { assume H, rw [← inv_inj'', inv_inv'', inv_zero'] at H, - apply p.ne_zero, sorry - /- exact_mod_cast H -/ }, + apply p.ne_zero, + rw [show (p : nnreal) = (p : ℕ), by rw coe_coe] at H, exact_mod_cast H, }, cases this with h h; [left, right], all_goals { apply nnreal_of_enat_le _ inv_p_ne_zero _ _ _ h, rw [← linear_ordered_structure.inv_le_inv one_ne_zero inv_p_ne_zero, inv_inv'', inv_one'], - apply le_of_lt, sorry - /- exact_mod_cast p.one_lt, -/ }, + apply le_of_lt, + rw [show (p : nnreal) = (p : ℕ), by rw coe_coe], + exact_mod_cast p.one_lt, }, end } end power_series @@ -169,13 +170,14 @@ begin change nnreal_of_enat _ _ = 0 at h, have inv_p_ne_zero : (p : nnreal)⁻¹ ≠ 0, { assume H, rw [← inv_inj'', inv_inv'', inv_zero'] at H, - apply p.ne_zero, sorry, -- exact_mod_cast H - }, + apply p.ne_zero, + rw [show (p : nnreal) = (p : ℕ), by rw coe_coe] at H, + exact_mod_cast H }, rwa [← nnreal_of_enat_top, (nnreal_of_enat_inj _ inv_p_ne_zero _).eq_iff, power_series.order_eq_top] at h, rw [← linear_ordered_structure.inv_lt_inv one_ne_zero inv_p_ne_zero, inv_inv'', inv_one'], - sorry - -- exact_mod_cast p.one_lt, + rw [show (p : nnreal) = (p : ℕ), by rw coe_coe], + exact_mod_cast p.one_lt, end lemma non_trivial : ¬ (valuation p K).is_trivial := @@ -183,13 +185,14 @@ begin assume H, cases H (localization.of (power_series.X)) with h h; erw valuation.localization_apply at h; change nnreal_of_enat _ _ = _ at h, { apply p.ne_zero, - simp only [nnreal.inv_eq_zero, nnreal_of_enat_one, - nat.cast_eq_zero, power_series.order_X] at h, - sorry }, + rw [show (p : nnreal) = (p : ℕ), by rw coe_coe] at h, + simpa only [nnreal.inv_eq_zero, nnreal_of_enat_one, + nat.cast_eq_zero, power_series.order_X] using h, }, { simp only [nnreal_of_enat_one, power_series.order_X] at h, rw [← inv_inj'', inv_inv'', inv_one'] at h, - apply p.ne_one, sorry, -- exact_mod_cast h - } + apply p.ne_one, + rw [show (p : nnreal) = (p : ℕ), by rw coe_coe] at h, + exact_mod_cast h } end local attribute [instance] algebra From 3565dbfdbc3e33497f441621fea91de34dbf7a78 Mon Sep 17 00:00:00 2001 From: Patrick Massot Date: Wed, 9 Oct 2019 21:44:31 +0200 Subject: [PATCH 09/37] Johan's limit lemma in valuation/perfection --- src/valuation/perfection.lean | 40 ++++++++++++++++++++++++++++++++++- 1 file changed, 39 insertions(+), 1 deletion(-) diff --git a/src/valuation/perfection.lean b/src/valuation/perfection.lean index 46453aae..a9156dcc 100644 --- a/src/valuation/perfection.lean +++ b/src/valuation/perfection.lean @@ -106,6 +106,31 @@ def perfection : valuation (perfect_closure R p) nnreal := end namespace perfection +open filter real + +lemma tendsto_pow_zero {x : ℝ} (hx : x ≠ 0) : tendsto (λ ε, x^ε) (nhds (0 : ℝ)) (nhds 1) := +begin + convert (continuous_rpow_of_ne_zero (λ y, hx) continuous_const continuous_id).continuous_at, + simp +end + +-- TODO: rename? +lemma johan {x ε : ℝ} (hx : 1 < x) (hε : 0 < ε) : ∃ r : ℝ, 0 < r ∧ x^r < 1 + ε := +begin + have lim := tendsto_pow_zero (by linarith : x ≠ 0), + rw metric.tendsto_nhds_nhds at lim, + simp only [dist_0_eq_abs, dist_eq, sub_zero] at lim, + rcases lim ε hε with ⟨r, rpos, H⟩, + use [r/2, by linarith], + have : abs (r/2) < r, by rw abs_of_nonneg ; linarith, + specialize H this, + have : 0 ≤ x ^ (r / 2) - 1, + { suffices : 1 ≤ x^(r/2), by linarith, + apply one_le_rpow ; linarith }, + rw abs_of_nonneg this at H, + linarith +end + variables (K : Type*) [discrete_field K] (p : ℕ) [hp : p.prime] [char_p K p] include hp @@ -127,7 +152,20 @@ begin apply real.one_lt_rpow hx, apply fpow_pos_of_pos, exact_mod_cast hp.pos, }, - sorry + rcases johan hx h with ⟨r, hr, H⟩, + -- TODO: the next block is copied from examples/padics, should we extract it? + obtain ⟨n, hn⟩ : ∃ n : ℕ, (p : ℝ)^-(n : ℤ) < r, + { have hp : (1:ℝ) < p := by exact_mod_cast nat.prime.one_lt ‹_›, + obtain ⟨n, hn⟩ : ∃ (n:ℕ), r⁻¹ < p^n := pow_unbounded_of_one_lt r⁻¹ hp, + use n, + have hp' : (0:ℝ) < p^n, + { rw ← fpow_of_nat, apply fpow_pos_of_pos, exact_mod_cast nat.prime.pos ‹_› }, + rw [inv_lt hr hp', inv_eq_one_div] at hn, + rwa [fpow_neg, fpow_of_nat], }, + use n, + transitivity (v x)^r, + exact rpow_lt_rpow_of_exponent_lt hx hn, + assumption end end perfection From bf38d1aee68a38d2c28fbdf67625f9417647d3cd Mon Sep 17 00:00:00 2001 From: Johan Commelin Date: Thu, 10 Oct 2019 09:24:14 +0200 Subject: [PATCH 10/37] Some fixes --- src/Frobenius.lean | 46 ++++++++++++++++++++++++++++++++----- src/examples/char_p.lean | 2 +- src/for_mathlib/char_p.lean | 2 +- src/for_mathlib/primes.lean | 1 + 4 files changed, 43 insertions(+), 8 deletions(-) diff --git a/src/Frobenius.lean b/src/Frobenius.lean index af502a55..b41ff6b3 100644 --- a/src/Frobenius.lean +++ b/src/Frobenius.lean @@ -18,8 +18,37 @@ notation x `∣` y `in` R := (x : R) ∣ (y : R) section open function -variables (R : Type*) [comm_ring R] (p : nat.primes) -lemma Frob_mod_surjective_char_p (h : surjective (Frobenius R)) (hp : ring_char R = p) : +variables (R : Type*) (A : Type*) [comm_ring R] [comm_ring A] [algebra R A] (p : nat.primes) + +lemma ring_char.eq_iff (n : ℕ) : + ring_char R = n ↔ char_p R n := +begin + split, + { rintro rfl, exact ring_char.char R }, + { intro h, exact (ring_char.eq R h).symm } +end + +def char_p.zmodp_algebra [hp : char_p R p] : algebra (zmodp p p.2) R := +algebra.of_ring_hom zmod.cast (@zmod.cast_is_ring_hom R _ ⟨p,_⟩ hp) + +instance zmod.char_p (n : ℕ+) : char_p (zmod n) n := +⟨λ k, zmod.eq_zero_iff_dvd_nat⟩ + +instance zmodp.char_p (p : ℕ) (hp : p.prime) : char_p (zmodp p hp) p := +zmod.char_p ⟨p, _⟩ + +lemma char_p_algebra [hp : char_p R p] (h : (0:A) ≠ 1) : char_p A p := +begin + letI := char_p.zmodp_algebra R, + letI : nonzero_comm_ring (algebra.comap (zmodp p p.2) R A) := + { zero_ne_one := h, .. ‹comm_ring A› }, + change char_p (algebra.comap (zmodp p p.2) R A) p, + convert char_p_algebra_over_field (zmodp p p.2), + { exact algebra.comap.algebra _ _ _ }, + { apply_instance } +end + +lemma Frob_mod_surjective_char_p [hp : char_p R p] (h : surjective (Frobenius R)) : surjective (Frob R∕p) := begin rintro ⟨x⟩, @@ -28,10 +57,15 @@ begin delta Frobenius, rw ← ideal.quotient.mk_pow, congr' 2, - haveI : char_p R p := by { rw ← hp, apply_instance }, - rw [show (p : R) = (p : ℕ), by rw coe_coe], - rw [char_p.cast_eq_zero, ideal.span_zero], - sorry + rw [char_p.eq R (ring_char.char R) hp, ring_char.eq_iff], + refine @char_p_algebra R _ _ _ + (algebra.of_ring_hom (ideal.quotient.mk _) (ideal.quotient.is_ring_hom_mk _)) _ hp _, + assume H, apply p.not_dvd_one, + rw [eq_comm, ← ideal.quotient.mk_one, ideal.quotient.eq_zero_iff_mem, + ideal.mem_span_singleton] at H, + rw [show (p : R) = (p : ℕ), by rw coe_coe] at H, + rwa [char_p.cast_eq_zero R, zero_dvd_iff, + ← nat.cast_one, char_p.cast_eq_zero_iff R p] at H, end end diff --git a/src/examples/char_p.lean b/src/examples/char_p.lean index de4bec32..5f19aa25 100644 --- a/src/examples/char_p.lean +++ b/src/examples/char_p.lean @@ -198,7 +198,7 @@ end local attribute [instance] algebra instance : char_p (laurent_series K) (ring_char K) := -@char_p_algebra K _ _ _ _ _ (ring_char.char _) +@char_p_algebra_over_field K _ _ _ _ _ (ring_char.char _) end laurent_series diff --git a/src/for_mathlib/char_p.lean b/src/for_mathlib/char_p.lean index be947104..dbf49eca 100644 --- a/src/for_mathlib/char_p.lean +++ b/src/for_mathlib/char_p.lean @@ -24,7 +24,7 @@ end variable (K) -lemma char_p_algebra [char_p K p] : char_p R p := +lemma char_p_algebra_over_field [char_p K p] : char_p R p := { cast_eq_zero_iff := λ n, begin have : injective (algebra_map R : K → R) := hom_injective _, diff --git a/src/for_mathlib/primes.lean b/src/for_mathlib/primes.lean index 56e68824..a533416c 100644 --- a/src/for_mathlib/primes.lean +++ b/src/for_mathlib/primes.lean @@ -12,6 +12,7 @@ instance : has_coe primes ℕ := ⟨subtype.val⟩ lemma ne_zero : (p : ℕ) ≠ 0 := p.2.ne_zero lemma ne_one : (p : ℕ) ≠ 1 := p.2.ne_one lemma one_lt : 1 < (p : ℕ) := p.2.one_lt +lemma not_dvd_one : ¬ (p : ℕ) ∣ 1 := p.2.not_dvd_one end primes end nat From 858046018eee2a0917ecbad2828e4e2f6c033073 Mon Sep 17 00:00:00 2001 From: Johan Commelin Date: Thu, 10 Oct 2019 15:28:37 +0200 Subject: [PATCH 11/37] Help! It's a big mess --- src/Frobenius.lean | 21 +-- src/examples/char_p.lean | 135 +++++++++++++----- src/examples/padics.lean | 2 +- .../linear_ordered_comm_group.lean | 78 +++++++--- src/valuation/basic.lean | 2 +- 5 files changed, 163 insertions(+), 75 deletions(-) diff --git a/src/Frobenius.lean b/src/Frobenius.lean index b41ff6b3..cb78473a 100644 --- a/src/Frobenius.lean +++ b/src/Frobenius.lean @@ -8,10 +8,10 @@ The main purpose of this file is to introduce notation that is not available in mathlib, and that we don't want to set up in the main file. -/ -/--The Frobenius endomorphism of a semiring-/ -noncomputable def Frobenius (α : Type*) [semiring α] : α → α := λ x, x^(ring_char α) +-- /--The Frobenius endomorphism of a semiring-/ +-- noncomputable def Frobenius (α : Type*) [semiring α] : α → α := λ x, x^(ring_char α) -notation `Frob` R `∕` x := Frobenius (ideal.quotient (ideal.span ({x} : set R))) +notation `Frob` R `∕` p := frobenius (ideal.quotient (ideal.span ({p} : set R))) p notation x `∣` y `in` R := (x : R) ∣ (y : R) @@ -48,24 +48,15 @@ begin { apply_instance } end -lemma Frob_mod_surjective_char_p [hp : char_p R p] (h : surjective (Frobenius R)) : +lemma frobenius_surjective_of_char_p [hp : char_p R p] (h : surjective (frobenius R p)) : surjective (Frob R∕p) := begin rintro ⟨x⟩, rcases h x with ⟨y, rfl⟩, refine ⟨ideal.quotient.mk _ y, _⟩, - delta Frobenius, + delta frobenius, rw ← ideal.quotient.mk_pow, - congr' 2, - rw [char_p.eq R (ring_char.char R) hp, ring_char.eq_iff], - refine @char_p_algebra R _ _ _ - (algebra.of_ring_hom (ideal.quotient.mk _) (ideal.quotient.is_ring_hom_mk _)) _ hp _, - assume H, apply p.not_dvd_one, - rw [eq_comm, ← ideal.quotient.mk_one, ideal.quotient.eq_zero_iff_mem, - ideal.mem_span_singleton] at H, - rw [show (p : R) = (p : ℕ), by rw coe_coe] at H, - rwa [char_p.cast_eq_zero R, zero_dvd_iff, - ← nat.cast_one, char_p.cast_eq_zero_iff R p] at H, + refl, end end diff --git a/src/examples/char_p.lean b/src/examples/char_p.lean index 5f19aa25..c56c8301 100644 --- a/src/examples/char_p.lean +++ b/src/examples/char_p.lean @@ -9,6 +9,7 @@ import perfectoid_space noncomputable theory open_locale classical +open function local postfix `ᵒ` : 66 := power_bounded_subring @@ -101,8 +102,6 @@ begin exact lt_of_le_of_ne b.2 h₁.symm } end -open function - @[simp] lemma nnreal_of_enat_inj (b : nnreal) (h₁ : b ≠ 0) (h₂ : b < 1) : injective (nnreal_of_enat b) := begin @@ -197,8 +196,8 @@ end local attribute [instance] algebra -instance : char_p (laurent_series K) (ring_char K) := -@char_p_algebra_over_field K _ _ _ _ _ (ring_char.char _) +instance [char_p K p] : char_p (laurent_series K) p := +char_p_algebra_over_field K end laurent_series @@ -206,20 +205,22 @@ def laurent_series_perfection (K : Type*) [discrete_field K] := perfect_closure (laurent_series K) (ring_char K) namespace laurent_series_perfection -variables (p : nat.primes) (K : Type*) [discrete_field K] [char_p K p] -include p +variables (p : nat.primes) (K : Type*) [discrete_field K] [hp : char_p K p] +include hp instance : discrete_field (laurent_series_perfection K) := -@perfect_closure.discrete_field (laurent_series K) _ _ (ring_char.prime p K) _ +@perfect_closure.discrete_field (laurent_series K) _ _ (ring_char.prime p K) $ +by { rw ← ring_char.eq K hp, apply_instance } def valuation : valuation (laurent_series_perfection K) nnreal := @valuation.perfection (laurent_series K) _ (laurent_series.valuation p K) -(ring_char K) (ring_char.prime p _) _ +(ring_char K) (ring_char.prime p _) $ +by { rw ← ring_char.eq K hp, apply_instance } lemma non_discrete (ε : nnreal) (h : 0 < ε) : ∃ x : laurent_series_perfection K, 1 < valuation p K x ∧ valuation p K x < 1 + ε := -@valuation.perfection.non_discrete _ _ _ (ring_char.prime p _) _ _ -(laurent_series.non_trivial p K) ε h +@valuation.perfection.non_discrete _ _ _ (ring_char.prime p _) +(by { rw ← ring_char.eq K hp, apply_instance }) _ (laurent_series.non_trivial p K) ε h lemma non_trivial : ¬ (valuation p K).is_trivial := begin @@ -228,6 +229,20 @@ begin exact zero_le _, end +lemma frobenius_surjective : surjective (frobenius (laurent_series_perfection K) p) := +begin + rw ring_char.eq K hp, + let F := (perfect_closure.frobenius_equiv (laurent_series K) _), + { exact F.surjective }, + { exact ring_char.prime p K }, + { rw ← ring_char.eq K hp, apply_instance } +end + +def algebra : algebra (laurent_series K) (laurent_series_perfection K) := +algebra.of_ring_hom (perfect_closure.of _ _) $ +@perfect_closure.is_ring_hom _ _ _ (ring_char.prime _ _) $ +by { rw ← ring_char.eq K hp, apply_instance } + end laurent_series_perfection namespace laurent_series_perfection @@ -246,10 +261,10 @@ variables {Γ₀ : Type*} [linear_ordered_comm_group_with_zero Γ₀] local attribute [instance] classical.decidable_linear_order -def le_one_subring (v : valuation R Γ₀) := {r : R // v r ≤ 1} +def le_one_subring (v : valuation R Γ₀) := {r : R | v r ≤ 1} -instance le_one_subring.is_subring (v : valuation R Γ₀) : comm_ring v.le_one_subring := -@subtype.comm_ring R _ {r : R | v r ≤ 1} +instance le_one_subring.is_subring (v : valuation R Γ₀) : is_subring v.le_one_subring := +-- @subtype.comm_ring R _ {r : R | v r ≤ 1} { zero_mem := show v 0 ≤ 1, by simp, one_mem := show v 1 ≤ 1, by simp, add_mem := λ r s (hr : v r ≤ 1) (hs : v s ≤ 1), show v (r+s) ≤ 1, @@ -263,21 +278,24 @@ instance le_one_subring.is_subring (v : valuation R Γ₀) : comm_ring v.le_one_ rwa one_mul end } +instance coe_nat_le_one_subring (v : valuation R Γ₀) : + has_coe ℕ v.le_one_subring := by apply_instance + end valuation section pfd_fld -open function parameter (p : nat.primes) -variables (K : Type) [discrete_field K] - -class perfectoid_field : Type := -[top : uniform_space K] -[top_fld : topological_division_ring K] -[complete : complete_space K] -[sep : separated K] -(v : valuation K nnreal) -(non_discrete : ∀ ε : nnreal, 0 < ε → ∃ x : K, 1 < v x ∧ v x < 1 + ε) -(Frobenius : surjective (Frob v.le_one_subring∕p)) +variables (K : Type) + +-- class perfectoid_field : Type 1 := +-- [fld : discrete_field K] +-- [top : uniform_space K] +-- [top_fld : topological_division_ring K] +-- [complete : complete_space K] +-- [sep : separated K] +-- (v : valuation K nnreal) +-- (non_discrete : ∀ ε : nnreal, 0 < ε → ∃ x : K, 1 < v x ∧ v x < 1 + ε) +-- (Frobenius : surjective (Frob v.le_one_subring ∕p)) end pfd_fld @@ -310,19 +328,60 @@ instance : separated (clsp p K) := completion.separated _ def valuation : valuation (clsp p K) nnreal := valued.extension_valuation -instance : perfectoid_field p (clsp p K) := -{ v := valuation p K, - non_discrete := λ ε h, - begin - choose x hx using laurent_series_perfection.non_discrete p K ε h, - delta clsp, use x, - convert hx using 2; exact valued.extension_extends _ - end, - Frobenius := - begin - apply Frob_mod_surjective_char_p, - sorry, - sorry, - end } +lemma frobenius_surjective : surjective (frobenius (clsp p K) p) := +begin + sorry +end + +instance laurent_series_valued : valued (laurent_series K) := +{ Γ₀ := nnreal, v := laurent_series.valuation p K } + +protected def algebra : algebra (laurent_series_perfection K) (clsp p K) := +algebra.of_ring_hom + (coe : (laurent_series_perfection K) → completion (laurent_series_perfection K)) $ +@completion.is_ring_hom_coe (laurent_series_perfection K) _ _ _ $ +@valued.uniform_add_group (laurent_series_perfection K) _ $ laurent_series_perfection.valued p K + +-- def rod_algebra : algebra (power_series K) (clsp p K) := +-- @algebra.comap.algebra _ _ _ _ _ _ _ $ +-- @algebra.comap.algebra (laurent_series K) (laurent_series_perfection K) (clsp p K) _ _ _ +-- (laurent_series_perfection.algebra p K) (clsp.algebra p K) + +-- def rod : Huber_ring.ring_of_definition (laurent_series K) (clsp p K) := +-- { +-- .. rod_algebra p K } + +-- def Huber_ring : Huber_ring (clsp p K) := +-- { pod := +-- begin +-- end } + +-- instance : perfectoid_field p (clsp p K) := +-- { v := valuation p K, +-- non_discrete := λ ε h, +-- begin +-- choose x hx using laurent_series_perfection.non_discrete p K ε h, +-- delta clsp, use x, +-- convert hx using 2; exact valued.extension_extends _ +-- end, +-- Frobenius := +-- begin +-- apply @surjective.of_comp _ _ _ _ (ideal.quotient.mk _) _, +-- conv {congr, simp only [frobenius, comp], funext, rw [← ideal.quotient.mk_pow]}, +-- apply surjective_comp, +-- { rintro ⟨x⟩, exact ⟨x, rfl⟩ }, +-- intro x, +-- choose y hy using frobenius_surjective p K x.val, +-- have hvy : valuation p K y ≤ 1, +-- { have aux := congr_arg (valuation p K) hy, +-- replace hy := x.property, +-- rw [← aux, frobenius, valuation.map_pow] at hy, clear aux, +-- apply linear_ordered_structure.le_one_of_pow_le_one _ _ hy, +-- exact_mod_cast p.ne_zero, }, +-- refine ⟨⟨y, hvy⟩, _⟩, +-- { rw [subtype.ext], convert hy, +-- convert @is_semiring_hom.map_pow _ _ _ _ subtype.val _ ⟨y,_⟩ p, +-- } +-- end } end clsp diff --git a/src/examples/padics.lean b/src/examples/padics.lean index 9dc018d4..03d0a9d6 100644 --- a/src/examples/padics.lean +++ b/src/examples/padics.lean @@ -221,7 +221,7 @@ begin suffices : u^(n+1) = 1 ↔ u = 1, { rwa [units.ext_iff, units.ext_iff, units.coe_pow] at this, }, split; intro h, - { exact linear_ordered_structure.eq_one_of_pow_eq_one h }, + { exact linear_ordered_structure.eq_one_of_pow_eq_one (nat.succ_ne_zero _) h }, { rw [h, one_pow], } }, by_cases hn' : 0 ≤ n, { lift n to ℕ using hn', rw [fpow_of_nat], norm_cast at hn, solve_by_elim }, diff --git a/src/for_mathlib/linear_ordered_comm_group.lean b/src/for_mathlib/linear_ordered_comm_group.lean index 5e8226f0..7e919d22 100644 --- a/src/for_mathlib/linear_ordered_comm_group.lean +++ b/src/for_mathlib/linear_ordered_comm_group.lean @@ -33,24 +33,9 @@ lemma mul_le_mul_right (H : x ≤ y) : ∀ z : α, x * z ≤ y * z := end linear_ordered_structure namespace linear_ordered_structure -variables {α : Type u} [linear_ordered_comm_group α] {x y z : α} -variables {β : Type v} [linear_ordered_comm_group β] - -class linear_ordered_comm_group.is_hom (f : α → β) extends is_group_hom f : Prop := -(ord : ∀ {a b : α}, a ≤ b → f a ≤ f b) - --- this is Kenny's; I think we should have iff -structure linear_ordered_comm_group.equiv extends equiv α β := -(is_hom : linear_ordered_comm_group.is_hom to_fun) - -lemma div_le_div (a b c d : α) : a * b⁻¹ ≤ c * d⁻¹ ↔ a * d ≤ c * b := -begin - split ; intro h, - have := mul_le_mul_right (mul_le_mul_right h b) d, - rwa [inv_mul_cancel_right, mul_assoc _ _ b, mul_comm _ b, ← mul_assoc, inv_mul_cancel_right] at this, - have := mul_le_mul_right (mul_le_mul_right h d⁻¹) b⁻¹, - rwa [mul_inv_cancel_right, _root_.mul_assoc, _root_.mul_comm d⁻¹ b⁻¹, ← mul_assoc, mul_inv_cancel_right] at this, -end +section monoid +variables {α : Type u} [linear_ordered_comm_monoid α] {x y z : α} +variables {β : Type v} [linear_ordered_comm_monoid β] lemma one_le_mul_of_one_le_of_one_le (Hx : 1 ≤ x) (Hy : 1 ≤ y) : 1 ≤ x * y := have h1 : x * 1 ≤ x * y, from mul_le_mul_left Hy x, @@ -77,12 +62,14 @@ begin end /-- Wedhorn Remark 1.6 (3) -/ -lemma eq_one_of_pow_eq_one {n : ℕ} (H : x ^ (n+1) = 1) : x = 1 := +lemma eq_one_of_pow_eq_one {n : ℕ} (hn : n ≠ 0) (H : x ^ n = 1) : x = 1 := begin + rcases nat.exists_eq_succ_of_ne_zero hn with ⟨n, rfl⟩, clear hn, induction n with n ih, { simpa using H }, { cases le_total x 1, - all_goals { have h1 := mul_le_mul_right h (x ^ (n+1)), + all_goals + { have h1 := mul_le_mul_right h (x ^ (n+1)), rw pow_succ at H, rw [H, one_mul] at h1 }, { have h2 := pow_le_one_of_le_one h, @@ -91,6 +78,37 @@ begin exact ih (le_antisymm h1 h2) } } end +open_locale classical + +lemma le_one_of_pow_le_one {a : α} (n : ℕ) (hn : n ≠ 0) (h : a^n ≤ 1) : a ≤ 1 := +begin + rcases lt_or_eq_of_le h with H|H, + { apply le_of_lt, contrapose! H, exact one_le_pow_of_one_le H, }, + { apply le_of_eq, exact eq_one_of_pow_eq_one hn H } +end + +end monoid + +section group +variables {α : Type u} [linear_ordered_comm_group α] {x y z : α} +variables {β : Type v} [linear_ordered_comm_group β] + +class linear_ordered_comm_group.is_hom (f : α → β) extends is_group_hom f : Prop := +(ord : ∀ {a b : α}, a ≤ b → f a ≤ f b) + +-- this is Kenny's; I think we should have iff +structure linear_ordered_comm_group.equiv extends equiv α β := +(is_hom : linear_ordered_comm_group.is_hom to_fun) + +lemma div_le_div (a b c d : α) : a * b⁻¹ ≤ c * d⁻¹ ↔ a * d ≤ c * b := +begin + split ; intro h, + have := mul_le_mul_right (mul_le_mul_right h b) d, + rwa [inv_mul_cancel_right, mul_assoc _ _ b, mul_comm _ b, ← mul_assoc, inv_mul_cancel_right] at this, + have := mul_le_mul_right (mul_le_mul_right h d⁻¹) b⁻¹, + rwa [mul_inv_cancel_right, _root_.mul_assoc, _root_.mul_comm d⁻¹ b⁻¹, ← mul_assoc, mul_inv_cancel_right] at this, +end + lemma inv_le_one_of_one_le (H : 1 ≤ x) : x⁻¹ ≤ 1 := by simpa using mul_le_mul_left H (x⁻¹) @@ -152,6 +170,7 @@ theorem ker.is_convex (f : α → β) (hf : linear_ordered_comm_group.is_hom f) def height (α : Type) [linear_ordered_comm_group α] : cardinal := cardinal.mk {S : set α // is_proper_convex S} +end group end linear_ordered_structure namespace with_zero @@ -391,6 +410,25 @@ end lemma square_gt_one {a : α} (h : 1 < a) : 1 < a*a := mul_gt_one' h h + +lemma pow_le_one {a : α} (h : a ≤ 1) (n : ℕ) : a^n ≤ 1 := +begin + induction n with n ih, {rwa pow_zero}, + rw pow_succ, + transitivity a, + { simpa only [mul_one] using mul_le_mul_left' ih }, + { exact h } +end + +lemma one_le_pow {a : α} (h : 1 ≤ a) (n : ℕ) : 1 ≤ a^n := +begin + induction n with n ih, {rwa pow_zero}, + rw pow_succ, + transitivity a, + { exact h }, + { simpa only [mul_one] using mul_le_mul_left' ih } +end + end actual_ordered_comm_monoid variables {Γ₀ : Type*} [linear_ordered_comm_group Γ₀] diff --git a/src/valuation/basic.lean b/src/valuation/basic.lean index 6a405b29..030a71d4 100644 --- a/src/valuation/basic.lean +++ b/src/valuation/basic.lean @@ -134,7 +134,7 @@ eq_inv_of_mul_right_eq_one' _ _ $ by rw [← v.map_mul, units.mul_inv, v.map_one begin show (units.map (v : R →* Γ₀) (-1 : units R) : Γ₀) = (1 : units Γ₀), rw ← units.ext_iff, - apply linear_ordered_structure.eq_one_of_pow_eq_one (_ : _ ^ 2 = _), + apply linear_ordered_structure.eq_one_of_pow_eq_one (nat.succ_ne_zero _) (_ : _ ^ 2 = _), rw [pow_two, ← monoid_hom.map_mul, units.ext_iff], show v ((-1) * (-1)) = 1, rw [neg_one_mul, neg_neg, v.map_one] From fcc13150a755cc6e6f4fea81ca255a356ae8fae8 Mon Sep 17 00:00:00 2001 From: Johan Commelin Date: Thu, 10 Oct 2019 20:02:51 +0200 Subject: [PATCH 12/37] gpow for group with zero --- src/for_mathlib/group_with_zero.lean | 130 +++++++++++++++++++++++++++ 1 file changed, 130 insertions(+) diff --git a/src/for_mathlib/group_with_zero.lean b/src/for_mathlib/group_with_zero.lean index f8cc4e66..c0cb1282 100644 --- a/src/for_mathlib/group_with_zero.lean +++ b/src/for_mathlib/group_with_zero.lean @@ -133,6 +133,10 @@ begin exact unit_ne_zero ((mk₀ a h.1) * (mk₀ b h.2)) end +instance : no_zero_divisors α := +{ eq_zero_or_eq_zero_of_mul_eq_zero := mul_eq_zero, + .. (‹_› : group_with_zero α) } + @[simp] lemma mul_eq_zero_iff {a b : α} : a * b = 0 ↔ a = 0 ∨ b = 0 := ⟨mul_eq_zero a b, by rintro (H|H); simp [H]⟩ @@ -183,6 +187,132 @@ begin simp [with_zero.coe_inj, units.ext_iff, *] } } end +theorem inv_comm_of_comm {a b : α} (H : a * b = b * a) : a⁻¹ * b = b * a⁻¹ := +begin + have : a⁻¹ * (b * a) * a⁻¹ = a⁻¹ * (a * b) * a⁻¹ := + congr_arg (λ x:α, a⁻¹ * x * a⁻¹) H.symm, + by_cases h : a = 0, { rw [h, inv_zero', zero_mul, mul_zero] }, + rwa [inv_mul_cancel_assoc_right _ _ h, mul_assoc, mul_inv_cancel_assoc_left _ _ h] at this, +end + +section nat_pow + +@[simp] theorem inv_pow (a : α) (n : ℕ) : (a⁻¹)^n = (a^n)⁻¹ := +by induction n with n ih; [exact inv_one'.symm, + rw [pow_succ', pow_succ, ih, mul_inv_rev]] + +-- This should be done for [no_zero_divisors] +lemma eq_zero_of_pow_eq_zero {a : α} {n : ℕ} (h : a^n = 0) : a = 0 := +begin + induction n with n ih, + { exfalso, rw pow_zero at h, exact one_ne_zero h }, + rw [pow_succ, mul_eq_zero_iff] at h, + cases h; solve_by_elim +end + +-- This should be done for [no_zero_divisors] +lemma pow_ne_zero {a : α} {n : ℕ} (h : a ≠ 0) : a^n ≠ 0 := +assume H, h $ eq_zero_of_pow_eq_zero H + +theorem pow_sub (a : α) {m n : ℕ} (ha : a ≠ 0) (h : n ≤ m) : a^(m - n) = a^m * (a^n)⁻¹ := +have h1 : m - n + n = m, from nat.sub_add_cancel h, +have h2 : a^(m - n) * a^n = a^m, by rw [←pow_add, h1], +eq_mul_inv_of_mul_eq (pow_ne_zero ha) h2 + +theorem pow_inv_comm (a : α) (m n : ℕ) : (a⁻¹)^m * a^n = a^n * (a⁻¹)^m := +by rw inv_pow; exact inv_comm_of_comm (pow_mul_comm _ _ _) + +end nat_pow + +section int_pow +open int + +/-- +The power operation in a group with zero. +This extends `monoid.pow` to negative integers +with the definition `a^(-n) = (a^n)⁻¹`. +-/ +def gpow (a : α) : ℤ → α +| (of_nat n) := a^n +| -[1+n] := (a^(nat.succ n))⁻¹ + +@[priority 10] instance : has_pow α ℤ := ⟨gpow⟩ + +@[simp] theorem gpow_coe_nat (a : α) (n : ℕ) : a ^ (n:ℤ) = a ^ n := rfl + +@[simp] theorem gpow_of_nat (a : α) (n : ℕ) : a ^ of_nat n = a ^ n := rfl + +@[simp] theorem gpow_neg_succ (a : α) (n : ℕ) : a ^ -[1+n] = (a ^ n.succ)⁻¹ := rfl + +local attribute [ematch] le_of_lt +open nat + +@[simp] theorem gpow_zero (a : α) : a ^ (0:ℤ) = 1 := rfl + +@[simp] theorem gpow_one (a : α) : a ^ (1:ℤ) = a := mul_one _ + +@[simp] theorem one_gpow : ∀ (n : ℤ), (1 : α) ^ n = 1 +| (n : ℕ) := one_pow _ +| -[1+ n] := show _⁻¹=(1:α), by rw [_root_.one_pow, inv_one'] + +@[simp] theorem gpow_neg (a : α) : ∀ (n : ℤ), a ^ -n = (a ^ n)⁻¹ +| (n+1:ℕ) := rfl +| 0 := inv_one'.symm +| -[1+ n] := (inv_inv'' _).symm + +theorem gpow_neg_one (x : α) : x ^ (-1:ℤ) = x⁻¹ := congr_arg has_inv.inv $ pow_one x + +theorem inv_gpow (a : α) : ∀n:ℤ, a⁻¹ ^ n = (a ^ n)⁻¹ +| (n : ℕ) := inv_pow a n +| -[1+ n] := congr_arg has_inv.inv $ inv_pow a (n+1) + +private lemma gpow_add_aux (a : α) (h : a ≠ 0) (m n : nat) : + a ^ ((of_nat m) + -[1+n]) = a ^ of_nat m * a ^ -[1+n] := +or.elim (nat.lt_or_ge m (nat.succ n)) + (assume h1 : m < succ n, + have h2 : m ≤ n, from le_of_lt_succ h1, + suffices a ^ -[1+ n-m] = a ^ of_nat m * a ^ -[1+n], + by rwa [of_nat_add_neg_succ_of_nat_of_lt h1], + show (a ^ nat.succ (n - m))⁻¹ = a ^ of_nat m * a ^ -[1+n], + by rw [← succ_sub h2, pow_sub _ h (le_of_lt h1), mul_inv_rev, inv_inv'']; refl) + (assume : m ≥ succ n, + suffices a ^ (of_nat (m - succ n)) = (a ^ (of_nat m)) * (a ^ -[1+ n]), + by rw [of_nat_add_neg_succ_of_nat_of_ge]; assumption, + suffices a ^ (m - succ n) = a ^ m * (a ^ n.succ)⁻¹, from this, + by rw pow_sub; assumption) + +theorem gpow_add (a : α) (h : a ≠ 0) : ∀ (i j : ℤ), a ^ (i + j) = a ^ i * a ^ j +| (of_nat m) (of_nat n) := pow_add _ _ _ +| (of_nat m) -[1+n] := gpow_add_aux _ h _ _ +| -[1+m] (of_nat n) := by rw [add_comm, gpow_add_aux _ h, + gpow_neg_succ, gpow_of_nat, ← inv_pow, ← pow_inv_comm] +| -[1+m] -[1+n] := + suffices (a ^ (m + succ (succ n)))⁻¹ = (a ^ m.succ)⁻¹ * (a ^ n.succ)⁻¹, from this, + by rw [← succ_add_eq_succ_add, add_comm, _root_.pow_add, mul_inv_rev] + +theorem gpow_add_one (a : α) (h : a ≠ 0) (i : ℤ) : a ^ (i + 1) = a ^ i * a := +by rw [gpow_add _ h, gpow_one] + +theorem gpow_one_add (a : α) (h : a ≠ 0) (i : ℤ) : a ^ (1 + i) = a * a ^ i := +by rw [gpow_add _ h, gpow_one] + +theorem gpow_mul_comm (a : α) (h : a ≠ 0) (i j : ℤ) : a ^ i * a ^ j = a ^ j * a ^ i := +by rw [← gpow_add _ h, ← gpow_add _ h, add_comm] + +theorem gpow_mul (a : α) : ∀ m n : ℤ, a ^ (m * n) = (a ^ m) ^ n +| (m : ℕ) (n : ℕ) := pow_mul _ _ _ +| (m : ℕ) -[1+ n] := (gpow_neg _ (m * succ n)).trans $ + show (a ^ (m * succ n))⁻¹ = _, by rw pow_mul; refl +| -[1+ m] (n : ℕ) := (gpow_neg _ (succ m * n)).trans $ + show (a ^ (m.succ * n))⁻¹ = _, by rw [pow_mul, ← inv_pow]; refl +| -[1+ m] -[1+ n] := (pow_mul a (succ m) (succ n)).trans $ + show _ = (_⁻¹^_)⁻¹, by rw [inv_pow, inv_inv''] + +theorem gpow_mul' (a : α) (m n : ℤ) : a ^ (m * n) = (a ^ n) ^ m := +by rw [mul_comm, gpow_mul] + +end int_pow + end group_with_zero /-- A type `α` is a commutative “group with zero” From 27201ec294eb6f3a97b127e63ed8257b61f308d5 Mon Sep 17 00:00:00 2001 From: Johan Commelin Date: Thu, 10 Oct 2019 21:00:42 +0200 Subject: [PATCH 13/37] Fix build --- src/continuous_valuations.lean | 2 +- src/examples/padics.lean | 3 ++- src/valuation/basic.lean | 5 +++-- 3 files changed, 6 insertions(+), 4 deletions(-) diff --git a/src/continuous_valuations.lean b/src/continuous_valuations.lean index a54619fa..8c6e72df 100644 --- a/src/continuous_valuations.lean +++ b/src/continuous_valuations.lean @@ -116,7 +116,7 @@ begin split; intro hx, { cases hv x with H H, {assumption}, { exfalso, rw H at hx, exact lt_irrefl _ hx }, }, - { rw hx, apply lt_of_le_of_ne linear_ordered_structure.zero_le zero_ne_one } }, + { rw hx, apply lt_of_le_of_ne linear_ordered_structure.zero_le, exact zero_ne_one } }, { resetI, intro g, exact is_open_discrete _ } end diff --git a/src/examples/padics.lean b/src/examples/padics.lean index 03d0a9d6..5b21aee5 100644 --- a/src/examples/padics.lean +++ b/src/examples/padics.lean @@ -282,8 +282,9 @@ def padic.Spa_unique : unique (Spa $ padic.Huber_pair p) := contrapose! h, obtain ⟨y, hy⟩ : ∃ y : ℤ_[p], x⁻¹ = y, { refine ⟨⟨x⁻¹, _⟩, rfl⟩, rw norm_inv, apply inv_le_one, apply le_of_lt, exact h }, - refine (linear_ordered_structure.inv_lt_inv _ one_ne_zero).mp _, + refine (linear_ordered_structure.inv_lt_inv _ _).mp _, { rw valuation.ne_zero_iff, contrapose! hx, use [0, hx] }, + { exact one_ne_zero }, { rw [inv_one', ← valuation.map_inv, hy], refine lt_of_le_of_ne (v.map_plus y) _, assume H, diff --git a/src/valuation/basic.lean b/src/valuation/basic.lean index 030a71d4..6a2a367a 100644 --- a/src/valuation/basic.lean +++ b/src/valuation/basic.lean @@ -315,11 +315,12 @@ begin { contrapose! h, cases h with h₁ h₂, by_cases hx : v x ≤ 1, { refine ⟨x⁻¹, _⟩, - rw [v.map_inv', ← linear_ordered_structure.inv_lt_inv _ one_ne_zero, + rw [v.map_inv', ← linear_ordered_structure.inv_lt_inv _ _, inv_inv'', inv_one'], { exact lt_of_le_of_ne hx h₂ }, { exact inv_ne_zero' _ h₁ }, - { rwa v.ne_zero_iff at h₁ } }, + { exact one_ne_zero }, + { rwa v.ne_zero_iff at h₁, } }, { push_neg at hx, exact ⟨_, hx⟩ } } end From a7a2dc66f6699e202b99f0524736ca8eeee8eb3c Mon Sep 17 00:00:00 2001 From: Johan Commelin Date: Thu, 10 Oct 2019 23:14:33 +0200 Subject: [PATCH 14/37] Start on the height of nnreal --- .../linear_ordered_comm_group_with_zero.lean | 22 +++++++++++++++++++ 1 file changed, 22 insertions(+) diff --git a/src/valuation/linear_ordered_comm_group_with_zero.lean b/src/valuation/linear_ordered_comm_group_with_zero.lean index cc034876..cbc26c06 100644 --- a/src/valuation/linear_ordered_comm_group_with_zero.lean +++ b/src/valuation/linear_ordered_comm_group_with_zero.lean @@ -200,6 +200,7 @@ end end linear_ordered_structure namespace nnreal +open linear_ordered_structure /-- The nonnegative real numbers form a linearly ordered commutative group with zero.-/ noncomputable instance : linear_ordered_comm_group_with_zero nnreal := @@ -212,4 +213,25 @@ noncomputable instance : linear_ordered_comm_group_with_zero nnreal := .. (infer_instance : linear_order nnreal), .. (infer_instance : comm_semiring nnreal) } +--move this +lemma cardinal.eq_one_iff_nonempty_subsingleton {α : Type*} : + cardinal.mk α = 1 ↔ (nonempty α ∧ subsingleton α) := +begin + symmetry, + rw [← cardinal.ne_zero_iff_nonempty, ← cardinal.le_one_iff_subsingleton], + rw [eq_iff_le_not_lt, ← cardinal.succ_zero, cardinal.lt_succ, cardinal.le_zero, and_comm], +end + +lemma height : height (units nnreal) = 1 := +begin + refine cardinal.eq_one_iff_nonempty_subsingleton.mpr ⟨⟨⟨set.univ, _⟩⟩, _⟩, + { constructor, any_goals { intros, exact set.mem_univ _ }, + have h2 : (2:nnreal) ≠ 0 := by norm_num, + let two : units nnreal := ⟨2,2⁻¹, mul_inv_cancel' _ h2, inv_mul_cancel' _ h2⟩, + refine ⟨1, two, set.mem_univ _, set.mem_univ _, _⟩, + sorry + }, + sorry +end + end nnreal From fc708642feec96a98146b9c3410fc85c7309eb8b Mon Sep 17 00:00:00 2001 From: Johan Commelin Date: Thu, 10 Oct 2019 23:14:50 +0200 Subject: [PATCH 15/37] Start on discrete valuations --- src/valuation/discrete.lean | 61 +++++++++++++++++++++++++++++++++++++ 1 file changed, 61 insertions(+) create mode 100644 src/valuation/discrete.lean diff --git a/src/valuation/discrete.lean b/src/valuation/discrete.lean new file mode 100644 index 00000000..1d15db43 --- /dev/null +++ b/src/valuation/discrete.lean @@ -0,0 +1,61 @@ +import valuation.basic + +/-! +# Discrete valuations + +We define discrete valuations +-/ + +universe variables u u₀ u₁ + +namespace valuation +variables {R : Type u} [ring R] +variables {Γ₀ : Type u₀} [linear_ordered_comm_group_with_zero Γ₀] +variables {Γ₀' : Type u₁} [linear_ordered_comm_group_with_zero Γ₀'] +variables (v : valuation R Γ₀) {v' : valuation R Γ₀'} + +def is_discrete : Prop := +∃ r : R, ∀ s : R, v s ≠ 0 → ∃ n : ℤ, v s = (v r)^n + +def is_non_discrete : Prop := (¬ v.is_trivial) ∧ (¬ v.is_discrete) + +namespace is_equiv +variable {v} + +lemma is_discrete (h : v.is_equiv v') : + v.is_discrete ↔ v'.is_discrete := +begin + apply exists_congr, intro r, + apply forall_congr, intro s, + apply imp_congr_ctx h.ne_zero, intro hs, + apply exists_congr, intro n, + sorry +end + +-- move this +lemma eq_zero (h : v.is_equiv v') {r : R} : + v r = 0 ↔ v' r = 0 := +by { rw [← v.map_zero, ← v'.map_zero], exact h.val_eq } + +-- move this +lemma eq_one (h : v.is_equiv v') {r : R} : + v r = 1 ↔ v' r = 1 := +by { rw [← v.map_one, ← v'.map_one], exact h.val_eq } + +-- move this +lemma is_trivial (h : v.is_equiv v') : + v.is_trivial ↔ v'.is_trivial := +begin + apply forall_congr, intro r, + exact or_congr h.eq_zero h.eq_one, +end + +lemma is_non_discrete (h : v.is_equiv v') : + v.is_non_discrete ↔ v'.is_non_discrete := +and_congr + (not_iff_not_of_iff h.is_trivial) + (not_iff_not_of_iff h.is_discrete) + +end is_equiv + +end valuation From 3b2e8e381c464c33a63c1296b2529fa4eedf67c9 Mon Sep 17 00:00:00 2001 From: Johan Commelin Date: Fri, 11 Oct 2019 11:23:27 +0200 Subject: [PATCH 16/37] We almost know that nnreal has height one --- .../linear_ordered_comm_group_with_zero.lean | 78 +++++++++++++++++-- 1 file changed, 73 insertions(+), 5 deletions(-) diff --git a/src/valuation/linear_ordered_comm_group_with_zero.lean b/src/valuation/linear_ordered_comm_group_with_zero.lean index cbc26c06..0e42005d 100644 --- a/src/valuation/linear_ordered_comm_group_with_zero.lean +++ b/src/valuation/linear_ordered_comm_group_with_zero.lean @@ -222,16 +222,84 @@ begin rw [eq_iff_le_not_lt, ← cardinal.succ_zero, cardinal.lt_succ, cardinal.le_zero, and_comm], end +-- move this +lemma exists_one_lt {α : Type*} [linear_ordered_comm_group α] (S : set α) [h : is_proper_convex S] : + ∃ a : α, a ∈ S ∧ 1 < a := +begin + choose x y hx hy hxy using h.exists_ne, + rcases lt_trichotomy 1 x with Hx|rfl|Hx, + { use [x, hx, Hx] }, + { rcases lt_trichotomy 1 y with Hy|rfl|Hy, + { use [y, hy, Hy] }, + { contradiction }, + { refine ⟨y⁻¹, is_convex.inv_mem hy, _⟩, + simpa using mul_lt_right y⁻¹ Hy, } }, + { refine ⟨x⁻¹, is_convex.inv_mem hx, _⟩, + simpa using mul_lt_right x⁻¹ Hx, } +end + +-- move this +lemma exists_lt_one {α : Type*} [linear_ordered_comm_group α] (S : set α) [h : is_proper_convex S] : + ∃ a : α, a ∈ S ∧ a < 1 := +begin + rcases exists_one_lt S with ⟨x, H1, H2⟩, + use [x⁻¹, is_convex.inv_mem H1], + simpa using mul_lt_right x⁻¹ H2, +end + +open_locale classical + +-- move this +lemma is_convex.mem_of_between' {α : Type*} [linear_ordered_comm_group α] + (S : set α) [h : is_proper_convex S] + {a b c : α} (ha : a ∈ S) (hc : c ∈ S) (hab : a ≤ b) (hbc : b ≤ c) : + b ∈ S := +begin + cases le_total b 1 with hb hb, + { exact is_convex.mem_of_between hab hb ha }, + rw ← _root_.inv_inv b, + apply is_convex.inv_mem, + apply @is_convex.mem_of_between α _ S _ c⁻¹ _ _ _ (is_convex.inv_mem hc), + { contrapose! hbc, have := mul_lt_right (b*c) hbc, + rwa [inv_mul_cancel_left, mul_left_comm, mul_left_inv, mul_one] at this }, + { contrapose! hb, simpa using mul_lt_right b hb, } +end + +-- move this +lemma is_convex.pow_mem {α : Type*} [linear_ordered_comm_group α] + (S : set α) [h : is_proper_convex S] {a : α} (ha : a ∈ S) (n : ℕ) : + a^n ∈ S := +begin + induction n with n ih, { rw pow_zero, exact is_convex.one_mem S }, + rw pow_succ, exact is_convex.mul_mem ha ih, +end + +-- move this +lemma is_convex.gpow_mem {α : Type*} [linear_ordered_comm_group α] + (S : set α) [h : is_proper_convex S] {a : α} (ha : a ∈ S) : + ∀ (n : ℤ), a^n ∈ S +| (int.of_nat n) := by { rw [gpow_of_nat], exact is_convex.pow_mem S ha n } +| -[1+n] := by { apply is_convex.inv_mem, exact is_convex.pow_mem S ha _ } + lemma height : height (units nnreal) = 1 := begin - refine cardinal.eq_one_iff_nonempty_subsingleton.mpr ⟨⟨⟨set.univ, _⟩⟩, _⟩, + refine cardinal.eq_one_iff_nonempty_subsingleton.mpr ⟨⟨⟨set.univ, _⟩⟩, ⟨_⟩⟩, { constructor, any_goals { intros, exact set.mem_univ _ }, have h2 : (2:nnreal) ≠ 0 := by norm_num, - let two : units nnreal := ⟨2,2⁻¹, mul_inv_cancel' _ h2, inv_mul_cancel' _ h2⟩, + let two : units nnreal := group_with_zero.mk₀ 2 (by norm_num), refine ⟨1, two, set.mem_univ _, set.mem_univ _, _⟩, - sorry - }, - sorry + rw [ne.def, units.ext_iff], show (1:nnreal) ≠ 2, by norm_num, }, + { suffices key : ∀ S : set (units nnreal), is_proper_convex S → S = set.univ, + { intros S T, rw [subtype.ext, key S.1 S.2, key T.1 T.2], }, + intros S hS, resetI, + rw set.eq_univ_iff_forall, intro y, + cases le_total 1 y with Hy Hy, + { rcases exists_one_lt S with ⟨x, hx, Hx⟩, + obtain ⟨n, hn⟩ : ∃ (n : ℕ), y ≤ x^n := sorry, + exact is_convex.mem_of_between' S (is_convex.one_mem S) (is_convex.pow_mem S hx _) Hy hn, }, + { rcases exists_lt_one S with ⟨x, hx, Hx⟩, + obtain ⟨n, hn⟩ : ∃ (n : ℕ), x^n ≤ y := sorry, + exact is_convex.mem_of_between hn Hy (is_convex.pow_mem S hx _) } } end end nnreal From 55f355a86e0fdc2615148d43611b34da8459be67 Mon Sep 17 00:00:00 2001 From: Johan Commelin Date: Fri, 11 Oct 2019 13:43:39 +0200 Subject: [PATCH 17/37] Move things around a bit --- src/for_mathlib/nnreal.lean | 104 +++++++++++++++++ .../linear_ordered_comm_group_with_zero.lean | 105 ------------------ 2 files changed, 104 insertions(+), 105 deletions(-) diff --git a/src/for_mathlib/nnreal.lean b/src/for_mathlib/nnreal.lean index a0ab5126..f4f9a410 100644 --- a/src/for_mathlib/nnreal.lean +++ b/src/for_mathlib/nnreal.lean @@ -1,6 +1,8 @@ import data.real.nnreal import analysis.complex.exponential +import valuation.linear_ordered_comm_group_with_zero + namespace nnreal @[simp] lemma coe_max (x y : nnreal) : ((max x y : nnreal) : ℝ) = max (x : ℝ) (y : ℝ) := @@ -30,4 +32,106 @@ by rw [← real.rpow_one a, ← nat.cast_one, rpow_nat_cast, real.rpow_nat_cast, lemma rpow_le_rpow {a b : nnreal} (h : a ≤ b) (hx : 0 ≤ x) : a^x ≤ b^x := show (a^x : ℝ) ≤ b^x, from real.rpow_le_rpow a.2 h hx +open linear_ordered_structure + +/-- The nonnegative real numbers form a linearly ordered commutative group with zero.-/ +noncomputable instance : linear_ordered_comm_group_with_zero nnreal := +{ inv_zero := by simp, + zero_le' := zero_le, + mul_le_mul_left := λ a b h c, mul_le_mul (le_refl _) h (zero_le _) (zero_le _), + mul_inv_cancel := λ a h, mul_inv_cancel h, + .. (infer_instance : zero_ne_one_class nnreal), + .. (infer_instance : has_inv nnreal), + .. (infer_instance : linear_order nnreal), + .. (infer_instance : comm_semiring nnreal) } + +--move this +lemma cardinal.eq_one_iff_nonempty_subsingleton {α : Type*} : + cardinal.mk α = 1 ↔ (nonempty α ∧ subsingleton α) := +begin + symmetry, + rw [← cardinal.ne_zero_iff_nonempty, ← cardinal.le_one_iff_subsingleton], + rw [eq_iff_le_not_lt, ← cardinal.succ_zero, cardinal.lt_succ, cardinal.le_zero, and_comm], +end + +-- move this +lemma exists_one_lt {α : Type*} [linear_ordered_comm_group α] (S : set α) [h : is_proper_convex S] : + ∃ a : α, a ∈ S ∧ 1 < a := +begin + choose x y hx hy hxy using h.exists_ne, + rcases lt_trichotomy 1 x with Hx|rfl|Hx, + { use [x, hx, Hx] }, + { rcases lt_trichotomy 1 y with Hy|rfl|Hy, + { use [y, hy, Hy] }, + { contradiction }, + { refine ⟨y⁻¹, is_convex.inv_mem hy, _⟩, + simpa using mul_lt_right y⁻¹ Hy, } }, + { refine ⟨x⁻¹, is_convex.inv_mem hx, _⟩, + simpa using mul_lt_right x⁻¹ Hx, } +end + +-- move this +lemma exists_lt_one {α : Type*} [linear_ordered_comm_group α] (S : set α) [h : is_proper_convex S] : + ∃ a : α, a ∈ S ∧ a < 1 := +begin + rcases exists_one_lt S with ⟨x, H1, H2⟩, + use [x⁻¹, is_convex.inv_mem H1], + simpa using mul_lt_right x⁻¹ H2, +end + +open_locale classical + +-- move this +lemma is_convex.mem_of_between' {α : Type*} [linear_ordered_comm_group α] + (S : set α) [h : is_proper_convex S] + {a b c : α} (ha : a ∈ S) (hc : c ∈ S) (hab : a ≤ b) (hbc : b ≤ c) : + b ∈ S := +begin + cases le_total b 1 with hb hb, + { exact is_convex.mem_of_between hab hb ha }, + rw ← _root_.inv_inv b, + apply is_convex.inv_mem, + apply @is_convex.mem_of_between α _ S _ c⁻¹ _ _ _ (is_convex.inv_mem hc), + { contrapose! hbc, have := mul_lt_right (b*c) hbc, + rwa [inv_mul_cancel_left, mul_left_comm, mul_left_inv, mul_one] at this }, + { contrapose! hb, simpa using mul_lt_right b hb, } +end + +-- move this +lemma is_convex.pow_mem {α : Type*} [linear_ordered_comm_group α] + (S : set α) [h : is_proper_convex S] {a : α} (ha : a ∈ S) (n : ℕ) : + a^n ∈ S := +begin + induction n with n ih, { rw pow_zero, exact is_convex.one_mem S }, + rw pow_succ, exact is_convex.mul_mem ha ih, +end + +-- move this +lemma is_convex.gpow_mem {α : Type*} [linear_ordered_comm_group α] + (S : set α) [h : is_proper_convex S] {a : α} (ha : a ∈ S) : + ∀ (n : ℤ), a^n ∈ S +| (int.of_nat n) := by { rw [gpow_of_nat], exact is_convex.pow_mem S ha n } +| -[1+n] := by { apply is_convex.inv_mem, exact is_convex.pow_mem S ha _ } + +lemma height : height (units nnreal) = 1 := +begin + refine cardinal.eq_one_iff_nonempty_subsingleton.mpr ⟨⟨⟨set.univ, _⟩⟩, ⟨_⟩⟩, + { constructor, any_goals { intros, exact set.mem_univ _ }, + have h2 : (2:nnreal) ≠ 0 := by norm_num, + let two : units nnreal := group_with_zero.mk₀ 2 (by norm_num), + refine ⟨1, two, set.mem_univ _, set.mem_univ _, _⟩, + rw [ne.def, units.ext_iff], show (1:nnreal) ≠ 2, by norm_num, }, + { suffices key : ∀ S : set (units nnreal), is_proper_convex S → S = set.univ, + { intros S T, rw [subtype.ext, key S.1 S.2, key T.1 T.2], }, + intros S hS, resetI, + rw set.eq_univ_iff_forall, intro y, + cases le_total 1 y with Hy Hy, + { rcases exists_one_lt S with ⟨x, hx, Hx⟩, + obtain ⟨n, hn⟩ : ∃ (n : ℕ), y ≤ x^n := sorry, + exact is_convex.mem_of_between' S (is_convex.one_mem S) (is_convex.pow_mem S hx _) Hy hn, }, + { rcases exists_lt_one S with ⟨x, hx, Hx⟩, + obtain ⟨n, hn⟩ : ∃ (n : ℕ), x^n ≤ y := sorry, + exact is_convex.mem_of_between hn Hy (is_convex.pow_mem S hx _) } } +end + end nnreal diff --git a/src/valuation/linear_ordered_comm_group_with_zero.lean b/src/valuation/linear_ordered_comm_group_with_zero.lean index 0e42005d..bc7f18c7 100644 --- a/src/valuation/linear_ordered_comm_group_with_zero.lean +++ b/src/valuation/linear_ordered_comm_group_with_zero.lean @@ -198,108 +198,3 @@ begin end end linear_ordered_structure - -namespace nnreal -open linear_ordered_structure - -/-- The nonnegative real numbers form a linearly ordered commutative group with zero.-/ -noncomputable instance : linear_ordered_comm_group_with_zero nnreal := -{ inv_zero := by simp, - zero_le' := zero_le, - mul_le_mul_left := λ a b h c, mul_le_mul (le_refl _) h (zero_le _) (zero_le _), - mul_inv_cancel := λ a h, mul_inv_cancel h, - .. (infer_instance : zero_ne_one_class nnreal), - .. (infer_instance : has_inv nnreal), - .. (infer_instance : linear_order nnreal), - .. (infer_instance : comm_semiring nnreal) } - ---move this -lemma cardinal.eq_one_iff_nonempty_subsingleton {α : Type*} : - cardinal.mk α = 1 ↔ (nonempty α ∧ subsingleton α) := -begin - symmetry, - rw [← cardinal.ne_zero_iff_nonempty, ← cardinal.le_one_iff_subsingleton], - rw [eq_iff_le_not_lt, ← cardinal.succ_zero, cardinal.lt_succ, cardinal.le_zero, and_comm], -end - --- move this -lemma exists_one_lt {α : Type*} [linear_ordered_comm_group α] (S : set α) [h : is_proper_convex S] : - ∃ a : α, a ∈ S ∧ 1 < a := -begin - choose x y hx hy hxy using h.exists_ne, - rcases lt_trichotomy 1 x with Hx|rfl|Hx, - { use [x, hx, Hx] }, - { rcases lt_trichotomy 1 y with Hy|rfl|Hy, - { use [y, hy, Hy] }, - { contradiction }, - { refine ⟨y⁻¹, is_convex.inv_mem hy, _⟩, - simpa using mul_lt_right y⁻¹ Hy, } }, - { refine ⟨x⁻¹, is_convex.inv_mem hx, _⟩, - simpa using mul_lt_right x⁻¹ Hx, } -end - --- move this -lemma exists_lt_one {α : Type*} [linear_ordered_comm_group α] (S : set α) [h : is_proper_convex S] : - ∃ a : α, a ∈ S ∧ a < 1 := -begin - rcases exists_one_lt S with ⟨x, H1, H2⟩, - use [x⁻¹, is_convex.inv_mem H1], - simpa using mul_lt_right x⁻¹ H2, -end - -open_locale classical - --- move this -lemma is_convex.mem_of_between' {α : Type*} [linear_ordered_comm_group α] - (S : set α) [h : is_proper_convex S] - {a b c : α} (ha : a ∈ S) (hc : c ∈ S) (hab : a ≤ b) (hbc : b ≤ c) : - b ∈ S := -begin - cases le_total b 1 with hb hb, - { exact is_convex.mem_of_between hab hb ha }, - rw ← _root_.inv_inv b, - apply is_convex.inv_mem, - apply @is_convex.mem_of_between α _ S _ c⁻¹ _ _ _ (is_convex.inv_mem hc), - { contrapose! hbc, have := mul_lt_right (b*c) hbc, - rwa [inv_mul_cancel_left, mul_left_comm, mul_left_inv, mul_one] at this }, - { contrapose! hb, simpa using mul_lt_right b hb, } -end - --- move this -lemma is_convex.pow_mem {α : Type*} [linear_ordered_comm_group α] - (S : set α) [h : is_proper_convex S] {a : α} (ha : a ∈ S) (n : ℕ) : - a^n ∈ S := -begin - induction n with n ih, { rw pow_zero, exact is_convex.one_mem S }, - rw pow_succ, exact is_convex.mul_mem ha ih, -end - --- move this -lemma is_convex.gpow_mem {α : Type*} [linear_ordered_comm_group α] - (S : set α) [h : is_proper_convex S] {a : α} (ha : a ∈ S) : - ∀ (n : ℤ), a^n ∈ S -| (int.of_nat n) := by { rw [gpow_of_nat], exact is_convex.pow_mem S ha n } -| -[1+n] := by { apply is_convex.inv_mem, exact is_convex.pow_mem S ha _ } - -lemma height : height (units nnreal) = 1 := -begin - refine cardinal.eq_one_iff_nonempty_subsingleton.mpr ⟨⟨⟨set.univ, _⟩⟩, ⟨_⟩⟩, - { constructor, any_goals { intros, exact set.mem_univ _ }, - have h2 : (2:nnreal) ≠ 0 := by norm_num, - let two : units nnreal := group_with_zero.mk₀ 2 (by norm_num), - refine ⟨1, two, set.mem_univ _, set.mem_univ _, _⟩, - rw [ne.def, units.ext_iff], show (1:nnreal) ≠ 2, by norm_num, }, - { suffices key : ∀ S : set (units nnreal), is_proper_convex S → S = set.univ, - { intros S T, rw [subtype.ext, key S.1 S.2, key T.1 T.2], }, - intros S hS, resetI, - rw set.eq_univ_iff_forall, intro y, - cases le_total 1 y with Hy Hy, - { rcases exists_one_lt S with ⟨x, hx, Hx⟩, - obtain ⟨n, hn⟩ : ∃ (n : ℕ), y ≤ x^n := sorry, - exact is_convex.mem_of_between' S (is_convex.one_mem S) (is_convex.pow_mem S hx _) Hy hn, }, - { rcases exists_lt_one S with ⟨x, hx, Hx⟩, - obtain ⟨n, hn⟩ : ∃ (n : ℕ), x^n ≤ y := sorry, - exact is_convex.mem_of_between hn Hy (is_convex.pow_mem S hx _) } } -end - -end nnreal From 16e718a02f7dd4e9f2a09e288e96933f23772fa4 Mon Sep 17 00:00:00 2001 From: Johan Commelin Date: Fri, 11 Oct 2019 14:12:50 +0200 Subject: [PATCH 18/37] Make the nondiscrete life easier --- src/valuation/discrete.lean | 51 ++++++++++++++++++++++++++----------- 1 file changed, 36 insertions(+), 15 deletions(-) diff --git a/src/valuation/discrete.lean b/src/valuation/discrete.lean index 1d15db43..b8ef1a6b 100644 --- a/src/valuation/discrete.lean +++ b/src/valuation/discrete.lean @@ -8,30 +8,23 @@ We define discrete valuations universe variables u u₀ u₁ +open_locale classical + namespace valuation variables {R : Type u} [ring R] variables {Γ₀ : Type u₀} [linear_ordered_comm_group_with_zero Γ₀] variables {Γ₀' : Type u₁} [linear_ordered_comm_group_with_zero Γ₀'] variables (v : valuation R Γ₀) {v' : valuation R Γ₀'} +def is_non_discrete : Prop := +∀ r : R, v r < 1 → ∃ s : R, v r < v s ∧ v s < 1 + def is_discrete : Prop := ∃ r : R, ∀ s : R, v s ≠ 0 → ∃ n : ℤ, v s = (v r)^n -def is_non_discrete : Prop := (¬ v.is_trivial) ∧ (¬ v.is_discrete) - namespace is_equiv variable {v} -lemma is_discrete (h : v.is_equiv v') : - v.is_discrete ↔ v'.is_discrete := -begin - apply exists_congr, intro r, - apply forall_congr, intro s, - apply imp_congr_ctx h.ne_zero, intro hs, - apply exists_congr, intro n, - sorry -end - -- move this lemma eq_zero (h : v.is_equiv v') {r : R} : v r = 0 ↔ v' r = 0 := @@ -42,6 +35,16 @@ lemma eq_one (h : v.is_equiv v') {r : R} : v r = 1 ↔ v' r = 1 := by { rw [← v.map_one, ← v'.map_one], exact h.val_eq } +-- move this +lemma lt_iff (h : v.is_equiv v') {r s : R} : + v r < v s ↔ v' r < v' s := +by { have := not_iff_not_of_iff (h s r), push_neg at this, exact this } + +-- move this +lemma lt_one (h : v.is_equiv v') {r : R} : + v r < 1 ↔ v' r < 1 := +by { rw [← v.map_one, ← v'.map_one], exact h.lt_iff } + -- move this lemma is_trivial (h : v.is_equiv v') : v.is_trivial ↔ v'.is_trivial := @@ -52,9 +55,27 @@ end lemma is_non_discrete (h : v.is_equiv v') : v.is_non_discrete ↔ v'.is_non_discrete := -and_congr - (not_iff_not_of_iff h.is_trivial) - (not_iff_not_of_iff h.is_discrete) +begin + apply forall_congr, intro r, + apply imp_congr_ctx h.lt_one, intro hr, + apply exists_congr, intro s, + rw [h.lt_iff, h.lt_one] +end + +-- This is not so trivial. But we don't need it atm. +-- lemma is_discrete (h : v.is_equiv v') : +-- v.is_discrete ↔ v'.is_discrete := +-- begin +-- apply exists_congr, intro r, +-- apply forall_congr, intro s, +-- apply imp_congr_ctx h.ne_zero, intro hs, +-- apply exists_congr, intro n, +-- sorry +-- end + +-- lemma trichotomy : +-- v.is_trivial ∨ v.is_discrete ∨ v.is_non_discrete := +-- sorry end is_equiv From d4981344443dc3cfab4518a40bc9792f69edc00b Mon Sep 17 00:00:00 2001 From: Johan Commelin Date: Fri, 11 Oct 2019 15:10:12 +0200 Subject: [PATCH 19/37] Move some lemmas in the proper place --- src/valuation/basic.lean | 23 +++++++++++++++++++++++ src/valuation/discrete.lean | 32 ++------------------------------ 2 files changed, 25 insertions(+), 30 deletions(-) diff --git a/src/valuation/basic.lean b/src/valuation/basic.lean index 6a2a367a..54ce5bc6 100644 --- a/src/valuation/basic.lean +++ b/src/valuation/basic.lean @@ -247,6 +247,22 @@ begin rwa [v₁.map_zero, v₂.map_zero] at this, end +lemma eq_zero (h : v₁.is_equiv v₂) {r : R} : + v₁ r = 0 ↔ v₂ r = 0 := +by { rw [← v₁.map_zero, ← v₂.map_zero], exact h.val_eq } + +lemma eq_one (h : v₁.is_equiv v₂) {r : R} : + v₁ r = 1 ↔ v₂ r = 1 := +by { rw [← v₁.map_one, ← v₂.map_one], exact h.val_eq } + +lemma lt_iff (h : v₁.is_equiv v₂) {r s : R} : + v₁ r < v₁ s ↔ v₂ r < v₂ s := +by { have := not_iff_not_of_iff (h s r), push_neg at this, exact this } + +lemma lt_one (h : v₁.is_equiv v₂) {r : R} : + v₁ r < 1 ↔ v₂ r < 1 := +by { rw [← v₁.map_one, ← v₂.map_one], exact h.lt_iff } + end is_equiv -- end of namespace lemma is_equiv_of_map_strict_mono [ring R] {v : valuation R Γ₀} @@ -324,6 +340,13 @@ begin { push_neg at hx, exact ⟨_, hx⟩ } } end +lemma is_equiv.is_trivial {v₁ : valuation R Γ₀} {v₂ : valuation R Γ'₀} (h : v₁.is_equiv v₂) : + v₁.is_trivial ↔ v₂.is_trivial := +begin + apply forall_congr, intro r, + exact or_congr h.eq_zero h.eq_one, +end + end trivial -- end of section section supp diff --git a/src/valuation/discrete.lean b/src/valuation/discrete.lean index b8ef1a6b..b83d0ed9 100644 --- a/src/valuation/discrete.lean +++ b/src/valuation/discrete.lean @@ -13,8 +13,8 @@ open_locale classical namespace valuation variables {R : Type u} [ring R] variables {Γ₀ : Type u₀} [linear_ordered_comm_group_with_zero Γ₀] -variables {Γ₀' : Type u₁} [linear_ordered_comm_group_with_zero Γ₀'] -variables (v : valuation R Γ₀) {v' : valuation R Γ₀'} +variables {Γ'₀ : Type u₁} [linear_ordered_comm_group_with_zero Γ'₀] +variables (v : valuation R Γ₀) {v' : valuation R Γ'₀} def is_non_discrete : Prop := ∀ r : R, v r < 1 → ∃ s : R, v r < v s ∧ v s < 1 @@ -25,34 +25,6 @@ def is_discrete : Prop := namespace is_equiv variable {v} --- move this -lemma eq_zero (h : v.is_equiv v') {r : R} : - v r = 0 ↔ v' r = 0 := -by { rw [← v.map_zero, ← v'.map_zero], exact h.val_eq } - --- move this -lemma eq_one (h : v.is_equiv v') {r : R} : - v r = 1 ↔ v' r = 1 := -by { rw [← v.map_one, ← v'.map_one], exact h.val_eq } - --- move this -lemma lt_iff (h : v.is_equiv v') {r s : R} : - v r < v s ↔ v' r < v' s := -by { have := not_iff_not_of_iff (h s r), push_neg at this, exact this } - --- move this -lemma lt_one (h : v.is_equiv v') {r : R} : - v r < 1 ↔ v' r < 1 := -by { rw [← v.map_one, ← v'.map_one], exact h.lt_iff } - --- move this -lemma is_trivial (h : v.is_equiv v') : - v.is_trivial ↔ v'.is_trivial := -begin - apply forall_congr, intro r, - exact or_congr h.eq_zero h.eq_one, -end - lemma is_non_discrete (h : v.is_equiv v') : v.is_non_discrete ↔ v'.is_non_discrete := begin From 4a96399b856663b5440599a56bc9ff276d5fa1d5 Mon Sep 17 00:00:00 2001 From: Johan Commelin Date: Fri, 11 Oct 2019 15:15:12 +0200 Subject: [PATCH 20/37] Add docstrings to definitons --- src/valuation/discrete.lean | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/src/valuation/discrete.lean b/src/valuation/discrete.lean index b83d0ed9..e570c2da 100644 --- a/src/valuation/discrete.lean +++ b/src/valuation/discrete.lean @@ -16,9 +16,13 @@ variables {Γ₀ : Type u₀} [linear_ordered_comm_group_with_zero Γ₀] variables {Γ'₀ : Type u₁} [linear_ordered_comm_group_with_zero Γ'₀] variables (v : valuation R Γ₀) {v' : valuation R Γ'₀} +/-- A valuation on a ring R is nondiscrete if for every element of R with value x < 1, +there is another element of R whose value lies between x and 1. -/ def is_non_discrete : Prop := ∀ r : R, v r < 1 → ∃ s : R, v r < v s ∧ v s < 1 +/-- A valuation on a ring R is discrete if there is an element x of the value monoid +such that the valuation of every element of R is either 0 or an integer power of x. -/ def is_discrete : Prop := ∃ r : R, ∀ s : R, v s ≠ 0 → ∃ n : ℤ, v s = (v r)^n @@ -45,10 +49,10 @@ end -- sorry -- end +end is_equiv + -- lemma trichotomy : -- v.is_trivial ∨ v.is_discrete ∨ v.is_non_discrete := -- sorry -end is_equiv - end valuation From 497c0ecc0a15266c79a5c2a193720b5dfb4ab660 Mon Sep 17 00:00:00 2001 From: Johan Commelin Date: Fri, 11 Oct 2019 15:47:30 +0200 Subject: [PATCH 21/37] Fix build --- src/examples/char_p.lean | 24 ++++++++++++++---------- src/valuation/perfection.lean | 5 +++-- 2 files changed, 17 insertions(+), 12 deletions(-) diff --git a/src/examples/char_p.lean b/src/examples/char_p.lean index c56c8301..dabe2222 100644 --- a/src/examples/char_p.lean +++ b/src/examples/char_p.lean @@ -63,15 +63,16 @@ begin have hm : m.dom := enat.dom_of_le_some h, rw [← enat.coe_get hm, enat.coe_le_coe] at h, rw [dif_pos hm, dif_pos hn], - rw [← linear_ordered_structure.inv_le_inv one_ne_zero h₁, inv_one'] at h₂, + rw [← linear_ordered_structure.inv_le_inv _ h₁, inv_one'] at h₂, have := pow_le_pow h₂ h, -- We need lots of norm_cast lemmas rwa [nnreal.coe_le, nnreal.coe_pow, nnreal.coe_pow, nnreal.coe_inv, ← pow_inv, ← pow_inv, ← nnreal.coe_pow, ← nnreal.coe_pow, ← nnreal.coe_inv, ← nnreal.coe_inv, ← nnreal.coe_le, linear_ordered_structure.inv_le_inv] at this, + any_goals { exact one_ne_zero }, all_goals { contrapose! h₁ }, any_goals { exact subtype.val_injective h₁ }, - all_goals { apply group_with_zero.pow_eq_zero, assumption } }, + any_goals { apply group_with_zero.pow_eq_zero, assumption } }, { rw dif_neg hn, exact zero_le _ } end @@ -84,12 +85,13 @@ begin have hm : m.dom := enat.dom_of_le_some (le_of_lt h), rw [← enat.coe_get hm, enat.coe_lt_coe] at h, rw [dif_pos hm, dif_pos hn], - rw [← linear_ordered_structure.inv_lt_inv one_ne_zero h₁, inv_one'] at h₂, + rw [← linear_ordered_structure.inv_lt_inv _ h₁, inv_one'] at h₂, have := pow_lt_pow h₂ h, -- We need lots of norm_cast lemmas rwa [nnreal.coe_lt, nnreal.coe_pow, nnreal.coe_pow, nnreal.coe_inv, ← pow_inv, ← pow_inv, ← nnreal.coe_pow, ← nnreal.coe_pow, ← nnreal.coe_inv, ← nnreal.coe_inv, ← nnreal.coe_lt, linear_ordered_structure.inv_lt_inv] at this, + any_goals { exact one_ne_zero }, all_goals { contrapose! h₁ }, any_goals { exact subtype.val_injective h₁ }, all_goals { apply group_with_zero.pow_eq_zero, assumption } }, @@ -136,10 +138,11 @@ def valuation : valuation (power_series K) nnreal := cases this with h h; [left, right], all_goals { apply nnreal_of_enat_le _ inv_p_ne_zero _ _ _ h, - rw [← linear_ordered_structure.inv_le_inv one_ne_zero inv_p_ne_zero, inv_inv'', inv_one'], - apply le_of_lt, - rw [show (p : nnreal) = (p : ℕ), by rw coe_coe], - exact_mod_cast p.one_lt, }, + rw [← linear_ordered_structure.inv_le_inv _ inv_p_ne_zero, inv_inv'', inv_one'], + { apply le_of_lt, + rw [show (p : nnreal) = (p : ℕ), by rw coe_coe], + exact_mod_cast p.one_lt, }, + { exact one_ne_zero } }, end } end power_series @@ -174,9 +177,10 @@ begin exact_mod_cast H }, rwa [← nnreal_of_enat_top, (nnreal_of_enat_inj _ inv_p_ne_zero _).eq_iff, power_series.order_eq_top] at h, - rw [← linear_ordered_structure.inv_lt_inv one_ne_zero inv_p_ne_zero, inv_inv'', inv_one'], - rw [show (p : nnreal) = (p : ℕ), by rw coe_coe], - exact_mod_cast p.one_lt, + rw [← linear_ordered_structure.inv_lt_inv _ inv_p_ne_zero, inv_inv'', inv_one'], + { rw [show (p : nnreal) = (p : ℕ), by rw coe_coe], + exact_mod_cast p.one_lt }, + { exact one_ne_zero } end lemma non_trivial : ¬ (valuation p K).is_trivial := diff --git a/src/valuation/perfection.lean b/src/valuation/perfection.lean index a9156dcc..0f95b7c9 100644 --- a/src/valuation/perfection.lean +++ b/src/valuation/perfection.lean @@ -141,9 +141,10 @@ begin { delta is_trivial at hv, push_neg at hv, rcases hv with ⟨x, h₁, h₂⟩, by_cases hx : 1 < v x, { use [x,hx] }, use x⁻¹, - rw [v.map_inv, ← linear_ordered_structure.inv_lt_inv _ one_ne_zero, inv_inv'', inv_one'], + rw [v.map_inv, ← linear_ordered_structure.inv_lt_inv _ _, inv_inv'', inv_one'], { push_neg at hx, exact lt_of_le_of_ne hx h₂ }, - { contrapose! h₁, rwa nnreal.inv_eq_zero at h₁ } }, + { contrapose! h₁, rwa nnreal.inv_eq_zero at h₁ }, + { exact one_ne_zero } }, suffices : ∃ n : ℕ, (v x)^(p^(-n : ℤ) : ℝ) < 1 + ε, { rcases this with ⟨n, hn⟩, refine ⟨quot.mk (perfect_closure.r K p) (n,x), _, hn⟩, From ae300911e9c0d89e26122171a33d775e6817e174 Mon Sep 17 00:00:00 2001 From: Johan Commelin Date: Fri, 11 Oct 2019 16:19:06 +0200 Subject: [PATCH 22/37] Cleanup nnreal.pow_enat --- src/examples/char_p.lean | 124 ++++-------------------------------- src/for_mathlib/nnreal.lean | 115 +++++++++++++++++++++++++++++++++ 2 files changed, 126 insertions(+), 113 deletions(-) diff --git a/src/examples/char_p.lean b/src/examples/char_p.lean index dabe2222..4095232c 100644 --- a/src/examples/char_p.lean +++ b/src/examples/char_p.lean @@ -13,119 +13,17 @@ open function local postfix `ᵒ` : 66 := power_bounded_subring -section - -def nnreal_of_enat (b : nnreal) (n : enat) : nnreal := -if h : n.dom then (b^n.get h) else 0 - -@[simp] lemma nnreal_of_enat_top (b : nnreal) : - nnreal_of_enat b ⊤ = 0 := -begin - rw [nnreal_of_enat, dif_neg], exact not_false -end - -@[simp] lemma nnreal_of_enat_zero (b : nnreal) : - nnreal_of_enat b 0 = 1 := -begin - rw [nnreal_of_enat, dif_pos, enat.get_zero, pow_zero], - exact trivial, -end - -@[simp] lemma nnreal_of_enat_one (b : nnreal) : - nnreal_of_enat b 1 = b := -begin - rw [nnreal_of_enat, dif_pos, enat.get_one, pow_one], - exact trivial, -end - -@[simp] lemma nnreal_of_enat_add (b : nnreal) (m n : enat) : - nnreal_of_enat b (m + n) = nnreal_of_enat b m * nnreal_of_enat b n := -begin - delta nnreal_of_enat, - by_cases hm : m.dom, - { by_cases hn : n.dom, - { have hmn : (m + n).dom := ⟨hm, hn⟩, - rw [dif_pos hm, dif_pos hn, dif_pos, - subtype.coe_ext, nnreal.coe_mul, ← nnreal.coe_mul, ← pow_add, enat.get_add, add_comm], - exact hmn, }, - { rw [dif_pos hm, dif_neg hn, dif_neg, mul_zero], - contrapose! hn with H, exact H.2 } }, - { rw [dif_neg hm, dif_neg, zero_mul], - contrapose! hm with H, exact H.1 }, -end - -@[simp] lemma nnreal_of_enat_le (b : nnreal) (h₁ : b ≠ 0) (h₂ : b ≤ 1) (m n : enat) (h : m ≤ n) : - nnreal_of_enat b n ≤ nnreal_of_enat b m := -begin - delta nnreal_of_enat, - by_cases hn : n.dom, - { rw ← enat.coe_get hn at h, - have hm : m.dom := enat.dom_of_le_some h, - rw [← enat.coe_get hm, enat.coe_le_coe] at h, - rw [dif_pos hm, dif_pos hn], - rw [← linear_ordered_structure.inv_le_inv _ h₁, inv_one'] at h₂, - have := pow_le_pow h₂ h, - -- We need lots of norm_cast lemmas - rwa [nnreal.coe_le, nnreal.coe_pow, nnreal.coe_pow, nnreal.coe_inv, ← pow_inv, ← pow_inv, - ← nnreal.coe_pow, ← nnreal.coe_pow, ← nnreal.coe_inv, ← nnreal.coe_inv, ← nnreal.coe_le, - linear_ordered_structure.inv_le_inv] at this, - any_goals { exact one_ne_zero }, - all_goals { contrapose! h₁ }, - any_goals { exact subtype.val_injective h₁ }, - any_goals { apply group_with_zero.pow_eq_zero, assumption } }, - { rw dif_neg hn, exact zero_le _ } -end - -@[simp] lemma nnreal_of_enat_lt (b : nnreal) (h₁ : b ≠ 0) (h₂ : b < 1) (m n : enat) (h : m < n) : - nnreal_of_enat b n < nnreal_of_enat b m := -begin - delta nnreal_of_enat, - by_cases hn : n.dom, - { rw ← enat.coe_get hn at h, - have hm : m.dom := enat.dom_of_le_some (le_of_lt h), - rw [← enat.coe_get hm, enat.coe_lt_coe] at h, - rw [dif_pos hm, dif_pos hn], - rw [← linear_ordered_structure.inv_lt_inv _ h₁, inv_one'] at h₂, - have := pow_lt_pow h₂ h, - -- We need lots of norm_cast lemmas - rwa [nnreal.coe_lt, nnreal.coe_pow, nnreal.coe_pow, nnreal.coe_inv, ← pow_inv, ← pow_inv, - ← nnreal.coe_pow, ← nnreal.coe_pow, ← nnreal.coe_inv, ← nnreal.coe_inv, ← nnreal.coe_lt, - linear_ordered_structure.inv_lt_inv] at this, - any_goals { exact one_ne_zero }, - all_goals { contrapose! h₁ }, - any_goals { exact subtype.val_injective h₁ }, - all_goals { apply group_with_zero.pow_eq_zero, assumption } }, - { rw dif_neg hn, - have : n = ⊤ := roption.eq_none_iff'.mpr hn, subst this, - replace h := ne_of_lt h, - rw enat.ne_top_iff at h, rcases h with ⟨m, rfl⟩, - rw dif_pos, swap, {trivial}, - apply pow_pos, - exact lt_of_le_of_ne b.2 h₁.symm } -end - -@[simp] lemma nnreal_of_enat_inj (b : nnreal) (h₁ : b ≠ 0) (h₂ : b < 1) : - injective (nnreal_of_enat b) := -begin - intros m n h, - wlog H : m ≤ n, - rcases lt_or_eq_of_le H with H|rfl, - { have := nnreal_of_enat_lt b h₁ h₂ m n H, - exfalso, exact ne_of_lt this h.symm, }, - { refl }, -end - -end +local attribute [instance] nnreal.pow_enat namespace power_series variables (p : nat.primes) variables (K : Type*) [discrete_field K] [char_p K p] def valuation : valuation (power_series K) nnreal := -{ to_fun := λ φ, nnreal_of_enat (p⁻¹) φ.order, - map_zero' := by rw [order_zero, nnreal_of_enat_top], - map_one' := by rw [order_one, nnreal_of_enat_zero], - map_mul' := λ x y, by rw [order_mul, nnreal_of_enat_add], +{ to_fun := λ φ, (p⁻¹) ^ φ.order, + map_zero' := by rw [order_zero, nnreal.pow_enat_top], + map_one' := by rw [order_one, nnreal.pow_enat_zero], + map_mul' := λ x y, by rw [order_mul, nnreal.pow_enat_add], map_add' := λ x y, begin have : _ ≤ _ := order_add_ge x y, @@ -137,7 +35,7 @@ def valuation : valuation (power_series K) nnreal := rw [show (p : nnreal) = (p : ℕ), by rw coe_coe] at H, exact_mod_cast H, }, cases this with h h; [left, right], all_goals - { apply nnreal_of_enat_le _ inv_p_ne_zero _ _ _ h, + { apply nnreal.pow_enat_le _ inv_p_ne_zero _ _ _ h, rw [← linear_ordered_structure.inv_le_inv _ inv_p_ne_zero, inv_inv'', inv_one'], { apply le_of_lt, rw [show (p : nnreal) = (p : ℕ), by rw coe_coe], @@ -169,13 +67,13 @@ valuation.localization (power_series.valuation p K) $ λ φ h, begin rw localization.fraction_ring.mem_non_zero_divisors_iff_ne_zero at h, contrapose! h, - change nnreal_of_enat _ _ = 0 at h, + change (_ : nnreal) ^ φ.order = 0 at h, have inv_p_ne_zero : (p : nnreal)⁻¹ ≠ 0, { assume H, rw [← inv_inj'', inv_inv'', inv_zero'] at H, apply p.ne_zero, rw [show (p : nnreal) = (p : ℕ), by rw coe_coe] at H, exact_mod_cast H }, - rwa [← nnreal_of_enat_top, (nnreal_of_enat_inj _ inv_p_ne_zero _).eq_iff, + rwa [← nnreal.pow_enat_top, (nnreal.pow_enat_inj _ inv_p_ne_zero _).eq_iff, power_series.order_eq_top] at h, rw [← linear_ordered_structure.inv_lt_inv _ inv_p_ne_zero, inv_inv'', inv_one'], { rw [show (p : nnreal) = (p : ℕ), by rw coe_coe], @@ -186,12 +84,12 @@ end lemma non_trivial : ¬ (valuation p K).is_trivial := begin assume H, cases H (localization.of (power_series.X)) with h h; - erw valuation.localization_apply at h; change nnreal_of_enat _ _ = _ at h, + erw valuation.localization_apply at h; change _ ^ _ = _ at h, { apply p.ne_zero, rw [show (p : nnreal) = (p : ℕ), by rw coe_coe] at h, - simpa only [nnreal.inv_eq_zero, nnreal_of_enat_one, + simpa only [nnreal.inv_eq_zero, nnreal.pow_enat_one, nat.cast_eq_zero, power_series.order_X] using h, }, - { simp only [nnreal_of_enat_one, power_series.order_X] at h, + { simp only [nnreal.pow_enat_one, power_series.order_X] at h, rw [← inv_inj'', inv_inv'', inv_one'] at h, apply p.ne_one, rw [show (p : nnreal) = (p : ℕ), by rw coe_coe] at h, diff --git a/src/for_mathlib/nnreal.lean b/src/for_mathlib/nnreal.lean index 666a3dcd..e54200db 100644 --- a/src/for_mathlib/nnreal.lean +++ b/src/for_mathlib/nnreal.lean @@ -47,4 +47,119 @@ noncomputable instance : linear_ordered_comm_group_with_zero nnreal := .. (infer_instance : linear_order nnreal), .. (infer_instance : comm_semiring nnreal) } +section pow_enat +noncomputable theory +open_locale classical +open function + +/--If r is a nonnegative real number and n an enat, +than b^n is defined as expected if n is natural, and b^infty = 0. +Hence, this should only be applied to b < 1.-/ +def pow_enat : has_pow nnreal enat := +⟨λ r n, if h : n.dom then (r^n.get h) else 0⟩ + +local attribute [instance] pow_enat + +lemma pow_enat_def {b : nnreal} {n : enat} : + b^n = if h : n.dom then (b^n.get h) else 0 := rfl + +@[simp] lemma pow_enat_top (b : nnreal) : + b ^ (⊤ : enat) = 0 := +begin + rw [pow_enat_def, dif_neg], exact not_false +end + +@[simp] lemma pow_enat_zero (b : nnreal) : + b ^ (0 : enat) = 1 := +begin + rw [pow_enat_def, dif_pos, enat.get_zero, pow_zero], + exact trivial, +end + +@[simp] lemma pow_enat_one (b : nnreal) : + b ^ (1 : enat) = b := +begin + rw [pow_enat_def, dif_pos, enat.get_one, pow_one], + exact trivial, +end + +@[simp] lemma pow_enat_add (b : nnreal) (m n : enat) : + b ^ (m + n) = b ^ m * b ^ n := +begin + iterate 3 {rw pow_enat_def}, + by_cases hm : m.dom, + { by_cases hn : n.dom, + { have hmn : (m + n).dom := ⟨hm, hn⟩, + rw [dif_pos hm, dif_pos hn, dif_pos, + subtype.coe_ext, nnreal.coe_mul, ← nnreal.coe_mul, ← pow_add, enat.get_add, add_comm], + exact hmn, }, + { rw [dif_pos hm, dif_neg hn, dif_neg, mul_zero], + contrapose! hn with H, exact H.2 } }, + { rw [dif_neg hm, dif_neg, zero_mul], + contrapose! hm with H, exact H.1 }, +end + +@[simp] lemma pow_enat_le (b : nnreal) (h₁ : b ≠ 0) (h₂ : b ≤ 1) (m n : enat) (h : m ≤ n) : + b ^ n ≤ b ^ m := +begin + iterate 2 {rw pow_enat_def}, + by_cases hn : n.dom, + { rw ← enat.coe_get hn at h, + have hm : m.dom := enat.dom_of_le_some h, + rw [← enat.coe_get hm, enat.coe_le_coe] at h, + rw [dif_pos hm, dif_pos hn], + rw [← linear_ordered_structure.inv_le_inv _ h₁, inv_one'] at h₂, + have := pow_le_pow h₂ h, + -- We need lots of norm_cast lemmas + rwa [nnreal.coe_le, nnreal.coe_pow, nnreal.coe_pow, nnreal.coe_inv, ← pow_inv, ← pow_inv, + ← nnreal.coe_pow, ← nnreal.coe_pow, ← nnreal.coe_inv, ← nnreal.coe_inv, ← nnreal.coe_le, + linear_ordered_structure.inv_le_inv] at this, + any_goals { exact one_ne_zero }, + all_goals { contrapose! h₁ }, + any_goals { exact subtype.val_injective h₁ }, + any_goals { apply group_with_zero.pow_eq_zero, assumption } }, + { rw dif_neg hn, exact zero_le _ } +end + +@[simp] lemma pow_enat_lt (b : nnreal) (h₁ : b ≠ 0) (h₂ : b < 1) (m n : enat) (h : m < n) : + b ^ n < b ^ m := +begin + iterate 2 {rw pow_enat_def}, + by_cases hn : n.dom, + { rw ← enat.coe_get hn at h, + have hm : m.dom := enat.dom_of_le_some (le_of_lt h), + rw [← enat.coe_get hm, enat.coe_lt_coe] at h, + rw [dif_pos hm, dif_pos hn], + rw [← linear_ordered_structure.inv_lt_inv _ h₁, inv_one'] at h₂, + have := pow_lt_pow h₂ h, + -- We need lots of norm_cast lemmas + rwa [nnreal.coe_lt, nnreal.coe_pow, nnreal.coe_pow, nnreal.coe_inv, ← pow_inv, ← pow_inv, + ← nnreal.coe_pow, ← nnreal.coe_pow, ← nnreal.coe_inv, ← nnreal.coe_inv, ← nnreal.coe_lt, + linear_ordered_structure.inv_lt_inv] at this, + any_goals { exact one_ne_zero }, + all_goals { contrapose! h₁ }, + any_goals { exact subtype.val_injective h₁ }, + all_goals { apply group_with_zero.pow_eq_zero, assumption } }, + { rw dif_neg hn, + have : n = ⊤ := roption.eq_none_iff'.mpr hn, subst this, + replace h := ne_of_lt h, + rw enat.ne_top_iff at h, rcases h with ⟨m, rfl⟩, + rw dif_pos, swap, {trivial}, + apply pow_pos, + exact lt_of_le_of_ne b.2 h₁.symm } +end + +@[simp] lemma pow_enat_inj (b : nnreal) (h₁ : b ≠ 0) (h₂ : b < 1) : + injective ((^) b : enat → nnreal) := +begin + intros m n h, + wlog H : m ≤ n, + rcases lt_or_eq_of_le H with H|rfl, + { have := pow_enat_lt b h₁ h₂ m n H, + exfalso, exact ne_of_lt this h.symm, }, + { refl }, +end + +end pow_enat + end nnreal From ef6f92ef338ae648ffd5f092c28ac511050bbf19 Mon Sep 17 00:00:00 2001 From: Johan Commelin Date: Fri, 11 Oct 2019 17:11:20 +0200 Subject: [PATCH 23/37] WIP --- src/valuation/basic.lean | 30 +++++++++++++++++++++++++----- src/valuation/perfection.lean | 24 ++++++++++++++++++++++++ 2 files changed, 49 insertions(+), 5 deletions(-) diff --git a/src/valuation/basic.lean b/src/valuation/basic.lean index 54ce5bc6..c31dbb59 100644 --- a/src/valuation/basic.lean +++ b/src/valuation/basic.lean @@ -323,7 +323,17 @@ begin cases x; [left, {right, cases x}]; refl end -lemma is_trivial_iff_val_le_one {K : Type*} [division_ring K] {v : valuation K Γ₀} : +lemma is_equiv.is_trivial {v₁ : valuation R Γ₀} {v₂ : valuation R Γ'₀} (h : v₁.is_equiv v₂) : + v₁.is_trivial ↔ v₂.is_trivial := +begin + apply forall_congr, intro r, + exact or_congr h.eq_zero h.eq_one, +end + +section division_ring +variables {K : Type*} [division_ring K] + +lemma is_trivial_iff_val_le_one {v : valuation K Γ₀} : v.is_trivial ↔ ∀ x:K, v x ≤ 1 := begin split; intros h x, @@ -340,13 +350,23 @@ begin { push_neg at hx, exact ⟨_, hx⟩ } } end -lemma is_equiv.is_trivial {v₁ : valuation R Γ₀} {v₂ : valuation R Γ'₀} (h : v₁.is_equiv v₂) : - v₁.is_trivial ↔ v₂.is_trivial := +lemma exists_lt_one_of_not_trivial (v : valuation K Γ₀) (hv : ¬ v.is_trivial) : + ∃ x : K, v x < 1 ∧ v x ≠ 0 := begin - apply forall_congr, intro r, - exact or_congr h.eq_zero h.eq_one, + delta is_trivial at hv, push_neg at hv, rcases hv with ⟨x, h₁, h₂⟩, + by_cases hx : v x < 1, { use [x, hx, h₁] }, + use x⁻¹, + have xne : x ≠ 0, { rwa ← v.ne_zero_iff }, + rw [v.map_inv' xne, ← linear_ordered_structure.inv_lt_inv _ _, inv_inv'', inv_one', + ← v.map_inv' xne, v.ne_zero_iff], + { push_neg at hx, replace hx := lt_of_le_of_ne hx (ne.symm h₂), + exact ⟨hx, inv_ne_zero xne⟩ }, + { exact one_ne_zero }, + { rw [← v.map_inv' xne, v.ne_zero_iff], exact inv_ne_zero xne }, end +end division_ring + end trivial -- end of section section supp diff --git a/src/valuation/perfection.lean b/src/valuation/perfection.lean index 0f95b7c9..3225c28d 100644 --- a/src/valuation/perfection.lean +++ b/src/valuation/perfection.lean @@ -3,6 +3,7 @@ import field_theory.perfect_closure import for_mathlib.nnreal import valuation.basic +import valuation.discrete lemma iterate_frobenius_apply {α : Type*} [monoid α] (p n : ℕ) (a : α) : (frobenius α p)^[n] a = a^p^n := @@ -103,6 +104,14 @@ def perfection : valuation (perfect_closure R p) nnreal := congr, end } +lemma perfection_apply (n : ℕ) (r : R) : + v.perfection R p (quot.mk _ ⟨n, r⟩) = v r ^ (p ^ (-n : ℤ) : ℝ) := rfl + +@[simp] lemma perfection_of (r : R) : + v.perfection R p (perfect_closure.of R p r) = v r := +show (v r) ^ _ = v r, +by simp only [fpow_zero, int.coe_nat_zero, nnreal.rpow_one, neg_zero] + end namespace perfection @@ -169,6 +178,21 @@ begin assumption end +lemma non_discrete' (v : valuation K nnreal) (hv : ¬ v.is_trivial) : + (v.perfection K p).is_non_discrete := +begin + intros r hr, + by_cases H : v.perfection K p r = 0, + { rcases exists_lt_one_of_not_trivial _ hv with ⟨x, h₁, h₂⟩, + rw H, refine ⟨(perfect_closure.of K p x), _, _⟩, + { contrapose! h₂, rwa [perfection_of, le_zero_iff_eq] at h₂ }, + { rwa perfection_of } }, + sorry + -- { refine ⟨perfect_field.pth_root 1 r, _, _⟩, + -- { }, + -- { } } +end + end perfection end valuation From b033a81d68b427974280a917f1e692b125b06e1f Mon Sep 17 00:00:00 2001 From: Patrick Massot Date: Sat, 12 Oct 2019 20:21:19 +0200 Subject: [PATCH 24/37] Add API for characteristic and subrings --- src/for_mathlib/char_p.lean | 117 +++++++++++++++++++++++++++++++++++- src/for_mathlib/primes.lean | 12 ---- 2 files changed, 116 insertions(+), 13 deletions(-) diff --git a/src/for_mathlib/char_p.lean b/src/for_mathlib/char_p.lean index dbf49eca..33a5628d 100644 --- a/src/for_mathlib/char_p.lean +++ b/src/for_mathlib/char_p.lean @@ -1,6 +1,9 @@ import algebra.char_p import ring_theory.algebra import ring_theory.ideal_operations +import ring_theory.principal_ideal_domain + +open function lemma map_nat_cast {α : Type*} {β : Type*} [semiring α] [semiring β] (f : α → β) [is_semiring_hom f] (n : ℕ) : @@ -10,7 +13,20 @@ begin rw [nat.cast_succ, nat.cast_succ, is_semiring_hom.map_add f, ih, is_semiring_hom.map_one f], end -open function + +section +variables (p : nat.primes) (R : Type*) [semiring R] [char_p R p] +include p + +lemma ring_char.prime : nat.prime (ring_char R) := +by { rw ← ring_char.eq R ‹_›, exact p.2 } + +end + +instance ring_char.char (R : Type*) [semiring R] : char_p R (ring_char R) := +{ cast_eq_zero_iff := ring_char.spec R } + +section variables {K : Type*} {R : Type*} {p : ℕ} [discrete_field K] [nonzero_comm_ring R] [algebra K R] -- is_field_hom.injective is not general enough @@ -31,3 +47,102 @@ lemma char_p_algebra_over_field [char_p K p] : char_p R p := rw [← char_p.cast_eq_zero_iff K, ← this.eq_iff, algebra.map_zero, map_nat_cast (algebra_map R : K → R)], end } +end + +section char_p_subring +open int +variables {R : Type*} [comm_ring R] + +lemma nat.eq_of_dvd {p q : ℕ} (h : p ∣ q) (h' : q ∣ p) : p = q := +begin + cases h with n hn, + cases h' with m hm, + cases nat.eq_zero_or_pos p, + simp [h, hn], + rw [hn, mul_assoc, eq_comm, nat.mul_right_eq_self_iff h, nat.mul_eq_one_iff] at hm, + simp [hn, hm.1], +end + +lemma int.nat_abs_dvd_iff {p : ℤ} {n : ℕ} : nat_abs p ∣ n ↔ p ∣ n := +begin + split; intro h, + refine dvd_trans _ (coe_nat_dvd.mpr h), rw dvd_nat_abs, + rw ←coe_nat_dvd, + refine dvd_trans _ h, + rw nat_abs_dvd, +end + +lemma cast_nat_abs_zero (k : ℤ) (h : (k : R) = 0) : (nat_abs k : R) = 0 := +begin + cases nat_abs_eq k with hpos hneg, + show (((nat_abs k) : ℤ) : R) = 0, + rwa ←hpos, + show (((nat_abs k) : ℤ) : R) = 0, + rw eq_neg_of_eq_neg hneg, + simp [h], +end + +variables {S : Type*} [comm_ring S] {φ : R → S} [is_ring_hom φ] + +lemma int.cast_ump : (int.cast : ℤ → S) = φ ∘ (int.cast : ℤ → R) := +begin + ext k, + induction k using int.induction_on with k ih k ih, + { simp, + change ((0 : ℤ) : S) = φ ((0 : ℤ) : R), + rw [int.cast_zero, int.cast_zero, is_ring_hom.map_zero φ] }, + { rw [is_ring_hom.map_add (int.cast : ℤ → S), ih, + is_ring_hom.map_add (φ ∘ (int.cast : ℤ → R)), + is_ring_hom.map_one (φ ∘ (int.cast : ℤ → R))], + simp, + exact int.cast_one }, + { rw [is_ring_hom.map_sub (int.cast : ℤ → S), ih, + is_ring_hom.map_sub (φ ∘ (int.cast : ℤ → R)), + is_ring_hom.map_one (φ ∘ (int.cast : ℤ → R))], + simp, + exact int.cast_one } +end + +variables {T : Type*} [comm_ring T] {ψ : S → T} [is_ring_hom ψ] +open is_ring_hom + +lemma is_ring_hom.ker_eq_of_inj (h : injective ψ) : ker (ψ ∘ φ) = ker φ := +begin + ext x, + rw [mem_ker, mem_ker, comp_app, ←map_zero ψ], + exact ⟨λ H, h H, congr_arg ψ⟩ +end + +open ideal.is_principal + +lemma char_is_char : ring_char R = nat_abs (generator (is_ring_hom.ker (int.cast : ℤ → R))) := +begin + apply nat.eq_of_dvd, + { rw ← ring_char.spec R, + apply cast_nat_abs_zero, + have := generator_mem (is_ring_hom.ker (int.cast : ℤ → R)), + rwa is_ring_hom.mem_ker at this + }, + { rw [int.nat_abs_dvd_iff, ← mem_iff_generator_dvd, is_ring_hom.mem_ker], + apply char_p.cast_eq_zero } +end + +lemma subring_ring_char (h : injective φ) : ring_char R = ring_char S := +begin + rw [char_is_char, char_is_char], + suffices : is_ring_hom.ker (int.cast : ℤ → R) = is_ring_hom.ker (int.cast : ℤ → S), by rw this, + have : (int.cast : ℤ → S) = φ ∘ (int.cast : ℤ → R), from int.cast_ump, + simp only [this], + exact (is_ring_hom.ker_eq_of_inj h).symm +end + +lemma char_p_ring_char (p : nat.primes) : char_p R p ↔ ring_char R = p := +⟨λ h, (ring_char.eq R h).symm, λ h, h ▸ (classical.some_spec (char_p.exists_unique R)).1⟩ + +lemma subring_char_p (p : nat.primes) (h : injective φ) : char_p S p ↔ char_p R p := +begin + repeat { rw char_p_ring_char }, + rwa subring_ring_char h +end + +end char_p_subring diff --git a/src/for_mathlib/primes.lean b/src/for_mathlib/primes.lean index a533416c..93b30679 100644 --- a/src/for_mathlib/primes.lean +++ b/src/for_mathlib/primes.lean @@ -18,15 +18,3 @@ end primes end nat instance monoid.prime_pow {α : Type*} [monoid α]: has_pow α nat.primes := ⟨λ x p, x^p.val⟩ - -section -variables (p : nat.primes) (R : Type*) [semiring R] [char_p R p] -include p - -lemma ring_char.prime : nat.prime (ring_char R) := -by { rw ← ring_char.eq R ‹_›, exact p.2 } - -end - -instance ring_char.char (R : Type*) [semiring R] : char_p R (ring_char R) := -{ cast_eq_zero_iff := ring_char.spec R } From 2dbc1b2794a1e603bc9ab393d5863a491bf4bc79 Mon Sep 17 00:00:00 2001 From: Patrick Massot Date: Sat, 12 Oct 2019 20:22:40 +0200 Subject: [PATCH 25/37] WIP towards surjective completion Frobenius --- src/examples/char_p.lean | 81 +++++++++++++++++++++++++++++++++++++++- 1 file changed, 79 insertions(+), 2 deletions(-) diff --git a/src/examples/char_p.lean b/src/examples/char_p.lean index 4095232c..bd011d20 100644 --- a/src/examples/char_p.lean +++ b/src/examples/char_p.lean @@ -1,5 +1,5 @@ import ring_theory.power_series -import algebra.char_p +import algebra.char_p algebra.group_power import for_mathlib.nnreal import for_mathlib.char_p @@ -214,13 +214,81 @@ def clsp := completion (laurent_series_perfection K) end +section char_p_completion +open uniform_space +variables {R : Type*} [comm_ring R] [uniform_space R] [uniform_add_group R] [separated R] + [topological_ring R] (p : nat.primes) [char_p R p] + +instance completion.char_p : char_p (completion R) p := +(subring_char_p p (completion.uniform_embedding_coe R).inj).mpr ‹_› + +end char_p_completion + +section +open uniform_space +--variables (K : Type*) [discrete_field K] [topological_space K] [topological_division_ring K] +variables {G : Type*} [add_comm_group G] [uniform_space G] [uniform_add_group G] +variables {H : Type*} [add_comm_group H] [uniform_space H] [uniform_add_group H] +variables {φ : G → H} {ψ : H → G} (h : φ ∘ ψ = id) [is_add_group_hom φ] [is_add_group_hom ψ] + (hφ : continuous φ) (hψ : continuous ψ) +include h hφ hψ +local notation `hat` x:90 := completion.map x + +lemma johan : surjective hat φ := +have key : hat φ ∘ hat ψ = id, + by { rw [← completion.map_id, ← h], + exact completion.map_comp (uniform_continuous_of_continuous hφ) + (uniform_continuous_of_continuous hψ) }, +λ y, ⟨(hat ψ) y, congr_fun key _⟩ +end + +namespace uniform_space.completion +open uniform_space +variables {α : Type*} [ring α] [uniform_space α] [topological_ring α] [uniform_add_group α] + +local infix `^` := monoid.pow + +@[move_cast] +lemma coe_pow (a : α) (n : ℕ): ((a^n : α) : completion α) = a^n := +begin + induction n with n ih, + exact completion.coe_one _, + change ↑(a*a^n) = ↑a*↑a^n, + rw [coe_mul, ih], +end +end uniform_space.completion + +section +open uniform_space +variables (p : nat.primes) (K : Type) [discrete_field K] [char_p K p] [uniform_space K] + [uniform_add_group K] [topological_division_ring K] [separated K] + +lemma completion.frobenius_eq : frobenius (completion K) p = completion.map (frobenius K p) := +begin + symmetry, + apply completion.map_unique, + { haveI hom : is_ring_hom (frobenius (completion K) p) := by { + apply frobenius.is_ring_hom _, + exact p.property, + exact completion.char_p _, + }, + haveI : topological_monoid (completion K) := topological_ring.to_topological_monoid _, + exact uniform_continuous_of_continuous (continuous_pow p) + }, + { intro x, + simp [frobenius], + erw completion.coe_pow, + refl } +end +end + namespace clsp open uniform_space variables (p : nat.primes) (K : Type) [discrete_field K] [char_p K p] include p local attribute [instance] valued.subgroups_basis subgroups_basis.topology - ring_filter_basis.topological_ring valued.uniform_space + ring_filter_basis.topological_ring valued.uniform_space valued.uniform_add_group instance : discrete_field (clsp p K) := completion.discrete_field instance : uniform_space (clsp p K) := completion.uniform_space _ @@ -232,6 +300,15 @@ def valuation : valuation (clsp p K) nnreal := valued.extension_valuation lemma frobenius_surjective : surjective (frobenius (clsp p K) p) := begin + dsimp [clsp], + set lsp := (laurent_series_perfection K), + haveI char : char_p lsp ↑p := sorry, + rw completion.frobenius_eq, + obtain ⟨ψ, inv, cont⟩ : ∃ ψ : (laurent_series_perfection K) → (laurent_series_perfection K), + (frobenius lsp p) ∘ ψ = id ∧ continuous ψ, + { + sorry }, + sorry end From ece3fa960af3ac1c34ed888ab41301f12e60001f Mon Sep 17 00:00:00 2001 From: Kevin Buzzard Date: Sun, 13 Oct 2019 10:14:08 +0100 Subject: [PATCH 26/37] apparently priority 10 is preferred to 0? --- src/valuation/topology.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/valuation/topology.lean b/src/valuation/topology.lean index 4c9bcaea..ffaedd5a 100644 --- a/src/valuation/topology.lean +++ b/src/valuation/topology.lean @@ -11,7 +11,7 @@ In this file, we define the topology induced by a valuation on a ring. local attribute [instance] classical.prop_decidable noncomputable theory -local attribute [instance, priority 0] classical.decidable_linear_order +local attribute [instance, priority 10] classical.decidable_linear_order open set valuation linear_ordered_structure From e9c461863482259c3c92d64d8cc29310e53201ac Mon Sep 17 00:00:00 2001 From: Kevin Buzzard Date: Sun, 13 Oct 2019 10:14:45 +0100 Subject: [PATCH 27/37] proposal of definition of perfectoid field --- src/perfectoid_field.lean | 47 +++++++++++++++++++++++++++++++++++++++ 1 file changed, 47 insertions(+) create mode 100644 src/perfectoid_field.lean diff --git a/src/perfectoid_field.lean b/src/perfectoid_field.lean new file mode 100644 index 00000000..a53a7417 --- /dev/null +++ b/src/perfectoid_field.lean @@ -0,0 +1,47 @@ +import valuation.topology +import examples.char_p +import Frobenius + +set_option old_structure_cmd true -- do we do this or not? + +class nondiscrete_valued_field (K : Type*) extends discrete_field K := +(v : valuation K nnreal) +(non_discrete : ∀ ε : nnreal, 0 < ε → ∃ x : K, 1 < v x ∧ v x < 1 + ε) + +noncomputable instance foo {K : Type} + [nondiscrete_valued_field K] : valued K := +{ Γ₀ := nnreal, + v := nondiscrete_valued_field.v K} + +-- Currently we know that clsp is a complete uniform topological field. +-- And this all comes from the completion machine + +open function nat + +local attribute [instance] valued.uniform_space valued.uniform_add_group +local notation `v` := valued.value + +noncomputable example (K : Type) [nondiscrete_valued_field K] : uniform_space K +:= by apply_instance + +-- separated should follow from the fact that the kernel of v is 0 +-- but I don't know how to steer it and I don't know if we need it. + +instance nondiscrete_valued_field.separated (K : Type) [nondiscrete_valued_field K] : + separated K := sorry + +local attribute [instance, priority 1000] comm_ring.to_ring + +class is_perfectoid_field (K : Type) [nondiscrete_valued_field K] (p : primes) : Prop := +[complete : complete_space K] +(Frobenius : surjective (Frob (valued.v K).le_one_subring ∕p)) + +-- Let K be the completion of the perfection of (Z/pZ)((t)). [done] +-- Show that K is a perfectoid field +-- show a perfectoid field is a perfectoid ring +-- Show that Spa(K) is a perfectoid space. + +-- is a valued R a Huber ring? + +theorem perfectoid_field.huber_ring (K : Type) (p : primes) + [nondiscrete_valued_field K] [is_perfectoid_field K p] : Huber_ring K := From 2c62cea322c0654f6132d7553c6551aceaed6a48 Mon Sep 17 00:00:00 2001 From: Kevin Buzzard Date: Sun, 13 Oct 2019 11:22:35 +0100 Subject: [PATCH 28/37] removing error at end of file --- src/perfectoid_field.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/perfectoid_field.lean b/src/perfectoid_field.lean index a53a7417..2e8adf57 100644 --- a/src/perfectoid_field.lean +++ b/src/perfectoid_field.lean @@ -13,7 +13,7 @@ noncomputable instance foo {K : Type} { Γ₀ := nnreal, v := nondiscrete_valued_field.v K} --- Currently we know that clsp is a complete uniform topological field. +-- Currently we know that clsp is a complete uniform topological field. -- And this all comes from the completion machine open function nat @@ -44,4 +44,4 @@ class is_perfectoid_field (K : Type) [nondiscrete_valued_field K] (p : primes) : -- is a valued R a Huber ring? theorem perfectoid_field.huber_ring (K : Type) (p : primes) - [nondiscrete_valued_field K] [is_perfectoid_field K p] : Huber_ring K := + [nondiscrete_valued_field K] [is_perfectoid_field K p] : Huber_ring K := sorry From 7fd90211690e41e6bc22f8c9667df66abbeaed88 Mon Sep 17 00:00:00 2001 From: Patrick Massot Date: Mon, 14 Oct 2019 00:09:23 +0200 Subject: [PATCH 29/37] Begin raising a valuation to a pnat power --- src/examples/valuations.lean | 62 ++++++++++++++++++++++++++++++++++++ 1 file changed, 62 insertions(+) create mode 100644 src/examples/valuations.lean diff --git a/src/examples/valuations.lean b/src/examples/valuations.lean new file mode 100644 index 00000000..840582a8 --- /dev/null +++ b/src/examples/valuations.lean @@ -0,0 +1,62 @@ +/- +Stuff in this file should eventually go to the valuation folder, +but keeping it here is faster at this point. +-/ + +import valuation.basic + +local attribute [instance, priority 0] classical.decidable_linear_order + +section +@[elab_as_eliminator] protected lemma pnat.induction_on {p : ℕ+ → Prop} + (i : ℕ+) (hz : p 1) (hp : ∀j : ℕ+, p j → p (j + 1)) : p i := +begin + sorry +end + +variables (Γ₀ : Type*) [linear_ordered_comm_group_with_zero Γ₀] +open linear_ordered_structure + +lemma linear_ordered_comm_group_with_zero.pow_strict_mono (n : ℕ+) : strict_mono (λ x : Γ₀, x^(n : ℕ)) := +begin + intros x y h, + induction n using pnat.induction_on with n ih, + { simpa }, + { simp only [] at *, + rw [pnat.add_coe, pnat.one_coe, pow_succ, pow_succ], -- here we miss some norm_cast attribute + by_cases hx : x = 0, + { simp [hx] at *, + + sorry }, + { -- do x * ih (using that x ≠ 0) and then h * y^n (using 0 < x^n < y^n) + sorry } } +end + +lemma linear_ordered_comm_group_with_zero.pow_mono (n : ℕ+) : monotone (λ x : Γ₀, x^(n : ℕ)) := +(linear_ordered_comm_group_with_zero.pow_strict_mono Γ₀ n).monotone + +variables {Γ₀} +lemma linear_ordered_comm_group_with_zero.pow_le_pow {x y : Γ₀} {n : ℕ+} : x^(n : ℕ) ≤ y^(n : ℕ) ↔ x ≤ y := +strict_mono.le_iff_le (linear_ordered_comm_group_with_zero.pow_strict_mono Γ₀ n) + +end + +variables {R : Type*} [ring R] + +variables {Γ₀ : Type*} [linear_ordered_comm_group_with_zero Γ₀] + +instance valuation.pow : has_pow (valuation R Γ₀) ℕ+ := +⟨λ v n, { to_fun := λ r, (v r)^n.val, + map_one' := by rw [v.map_one, one_pow], + map_mul' := λ x y, by rw [v.map_mul, mul_pow], + map_zero' := by rw [valuation.map_zero, ← nat.succ_pred_eq_of_pos n.2, pow_succ, zero_mul], + map_add' := begin + intros x y, + wlog vyx : v y ≤ v x using x y, + { have : (v y)^n.val ≤ (v x)^n.val, by apply linear_ordered_comm_group_with_zero.pow_mono ; assumption, + rw max_eq_left this, + apply linear_ordered_comm_group_with_zero.pow_mono, + convert v.map_add x y, + rw max_eq_left vyx }, + { rwa [add_comm, max_comm] }, + end }⟩ From 983fc781905d5c11b40f73119a8d0c1e3b45566c Mon Sep 17 00:00:00 2001 From: Johan Commelin Date: Mon, 14 Oct 2019 07:08:33 +0200 Subject: [PATCH 30/37] Two of Patrick's sorrys done --- src/examples/valuations.lean | 13 +++++++++---- src/for_mathlib/group_with_zero.lean | 9 +++++++++ 2 files changed, 18 insertions(+), 4 deletions(-) diff --git a/src/examples/valuations.lean b/src/examples/valuations.lean index 840582a8..93c261ac 100644 --- a/src/examples/valuations.lean +++ b/src/examples/valuations.lean @@ -11,7 +11,12 @@ section @[elab_as_eliminator] protected lemma pnat.induction_on {p : ℕ+ → Prop} (i : ℕ+) (hz : p 1) (hp : ∀j : ℕ+, p j → p (j + 1)) : p i := begin - sorry + cases i with i hi, + rcases nat.exists_eq_succ_of_ne_zero (ne_of_gt hi) with ⟨i, rfl⟩, + induction i with i IH, {assumption}, + have h : 0 < i + 1, {exact nat.succ_pos i}, + apply hp ⟨i+1, h⟩, + exact IH _, end variables (Γ₀ : Type*) [linear_ordered_comm_group_with_zero Γ₀] @@ -25,9 +30,9 @@ begin { simp only [] at *, rw [pnat.add_coe, pnat.one_coe, pow_succ, pow_succ], -- here we miss some norm_cast attribute by_cases hx : x = 0, - { simp [hx] at *, - - sorry }, + { subst x, rw group_with_zero.zero_pow_pnat at ih ⊢, rw zero_mul, + let := (group_with_zero.mk₀ _ (ne_of_gt h)) * (group_with_zero.mk₀ _ (ne_of_gt ih)), + exact zero_lt_unit this, }, { -- do x * ih (using that x ≠ 0) and then h * y^n (using 0 < x^n < y^n) sorry } } end diff --git a/src/for_mathlib/group_with_zero.lean b/src/for_mathlib/group_with_zero.lean index b3c22b01..87f96f81 100644 --- a/src/for_mathlib/group_with_zero.lean +++ b/src/for_mathlib/group_with_zero.lean @@ -214,6 +214,15 @@ end lemma pow_ne_zero {a : α} {n : ℕ} (h : a ≠ 0) : a^n ≠ 0 := assume H, h $ eq_zero_of_pow_eq_zero H +lemma zero_pow (n : ℕ) (hn : n ≠ 0) : (0:α)^n = 0 := +begin + rcases nat.exists_eq_succ_of_ne_zero hn with ⟨n,rfl⟩, + rw [pow_succ, zero_mul], refl +end + +lemma zero_pow_pnat (n : ℕ+) : (0:α)^(n:ℕ) = 0 := +zero_pow n (ne_of_gt n.2) + theorem pow_sub (a : α) {m n : ℕ} (ha : a ≠ 0) (h : n ≤ m) : a^(m - n) = a^m * (a^n)⁻¹ := have h1 : m - n + n = m, from nat.sub_add_cancel h, have h2 : a^(m - n) * a^n = a^m, by rw [←pow_add, h1], From fea815ae4794b9e56bb2643f38b90dade5eee49d Mon Sep 17 00:00:00 2001 From: Johan Commelin Date: Mon, 14 Oct 2019 09:33:00 +0200 Subject: [PATCH 31/37] Remove a sorry, golf the proof --- src/examples/valuations.lean | 12 +++--------- 1 file changed, 3 insertions(+), 9 deletions(-) diff --git a/src/examples/valuations.lean b/src/examples/valuations.lean index 93c261ac..96bd66ae 100644 --- a/src/examples/valuations.lean +++ b/src/examples/valuations.lean @@ -25,16 +25,10 @@ open linear_ordered_structure lemma linear_ordered_comm_group_with_zero.pow_strict_mono (n : ℕ+) : strict_mono (λ x : Γ₀, x^(n : ℕ)) := begin intros x y h, - induction n using pnat.induction_on with n ih, - { simpa }, - { simp only [] at *, + induction n using pnat.induction_on with n ih, { simpa }, + { dsimp only [] at *, rw [pnat.add_coe, pnat.one_coe, pow_succ, pow_succ], -- here we miss some norm_cast attribute - by_cases hx : x = 0, - { subst x, rw group_with_zero.zero_pow_pnat at ih ⊢, rw zero_mul, - let := (group_with_zero.mk₀ _ (ne_of_gt h)) * (group_with_zero.mk₀ _ (ne_of_gt ih)), - exact zero_lt_unit this, }, - { -- do x * ih (using that x ≠ 0) and then h * y^n (using 0 < x^n < y^n) - sorry } } + apply linear_ordered_structure.mul_lt_mul' h ih, } end lemma linear_ordered_comm_group_with_zero.pow_mono (n : ℕ+) : monotone (λ x : Γ₀, x^(n : ℕ)) := From dfe61cfc95a8586bb255faa5042a01330e3738b9 Mon Sep 17 00:00:00 2001 From: Johan Commelin Date: Mon, 14 Oct 2019 10:29:00 +0200 Subject: [PATCH 32/37] Powers of valuations are equivalent --- src/examples/valuations.lean | 35 +++++++++++++++++++++++++++++------ 1 file changed, 29 insertions(+), 6 deletions(-) diff --git a/src/examples/valuations.lean b/src/examples/valuations.lean index 96bd66ae..d513a3f4 100644 --- a/src/examples/valuations.lean +++ b/src/examples/valuations.lean @@ -40,22 +40,45 @@ strict_mono.le_iff_le (linear_ordered_comm_group_with_zero.pow_strict_mono Γ₀ end +namespace valuation variables {R : Type*} [ring R] +variables {Γ₀ : Type*} [linear_ordered_comm_group_with_zero Γ₀] +variables (v : valuation R Γ₀) -variables {Γ₀ : Type*} [linear_ordered_comm_group_with_zero Γ₀] - -instance valuation.pow : has_pow (valuation R Γ₀) ℕ+ := -⟨λ v n, { to_fun := λ r, (v r)^n.val, +instance : has_pow (valuation R Γ₀) ℕ+ := +⟨λ v n, { to_fun := λ r, (v r)^(n : ℕ), map_one' := by rw [v.map_one, one_pow], map_mul' := λ x y, by rw [v.map_mul, mul_pow], - map_zero' := by rw [valuation.map_zero, ← nat.succ_pred_eq_of_pos n.2, pow_succ, zero_mul], + map_zero' := show (v 0)^n.val = 0, + by rw [valuation.map_zero, ← nat.succ_pred_eq_of_pos n.2, pow_succ, zero_mul], map_add' := begin intros x y, wlog vyx : v y ≤ v x using x y, - { have : (v y)^n.val ≤ (v x)^n.val, by apply linear_ordered_comm_group_with_zero.pow_mono ; assumption, + { have : (v y)^(n:ℕ) ≤ (v x)^(n:ℕ), + by apply linear_ordered_comm_group_with_zero.pow_mono ; assumption, rw max_eq_left this, apply linear_ordered_comm_group_with_zero.pow_mono, convert v.map_add x y, rw max_eq_left vyx }, { rwa [add_comm, max_comm] }, end }⟩ + +@[simp] protected lemma pow_one : v^(1:ℕ+) = v := +ext $ λ r, pow_one (v r) + +protected lemma pow_mul (m n : ℕ+) : v^(m*n) = (v^m)^n := +ext $ λ r, pow_mul (v r) m n + +lemma is_equiv_of_pow (v : valuation R Γ₀) (m n : ℕ+) : is_equiv (v^m) (v^n) := +begin + intros r s, + change (v r) ^ (m:ℕ) ≤ (v s) ^ (m:ℕ) ↔ _, + rw [← linear_ordered_comm_group_with_zero.pow_le_pow, ← pow_mul, ← pow_mul, + mul_comm, pow_mul, pow_mul, linear_ordered_comm_group_with_zero.pow_le_pow], + { exact iff.rfl } +end + +lemma is_equiv_of_pow_self (v : valuation R Γ₀) (n : ℕ+) : is_equiv v (v^n) := +by simpa using v.is_equiv_of_pow 1 n + +end valuation From cf4f6cba89bccfbf0eb6b9833cb132cb4d14abfd Mon Sep 17 00:00:00 2001 From: Johan Commelin Date: Mon, 14 Oct 2019 10:32:11 +0200 Subject: [PATCH 33/37] Better names --- src/examples/valuations.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/examples/valuations.lean b/src/examples/valuations.lean index d513a3f4..4cc0d18b 100644 --- a/src/examples/valuations.lean +++ b/src/examples/valuations.lean @@ -69,7 +69,7 @@ ext $ λ r, pow_one (v r) protected lemma pow_mul (m n : ℕ+) : v^(m*n) = (v^m)^n := ext $ λ r, pow_mul (v r) m n -lemma is_equiv_of_pow (v : valuation R Γ₀) (m n : ℕ+) : is_equiv (v^m) (v^n) := +lemma is_equiv_pow_pow (v : valuation R Γ₀) (m n : ℕ+) : is_equiv (v^m) (v^n) := begin intros r s, change (v r) ^ (m:ℕ) ≤ (v s) ^ (m:ℕ) ↔ _, @@ -78,7 +78,7 @@ begin { exact iff.rfl } end -lemma is_equiv_of_pow_self (v : valuation R Γ₀) (n : ℕ+) : is_equiv v (v^n) := -by simpa using v.is_equiv_of_pow 1 n +lemma is_equiv_pow_self (v : valuation R Γ₀) (n : ℕ+) : is_equiv v (v^n) := +by simpa using v.is_equiv_pow_pow 1 n end valuation From 47d63729b168a3c8fb3add0db4d12824e3a56e02 Mon Sep 17 00:00:00 2001 From: Johan Commelin Date: Mon, 14 Oct 2019 11:43:21 +0200 Subject: [PATCH 34/37] Is this sorry even provable? --- src/examples/valuations.lean | 31 +++++++++++++++++++++++++++++++ 1 file changed, 31 insertions(+) diff --git a/src/examples/valuations.lean b/src/examples/valuations.lean index 4cc0d18b..04272b32 100644 --- a/src/examples/valuations.lean +++ b/src/examples/valuations.lean @@ -4,6 +4,7 @@ but keeping it here is faster at this point. -/ import valuation.basic +import valuation.topology local attribute [instance, priority 0] classical.decidable_linear_order @@ -43,6 +44,7 @@ end namespace valuation variables {R : Type*} [ring R] variables {Γ₀ : Type*} [linear_ordered_comm_group_with_zero Γ₀] +variables {Γ'₀ : Type*} [linear_ordered_comm_group_with_zero Γ'₀] variables (v : valuation R Γ₀) instance : has_pow (valuation R Γ₀) ℕ+ := @@ -81,4 +83,33 @@ end lemma is_equiv_pow_self (v : valuation R Γ₀) (n : ℕ+) : is_equiv v (v^n) := by simpa using v.is_equiv_pow_pow 1 n +namespace is_equiv + +open_locale uniformity + +lemma uniformity_eq_aux (h₁ : valued R) (h₂ : valued R) (h : h₁.v.is_equiv h₂.v) : + @valued.uniform_space R _ h₁ ≤ id (@valued.uniform_space R _ h₂) := +begin + rw ← uniform_space_comap_id, + rw ← uniform_continuous_iff, + apply @uniform_continuous_of_continuous R R + (@valued.uniform_space R _ h₁) _ (@valued.uniform_add_group R _ h₁) + (@valued.uniform_space R _ h₂) _ (@valued.uniform_add_group R _ h₂), + apply @topological_add_group.continuous_of_continuous_at_zero _ _ _ _ _ _ _ _ _ _ _, + any_goals { apply_instance }, + { exact @uniform_add_group.to_topological_add_group R (@valued.uniform_space R _ h₁) _ (@valued.uniform_add_group R _ h₁), }, + { exact @uniform_add_group.to_topological_add_group R (@valued.uniform_space R _ h₂) _ (@valued.uniform_add_group R _ h₂), }, + { intros U, + rw [id.def, filter.map_id, valued.mem_nhds_zero, (@valued.mem_nhds_zero R _ h₁ U)], + rintros ⟨γ, hU⟩, + sorry -- is this provable with the current definitions?? + }, +end + +lemma uniformity_eq (h₁ : valued R) (h₂ : valued R) (h : h₁.v.is_equiv h₂.v) : + @valued.uniform_space R _ h₁ = @valued.uniform_space R _ h₂ := +le_antisymm (h.uniformity_eq_aux h₁ h₂) (h.symm.uniformity_eq_aux h₂ h₁) + +end is_equiv + end valuation From 31967efac84e2195e788b2002ada243f828f6eca Mon Sep 17 00:00:00 2001 From: Johan Commelin Date: Mon, 14 Oct 2019 14:50:35 +0200 Subject: [PATCH 35/37] Make valuations indexed by parameter --- src/examples/char_p.lean | 105 +++++++++++++++++----------------- src/valuation/perfection.lean | 28 ++++----- 2 files changed, 66 insertions(+), 67 deletions(-) diff --git a/src/examples/char_p.lean b/src/examples/char_p.lean index bd011d20..98d92d6b 100644 --- a/src/examples/char_p.lean +++ b/src/examples/char_p.lean @@ -16,11 +16,10 @@ local postfix `ᵒ` : 66 := power_bounded_subring local attribute [instance] nnreal.pow_enat namespace power_series -variables (p : nat.primes) -variables (K : Type*) [discrete_field K] [char_p K p] +variables (K : Type*) [discrete_field K] -def valuation : valuation (power_series K) nnreal := -{ to_fun := λ φ, (p⁻¹) ^ φ.order, +def valuation (b : {r : nnreal // 0 < r ∧ r < 1}) : valuation (power_series K) nnreal := +{ to_fun := λ φ, b ^ φ.order, map_zero' := by rw [order_zero, nnreal.pow_enat_top], map_one' := by rw [order_one, nnreal.pow_enat_zero], map_mul' := λ x y, by rw [order_mul, nnreal.pow_enat_add], @@ -29,18 +28,11 @@ def valuation : valuation (power_series K) nnreal := have : _ ≤ _ := order_add_ge x y, rw min_le_iff at this, rw le_max_iff, - have inv_p_ne_zero : (p : nnreal)⁻¹ ≠ 0, - { assume H, rw [← inv_inj'', inv_inv'', inv_zero'] at H, - apply p.ne_zero, - rw [show (p : nnreal) = (p : ℕ), by rw coe_coe] at H, exact_mod_cast H, }, + have b_ne_zero : (b : nnreal) ≠ 0 := ne_of_gt b.2.left, cases this with h h; [left, right], all_goals - { apply nnreal.pow_enat_le _ inv_p_ne_zero _ _ _ h, - rw [← linear_ordered_structure.inv_le_inv _ inv_p_ne_zero, inv_inv'', inv_one'], - { apply le_of_lt, - rw [show (p : nnreal) = (p : ℕ), by rw coe_coe], - exact_mod_cast p.one_lt, }, - { exact one_ne_zero } }, + { apply nnreal.pow_enat_le _ b_ne_zero _ _ _ h, + exact le_of_lt b.2.right, }, end } end power_series @@ -62,38 +54,27 @@ algebra.of_ring_hom (localization.of ∘ power_series.C K) $ variables [char_p K p] -def valuation : valuation (laurent_series K) nnreal := -valuation.localization (power_series.valuation p K) $ λ φ h, +def valuation (b : {r : nnreal // 0 < r ∧ r < 1}) : valuation (laurent_series K) nnreal := +valuation.localization (power_series.valuation K b) $ λ φ h, begin rw localization.fraction_ring.mem_non_zero_divisors_iff_ne_zero at h, contrapose! h, change (_ : nnreal) ^ φ.order = 0 at h, - have inv_p_ne_zero : (p : nnreal)⁻¹ ≠ 0, - { assume H, rw [← inv_inj'', inv_inv'', inv_zero'] at H, - apply p.ne_zero, - rw [show (p : nnreal) = (p : ℕ), by rw coe_coe] at H, - exact_mod_cast H }, - rwa [← nnreal.pow_enat_top, (nnreal.pow_enat_inj _ inv_p_ne_zero _).eq_iff, - power_series.order_eq_top] at h, - rw [← linear_ordered_structure.inv_lt_inv _ inv_p_ne_zero, inv_inv'', inv_one'], - { rw [show (p : nnreal) = (p : ℕ), by rw coe_coe], - exact_mod_cast p.one_lt }, - { exact one_ne_zero } + have b_ne_zero : (b : nnreal) ≠ 0 := ne_of_gt b.2.left, + rw ← power_series.order_eq_top, + apply (nnreal.pow_enat_inj _ b_ne_zero b.2.right), + rwa nnreal.pow_enat_top, end -lemma non_trivial : ¬ (valuation p K).is_trivial := +lemma non_trivial (b : {r : nnreal // 0 < r ∧ r < 1}) : ¬ (valuation K b).is_trivial := begin + have b_ne_zero : (b : nnreal) ≠ 0 := ne_of_gt b.2.left, assume H, cases H (localization.of (power_series.X)) with h h; erw valuation.localization_apply at h; change _ ^ _ = _ at h, - { apply p.ne_zero, - rw [show (p : nnreal) = (p : ℕ), by rw coe_coe] at h, - simpa only [nnreal.inv_eq_zero, nnreal.pow_enat_one, - nat.cast_eq_zero, power_series.order_X] using h, }, + { apply b_ne_zero, + simpa only [nnreal.pow_enat_one, power_series.order_X] using h }, { simp only [nnreal.pow_enat_one, power_series.order_X] at h, - rw [← inv_inj'', inv_inv'', inv_one'] at h, - apply p.ne_one, - rw [show (p : nnreal) = (p : ℕ), by rw coe_coe] at h, - exact_mod_cast h } + exact ne_of_lt b.2.right h, }, end local attribute [instance] algebra @@ -114,19 +95,20 @@ instance : discrete_field (laurent_series_perfection K) := @perfect_closure.discrete_field (laurent_series K) _ _ (ring_char.prime p K) $ by { rw ← ring_char.eq K hp, apply_instance } -def valuation : valuation (laurent_series_perfection K) nnreal := -@valuation.perfection (laurent_series K) _ (laurent_series.valuation p K) +def valuation (b : {r : nnreal // 0 < r ∧ r < 1}) : + valuation (laurent_series_perfection K) nnreal := +@valuation.perfection (laurent_series K) _ (laurent_series.valuation K b) (ring_char K) (ring_char.prime p _) $ by { rw ← ring_char.eq K hp, apply_instance } -lemma non_discrete (ε : nnreal) (h : 0 < ε) : - ∃ x : laurent_series_perfection K, 1 < valuation p K x ∧ valuation p K x < 1 + ε := +lemma non_discrete (b : {r : nnreal // 0 < r ∧ r < 1}) (ε : nnreal) (h : 0 < ε) : + ∃ x : laurent_series_perfection K, 1 < valuation p K b x ∧ valuation p K b x < 1 + ε := @valuation.perfection.non_discrete _ _ _ (ring_char.prime p _) -(by { rw ← ring_char.eq K hp, apply_instance }) _ (laurent_series.non_trivial p K) ε h +(by { rw ← ring_char.eq K hp, apply_instance }) _ (laurent_series.non_trivial K b) ε h -lemma non_trivial : ¬ (valuation p K).is_trivial := +lemma non_trivial (b : {r : nnreal // 0 < r ∧ r < 1}) : ¬ (valuation p K b).is_trivial := begin - rcases non_discrete p K 2 (by norm_num) with ⟨x, h₁, h₂⟩, + rcases non_discrete p K b 2 (by norm_num) with ⟨x, h₁, h₂⟩, contrapose! h₁, cases h₁ x with h h; rw h, exact zero_le _, end @@ -152,8 +134,24 @@ namespace laurent_series_perfection variables (p : nat.primes) (K : Type) [discrete_field K] [char_p K p] include p -instance : valued (laurent_series_perfection K) := -{ Γ₀ := nnreal, v := valuation p K } +protected def valued (b : {r : nnreal // 0 < r ∧ r < 1}) : valued (laurent_series_perfection K) := +{ Γ₀ := nnreal, v := valuation p K b } + +def valued_p : valued (laurent_series_perfection K) := +laurent_series_perfection.valued p K ⟨p⁻¹, +begin + have p_inv_ne_zero : (p⁻¹ : nnreal) ≠ 0, + { assume H, apply p.ne_zero, + rw [← inv_inj'', inv_zero', inv_inv'', eq_comm, (show (p:nnreal) = (p:ℕ), by rw coe_coe)] at H, + exact_mod_cast H.symm, }, + split, + { exact lt_of_le_of_ne (zero_le _) p_inv_ne_zero.symm, }, + { rw [← linear_ordered_structure.inv_lt_inv, inv_one', inv_inv'', + (show (p:nnreal) = (p:ℕ), by rw coe_coe)], + { exact_mod_cast p.one_lt }, + { exact one_ne_zero }, + { exact p_inv_ne_zero } } +end⟩ end laurent_series_perfection @@ -207,7 +205,7 @@ variables (p : nat.primes) (K : Type) [discrete_field K] [char_p K p] include p local attribute [instance] valued.subgroups_basis subgroups_basis.topology - ring_filter_basis.topological_ring valued.uniform_space + ring_filter_basis.topological_ring valued.uniform_space laurent_series_perfection.valued_p /-- The completion of the perfection of the Laurent series over a field. -/ def clsp := completion (laurent_series_perfection K) @@ -289,6 +287,7 @@ include p local attribute [instance] valued.subgroups_basis subgroups_basis.topology ring_filter_basis.topological_ring valued.uniform_space valued.uniform_add_group + laurent_series_perfection.valued_p instance : discrete_field (clsp p K) := completion.discrete_field instance : uniform_space (clsp p K) := completion.uniform_space _ @@ -312,14 +311,14 @@ begin sorry end -instance laurent_series_valued : valued (laurent_series K) := -{ Γ₀ := nnreal, v := laurent_series.valuation p K } +-- instance laurent_series_valued : valued (laurent_series K) := +-- { Γ₀ := nnreal, v := laurent_series.valuation p K } -protected def algebra : algebra (laurent_series_perfection K) (clsp p K) := -algebra.of_ring_hom - (coe : (laurent_series_perfection K) → completion (laurent_series_perfection K)) $ -@completion.is_ring_hom_coe (laurent_series_perfection K) _ _ _ $ -@valued.uniform_add_group (laurent_series_perfection K) _ $ laurent_series_perfection.valued p K +-- protected def algebra : algebra (laurent_series_perfection K) (clsp p K) := +-- algebra.of_ring_hom +-- (coe : (laurent_series_perfection K) → completion (laurent_series_perfection K)) $ +-- @completion.is_ring_hom_coe (laurent_series_perfection K) _ _ _ $ +-- @valued.uniform_add_group (laurent_series_perfection K) _ $ laurent_series_perfection.valued p K -- def rod_algebra : algebra (power_series K) (clsp p K) := -- @algebra.comap.algebra _ _ _ _ _ _ _ $ diff --git a/src/valuation/perfection.lean b/src/valuation/perfection.lean index 3225c28d..5072ffb5 100644 --- a/src/valuation/perfection.lean +++ b/src/valuation/perfection.lean @@ -178,20 +178,20 @@ begin assumption end -lemma non_discrete' (v : valuation K nnreal) (hv : ¬ v.is_trivial) : - (v.perfection K p).is_non_discrete := -begin - intros r hr, - by_cases H : v.perfection K p r = 0, - { rcases exists_lt_one_of_not_trivial _ hv with ⟨x, h₁, h₂⟩, - rw H, refine ⟨(perfect_closure.of K p x), _, _⟩, - { contrapose! h₂, rwa [perfection_of, le_zero_iff_eq] at h₂ }, - { rwa perfection_of } }, - sorry - -- { refine ⟨perfect_field.pth_root 1 r, _, _⟩, - -- { }, - -- { } } -end +-- lemma non_discrete' (v : valuation K nnreal) (hv : ¬ v.is_trivial) : +-- (v.perfection K p).is_non_discrete := +-- begin +-- intros r hr, +-- by_cases H : v.perfection K p r = 0, +-- { rcases exists_lt_one_of_not_trivial _ hv with ⟨x, h₁, h₂⟩, +-- rw H, refine ⟨(perfect_closure.of K p x), _, _⟩, +-- { contrapose! h₂, rwa [perfection_of, le_zero_iff_eq] at h₂ }, +-- { rwa perfection_of } }, +-- sorry +-- -- { refine ⟨perfect_field.pth_root 1 r, _, _⟩, +-- -- { }, +-- -- { } } +-- end end perfection From 4cc5012498ad77dde76af709750bfca6411c77a6 Mon Sep 17 00:00:00 2001 From: Johan Commelin Date: Mon, 14 Oct 2019 16:17:23 +0200 Subject: [PATCH 36/37] WIP --- src/examples/char_p.lean | 51 +++++++++++---------------------------- src/perfectoid_field.lean | 32 +++++++++++++++++++++++- 2 files changed, 45 insertions(+), 38 deletions(-) diff --git a/src/examples/char_p.lean b/src/examples/char_p.lean index 98d92d6b..5038291d 100644 --- a/src/examples/char_p.lean +++ b/src/examples/char_p.lean @@ -6,6 +6,7 @@ import for_mathlib.char_p import valuation.perfection import perfectoid_space +import perfectoid_field noncomputable theory open_locale classical @@ -155,49 +156,25 @@ end⟩ end laurent_series_perfection -namespace valuation -variables {R : Type*} [comm_ring R] -variables {Γ₀ : Type*} [linear_ordered_comm_group_with_zero Γ₀] +def vlsp (K : Type) [discrete_field K] (b : {r : nnreal // 0 < r ∧ r < 1}) := +laurent_series_perfection K -local attribute [instance] classical.decidable_linear_order - -def le_one_subring (v : valuation R Γ₀) := {r : R | v r ≤ 1} +namespace vlsp +variables (p : nat.primes) (K : Type) [discrete_field K] [char_p K p] +variables (b : {r : nnreal // 0 < r ∧ r < 1}) +include p -instance le_one_subring.is_subring (v : valuation R Γ₀) : is_subring v.le_one_subring := --- @subtype.comm_ring R _ {r : R | v r ≤ 1} -{ zero_mem := show v 0 ≤ 1, by simp, - one_mem := show v 1 ≤ 1, by simp, - add_mem := λ r s (hr : v r ≤ 1) (hs : v s ≤ 1), show v (r+s) ≤ 1, - by calc v (r + s) ≤ max (v r) (v s) : v.map_add r s - ... ≤ 1 : max_le hr hs, - neg_mem := λ r (hr : v r ≤ 1), show v (-r) ≤ 1, by rwa [v.map_neg], - mul_mem := λ r s (hr : v r ≤ 1) (hs : v s ≤ 1), show v (r*s) ≤ 1, - begin - rw v.map_mul, - refine le_trans (actual_ordered_comm_monoid.mul_le_mul_right' hr) _, - rwa one_mul - end } +instance : discrete_field (vlsp K b) := +laurent_series_perfection.discrete_field p K -instance coe_nat_le_one_subring (v : valuation R Γ₀) : - has_coe ℕ v.le_one_subring := by apply_instance +local attribute [instance] valued.subgroups_basis subgroups_basis.topology + ring_filter_basis.topological_ring valued.uniform_space -end valuation +instance : valued (vlsp K b) := laurent_series_perfection.valued p K b -section pfd_fld -parameter (p : nat.primes) -variables (K : Type) --- class perfectoid_field : Type 1 := --- [fld : discrete_field K] --- [top : uniform_space K] --- [top_fld : topological_division_ring K] --- [complete : complete_space K] --- [sep : separated K] --- (v : valuation K nnreal) --- (non_discrete : ∀ ε : nnreal, 0 < ε → ∃ x : K, 1 < v x ∧ v x < 1 + ε) --- (Frobenius : surjective (Frob v.le_one_subring ∕p)) -end pfd_fld +end vlsp section open uniform_space @@ -247,7 +224,7 @@ variables {α : Type*} [ring α] [uniform_space α] [topological_ring α] [unifo local infix `^` := monoid.pow @[move_cast] -lemma coe_pow (a : α) (n : ℕ): ((a^n : α) : completion α) = a^n := +lemma coe_pow (a : α) (n : ℕ) : ((a^n : α) : completion α) = a^n := begin induction n with n ih, exact completion.coe_one _, diff --git a/src/perfectoid_field.lean b/src/perfectoid_field.lean index 2e8adf57..095ba057 100644 --- a/src/perfectoid_field.lean +++ b/src/perfectoid_field.lean @@ -1,9 +1,39 @@ +import for_mathlib.nnreal + import valuation.topology -import examples.char_p +import Huber_pair import Frobenius set_option old_structure_cmd true -- do we do this or not? +namespace valuation +variables {R : Type*} [comm_ring R] +variables {Γ₀ : Type*} [linear_ordered_comm_group_with_zero Γ₀] + +local attribute [instance] classical.decidable_linear_order + +def le_one_subring (v : valuation R Γ₀) := {r : R | v r ≤ 1} + +instance le_one_subring.is_subring (v : valuation R Γ₀) : is_subring v.le_one_subring := +-- @subtype.comm_ring R _ {r : R | v r ≤ 1} +{ zero_mem := show v 0 ≤ 1, by simp, + one_mem := show v 1 ≤ 1, by simp, + add_mem := λ r s (hr : v r ≤ 1) (hs : v s ≤ 1), show v (r+s) ≤ 1, + by calc v (r + s) ≤ max (v r) (v s) : v.map_add r s + ... ≤ 1 : max_le hr hs, + neg_mem := λ r (hr : v r ≤ 1), show v (-r) ≤ 1, by rwa [v.map_neg], + mul_mem := λ r s (hr : v r ≤ 1) (hs : v s ≤ 1), show v (r*s) ≤ 1, + begin + rw v.map_mul, + refine le_trans (actual_ordered_comm_monoid.mul_le_mul_right' hr) _, + rwa one_mul + end } + +instance coe_nat_le_one_subring (v : valuation R Γ₀) : + has_coe ℕ v.le_one_subring := by apply_instance + +end valuation + class nondiscrete_valued_field (K : Type*) extends discrete_field K := (v : valuation K nnreal) (non_discrete : ∀ ε : nnreal, 0 < ε → ∃ x : K, 1 < v x ∧ v x < 1 + ε) From 7cb6f59f3928243741f3992cd5b2ed4d03127fe7 Mon Sep 17 00:00:00 2001 From: Johan Commelin Date: Tue, 15 Oct 2019 18:47:49 +0200 Subject: [PATCH 37/37] Change D(T/s) to R(T/s) in comments --- src/Spa/localization_Huber.lean | 6 +++--- src/Spa/stalk_valuation.lean | 6 +++--- 2 files changed, 6 insertions(+), 6 deletions(-) diff --git a/src/Spa/localization_Huber.lean b/src/Spa/localization_Huber.lean index 98be980d..70e917ac 100644 --- a/src/Spa/localization_Huber.lean +++ b/src/Spa/localization_Huber.lean @@ -108,7 +108,7 @@ begin end /--The natural map from the localization A⟮T/s⟯ of a Huber pair A -at a rational open subset D(T/s) +at a rational open subset R(T/s) to the valuation field of a valuation that does not have s in its support.-/ noncomputable def to_valuation_field (hs : v s ≠ 0) : A⟮T/s⟯ → (valuation_field v) := Huber_ring.away.lift T s (valuation_field_mk v) (unit_s hs) rfl @@ -149,13 +149,13 @@ lemma to_valuation_field_cts_aux {r : spa.rational_open_data A} {v : spa A} (hv : v ∈ r.open_set) : (Spv.out v.1) (r.s) ≠ 0 := hv.2 /-- The natural map from A(T/s) to the valuation field of a valuation v contained in -the rational open subset D(T/s). -/ +the rational open subset R(T/s). -/ def to_valuation_field {r : spa.rational_open_data A} {v : spa A} (hv : v ∈ r.open_set) : spa.rational_open_data.localization r → valuation_field (Spv.out (v.val)) := (to_valuation_field $ to_valuation_field_cts_aux hv) /-- The natural map from A(T/s) to the valuation field of a valuation v contained in -the rational open subset D(T/s) is a ring homomorphism. -/ +the rational open subset R(T/s) is a ring homomorphism. -/ instance {r : spa.rational_open_data A} {v : spa A} (hv : v ∈ r.open_set) : is_ring_hom (to_valuation_field hv) := by {delta to_valuation_field, apply_instance} diff --git a/src/Spa/stalk_valuation.lean b/src/Spa/stalk_valuation.lean index d1375bee..ed5f0252 100644 --- a/src/Spa/stalk_valuation.lean +++ b/src/Spa/stalk_valuation.lean @@ -32,7 +32,7 @@ and define the map on the sections s in F(U) for open neigbourhoods U of x. But we have to check a compatibility condition, and this takes some effort. Let us translate this to the context of the structure presheaf of the adic spectrum. -The sections above a rational open subset D(T/s) are: +The sections above a rational open subset R(T/s) are: rat_open_data_completion r := A @@ -56,7 +56,7 @@ local attribute [instance] valued.uniform_space namespace rational_open_data /-- The natural map from A to the completion of the valuation field of a valuation v -contained in D(T/s). -/ +contained in R(T/s). -/ noncomputable def to_complete_valuation_field (r : rational_open_data A) {v : spa A} (hv : v ∈ r.open_set) : rat_open_data_completion r → completion (valuation_field (Spv.out v.1)) := @@ -65,7 +65,7 @@ completion.map (Huber_pair.rational_open_data.to_valuation_field hv) variables {r r1 r2 : rational_open_data A} {v : spa A} (hv : v ∈ r.open_set) /-- The natural map from A to the completion of the valuation field of a valuation v -contained in D(T/s) is a ring homomorphism. -/ +contained in R(T/s) is a ring homomorphism. -/ instance to_complete_valuation_field_is_ring_hom : is_ring_hom (r.to_complete_valuation_field hv) := completion.is_ring_hom_map (Huber_pair.rational_open_data.to_valuation_field_cts hv)