# Equal and mixed characteristic #

In commutative algebra, some statements 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: CharP R p (where p ≠ 0)
2. Equal characteristic zero: Algebra ℚ R
3. Mixed characteristic: MixedCharZero R p (where p is prime)

## Main definitions #

• MixedCharZero : 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_equalCharZero_mixedCharZero : 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_localRing : In a local ring we can assume that p is a prime power.

## Implementation Notes #

We use the terms EqualCharZero and AlgebraRat despite not being such definitions in mathlib. The former refers to the statement ∀ I : Ideal R, I ≠ ⊤ → CharZero (R ⧸ I), the latter refers to the existence of an instance [Algebra ℚ R]. The two are shown to be equivalent conditions.

## TODO #

• Relate mixed characteristic in a local ring to p-adic numbers [NumberTheory.PAdics].

### Mixed characteristic #

class MixedCharZero (R : Type u_1) [] (p : ) :

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

Remark: For p = 0, MixedChar R 0 is a meaningless definition (i.e. satisfied by any ring) as R ⧸ ⊥ ≅ R has by definition always characteristic zero. One could require (I ≠ ⊥) in the definition, but then MixedChar 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).

Instances
theorem MixedCharZero.toCharZero {R : Type u_1} [] (p : ) [self : ] :
theorem MixedCharZero.charP_quotient {R : Type u_1} [] {p : } [self : ] :
∃ (I : ), I CharP (R I) p
theorem MixedCharZero.reduce_to_p_prime (R : Type u_1) [] {P : Prop} :
(∀ 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 MixedCharZero.reduce_to_maximal_ideal (R : Type u_1) [] {p : } (hp : ) :
(∃ (I : ), I CharP (R I) p) ∃ (I : ), I.IsMaximal CharP (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.pnatDen) for the direction (1) ← (2).

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

theorem EqualCharZero.of_algebraRat (R : Type u_1) [] [] (I : ) :
I CharZero (R I)

ℚ-algebra implies equal characteristic.

theorem EqualCharZero.PNat.isUnit_natCast {R : Type u_1} [] [h : Fact (∀ (I : ), I CharZero (R I))] (n : ℕ+) :
IsUnit n

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

noncomputable def EqualCharZero.pnatCast {R : Type u_1} [] [Fact (∀ (I : ), I CharZero (R I))] :
ℕ+Rˣ
Equations
• n = .unit
Instances For
noncomputable instance EqualCharZero.coePNatUnits {R : Type u_1} [] [Fact (∀ (I : ), I CharZero (R I))] :

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

Equations
• EqualCharZero.coePNatUnits = { coe := EqualCharZero.pnatCast }
@[simp]
theorem EqualCharZero.pnatCast_one {R : Type u_1} [] [Fact (∀ (I : ), I CharZero (R I))] :
1 = 1

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

@[simp]
theorem EqualCharZero.pnatCast_eq_natCast {R : Type u_1} [] [Fact (∀ (I : ), I CharZero (R I))] (n : ℕ+) :
n = n

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

noncomputable def EqualCharZero.algebraRat {R : Type u_1} [] (h : ∀ (I : ), I CharZero (R I)) :

Equal characteristic implies ℚ-algebra.

Equations
• = { toFun := fun (x : ) => x.num /ₚ x.pnatDen, map_one' := , map_mul' := , map_zero' := , map_add' := }.toAlgebra
Instances For
theorem EqualCharZero.of_not_mixedCharZero (R : Type u_1) [] [] (h : p > 0, ¬) (I : ) :
I CharZero (R I)

Not mixed characteristic implies equal characteristic.

theorem EqualCharZero.to_not_mixedCharZero (R : Type u_1) [] (h : ∀ (I : ), I CharZero (R I)) (p : ) :
p > 0¬

Equal characteristic implies not mixed characteristic.

theorem EqualCharZero.iff_not_mixedCharZero (R : Type u_1) [] [] :
(∀ (I : ), I CharZero (R I)) p > 0, ¬

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

theorem EqualCharZero.nonempty_algebraRat_iff (R : Type u_1) [] :
Nonempty (Algebra R) ∀ (I : ), I CharZero (R I)

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

theorem isEmpty_algebraRat_iff_mixedCharZero (R : Type u_1) [] [] :
IsEmpty (Algebra R) 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_equalCharZero_mixedCharZero (R : Type u_1) [] {P : Prop} [] (h_equal : 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) [] {P : Prop} (h_pos : ∀ (p : ), p 0CharP R pP) (h_equal : 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) [] {P : Prop} [] (h_pos : ∀ (p : ), CharP R pP) (h_equal : P) (h_mixed : ∀ (p : ), P) :
P

In an IsDomain R, split any Prop over R into the three cases:

• prime characteristic.
• equal characteristic zero.
• mixed characteristic (0, p).
theorem split_by_characteristic_localRing (R : Type u_1) [] {P : Prop} [] (h_pos : ∀ (p : ), CharP R pP) (h_equal : P) (h_mixed : ∀ (p : ), P) :
P

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

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