IsUnit and CharP

Stream: Is there code for X?

[Eric Wieser]

Is the following true? What counterexample am I missing if not?

variable {A : Type*} [Ring A] (p : ℕ) [Fact (Nat.Prime p)] [CharP A p]
theorem natCast_iff_of_charP {n : ℕ} : IsUnit (n : A) ↔ ¬ (p ∣ n) := sorry

[Eric Wieser]

Answer: Yes, but my proof in #22237 is super ugly

[Eric Wieser]

import Mathlib

variable {A : Type*} [Ring A] (p : ℕ) [Fact (Nat.Prime p)] [CharP A p]

theorem natCast_iff_of_charP {n : ℕ} : IsUnit (n : A) ↔ ¬ (p ∣ n) := by
  constructor
  · rintro ⟨x, hx⟩
    rw [← CharP.cast_eq_zero_iff (R := A), ← hx]
    have := CharP.nontrivial_of_char_ne_one (R := A) (Nat.Prime.ne_one Fact.out : p ≠ 1)
    exact x.ne_zero
  · intro h
    rw [ ← ZMod.cast_natCast' (n := p)]
    let u : (ZMod p)ˣ := .mk0 ↑n (ZMod.natCast_zmod_eq_zero_iff_dvd _ _ |>.not.mpr h)
    let u' := u.map (ZMod.castHom (dvd_refl p) A).toMonoidHom
    exact ⟨u', rfl⟩

[Eric Wieser]

Going through ZMod.cast feels a little silly

[Aaron Liu]

I would have done it the same way

[Eric Wieser]

Maybe the resolution I want here is "generalize the approach used to build the inverse on zmod"

[Kevin Buzzard]

The inverse is p.gcdB n if that's any help

[Kevin Buzzard]

  · intro h
    rw [← Nat.Prime.coprime_iff_not_dvd Fact.out] at h
    have := h ▸ p.gcd_eq_gcd_ab n
    -- this : ↑1 = ↑p * p.gcdA n + ↑n * p.gcdB n

[Yakov Pechersky]

I would except a lemma like docs#CharTwo.two_zsmul to exist but for smul and arbitrary CharP.

[Yakov Pechersky]

Why wouldn't ZMod be the right thing to go through?

[Eric Wieser]

#22669

[Eric Wieser]

Is this stronger result true?

import Mathlib

variable [Ring R] {p : ℕ} [CharP R p]
-- I already have the other direction
theorem CharP.coprime_of_isUnit {n : ℕ} : IsUnit (n : R) → n.Coprime p

[Adam Topaz]

Yes

[Adam Topaz]

I assume we have the characterization of units in ZMod? docs#ZMod.isUnit_iff_coprime

[Eric Wieser]

docs#ZMod.isUnit_iff_coprime indeed exists

[Eric Wieser]

I don't see how to ensure that there aren't some "surprise" units in R for things that weren't units in ZMod p

[Adam Topaz]

I guess one needs to know something about the localizations of $\mathbb{Z}/n$, but I'm trying to think of a more elementary proof...

[Aaron Liu]

The non-units in ZMod p are zero-divisors

[Eric Wieser]

I'm thinking of the elements of R which live outside the range of ZMod.cast

[Aaron Liu]

Zero divisors can't be units, and that property is preserved by ring homomorphisms.

[Adam Topaz]

Right, exactly.

[Adam Topaz]

Well, they're preserved by \emph{injective} ring hom :)

[Eric Wieser]

I'm guessing I can't avoid ZMod so easily for this case?

[Adam Topaz]

I don't think so :)

[Aaron Liu]

Adam Topaz said:

Well, they're preserved by \emph{injective} ring hom :)

(forgot about 0)

[Antoine Chambert-Loir]

What about the zero ring?

[Antoine Chambert-Loir]

In any case, if a prime p is nilpotent in R, say p ^ m = 0, and n is prime to p, then there are natural integers such that a * n = b * p ^ m + 1, and this implies that n is invertible in R.