Skip to content

Commit

Permalink
refactor: generalize CharP+Prime to ExpChar in frobenius (#10016)
Browse files Browse the repository at this point in the history 
Consequently, the part about `frobenius` in Algebra/CharP/Basic is moved to CharP/ExpChar, and imports are adjusted as necessary.

+ Add instances from `CharP+Fact(Nat.Prime)` and `CharZero` to `ExpChar`, to allow lemmas generalized to ExpChar still apply to CharP.

+ Remove lemmas in Algebra/CharP/ExpChar from [#9799](1e74fcf) because they coincide with the generalized lemmas, and golf the other lemmas (in Algebra/CharP/Basic).

+ Define the RingHom `iterateFrobenius` and the semilinear map `LinearMap.(iterate)Frobenius` for an algebra. When the characteristic is zero (ExpChar is 1), these are all equal to the identity map (· ^ 1). Also define `iterateFrobeniusEquiv` for perfect rings.

+ Fix and/or generalize other files.



Co-authored-by: Junyan Xu <junyanxu.math@gmail.com>
Co-authored-by: acmepjz <acme_pjz@hotmail.com>
  • Loading branch information
@alreadydone @acmepjz
3 people committed Feb 2, 2024
1 parent 0311bbc commit 96a6d29
Show file tree
Hide file tree
Showing 9 changed files with 241 additions and 215 deletions.
140 changes: 6 additions & 134 deletions Mathlib/Algebra/CharP/Basic.lean
View file
Expand Up @@ -346,140 +346,6 @@ theorem RingHom.charP_iff_charP {K L : Type*} [DivisionRing K] [Semiring L] [Non
simp only [charP_iff, ← f.injective.eq_iff, map_natCast f, f.map_zero]
#align ring_hom.char_p_iff_char_p RingHom.charP_iff_charP

section frobenius

section CommSemiring

variable [CommSemiring R] {S : Type v} [CommSemiring S] (f : R →* S) (g : R →+* S) (p : ℕ)
[Fact p.Prime] [CharP R p] [CharP S p] (x y : R)

/-- The frobenius map that sends x to x^p -/
def frobenius : R →+* R where
toFun x := x ^ p
map_one' := one_pow p
map_mul' x y := mul_pow x y p
map_zero' := zero_pow (Fact.out (p := Nat.Prime p)).ne_zero
map_add' := add_pow_char R
#align frobenius frobenius

variable {R}

theorem frobenius_def : frobenius R p x = x ^ p :=
rfl
#align frobenius_def frobenius_def

theorem iterate_frobenius (n : ℕ) : (frobenius R p)^[n] x = x ^ p ^ n := by
induction n with
| zero => simp
| succ n n_ih =>
rw [Function.iterate_succ', pow_succ', pow_mul, Function.comp_apply, frobenius_def, n_ih]
#align iterate_frobenius iterate_frobenius

theorem frobenius_mul : frobenius R p (x * y) = frobenius R p x * frobenius R p y :=
(frobenius R p).map_mul x y
#align frobenius_mul frobenius_mul

theorem frobenius_one : frobenius R p 1 = 1 :=
one_pow _
#align frobenius_one frobenius_one

theorem MonoidHom.map_frobenius : f (frobenius R p x) = frobenius S p (f x) :=
f.map_pow x p
#align monoid_hom.map_frobenius MonoidHom.map_frobenius

theorem RingHom.map_frobenius : g (frobenius R p x) = frobenius S p (g x) :=
g.map_pow x p
#align ring_hom.map_frobenius RingHom.map_frobenius

theorem MonoidHom.map_iterate_frobenius (n : ℕ) :
f ((frobenius R p)^[n] x) = (frobenius S p)^[n] (f x) :=
Function.Semiconj.iterate_right (f.map_frobenius p) n x
#align monoid_hom.map_iterate_frobenius MonoidHom.map_iterate_frobenius

theorem RingHom.map_iterate_frobenius (n : ℕ) :
g ((frobenius R p)^[n] x) = (frobenius S p)^[n] (g x) :=
g.toMonoidHom.map_iterate_frobenius p x n
#align ring_hom.map_iterate_frobenius RingHom.map_iterate_frobenius

theorem MonoidHom.iterate_map_frobenius (f : R →* R) (p : ℕ) [Fact p.Prime] [CharP R p] (n : ℕ) :
f^[n] (frobenius R p x) = frobenius R p (f^[n] x) :=
f.iterate_map_pow _ _ _
#align monoid_hom.iterate_map_frobenius MonoidHom.iterate_map_frobenius

theorem RingHom.iterate_map_frobenius (f : R →+* R) (p : ℕ) [Fact p.Prime] [CharP R p] (n : ℕ) :
f^[n] (frobenius R p x) = frobenius R p (f^[n] x) :=
f.iterate_map_pow _ _ _
#align ring_hom.iterate_map_frobenius RingHom.iterate_map_frobenius

variable (R)

theorem frobenius_zero : frobenius R p 0 = 0 :=
(frobenius R p).map_zero
#align frobenius_zero frobenius_zero

theorem frobenius_add : frobenius R p (x + y) = frobenius R p x + frobenius R p y :=
(frobenius R p).map_add x y
#align frobenius_add frobenius_add

theorem frobenius_nat_cast (n : ℕ) : frobenius R p n = n :=
map_natCast (frobenius R p) n
#align frobenius_nat_cast frobenius_nat_cast

open BigOperators

variable {R}

theorem list_sum_pow_char (l : List R) : l.sum ^ p = (l.map (· ^ p : R → R)).sum :=
(frobenius R p).map_list_sum _
#align list_sum_pow_char list_sum_pow_char

theorem multiset_sum_pow_char (s : Multiset R) : s.sum ^ p = (s.map (· ^ p : R → R)).sum :=
(frobenius R p).map_multiset_sum _
#align multiset_sum_pow_char multiset_sum_pow_char

theorem sum_pow_char {ι : Type*} (s : Finset ι) (f : ι → R) :
(∑ i in s, f i) ^ p = ∑ i in s, f i ^ p :=
(frobenius R p).map_sum _ _
#align sum_pow_char sum_pow_char

variable (n : ℕ)

theorem list_sum_pow_char_pow (l : List R) : l.sum ^ p ^ n = (l.map (· ^ p ^ n : R → R)).sum := by
induction n with
| zero => simp_rw [pow_zero, pow_one, List.map_id']
| succ n ih => simp_rw [pow_succ', pow_mul, ih, list_sum_pow_char, List.map_map]; rfl

theorem multiset_sum_pow_char_pow (s : Multiset R) :
s.sum ^ p ^ n = (s.map (· ^ p ^ n : R → R)).sum := by
induction n with
| zero => simp_rw [pow_zero, pow_one, Multiset.map_id']
| succ n ih => simp_rw [pow_succ', pow_mul, ih, multiset_sum_pow_char, Multiset.map_map]; rfl

theorem sum_pow_char_pow {ι : Type*} (s : Finset ι) (f : ι → R) :
(∑ i in s, f i) ^ p ^ n = ∑ i in s, f i ^ p ^ n := by
induction n with
| zero => simp_rw [pow_zero, pow_one]
| succ n ih => simp_rw [pow_succ', pow_mul, ih, sum_pow_char]

end CommSemiring

section CommRing

variable [CommRing R] {S : Type v} [CommRing S] (f : R →* S) (g : R →+* S) (p : ℕ) [Fact p.Prime]
[CharP R p] [CharP S p] (x y : R)

theorem frobenius_neg : frobenius R p (-x) = -frobenius R p x :=
(frobenius R p).map_neg x
#align frobenius_neg frobenius_neg

theorem frobenius_sub : frobenius R p (x - y) = frobenius R p x - frobenius R p y :=
(frobenius R p).map_sub x y
#align frobenius_sub frobenius_sub

end CommRing

end frobenius

namespace CharP

section
Expand Down Expand Up @@ -710,6 +576,12 @@ instance Prod.charP [CharP S p] : CharP (R × S) p := by
convert Nat.lcm.charP R S p p; simp
#align prod.char_p Prod.charP

instance Prod.charZero_of_left [CharZero R] : CharZero (R × S) where
cast_injective _ _ h := CharZero.cast_injective congr(Prod.fst $h)

instance Prod.charZero_of_right [CharZero S] : CharZero (R × S) where
cast_injective _ _ h := CharZero.cast_injective congr(Prod.snd $h)

end Prod

instance ULift.charP [AddMonoidWithOne R] (p : ℕ) [CharP R p] : CharP (ULift.{v} R) p where
Expand Down
211 changes: 173 additions & 38 deletions Mathlib/Algebra/CharP/ExpChar.lean
View file
Expand Up @@ -46,6 +46,16 @@ class inductive ExpChar (R : Type u) [Semiring R] : ℕ → Prop
#align exp_char ExpChar
#align exp_char.prime ExpChar.prime

instance expChar_prime (p) [CharP R p] [Fact p.Prime] : ExpChar R p := ExpChar.prime Fact.out
instance expChar_zero [CharZero R] : ExpChar R 1 := ExpChar.zero

instance (S : Type*) [Semiring S] (p) [ExpChar R p] [ExpChar S p] : ExpChar (R × S) p := by
obtain hp | ⟨hp⟩ := ‹ExpChar R p›
· have := Prod.charZero_of_left R S; exact .zero
obtain _ | _ := ‹ExpChar S p›
· exact (Nat.not_prime_one hp).elim
· have := Prod.charP R S p; exact .prime hp

variable {R} in
/-- The exponential characteristic is unique. -/
theorem ExpChar.eq {p q : ℕ} (hp : ExpChar R p) (hq : ExpChar R q) : p = q := by
Expand Down Expand Up @@ -244,46 +254,171 @@ theorem ExpChar.neg_one_pow_expChar_pow [Ring R] (q n : ℕ) [hR : ExpChar R q]
· simp only [one_pow, pow_one]
haveI := Fact.mk hprime; exact CharP.neg_one_pow_char_pow R q n

section BigOperators
section frobenius

section CommSemiring

variable [CommSemiring R] {S : Type*} [CommSemiring S] (f : R →* S) (g : R →+* S) (p m n : ℕ)
[ExpChar R p] [ExpChar S p] (x y : R)

/-- The frobenius map that sends x to x^p -/
def frobenius : R →+* R where
__ := powMonoidHom p
map_zero' := zero_pow (expChar_pos R p).ne'
map_add' := add_pow_expChar R
#align frobenius frobenius

/-- The iterated frobenius map sending x to x^p^n -/
def iterateFrobenius : R →+* R where
__ := powMonoidHom (p ^ n)
map_zero' := zero_pow (expChar_pow_pos R p n).ne'
map_add' := add_pow_expChar_pow R

variable {R}

theorem frobenius_def : frobenius R p x = x ^ p := rfl
#align frobenius_def frobenius_def

theorem iterateFrobenius_def : iterateFrobenius R p n x = x ^ p ^ n := rfl

theorem iterate_frobenius : (frobenius R p)^[n] x = x ^ p ^ n := congr_fun (pow_iterate p n) x
#align iterate_frobenius iterate_frobenius

variable (R)

theorem coe_iterateFrobenius : iterateFrobenius R p n = (frobenius R p)^[n] :=
(pow_iterate p n).symm

@[simp]
theorem iterateFrobenius_one : iterateFrobenius R p 1 = frobenius R p := by
simp_rw [iterateFrobenius, frobenius, pow_one]

@[simp]
theorem iterateFrobenius_zero : iterateFrobenius R p 0 = RingHom.id R := by
simp_rw [iterateFrobenius, powMonoidHom, pow_zero, pow_one]
rfl

theorem iterateFrobenius_add :
iterateFrobenius R p (m + n) = (iterateFrobenius R p m).comp (iterateFrobenius R p n) := by
ext x
simp_rw [RingHom.comp_apply, iterateFrobenius_def, add_comm m n, pow_add, pow_mul]

theorem coe_iterateFrobenius_mul : iterateFrobenius R p (m * n) = (iterateFrobenius R p m)^[n] := by
simp_rw [coe_iterateFrobenius, Function.iterate_mul]

variable {R}

theorem frobenius_mul : frobenius R p (x * y) = frobenius R p x * frobenius R p y :=
(frobenius R p).map_mul x y
#align frobenius_mul frobenius_mul

theorem frobenius_one : frobenius R p 1 = 1 :=
one_pow _
#align frobenius_one frobenius_one

theorem MonoidHom.map_frobenius : f (frobenius R p x) = frobenius S p (f x) :=
f.map_pow x p
#align monoid_hom.map_frobenius MonoidHom.map_frobenius

theorem RingHom.map_frobenius : g (frobenius R p x) = frobenius S p (g x) :=
g.map_pow x p
#align ring_hom.map_frobenius RingHom.map_frobenius

theorem MonoidHom.map_iterate_frobenius (n : ℕ) :
f ((frobenius R p)^[n] x) = (frobenius S p)^[n] (f x) :=
Function.Semiconj.iterate_right (f.map_frobenius p) n x
#align monoid_hom.map_iterate_frobenius MonoidHom.map_iterate_frobenius

theorem RingHom.map_iterate_frobenius (n : ℕ) :
g ((frobenius R p)^[n] x) = (frobenius S p)^[n] (g x) :=
g.toMonoidHom.map_iterate_frobenius p x n
#align ring_hom.map_iterate_frobenius RingHom.map_iterate_frobenius

theorem MonoidHom.iterate_map_frobenius (f : R →* R) (p : ℕ) [ExpChar R p] (n : ℕ) :
f^[n] (frobenius R p x) = frobenius R p (f^[n] x) :=
f.iterate_map_pow _ _ _
#align monoid_hom.iterate_map_frobenius MonoidHom.iterate_map_frobenius

theorem RingHom.iterate_map_frobenius (f : R →+* R) (p : ℕ) [ExpChar R p] (n : ℕ) :
f^[n] (frobenius R p x) = frobenius R p (f^[n] x) :=
f.iterate_map_pow _ _ _
#align ring_hom.iterate_map_frobenius RingHom.iterate_map_frobenius

variable (R S)

/-- The frobenius map of an algebra as a frobenius-semilinear map. -/
nonrec def LinearMap.frobenius [Algebra R S] : S →ₛₗ[frobenius R p] S where
__ := frobenius S p
map_smul' r s := show frobenius S p _ = _ by
simp_rw [Algebra.smul_def, map_mul, ← (algebraMap R S).map_frobenius]; rfl

/-- The iterated frobenius map of an algebra as a iterated-frobenius-semilinear map. -/
nonrec def LinearMap.iterateFrobenius [Algebra R S] : S →ₛₗ[iterateFrobenius R p n] S where
__ := iterateFrobenius S p n
map_smul' f s := show iterateFrobenius S p n _ = _ by
simp_rw [iterateFrobenius_def, Algebra.smul_def, mul_pow, ← map_pow]; rfl

theorem LinearMap.frobenius_def [Algebra R S] (x : S) : frobenius R S p x = x ^ p := rfl

theorem LinearMap.iterateFrobenius_def [Algebra R S] (n : ℕ) (x : S) :
iterateFrobenius R S p n x = x ^ p ^ n := rfl

theorem frobenius_zero : frobenius R p 0 = 0 :=
(frobenius R p).map_zero
#align frobenius_zero frobenius_zero

theorem frobenius_add : frobenius R p (x + y) = frobenius R p x + frobenius R p y :=
(frobenius R p).map_add x y
#align frobenius_add frobenius_add

theorem frobenius_nat_cast (n : ℕ) : frobenius R p n = n :=
map_natCast (frobenius R p) n
#align frobenius_nat_cast frobenius_nat_cast

open BigOperators

variable {R}

variable [CommSemiring R] (q : ℕ) [hR : ExpChar R q] (n : ℕ)

theorem list_sum_pow_expChar (l : List R) : l.sum ^ q = (l.map (· ^ q : R → R)).sum := by
cases hR with
| zero => simp_rw [pow_one, List.map_id']
| prime hprime => haveI := Fact.mk hprime; exact list_sum_pow_char q l

theorem multiset_sum_pow_expChar (s : Multiset R) : s.sum ^ q = (s.map (· ^ q : R → R)).sum := by
cases hR with
| zero => simp_rw [pow_one, Multiset.map_id']
| prime hprime => haveI := Fact.mk hprime; exact multiset_sum_pow_char q s

theorem sum_pow_expChar {ι : Type*} (s : Finset ι) (f : ι → R) :
(∑ i in s, f i) ^ q = ∑ i in s, f i ^ q := by
cases hR with
| zero => simp_rw [pow_one]
| prime hprime => haveI := Fact.mk hprime; exact sum_pow_char q s f

theorem list_sum_pow_expChar_pow (l : List R) :
l.sum ^ q ^ n = (l.map (· ^ q ^ n : R → R)).sum := by
cases hR with
| zero => simp_rw [one_pow, pow_one, List.map_id']
| prime hprime => haveI := Fact.mk hprime; exact list_sum_pow_char_pow q n l

theorem multiset_sum_pow_expChar_pow (s : Multiset R) :
s.sum ^ q ^ n = (s.map (· ^ q ^ n : R → R)).sum := by
cases hR with
| zero => simp_rw [one_pow, pow_one, Multiset.map_id']
| prime hprime => haveI := Fact.mk hprime; exact multiset_sum_pow_char_pow q n s

theorem sum_pow_expChar_pow {ι : Type*} (s : Finset ι) (f : ι → R) :
(∑ i in s, f i) ^ q ^ n = ∑ i in s, f i ^ q ^ n := by
cases hR with
| zero => simp_rw [one_pow, pow_one]
| prime hprime => haveI := Fact.mk hprime; exact sum_pow_char_pow q n s f

end BigOperators
theorem list_sum_pow_char (l : List R) : l.sum ^ p = (l.map (· ^ p : R → R)).sum :=
(frobenius R p).map_list_sum _
#align list_sum_pow_char list_sum_pow_char

theorem multiset_sum_pow_char (s : Multiset R) : s.sum ^ p = (s.map (· ^ p : R → R)).sum :=
(frobenius R p).map_multiset_sum _
#align multiset_sum_pow_char multiset_sum_pow_char

theorem sum_pow_char {ι : Type*} (s : Finset ι) (f : ι → R) :
(∑ i in s, f i) ^ p = ∑ i in s, f i ^ p :=
(frobenius R p).map_sum _ _
#align sum_pow_char sum_pow_char

variable (n : ℕ)

theorem list_sum_pow_char_pow (l : List R) : l.sum ^ p ^ n = (l.map (· ^ p ^ n : R → R)).sum :=
(iterateFrobenius R p n).map_list_sum _

theorem multiset_sum_pow_char_pow (s : Multiset R) :
s.sum ^ p ^ n = (s.map (· ^ p ^ n : R → R)).sum :=
(iterateFrobenius R p n).map_multiset_sum _

theorem sum_pow_char_pow {ι : Type*} (s : Finset ι) (f : ι → R) :
(∑ i in s, f i) ^ p ^ n = ∑ i in s, f i ^ p ^ n :=
(iterateFrobenius R p n).map_sum _ _

end CommSemiring

section CommRing

variable [CommRing R] (p : ℕ) [ExpChar R p] (x y : R)

theorem frobenius_neg : frobenius R p (-x) = -frobenius R p x :=
(frobenius R p).map_neg x
#align frobenius_neg frobenius_neg

theorem frobenius_sub : frobenius R p (x - y) = frobenius R p x - frobenius R p y :=
(frobenius R p).map_sub x y
#align frobenius_sub frobenius_sub

end CommRing

end frobenius

0 comments on commit 96a6d29

Please sign in to comment.