mathlib3 documentation

algebra.char_p.mixed_char_zero

Equal and mixed characteristic #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

In commutative algebra, some statments are simpler when working over a ℚ-algebra R, in which case one also says that the ring has "equal characteristic zero". A ring that is not a ℚ-algebra has either positive characteristic or there exists a prime ideal I ⊂ R such that the quotient R ⧸ I has positive characteristic p > 0. In this case one speaks of "mixed characteristic (0, p)", where p is only unique if R is local.

Examples of mixed characteristic rings are ℤ or the p-adic integers/numbers.

This file provides the main theorem split_by_characteristic that splits any proposition P into the following three cases:

Positive characteristic: char_p R p (where p ≠ 0)
Equal characteristic zero: algebra ℚ R
Mixed characteristic: mixed_char_zero R p (where p is prime)

Main definitions #

mixed_char_zero : A ring has mixed characteristic (0, p) if it has characteristic zero and there exists an ideal such that the quotient R ⧸ I has characteristic p.

Main results #

split_equal_mixed_char : Split a statement into equal/mixed characteristic zero.

This main theorem has the following three corollaries which include the positive characteristic case for convenience:

split_by_characteristic : Generally consider positive char p ≠ 0.
split_by_characteristic_domain : In a domain we can assume that p is prime.
split_by_characteristic_local_ring : In a local ring we can assume that p is a prime power.

TODO #

Relate mixed characteristic in a local ring to p-adic numbers [number_theory.padics].

Mixed characteristic #

@[class]

structure mixed_char_zero (R : Type u_1) [comm_ring R] (p : ℕ) :

Prop

to_char_zero : char_zero R
char_p_quotient : ∃ (I : ideal R), I ≠ ⊤ ∧ char_p (R ⧸ I) p

A ring of characteristic zero is of "mixed characteristic (0, p)" if there exists an ideal such that the quotient R ⧸ I has caracteristic p.

