# mathlib3documentation

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:

1. Positive characteristic: char_p R p (where p ≠ 0)
2. Equal characteristic zero: algebra ℚ R
3. 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

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 P) (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:

1. R is a ℚ-algebra.
2. The quotient R ⧸ I has characteristic zero for any proper ideal I ⊂ R.
3. 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] [ R] (I : ideal R) :

ℚ-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))] :

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

Equations
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)) :
R

Equal characteristic implies ℚ-algebra.

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

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) :

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 ¬

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 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 R) (p : ) (H : p > 0),

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 : R P) (h_mixed : (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 p P) (h_equal : R P) (h_mixed : (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 : ), p P) (h_equal : R P) (h_mixed : (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 : ), p P) (h_equal : R P) (h_mixed : (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).