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

- Positive characteristic:
`CharP R p`

(where`p ≠ 0`

) - Equal characteristic zero:
`Algebra ℚ R`

- 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 #

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

## Instances

Reduction to `p`

prime: When proving any statement `P`

about mixed characteristic rings we
can always assume that `p`

is prime.

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.pnatDen`

)
for the direction `(1) ← (2)`

.

Note: Property `(2)`

is denoted as `EqualCharZero`

in the statement names below.

Equal characteristic implies `ℚ`

-algebra.

## Equations

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

## Instances For

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.

Split any `Prop`

over `R`

into the three cases:

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

.

In an `IsDomain R`

, split any `Prop`

over `R`

into the three cases:

*prime*characteristic.- equal characteristic zero.
- mixed characteristic
`(0, p)`

.

In a `LocalRing R`

, split any `Prop`

over `R`

into the three cases:

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

.