Remark: For p = 0, mixed_char R 0 is a meaningless definition as R ⧸ ⊥ ≅ R has by definition always characteristic zero. One could require (I ≠ ⊥) in the definition, but then mixed_char R 0 would mean something like ℤ-algebra of extension degree ≥ 1 and would be completely independent from whether something is a ℚ-algebra or not (e.g. ℚ[X] would satisfy it but ℚ wouldn't).

theorem mixed_char_zero.reduce_to_p_prime (R : Type u_1) [comm_ring R] {P : Prop} :

(∀ (p : ℕ), p > 0 → mixed_char_zero R p → P) ↔ ∀ (p : ℕ), nat.prime p → mixed_char_zero R p → P

Reduction to p prime: When proving any statement P about mixed characteristic rings we can always assume that p is prime.

theorem mixed_char_zero.reduce_to_maximal_ideal (R : Type u_1) [comm_ring R] {p : ℕ} (hp : nat.prime p) :

(∃ (I : ideal R), I ≠ ⊤ ∧ char_p (R ⧸ I) p) ↔ ∃ (I : ideal R), I.is_maximal ∧ char_p (R ⧸ I) p

Reduction to I prime ideal: When proving statements about mixed characteristic rings, after we reduced to p prime, we can assume that the ideal I in the definition is maximal.

Equal characteristic zero #

A commutative ring R has "equal characteristic zero" if it satisfies one of the following equivalent properties:

R is a ℚ-algebra.
The quotient R ⧸ I has characteristic zero for any proper ideal I ⊂ R.
R has characteristic zero and does not have mixed characteristic for any prime p.

We show (1) ↔ (2) ↔ (3), and most of the following is concerned with constructing an explicit algebra map ℚ →+* R (given by x ↦ (x.num : R) /ₚ ↑x.pnat_denom) for the direction (1) ← (2).

Note: Property (2) is denoted as equal_char_zero in the statement names below.

@[nolint]

theorem Q_algebra_to_equal_char_zero (R : Type u_1) [comm_ring R] [nontrivial R] [algebra ℚ R] (I : ideal R) :

I ≠ ⊤ → char_zero (R ⧸ I)

ℚ-algebra implies equal characteristic.

theorem equal_char_zero.pnat_coe_is_unit (R : Type u_1) [comm_ring R] [h : fact (∀ (I : ideal R), I ≠ ⊤ → char_zero (R ⧸ I))] (n : ℕ+) :

Internal: Not intended to be used outside this local construction.

@[protected, instance]

noncomputable def equal_char_zero.pnat_has_coe_units (R : Type u_1) [comm_ring R] [fact (∀ (I : ideal R), I ≠ ⊤ → char_zero (R ⧸ I))] :

has_coe_t ℕ+ Rˣ

Internal: Not intended to be used outside this local construction.

Equations

equal_char_zero.pnat_has_coe_units R = {coe := λ (n : ℕ+), _.unit}

theorem equal_char_zero.pnat_coe_units_eq_one (R : Type u_1) [comm_ring R] [fact (∀ (I : ideal R), I ≠ ⊤ → char_zero (R ⧸ I))] :

↑1 = 1

Internal: Not intended to be used outside this local construction.

theorem equal_char_zero.pnat_coe_units_coe_eq_coe (R : Type u_1) [comm_ring R] [fact (∀ (I : ideal R), I ≠ ⊤ → char_zero (R ⧸ I))] (n : ℕ+) :

Internal: Not intended to be used outside this local construction.

noncomputable def equal_char_zero_to_Q_algebra (R : Type u_1) [comm_ring R] (h : ∀ (I : ideal R), I ≠ ⊤ → char_zero (R ⧸ I)) :

Equal characteristic implies ℚ-algebra.

Equations

equal_char_zero_to_Q_algebra R h = {to_fun := λ (x : ℚ), ↑(x.num) /ₚ ↑(x.pnat_denom), map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}.to_algebra

theorem not_mixed_char_to_equal_char_zero (R : Type u_1) [comm_ring R] [char_zero R] (h : ∀ (p : ℕ), p > 0 → ¬mixed_char_zero R p) (I : ideal R) :

I ≠ ⊤ → char_zero (R ⧸ I)

Not mixed characteristic implies equal characteristic.

theorem equal_char_zero_to_not_mixed_char (R : Type u_1) [comm_ring R] (h : ∀ (I : ideal R), I ≠ ⊤ → char_zero (R ⧸ I)) (p : ℕ) (H : p > 0) :

¬mixed_char_zero R p

Equal characteristic implies not mixed characteristic.

theorem equal_char_zero_iff_not_mixed_char (R : Type u_1) [comm_ring R] [char_zero R] :

(∀ (I : ideal R), I ≠ ⊤ → char_zero (R ⧸ I)) ↔ ∀ (p : ℕ), p > 0 → ¬mixed_char_zero R p

A ring of characteristic zero has equal characteristic iff it does not have mixed characteristic for any p.

theorem Q_algebra_iff_equal_char_zero (R : Type u_1) [comm_ring R] [nontrivial R] :

nonempty (algebra ℚ R) ↔ ∀ (I : ideal R), I ≠ ⊤ → char_zero (R ⧸ I)

A ring is a ℚ-algebra iff it has equal characteristic zero.

theorem not_Q_algebra_iff_not_equal_char_zero (R : Type u_1) [comm_ring R] [char_zero R] :

is_empty (algebra ℚ R) ↔ ∃ (p : ℕ) (H : p > 0), mixed_char_zero R p

A ring of characteristic zero is not a ℚ-algebra iff it has mixed characteristic for some p.

Splitting statements into different characteristic #

Statements to split a proof by characteristic. There are 3 theorems here that are very similar. They only differ in the assumptions we can make on the positive characteristic case: Generally we need to consider all p ≠ 0, but if R is a local ring, we can assume that p is a prime power. And if R is a domain, we can even assume that p is prime.

theorem split_equal_mixed_char (R : Type u_1) [comm_ring R] {P : Prop} [char_zero R] (h_equal : algebra ℚ R → P) (h_mixed : ∀ (p : ℕ), nat.prime p → mixed_char_zero R p → P) :

P

Split a Prop in characteristic zero into equal and mixed characteristic.

theorem split_by_characteristic (R : Type u_1) [comm_ring R] {P : Prop} (h_pos : ∀ (p : ℕ), p ≠ 0 → char_p R p → P) (h_equal : algebra ℚ R → P) (h_mixed : ∀ (p : ℕ), nat.prime p → mixed_char_zero R p → P) :

P

Split any Prop over R into the three cases:

positive characteristic.
equal characteristic zero.
mixed characteristic (0, p).

theorem split_by_characteristic_domain (R : Type u_1) [comm_ring R] {P : Prop} [is_domain R] (h_pos : ∀ (p : ℕ), nat.prime p → char_p R p → P) (h_equal : algebra ℚ R → P) (h_mixed : ∀ (p : ℕ), nat.prime p → mixed_char_zero R p → P) :

P

In a is_domain R, split any Prop over R into the three cases:

prime characteristic.
equal characteristic zero.
mixed characteristic (0, p).

theorem split_by_characteristic_local_ring (R : Type u_1) [comm_ring R] {P : Prop} [local_ring R] (h_pos : ∀ (p : ℕ), is_prime_pow p → char_p R p → P) (h_equal : algebra ℚ R → P) (h_mixed : ∀ (p : ℕ), nat.prime p → mixed_char_zero R p → P) :

P

In a local_ring R, split any Prop over R into the three cases:

prime power characteristic.
equal characteristic zero.
mixed characteristic (0, p).