CharZero_of_ringChar_zero

Stream: Is there code for X?

[Damiano Testa]

Dear All,

I could not find the result below in mathlib: is it there? If not, should I PR it?

import Mathlib.Algebra.CharP.Basic

-- is this already in mathlib?
theorem CharZero_of_ringChar_zero [NonAssocRing F] (c0 : ringChar F = 0) : CharZero F := sorry

Thanks!

[Richard Copley]

Do you mind if I post a proof? You can tell me how stupid it is and how you would have done it :smile:

[Kevin Buzzard]

Please do -- that's how the site works :-) We all learn together.

[Richard Copley]

import Mathlib.Algebra.CharP.Basic

theorem CharZero_of_ringChar_zero [NonAssocRing F] (c0 : ringChar F = 0) : CharZero F := by
  have char_eq_zero : CharP F 0 := ringChar.of_eq c0
  have f {a b : ℕ} (hle : a ≤ b) (heq : (a : F) = b) : a = b := by
    apply Nat.le_antisymm hle ∘ Nat.le_of_sub_eq_zero ∘ Nat.eq_zero_of_zero_dvd
    rw [← CharP.cast_eq_zero_iff F 0, Nat.cast_sub hle, sub_eq_zero, heq]
  constructor
  intro a b
  cases Nat.le_total a b with
  | inl hab => exact f hab
  | inr hba => rewrite [eq_comm, eq_comm (a := a)] ; exact f hba

[Richard Copley]

Ha, it is pretty stupid. This is better:

import Mathlib.Algebra.CharP.Basic

theorem CharZero_of_ringChar_zero [NonAssocRing F] (c0 : ringChar F = 0) : CharZero F := by
  have char_eq_zero : CharP F 0 := ringChar.of_eq c0
  exact CharP.charP_to_charZero F

[Damiano Testa]

This is what I had:

open CharP in
theorem ringChar_zero_iff_CharZero [NonAssocRing F] : ringChar F = 0 ↔ CharZero F := by
  rw [ringChar.eq_iff]
  exact ⟨fun _ => charP_to_charZero F, fun _ => ofCharZero F⟩

[Damiano Testa]

(After posting the initial question, I realized that, even though I did not need it, the converse also held.)

[Eric Rodriguez]

one direction holds for semirings, I think

[Damiano Testa]

example [NonAssocSemiring F] [CharZero F] : ringChar F = 0 := ringChar.eq_zero

[Damiano Testa]

Anyway, my question is more about the fact that I always find it hard to navigate the API around characteristics of [remove your favourite subset of assumptions]-rings.

[Jireh Loreaux]

Here's a fun fact which I have been trying to use to my advantage recently: docs#CharZero isn't even technically about rings (per the definition)!

[Eric Rodriguez]

(how can you use this to your advantage?)

[Jireh Loreaux]

If R is a Ring and a StarOrderedRing which is also Nontrivial, then the subtype { x : R // 0 ≤ x}is an AddCommMonoidWithOne and docs#StrictOrderedSemiring.to_charZero generalizes a bit (see #4871 or #6310), so in particular you can get these lemmas for free for α := {x : R // 0 ≤ x}.

[Damiano Testa]

#6572

[Oliver Nash]

It's a bit sad that we can write CharP R 0 as well as CharZero R and furthermore that they are not even propositionally equivalent without additive inverses. I thus wonder:

1. do we ever want the weird meaning of CharP R 0 when we have no additive inverses?
2. if the answer to 1 is "no" then could we redefine CharP so that CharP R 0 means what CharZero R means and then either delete CharZero or make it an abbreviation for CharP R 0?

[Damiano Testa]

I did not think carefully about formalizing Char, but I do find it always tricky to move around this part of the library.

I personally do not have a good reason behind the current CharP R 0. I think that I wrote the counterexample and I did so because I found CharP R 0 weird!

I sometimes think about whether having a class CharIsPrimeOrZero would improve the situation, but this has never gone past the thinking stage.

[Oliver Nash]

For the sake of definiteness, I propose replacing docs#CharP with:

class ActualCharP (R : Type*) [AddMonoidWithOne R] (p : ℕ) : Prop where
    cast_eq_iff : ∀ x y : ℕ, (x : R) = (y : R) ↔ (x : ZMod p) = (y : ZMod p)

and removing CharZero.

I'd appreciate any feedback.

[Damiano Testa]

Am I right that p = 1 always works? And for "more composite" ps even more will work?

[Oliver Nash]

Yes (except for the p = 1 point, as clarified by Eric below). Note that ActualCharP is equivalent to docs#CharP when we have additive inverses and it's easy to read off these these conclusions from the statement there.

[Oliver Nash]

For emphasis: what I have proposed is propositionally identical to docs#CharP for an AddGroupWithOne.

[Eric Rodriguez]

I don't see how p = 1 works?

[Eric Rodriguez]

I think this is a good idea, however

[Damiano Testa]

Eric, you are right: I only thought of one implication, not the iff!

[Oliver Nash]

Eric's correction got me worried enough to prove my various claims above:

import Mathlib.Algebra.CharP.Basic
import Mathlib.Data.ZMod.Basic

class ActualCharP (R : Type*) [AddMonoidWithOne R] (p : ℕ) : Prop where
    cast_eq_iff : ∀ x y : ℕ, (x : R) = (y : R) ↔ (x : ZMod p) = (y : ZMod p)

-- No change if we have additive inverses
example (R : Type*) [AddGroupWithOne R] (p : ℕ) :
    CharP R p ↔ ActualCharP R p := by
  refine' ⟨fun h ↦ ⟨fun x y ↦ _⟩, _⟩
  · rw [CharP.natCast_eq_natCast R p, ← ZMod.eq_iff_modEq_nat]
  · rintro ⟨h⟩
    refine' CharP.mk fun x ↦ _
    specialize h x 0
    rw [Nat.cast_zero] at h
    rw [h, Nat.cast_zero]
    exact ZMod.nat_cast_zmod_eq_zero_iff_dvd x p

-- What's more:
example (R : Type*) [AddMonoidWithOne R] : CharZero R ↔ ActualCharP R 0 := by
  refine' ⟨fun h ↦ ⟨by simp⟩, _⟩
  rintro ⟨h⟩
  refine' CharZero.mk fun x y hxy ↦ _
  specialize h x y
  simp only [Nat.cast_inj] at h
  rw [← h, hxy]