Towards an example of a perfectoid field

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
@@ -13,117 +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 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 { 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
-
-@[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
-
-@[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,
@@ -135,11 +35,12 @@ 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,
-      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, },
+    { 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 } },
   end }
 
 end power_series
@@ -166,28 +67,29 @@ 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 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 :=
 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,
@@ -312,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 _
@@ -330,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