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) [CommRing 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 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).

• toCharZero : CharZero R
• charP_quotient : ∃ (I : Ideal R), I ≠ ⊤ ∧ CharP (R ⧸ I) p

theorem MixedCharZero.toCharZero {R : Type u_1} : ∀ {inst : CommRing R} (p : ℕ) [self : MixedCharZero R p], CharZero R

theorem MixedCharZero.charP_quotient {R : Type u_1} : ∀ {inst : CommRing R} {p : ℕ} [self : MixedCharZero R p], ∃ (I : Ideal R), I ≠ ⊤ ∧ CharP (R ⧸ I) p

theorem MixedCharZero.reduce_to_p_prime (R : Type u_1) [CommRing R] {P : Prop} : (∀ p > 0, MixedCharZero R p → P) ↔ ∀ (p : ℕ), Nat.Prime p → MixedCharZero 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 MixedCharZero.reduce_to_maximal_ideal (R : Type u_1) [CommRing R] {p : ℕ} (hp : Nat.Prime p) : (∃ (I : Ideal R), I ≠ ⊤ ∧ CharP (R ⧸ I) p) ↔ ∃ (I : Ideal R), 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) [CommRing R] [Algebra ℚ R] (I : Ideal R) : I ≠ ⊤ → CharZero (R ⧸ I)

ℚ-algebra implies equal characteristic.

theorem EqualCharZero.PNat.isUnit_natCast {R : Type u_1} [CommRing R] [h : Fact (∀ (I : Ideal R), 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} [CommRing R] [Fact (∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I))] : ℕ+ → Rˣ

Equations

• ↑n = ⋯.unit

noncomputable instance EqualCharZero.coePNatUnits {R : Type u_1} [CommRing R] [Fact (∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I))] : Coe ℕ+ Rˣ

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} [CommRing R] [Fact (∀ (I : Ideal R), 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} [CommRing R] [Fact (∀ (I : Ideal R), 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} [CommRing R] (h : ∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I)) : Algebra ℚ R

Equal characteristic implies ℚ-algebra.

Equations

• EqualCharZero.algebraRat h = { toFun := fun (x : ℚ) => ↑x.num /ₚ ↑x.pnatDen, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }.toAlgebra

theorem EqualCharZero.of_not_mixedCharZero (R : Type u_1) [CommRing R] [CharZero R] (h : ∀ p > 0, ¬MixedCharZero R p) (I : Ideal R) : I ≠ ⊤ → CharZero (R ⧸ I)

Not mixed characteristic implies equal characteristic.

theorem EqualCharZero.to_not_mixedCharZero (R : Type u_1) [CommRing R] (h : ∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I)) (p : ℕ) : p > 0 → ¬MixedCharZero R p

Equal characteristic implies not mixed characteristic.

theorem EqualCharZero.iff_not_mixedCharZero (R : Type u_1) [CommRing R] [CharZero R] : (∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I)) ↔ ∀ p > 0, ¬MixedCharZero R p

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) [CommRing R] : Nonempty (Algebra ℚ R) ↔ ∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I)

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

theorem isEmpty_algebraRat_iff_mixedCharZero (R : Type u_1) [CommRing R] [CharZero R] : IsEmpty (Algebra ℚ R) ↔ ∃ p > 0, MixedCharZero 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_equalCharZero_mixedCharZero (R : Type u_1) [CommRing R] {P : Prop} [CharZero R] (h_equal : Algebra ℚ R → P) (h_mixed : ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P) : P

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

theorem split_by_characteristic (R : Type u_1) [CommRing R] {P : Prop} (h_pos : ∀ (p : ℕ), p ≠ 0 → CharP R p → P) (h_equal : Algebra ℚ R → P) (h_mixed : ∀ (p : ℕ), Nat.Prime p → MixedCharZero 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) [CommRing R] {P : Prop} [IsDomain R] (h_pos : ∀ (p : ℕ), Nat.Prime p → CharP R p → P) (h_equal : Algebra ℚ R → P) (h_mixed : ∀ (p : ℕ), Nat.Prime p → MixedCharZero R 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) [CommRing R] {P : Prop} [LocalRing R] (h_pos : ∀ (p : ℕ), IsPrimePow p → CharP R p → P) (h_equal : Algebra ℚ R → P) (h_mixed : ∀ (p : ℕ), Nat.Prime p → MixedCharZero R 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).