Last active
July 20, 2018 13:20
-
-
Save jcommelin/b09dcc1c3494e123e84afc96a91fd61c to your computer and use it in GitHub Desktop.
delta rings
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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 |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment