-
Notifications
You must be signed in to change notification settings - Fork 257
/
Algebra.lean
51 lines (39 loc) · 1.5 KB
/
Algebra.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
/-
Copyright (c) 2021 Johan Commelin. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Johan Commelin
-/
import Mathlib.Data.ZMod.Basic
import Mathlib.Algebra.Algebra.Basic
#align_import data.zmod.algebra from "leanprover-community/mathlib"@"0723536a0522d24fc2f159a096fb3304bef77472"
/-!
# The `ZMod n`-algebra structure on rings whose characteristic divides `n`
-/
namespace ZMod
variable (R : Type*) [Ring R]
instance (p : ℕ) : Subsingleton (Algebra (ZMod p) R) :=
⟨fun _ _ => Algebra.algebra_ext _ _ <| RingHom.congr_fun <| Subsingleton.elim _ _⟩
section
variable {n : ℕ} (m : ℕ) [CharP R m]
/-- The `ZMod n`-algebra structure on rings whose characteristic `m` divides `n`.
See note [reducible non-instances]. -/
@[reducible]
def algebra' (h : m ∣ n) : Algebra (ZMod n) R :=
{ ZMod.castHom h R with
smul := fun a r => cast a * r
commutes' := fun a r =>
show (cast a * r : R) = r * cast a by
rcases ZMod.int_cast_surjective a with ⟨k, rfl⟩
show ZMod.castHom h R k * r = r * ZMod.castHom h R k
rw [map_intCast, Int.cast_comm]
smul_def' := fun a r => rfl }
#align zmod.algebra' ZMod.algebra'
end
/-- The `zmod p`-algebra structure on a ring of characteristic `p`. This is not an
instance since it creates a diamond with `algebra.id`.
See note [reducible non-instances]. -/
@[reducible]
def algebra (p : ℕ) [CharP R p] : Algebra (ZMod p) R :=
algebra' R p dvd_rfl
#align zmod.algebra ZMod.algebra
end ZMod