[Merged by Bors] - feat(algebra/char_p/mixed_char_zero): define mixed/equal characteristic zero

[joneugster]

API for equal/mixed characteristic zero with main theorem to split propositions by characteristics.

---

This is a stand-alone PR contained in one file and should therefore be rather quick to review. The main result of this PR is theorem split_by_characteristic.

Often it is useful to consider mixed characteristic (0, p) and equal characteristic zero independently. This document provides the definitions and API.

This definition exists for example in nLab.

A commutative ring R of characteristic 0 is called a ring of mixed characteristic if R has an Ideal I such that the quotient R/I is of prime characteristic.

Similar the definition exists in Stacks Project (Tag 09EK), although in a slightly less general context.

Let A be a discrete valuation ring. We say A has mixed characteristic if the characteristic of the residue field of A is p>0 and the characteristic of the fraction field of A is 0. In this case we obtain an extension of discrete valuation rings Z(p)⊂A and the absolute ramification index of A is the ramification index of this extension.

• depends on: [Merged by Bors] - feat(tactic/field_simp): extend field_simp to partial division and units #14897
• depends on: [Merged by Bors] - feat(data/rat/defs): add denominator as pnat #15101
• depends on: [Merged by Bors] - feat(data/rat/defs): add two lemmas for pnat_denom of 0 and 1 #15864

[Vierkantor]

I must say that I can't really think of a case where we already have an instance algebra ℚ R on our hands but no char_zero. Do you have a specific use case in mind? (I was thinking along the lines of polynomial ℚ, but we already directly show that polynomial has the same characteristic without going through algebra.)

Otherwise these definitions are definitely not suitable as (local) instances as you remark above, so let's add a docstring to warn the users. (I believe using it as haveI : char_zero R := Q_algebra_char_zero R is safe, since char_zero lives in Prop there won't be any defeq issues.)

Another remark is that we assume semiring R in the first lemma but algebra ℚ R means that R contains -1 so it is at least a ring. This is probably fine, but a little surprising.

A final little thing is that I don't really like the names. How about these?

Suggested change

	lemma Q_algebra_char_p_zero [semiring R] [algebra ℚ R] : char_p R 0 :=
	char_p_of_injective_algebra_map (algebra_map ℚ R).injective 0
	lemma Q_algebra_char_zero [ring R] [algebra ℚ R] : char_zero R :=
	@char_p.char_p_to_char_zero R _ (Q_algebra_char_p_zero R)
	/-- A nontrivial `ℚ`-algebra has `char_p` equal to zero.
	This cannot be a (local) instance because it would immediately form a loop with the instance `algebra_rat`.
	It's probably easier to go the other way: prove `char_zero R` and automatically receive an `algebra ℚ R` instance.
	-/
	lemma algebra_rat.char_p_zero [semiring R] [algebra ℚ R] : char_p R 0 :=
	char_p_of_injective_algebra_map (algebra_map ℚ R).injective 0
	/-- A nontrivial `ℚ`-algebra has characteristic zero.
	This cannot be a (local) instance because it would immediately form a loop with the instance `algebra_rat`.
	It's probably easier to go the other way: prove `char_zero R` and automatically receive an `algebra ℚ R` instance.
	-/
	lemma algebra_rat.char_zero [ring R] [algebra ℚ R] : char_zero R :=
	@char_p.char_p_to_char_zero R _ (Q_algebra_char_p_zero R)

[Vierkantor]

Update: I see, something like this gets used for example in Q_algebra_to_equal_char_zero.

[joneugster]

Another remark is that we assume semiring R in the first lemma but algebra ℚ R means that R contains -1 so it is at least a ring. This is probably fine, but a little surprising.
Would it be worth adding that comment as something like instance xyz [semiring R] [algebra ℚ R] : ring R := sorry in a new PR?

I personally don't care (here in this PR) about semirings and that first lemma, just added it because char_p _ 0 and char_zero run somewhat parallel.

[Vierkantor]

The nicer way I know is the transitivity tactic.

[joneugster]

Thank you @Vierkantor and @jcommelin ! (especially also for the tactics-tutorial)
I've now incorporated all suggestions you've made.

[jcommelin]

Thanks 🎉

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests