OrderedAddCommGroup has CharZero

Stream: Is there code for X?

[Violeta Hernández]

If an ordered group satisfies 0 < 1, then NatCast should be injective, right? Do we have something like this?

[Aaron Liu]

We have docs#StrictOrderedSemiring.toCharZero

[Violeta Hernández]

That's stronger than what I have, unfortunately, since my structure has no multiplication.

[Kevin Buzzard]

Whatever you mean by "group" it won't have both a 0 and a 1

[Kevin Buzzard]

Can you formalise the question?

[Aaron Liu]

Its proof doesn't need multiplication, so we could generalize this?

[Kevin Buzzard]

Do we have some kind of docs#AddMonoidWithOne

[Violeta Hernández]

docs#AddCommGroupWithOne is my relevant structure

[Violeta Hernández]

Though it might even work for non-commutative groups or monoids, I'm not sure

[Kevin Buzzard]

You'll need the order to be compatible with the addition so it's not over yet

[Violeta Hernández]

AddMonoidWithOne does seem too weak since the order doesn't interact with the structure

[Violeta Hernández]

But perhaps AddMonoidWithOne + AddRightStrictMono + 0 < 1 is enough?

[Aaron Liu]

import Mathlib

example {α : Type*} [AddMonoidWithOne α] [PartialOrder α] [ZeroLEOneClass α]
    [NeZero (1 : α)] [AddLeftStrictMono α] : CharZero α where
  cast_injective :=
    (strictMono_nat_of_lt_succ fun n ↦ by rw [Nat.cast_succ]; apply lt_add_one).injective

[Violeta Hernández]

That works for me!

[Violeta Hernández]

Does this generalize docs#StrictOrderedSemiring.toCharZero, or is it an incomparable set of assumptions?

[Aaron Liu]

95% sure its strictly more general but I'll check

[Violeta Hernández]

It generalizes!

import Mathlib

variable {α : Type*}

theorem foo [AddMonoidWithOne α] [PartialOrder α] [ZeroLEOneClass α] [NeZero (1 : α)] [AddLeftStrictMono α] : CharZero α where
  cast_injective :=
    (strictMono_nat_of_lt_succ fun n ↦ by rw [Nat.cast_succ]; apply lt_add_one).injective

example [StrictOrderedSemiring α] : CharZero α := foo

[Violeta Hernández]

Would you like to go ahead and PR this?

[Aaron Liu]

Sure

[Aaron Liu]

Should I keep the name?

[Violeta Hernández]

I think the deprecation policy generally doesn't apply to instance names

[Violeta Hernández]

You could call the new instance something like AddMonoidWithOne.toCharZero and just remove the old one

[Aaron Liu]

It feels weird having an AddMonoidWithOne class in the middle of all the StrictOrderedSemiring classes

[Aaron Liu]

#23034

[Violeta Hernández]

Can that instance perhaps be moved to some earlier file?

[Violeta Hernández]

What does #find_home AddMonoidWithOne.toCharZero give you?

[Aaron Liu]

It gave me Mathlib/Algebra/Order/Ring/Defs (the same file)

[Jireh Loreaux]

I'm fairly sure I already made this generalization somewhere, but I think I scoped the instance for performance reasons. I'll try to find it tomorrow.

[Aaron Liu]

MathlibTest.linarith failed with timeout at whnf

[Aaron Liu]

@Violeta Hernández Do you still need this?