Z_p is a Henselian local ring

Stream: maths

[Johan Commelin]

class henselian (R : Type*) [comm_ring R] extends local_ring R : Prop :=
(is_henselian : ∀ (f : polynomial R) (hf : f.monic) (a₀ : R) (h₁ : f.eval a₀ ∈ maximal_ideal R)
  (h₂ : is_unit (f.derivative.eval a₀)),
  ∃ a : R, f.is_root a ∧ (a - a₀ ∈ maximal_ideal R))

instance is_adic_complete.henselian (R : Type*)
  [comm_ring R] [local_ring R] [is_adic_complete (maximal_ideal R) R] :
  henselian R :=
-- long proof

instance (p : ℕ) [fact p.prime] : henselian ℤ_[p] := infer_instance

https://github.com/leanprover-community/mathlib/pull/8986/files#diff-cfe5a51d476c544368bad568fb985d5b8dae8a645bd7434e8da6b9a9da5f29e4R664

[Johan Commelin]

I still need to clean up a bunch of prerequisites. But the code is sorry free.

[Kevin Buzzard]

Dumb maths question: is this equivalent to "a factorization of f mod m into coprime monics lifts"? You've just done the case where a factor is linear.

[Kevin Buzzard]

Henselization is I think like localization and completion -- it's unique up to unique isomorphism.

[Kevin Buzzard]

Dumb Lean question: why should these things be classes rather than structures? Is it just because they're props so they may as well be?

[Adam Topaz]

Kevin Buzzard said:

Dumb maths question: is this equivalent to "a factorization of f mod m into coprime monics lifts"? You've just done the case where a factor is linear.

This is equivalent, but the proof is not easy: stacks#04GG

[Adam Topaz]

It's time to work on etale maps :)

[Adam Topaz]

(There may be a more elementary proof of this equivalence though.)

[Kevin Buzzard]

My feeling is that if we take any interesting class of morphisms of schemes (e.g. finite, etale, affine...) and define this concept for rings and then try to extend it to schemes, we will find out pretty quickly what we should be doing next in algebraic geometry (or we might even find that our current set-up is not ideal).

[Johan Commelin]

I've finished cleaning up the whole mess. It's now about 10 PRs

[Johan Commelin]

The next two PRs in this saga are

• #8991 feat(ring_theory/ideal/local_ring): residue field is an algebra
• #8993 feat(linear_algebra/smodeq): sub_mem, eval

[Johan Commelin]

Another one is unblocked:

• #8994 feat(ring_theory/discrete_valuation_ring): is_Hausdorff

[Johan Commelin]

And we're ready for the "big" one:

• #8986 feat(ring_theory/henselian): Henselian local rings

[Johan Commelin]

The PR contains

  -- `R` is a local ring
  let inv : R → R := λ x, if hx : is_unit x then ↑hx.some⁻¹ else 0,
  have hinv : ∀ x, is_unit x → x * inv x = 1,
  { intros x hx, simp only [hx, inv, dif_pos], convert units.mul_inv hx.some, rw hx.some_spec },

as part of a proof.
Should we have a noncomputable monoid_with_zero.inv globally?

[Johan Commelin]

Hmm, if the junk value is 1, it could even be defined for arbitrary monoids.

[Anne Baanen]

That seems like it would give a lot of defeq issues, if you want to use monoid.inv in the place of group_with_zero.has_inv.inv.

[Johan Commelin]

If we define it globally, it should come with a big warning sign: :danger: :nuclear: :biohazard: USE WITH CARE!

[Reid Barton]

probably it should not be called inv, since it isn't the inverse

[Kevin Buzzard]

of course the same could be said for inv on a field...

[Anne Baanen]

inv_ish? :upside_down:

[Anne Baanen]

notation x`☡` := monoid.accursed_unutterable_unsafe_inv

[Kevin Buzzard]

That notation is already taken for nat.sub on my branch of mathlib.

[Johan Commelin]

It's only three lines of code. I'm fine with keeping it inline in the proof, for now.

[Johan Commelin]

If it shows up more often, we can extract it into a global def.

[Yakov Pechersky]

We kinda have this already for fields and my wip PR on matrices, where one can upgrade a monoid to a div_inv_monoid over some predicate. Cf fpow

[Eric Wieser]

Isn't this docs#ring.inverse?

[Eric Wieser]

Which just to keep things interesting, only requires monoid_with_zero

[Johan Commelin]

@Eric Wieser Brilliant, so it already exists.

[Eric Wieser]

Having looked at its definition, it might be better to replace h.some with h.unit

[Johan Commelin]

I don't have thoughts about that

[Johan Commelin]

Eric Wieser said:

Having looked at its definition, it might be better to replace h.some with h.unit

Done. And updated the henselian PR to use ring.inverse