neZeroSubmonoid

Stream: mathlib4

[Kenny Lau]

import Mathlib.Algebra.Group.Equiv.Defs
import Mathlib.Algebra.Group.Submonoid.Defs
import Mathlib.Algebra.GroupWithZero.Units.Basic

variable (α : Type*) [MulZeroOneClass α] [Nontrivial α] [NoZeroDivisors α]

def neZeroSubmonoid : Submonoid α where
  carrier := { x | x ≠ 0 }
  mul_mem' := mul_ne_zero
  one_mem' := one_ne_zero

instance (x : neZeroSubmonoid α) : NeZero (x : α) :=
  ⟨x.property⟩

@[simps] def Units.equivNeZeroSubmonoid (α : Type*) [GroupWithZero α] :
    Units α ≃* neZeroSubmonoid α where
  toFun x := ⟨x, x.ne_zero⟩
  invFun x := Units.mk0 x x.2
  map_mul' x y := rfl

[Kenny Lau]

I think we've reached the point that we would benefit from having neZeroSubmonoid

[Kenny Lau]

this would for example make IsValuativeTopology smoother:

/-- We say that a topology on `R` is valuative if the neighborhoods of `0` in `R`
are determined by the relation `· ≤ᵥ ·`. -/
class IsValuativeTopology (R : Type*) [CommRing R] [ValuativeRel R] [TopologicalSpace R] where
  mem_nhds_iff {s : Set R} {x : R} : s ∈ 𝓝 (x : R) ↔
    ∃ γ : (ValueGroupWithZero R)ˣ, (x + ·) '' { z | valuation _ z < γ } ⊆ s

[Kenny Lau]

in the context of ring theory, neZeroSubmonoid is useful for domains as well

[Kenny Lau]

uh... as I'm typing this I remembered that nonZeroDivisors exists

[Kenny Lau]

@Yakov Pechersky do you want to refactor the current uses of Units (ValueGroupWithZero R) to nonZeroDivisors (ValueGroupWithZero R)?

[Yakov Pechersky]

No, not really =C. One could make a version of that mem_nhds_iff to place the non-zero aspect into the p portion of the l.HasBasis p s, but it's not clear why one phrasing is better than the other, especially since we have Units.val in one direction, but no clean nonZeroDivisors -> Units in the other. And since the codomain is a groupWithZero, != 0 is a simpler way of referring to being a "nonZeroDivisor" anyway.

[Kenny Lau]

units are slightly harder to make

[Kenny Lau]

I just remember having to type Units.mk0 and u.ne_zero a lot of times when I was working with local fields

[Yakov Pechersky]

Units.mk0 and IsUnit.mk0 are pretty easy, especially with lift tactic support.

[Kenny Lau]

then at that point it's like, what benefit is there of using units, when what i'm just using is ne_zero

[Yakov Pechersky]

We also have docs#GroupWithZero.eq_zero_or_unit, which lends itself easily to an rcases or obtain with a rfl destruct

[Yakov Pechersky]

The nice thing about G0ˣ is that you have a group still, you can multiply in it. I don't care either which way about how the class is defined, as long as the helper HasBasis lemmas exist.

[Kenny Lau]

you can also multiply by nonZeroDivisors