/
Quotient.lean
66 lines (55 loc) · 2.8 KB
/
Quotient.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
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
/-
Copyright (c) 2020 Kenny Lau. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Kenny Lau, Eric Wieser
-/
import Mathlib.Algebra.CharP.Basic
import Mathlib.RingTheory.Ideal.Quotient
import Mathlib.RingTheory.Ideal.Operations
#align_import algebra.char_p.quotient from "leanprover-community/mathlib"@"85e3c05a94b27c84dc6f234cf88326d5e0096ec3"
/-!
# Characteristic of quotients rings
-/
universe u v
namespace CharP
theorem quotient (R : Type u) [CommRing R] (p : ℕ) [hp1 : Fact p.Prime] (hp2 : ↑p ∈ nonunits R) :
CharP (R ⧸ (Ideal.span ({(p : R)} : Set R) : Ideal R)) p :=
have hp0 : (p : R ⧸ (Ideal.span {(p : R)} : Ideal R)) = 0 :=
map_natCast (Ideal.Quotient.mk (Ideal.span {(p : R)} : Ideal R)) p ▸
Ideal.Quotient.eq_zero_iff_mem.2 (Ideal.subset_span <| Set.mem_singleton _)
ringChar.of_eq <|
Or.resolve_left ((Nat.dvd_prime hp1.1).1 <| ringChar.dvd hp0) fun h1 =>
hp2 <|
isUnit_iff_dvd_one.2 <|
Ideal.mem_span_singleton.1 <|
Ideal.Quotient.eq_zero_iff_mem.1 <|
@Subsingleton.elim _ (@CharOne.subsingleton _ _ (ringChar.of_eq h1)) _ _
#align char_p.quotient CharP.quotient
/-- If an ideal does not contain any coercions of natural numbers other than zero, then its quotient
inherits the characteristic of the underlying ring. -/
theorem quotient' {R : Type*} [CommRing R] (p : ℕ) [CharP R p] (I : Ideal R)
(h : ∀ x : ℕ, (x : R) ∈ I → (x : R) = 0) : CharP (R ⧸ I) p :=
⟨fun x => by
rw [← cast_eq_zero_iff R p x, ← map_natCast (Ideal.Quotient.mk I)]
refine' Ideal.Quotient.eq.trans (_ : ↑x - 0 ∈ I ↔ _)
rw [sub_zero]
exact ⟨h x, fun h' => h'.symm ▸ I.zero_mem⟩⟩
#align char_p.quotient' CharP.quotient'
/-- `CharP.quotient'` as an `Iff`. -/
theorem quotient_iff {R : Type*} [CommRing R] (n : ℕ) [CharP R n] (I : Ideal R) :
CharP (R ⧸ I) n ↔ ∀ x : ℕ, ↑x ∈ I → (x : R) = 0 := by
refine ⟨fun _ x hx => ?_, CharP.quotient' n I⟩
rw [CharP.cast_eq_zero_iff R n, ← CharP.cast_eq_zero_iff (R ⧸ I) n _]
exact (Submodule.Quotient.mk_eq_zero I).mpr hx
/-- `CharP.quotient_iff`, but stated in terms of inclusions of ideals. -/
theorem quotient_iff_le_ker_natCast {R : Type*} [CommRing R] (n : ℕ) [CharP R n] (I : Ideal R) :
CharP (R ⧸ I) n ↔ I.comap (Nat.castRingHom R) ≤ RingHom.ker (Nat.castRingHom R) := by
rw [CharP.quotient_iff, RingHom.ker_eq_comap_bot]; rfl
end CharP
theorem Ideal.Quotient.index_eq_zero {R : Type*} [CommRing R] (I : Ideal R) :
(↑I.toAddSubgroup.index : R ⧸ I) = 0 := by
rw [AddSubgroup.index, Nat.card_eq]
split_ifs with hq; swap; simp
letI : Fintype (R ⧸ I) := @Fintype.ofFinite _ hq
exact CharP.cast_card_eq_zero (R ⧸ I)
#align ideal.quotient.index_eq_zero Ideal.Quotient.index_eq_zero