Help! It's a big mess

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

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,29 +196,31 @@ 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
 
 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

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 },

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 Γ₀]

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]