Skip to content

Commit 6757988

Browse files
mistarromistarro
committed
refactor(Algebra/CharP): Frobenius map definition in Mathlib.Algebra.CharP.Frobenius (#23444)
The Frobenius map definitions are now in `Mathlib.Algebra.CharP.Frobenius` to reduce confusion (before it was split between `Lemmas` and `ExpChar` after PR #18023). As `Mathlib.Algebra.CharP.Two` forbids definitions of `Algebra` and `LinearMap` and at the same time depends on the results requiring additive part of the Frobenius map, that part is placed in `Lemmas` and reused in the definitions of `frobenius` and `iterateFrobenius`.
1 parent ab457a5 commit 6757988

File tree

9 files changed

+153
-169
lines changed

9 files changed

+153
-169
lines changed

‎Mathlib.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -193,7 +193,7 @@ import Mathlib.Algebra.CharP.Algebra
193193
import Mathlib.Algebra.CharP.Basic
194194
import Mathlib.Algebra.CharP.CharAndCard
195195
import Mathlib.Algebra.CharP.Defs
196-
import Mathlib.Algebra.CharP.ExpChar
196+
import Mathlib.Algebra.CharP.Frobenius
197197
import Mathlib.Algebra.CharP.IntermediateField
198198
import Mathlib.Algebra.CharP.Invertible
199199
import Mathlib.Algebra.CharP.Lemmas

‎Mathlib/Algebra/CharP/ExpChar.lean‎

Lines changed: 0 additions & 72 deletions
This file was deleted.

‎Mathlib/Algebra/CharP/Frobenius.lean‎

Lines changed: 134 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,134 @@
1+
/-
2+
Copyright (c) 2021 Jakob Scholbach. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Jakob Scholbach
5+
-/
6+
import Mathlib.Algebra.Algebra.Defs
7+
import Mathlib.Algebra.CharP.Lemmas
8+
9+
/-!
10+
### The Frobenius endomorphism
11+
12+
## Tags
13+
14+
Frobenius endomorphism
15+
16+
## Implementation notes
17+
18+
The definitions of `frobenius` and `iterateFrobenius` ring homomorphisms are in
19+
`Mathlib.Algebra.CharP.Lemmas` as they are needed for some results that in turn are used in files
20+
forbidding to import algebra-related definitions (see `Mathlib.Algebra.CharP.Two.lean`).
21+
-/
22+
23+
section CommSemiring
24+
25+
variable {R : Type*} [CommSemiring R] {S : Type*} [CommSemiring S]
26+
variable (f : R →* S) (g : R →+* S) (p m n : ℕ) [ExpChar R p] [ExpChar S p] (x y : R)
27+
28+
lemma frobenius_def : frobenius R p x = x ^ p := rfl
29+
30+
lemma iterateFrobenius_def : iterateFrobenius R p n x = x ^ p ^ n := rfl
31+
32+
lemma iterate_frobenius : (frobenius R p)^[n] x = x ^ p ^ n := congr_fun (pow_iterate p n) x
33+
34+
variable (R)
35+
36+
lemma iterateFrobenius_eq_pow : iterateFrobenius R p n = frobenius R p ^ n := by
37+
ext; simp [iterateFrobenius_def, iterate_frobenius]
38+
39+
lemma coe_iterateFrobenius : iterateFrobenius R p n = (frobenius R p)^[n] :=
40+
(pow_iterate p n).symm
41+
42+
lemma iterateFrobenius_one_apply : iterateFrobenius R p 1 x = x ^ p := by
43+
rw [iterateFrobenius_def, pow_one]
44+
45+
@[simp]
46+
lemma iterateFrobenius_one : iterateFrobenius R p 1 = frobenius R p :=
47+
RingHom.ext (iterateFrobenius_one_apply R p)
48+
49+
lemma iterateFrobenius_zero_apply : iterateFrobenius R p 0 x = x := by
50+
rw [iterateFrobenius_def, pow_zero, pow_one]
51+
52+
@[simp]
53+
lemma iterateFrobenius_zero : iterateFrobenius R p 0 = RingHom.id R :=
54+
RingHom.ext (iterateFrobenius_zero_apply R p)
55+
56+
lemma iterateFrobenius_add_apply :
57+
iterateFrobenius R p (m + n) x = iterateFrobenius R p m (iterateFrobenius R p n x) := by
58+
simp_rw [iterateFrobenius_def, add_comm m n, pow_add, pow_mul]
59+
60+
lemma iterateFrobenius_add :
61+
iterateFrobenius R p (m + n) = (iterateFrobenius R p m).comp (iterateFrobenius R p n) :=
62+
RingHom.ext (iterateFrobenius_add_apply R p m n)
63+
64+
lemma iterateFrobenius_mul_apply :
65+
iterateFrobenius R p (m * n) x = (iterateFrobenius R p m)^[n] x := by
66+
simp_rw [coe_iterateFrobenius, Function.iterate_mul]
67+
68+
lemma coe_iterateFrobenius_mul : iterateFrobenius R p (m * n) = (iterateFrobenius R p m)^[n] :=
69+
funext (iterateFrobenius_mul_apply R p m n)
70+
71+
variable {R}
72+
73+
lemma frobenius_mul : frobenius R p (x * y) = frobenius R p x * frobenius R p y :=
74+
map_mul (frobenius R p) x y
75+
76+
lemma frobenius_one : frobenius R p 1 = 1 := one_pow _
77+
78+
lemma MonoidHom.map_frobenius : f (frobenius R p x) = frobenius S p (f x) := map_pow f x p
79+
lemma RingHom.map_frobenius : g (frobenius R p x) = frobenius S p (g x) := map_pow g x p
80+
81+
lemma MonoidHom.map_iterate_frobenius (n : ℕ) :
82+
f ((frobenius R p)^[n] x) = (frobenius S p)^[n] (f x) :=
83+
Function.Semiconj.iterate_right (f.map_frobenius p) n x
84+
85+
lemma RingHom.map_iterate_frobenius (n : ℕ) :
86+
g ((frobenius R p)^[n] x) = (frobenius S p)^[n] (g x) :=
87+
g.toMonoidHom.map_iterate_frobenius p x n
88+
89+
lemma MonoidHom.iterate_map_frobenius (f : R →* R) (p : ℕ) [ExpChar R p] (n : ℕ) :
90+
f^[n] (frobenius R p x) = frobenius R p (f^[n] x) :=
91+
iterate_map_pow f _ _ _
92+
93+
lemma RingHom.iterate_map_frobenius (f : R →+* R) (p : ℕ) [ExpChar R p] (n : ℕ) :
94+
f^[n] (frobenius R p x) = frobenius R p (f^[n] x) := iterate_map_pow f _ _ _
95+
96+
variable (R S)
97+
98+
/-- The frobenius map of an algebra as a frobenius-semilinear map. -/
99+
nonrec def LinearMap.frobenius [Algebra R S] : S →ₛₗ[frobenius R p] S where
100+
__ := frobenius S p
101+
map_smul' r s := show frobenius S p _ = _ by
102+
simp_rw [Algebra.smul_def, map_mul, ← (algebraMap R S).map_frobenius]; rfl
103+
104+
/-- The iterated frobenius map of an algebra as a iterated-frobenius-semilinear map. -/
105+
nonrec def LinearMap.iterateFrobenius [Algebra R S] : S →ₛₗ[iterateFrobenius R p n] S where
106+
__ := iterateFrobenius S p n
107+
map_smul' f s := show iterateFrobenius S p n _ = _ by
108+
simp_rw [iterateFrobenius_def, Algebra.smul_def, mul_pow, ← map_pow]; rfl
109+
110+
theorem LinearMap.frobenius_def [Algebra R S] (x : S) : frobenius R S p x = x ^ p := rfl
111+
112+
theorem LinearMap.iterateFrobenius_def [Algebra R S] (n : ℕ) (x : S) :
113+
iterateFrobenius R S p n x = x ^ p ^ n := rfl
114+
115+
theorem frobenius_zero : frobenius R p 0 = 0 :=
116+
(frobenius R p).map_zero
117+
118+
theorem frobenius_add : frobenius R p (x + y) = frobenius R p x + frobenius R p y :=
119+
(frobenius R p).map_add x y
120+
121+
theorem frobenius_natCast (n : ℕ) : frobenius R p n = n :=
122+
map_natCast (frobenius R p) n
123+
124+
end CommSemiring
125+
126+
section CommRing
127+
128+
variable {R : Type*} [CommRing R] (p : ℕ) [ExpChar R p] (x y : R)
129+
130+
lemma frobenius_neg : frobenius R p (-x) = -frobenius R p x := map_neg ..
131+
132+
lemma frobenius_sub : frobenius R p (x - y) = frobenius R p x - frobenius R p y := map_sub ..
133+
134+
end CommRing

‎Mathlib/Algebra/CharP/Lemmas.lean‎

Lines changed: 13 additions & 91 deletions
Original file line numberDiff line numberDiff line change
@@ -279,97 +279,30 @@ lemma prime_ringChar : Nat.Prime (ringChar R) := by
279279
end Ring
280280
end CharP
281281

282-
/-! ### The Frobenius automorphism -/
283-
284-
section frobenius
285-
section CommSemiring
286-
variable [CommSemiring R] {S : Type*} [CommSemiring S] (f : R →* S) (g : R →+* S) (p m n : ℕ)
287-
[ExpChar R p] [ExpChar S p] (x y : R)
282+
/-
283+
Preliminary definitions and results for the Frobenius map.
284+
Necessary here for simple results about sums of `p`-powers that are used in files forbidding
285+
to import algebra-related definitions (see `Mathlib.Algebra.CharP.Two.lean`).
286+
-/
287+
section Frobenius
288288

289-
open ExpChar
289+
variable (R : Type*) [CommSemiring R]
290+
variable (p n : ℕ) [ExpChar R p]
290291

291-
variable (R) in
292-
/-- The frobenius map `x ↦ x ^ p`. -/
292+
/-- The Frobenius map `x ↦ x ^ p`. -/
293293
def frobenius : R →+* R where
294294
__ := powMonoidHom p
295295
map_zero' := zero_pow (expChar_pos R p).ne'
296296
map_add' _ _ := add_pow_expChar ..
297297

298-
variable (R) in
299-
/-- The iterated frobenius map `x ↦ x ^ p ^ n`. -/
298+
/-- The iterated Frobenius map `x ↦ x ^ p ^ n`. -/
300299
def iterateFrobenius : R →+* R where
301300
__ := powMonoidHom (p ^ n)
302301
map_zero' := zero_pow (expChar_pow_pos R p n).ne'
303302
map_add' _ _ := add_pow_expChar_pow ..
304303

305-
lemma frobenius_def : frobenius R p x = x ^ p := rfl
306-
307-
lemma iterateFrobenius_def : iterateFrobenius R p n x = x ^ p ^ n := rfl
308-
309-
lemma iterate_frobenius : (frobenius R p)^[n] x = x ^ p ^ n := congr_fun (pow_iterate p n) x
310-
311-
variable (R)
312-
313-
lemma iterateFrobenius_eq_pow : iterateFrobenius R p n = frobenius R p ^ n := by
314-
ext; simp [iterateFrobenius_def, iterate_frobenius]
315-
316-
lemma coe_iterateFrobenius : iterateFrobenius R p n = (frobenius R p)^[n] :=
317-
(pow_iterate p n).symm
318-
319-
lemma iterateFrobenius_one_apply : iterateFrobenius R p 1 x = x ^ p := by
320-
rw [iterateFrobenius_def, pow_one]
321-
322-
@[simp]
323-
lemma iterateFrobenius_one : iterateFrobenius R p 1 = frobenius R p :=
324-
RingHom.ext (iterateFrobenius_one_apply R p)
325-
326-
lemma iterateFrobenius_zero_apply : iterateFrobenius R p 0 x = x := by
327-
rw [iterateFrobenius_def, pow_zero, pow_one]
328-
329-
@[simp]
330-
lemma iterateFrobenius_zero : iterateFrobenius R p 0 = RingHom.id R :=
331-
RingHom.ext (iterateFrobenius_zero_apply R p)
332-
333-
lemma iterateFrobenius_add_apply :
334-
iterateFrobenius R p (m + n) x = iterateFrobenius R p m (iterateFrobenius R p n x) := by
335-
simp_rw [iterateFrobenius_def, add_comm m n, pow_add, pow_mul]
336-
337-
lemma iterateFrobenius_add :
338-
iterateFrobenius R p (m + n) = (iterateFrobenius R p m).comp (iterateFrobenius R p n) :=
339-
RingHom.ext (iterateFrobenius_add_apply R p m n)
340-
341-
lemma iterateFrobenius_mul_apply :
342-
iterateFrobenius R p (m * n) x = (iterateFrobenius R p m)^[n] x := by
343-
simp_rw [coe_iterateFrobenius, Function.iterate_mul]
344-
345-
lemma coe_iterateFrobenius_mul : iterateFrobenius R p (m * n) = (iterateFrobenius R p m)^[n] :=
346-
funext (iterateFrobenius_mul_apply R p m n)
347-
348304
variable {R}
349305

350-
lemma frobenius_mul : frobenius R p (x * y) = frobenius R p x * frobenius R p y :=
351-
map_mul (frobenius R p) x y
352-
353-
lemma frobenius_one : frobenius R p 1 = 1 := one_pow _
354-
355-
lemma MonoidHom.map_frobenius : f (frobenius R p x) = frobenius S p (f x) := map_pow f x p
356-
lemma RingHom.map_frobenius : g (frobenius R p x) = frobenius S p (g x) := map_pow g x p
357-
358-
lemma MonoidHom.map_iterate_frobenius (n : ℕ) :
359-
f ((frobenius R p)^[n] x) = (frobenius S p)^[n] (f x) :=
360-
Function.Semiconj.iterate_right (f.map_frobenius p) n x
361-
362-
lemma RingHom.map_iterate_frobenius (n : ℕ) :
363-
g ((frobenius R p)^[n] x) = (frobenius S p)^[n] (g x) :=
364-
g.toMonoidHom.map_iterate_frobenius p x n
365-
366-
lemma MonoidHom.iterate_map_frobenius (f : R →* R) (p : ℕ) [ExpChar R p] (n : ℕ) :
367-
f^[n] (frobenius R p x) = frobenius R p (f^[n] x) :=
368-
iterate_map_pow f _ _ _
369-
370-
lemma RingHom.iterate_map_frobenius (f : R →+* R) (p : ℕ) [ExpChar R p] (n : ℕ) :
371-
f^[n] (frobenius R p x) = frobenius R p (f^[n] x) := iterate_map_pow f _ _ _
372-
373306
lemma list_sum_pow_char (l : List R) : l.sum ^ p = (l.map (· ^ p : R → R)).sum :=
374307
map_list_sum (frobenius R p) _
375308

@@ -379,25 +312,14 @@ lemma multiset_sum_pow_char (s : Multiset R) : s.sum ^ p = (s.map (· ^ p : R
379312
lemma sum_pow_char {ι : Type*} (s : Finset ι) (f : ι → R) : (∑ i ∈ s, f i) ^ p = ∑ i ∈ s, f i ^ p :=
380313
map_sum (frobenius R p) _ _
381314

382-
variable (n : ℕ)
383-
384315
lemma list_sum_pow_char_pow (l : List R) : l.sum ^ p ^ n = (l.map (· ^ p ^ n : R → R)).sum :=
385316
map_list_sum (iterateFrobenius R p n) _
386317

387318
lemma multiset_sum_pow_char_pow (s : Multiset R) :
388-
s.sum ^ p ^ n = (s.map (· ^ p ^ n : R → R)).sum := map_multiset_sum (iterateFrobenius R p n) _
319+
s.sum ^ p ^ n = (s.map (· ^ p ^ n : R → R)).sum :=
320+
map_multiset_sum (iterateFrobenius R p n) _
389321

390322
lemma sum_pow_char_pow {ι : Type*} (s : Finset ι) (f : ι → R) :
391323
(∑ i ∈ s, f i) ^ p ^ n = ∑ i ∈ s, f i ^ p ^ n := map_sum (iterateFrobenius R p n) _ _
392324

393-
end CommSemiring
394-
395-
section CommRing
396-
variable [CommRing R] (p : ℕ) [ExpChar R p] (x y : R)
397-
398-
lemma frobenius_neg : frobenius R p (-x) = -frobenius R p x := map_neg ..
399-
400-
lemma frobenius_sub : frobenius R p (x - y) = frobenius R p x - frobenius R p y := map_sub ..
401-
402-
end CommRing
403-
end frobenius
325+
end Frobenius

‎Mathlib/Algebra/CharP/Reduced.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ Copyright (c) 2018 Kenny Lau. All rights reserved.
33
Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Kenny Lau, Joey van Langen, Casper Putz
55
-/
6-
import Mathlib.Algebra.CharP.Lemmas
6+
import Mathlib.Algebra.CharP.Frobenius
77
import Mathlib.RingTheory.Nilpotent.Defs
88

99
/-!

‎Mathlib/Algebra/Polynomial/Expand.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ Copyright (c) 2020 Kenny Lau. All rights reserved.
33
Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Kenny Lau
55
-/
6-
import Mathlib.Algebra.CharP.Lemmas
6+
import Mathlib.Algebra.CharP.Frobenius
77
import Mathlib.Algebra.Polynomial.Derivative
88
import Mathlib.Algebra.Polynomial.RingDivision
99
import Mathlib.RingTheory.Polynomial.Basic

‎Mathlib/FieldTheory/PerfectClosure.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ Copyright (c) 2018 Kenny Lau. All rights reserved.
33
Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Kenny Lau, Yury Kudryashov
55
-/
6-
import Mathlib.Algebra.CharP.ExpChar
6+
import Mathlib.Algebra.CharP.Lemmas
77
import Mathlib.FieldTheory.Perfect
88

99
/-!

‎Mathlib/FieldTheory/PurelyInseparable/PerfectClosure.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ Copyright (c) 2024 Jz Pan. All rights reserved.
33
Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Jz Pan
55
-/
6-
import Mathlib.Algebra.CharP.ExpChar
6+
import Mathlib.Algebra.CharP.Lemmas
77
import Mathlib.Algebra.CharP.IntermediateField
88
import Mathlib.FieldTheory.PurelyInseparable.Basic
99

‎Mathlib/RingTheory/Perfection.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ Copyright (c) 2020 Kenny Lau. All rights reserved.
33
Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Kenny Lau
55
-/
6-
import Mathlib.Algebra.CharP.ExpChar
6+
import Mathlib.Algebra.CharP.Frobenius
77
import Mathlib.Algebra.CharP.Pi
88
import Mathlib.Algebra.CharP.Quotient
99
import Mathlib.Algebra.CharP.Subring

0 commit comments

Comments
 (0)