import data.nat.prime
import algebra.group_power
import tactic.ring

universes u v

namespace nat

class Prime :=
(p : ℕ) (pp : nat.prime p)

end nat

open nat.Prime
variable [nat.Prime] -- fix a prime p

def Frob {A : Type u} [ring A] (x : A) := x^p

def delta_ring.aux {A : Type u} [comm_ring A] : A → A → A := sorry
-- λ a b, (a^p + b^p - (a+b)^p)/p

class delta_ring (A : Type u) extends comm_ring A :=
(δ : A → A)
(zero_prop : δ(0) = 0)
(one_prop  : δ(1) = 0)
(add_prop  : ∀ {a b}, δ(a+b) = δ(a) + δ(b) + (delta_ring.aux a b))
(mul_prop  : ∀ {a b}, δ(a*b) = a^p*δ(b) + b^p*δ(a) + p*δ(a)*δ(b))

namespace delta_ring

variables {A : Type u} [delta_ring A]

@[simp] lemma delta_zero : δ(0:A) = 0 := zero_prop A
@[simp] lemma delta_one  : δ(1:A) = 0 :=  one_prop A
@[simp] lemma aux_prop (a b : A) : (p : A) * delta_ring.aux a b = (a^p + b^p - (a+b)^p) := sorry

def Frob_lift (x : A) := x^p + p*δ(x)

instance : is_ring_hom (Frob_lift : A → A) :=
{ map_one := by simp [Frob_lift],
  map_add :=
  begin
    intros a b,
    simp [Frob_lift,add_prop,left_distrib]
  end,
  map_mul :=
  begin
    intros a b,
    simp [Frob_lift,mul_prop,mul_pow],
    ring
  end }

end delta_ring