Towards an example of a perfectoid field

src/Frobenius.lean

@@ -1,14 +1,62 @@
 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
 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)
+
+section
+open function
+
+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 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,
+  rw ← ideal.quotient.mk_pow,
+  refl,
+end
+
+end

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}
 

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<T/s>
 
@@ -56,7 +56,7 @@ local attribute [instance] valued.uniform_space
 namespace rational_open_data
 
 /-- The natural map from A<T/s> 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<T/s> 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)