In a trivial monoid, everything is a unit

Stream: Is there code for X?

[Michael Stoll]

Is the following in mathlib?

import algebra.group.units

lemma monoid.unit_of_not_nontrivial {M : Type*} [monoid M] (hM : ¬ nontrivial M) (x : M) :
  is_unit x :=
cast (congr_arg is_unit $ subsingleton_iff.mp (not_nontrivial_iff_subsingleton.mp hM) 1 x)
  is_unit_one
````

[Yaël Dillies]

You would definitely spell it out with [subsingleton M] rather than (hM : ¬ nontrivial M).

[Alex J. Best]

docs#is_unit_of_subsingleton

[Eric Rodriguez]

One of the areas I find mathlib covers the most well is the trivial case :b

[Michael Stoll]

If I want to distinguish cases according to nontrivial M, how do I get [subsingleton M] from ¬ nontrivial M?

[Alex J. Best]

There are various useful lemmas near docs#subsingleton_or_nontrivial

[Michael Stoll]

OK; I realize that I'm already using this in my proof :grinning:

[Michael Stoll]

Still, I think my version has the advantage that I don't have to introduce a [subsingleton] instance first.

[Alex J. Best]

Do you know the tactic#nontriviality? Most of these lemmas are structured around having that tactic be able to take care of the trivial case in one line, with little or no help from the user.

[Michael Stoll]

I have a piece of code like

    by_cases hR : nontrivial R,
    { haveI := hR,
      rw [ring.inverse_non_unit a ha, map_nonunit χ not_is_unit_zero], },
    { exact false.rec _ (ha (monoid.unit_of_not_nontrivial hR a)), },

I.e., I need to make a distinction between the case that a ring is nontrivial and the trivial case.
I guess I could replace the haveI := hR line by nontriviality, but this does not look like a big improvement...

[Michael Stoll]

(Note that the claim that 0 is not a unit is only valid in nontrivial rings.)

[Alex J. Best]

Yes, the idea is that the nontriviality R tactic does lines 1,2,4 of your snippet in one (readable) command.

[Alex J. Best]

There are many examples in files about polynomial degrees for instance, where many results about e.g. deg x^n only hold in a non-zero ring.

[Michael Stoll]

How does the tactic remove the need to distinguish cases? I do want to allow the ring to be trivial.

[Alex J. Best]

It clears that case for you, using an appropriate simp lemma normally. Letting you focus on the nontrivial case.

[Michael Stoll]

If I put nontriviality R before the first line, I get the error

Could not prove goal assuming `subsingleton R`

So how does it clear the trivial case?

[Michael Stoll]

I guess the trivial case is not so trivial after all...

[Ruben Van de Velde]

Do you have a #mwe?

[Alex J. Best]

If you set up your original lemma in https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/In.20a.20trivial.20monoid.2C.20everything.20is.20a.20unit/near/286259980 using a subsingleton assumption rather than not nontrivial it might work, but its hard to say without runnable code

[Michael Stoll]

#mwe seems to be difficult without copying a lot of code.
The goal is of the form ⇑χ (ring.inverse a) = 0 with a : R and ha : ¬is_unit a in the state, where χ : mul_char R R' (a monoid hom. that sends non-units to zero).
If I replace χ by just a monoid hom, it works.

[Michael Stoll]

Which is perhaps strange, since is_unit_of_subsingleton gives a contradiction with ha regardless of the goal.

[Michael Stoll]

Even with a mul_char, if I isolate this part of the code, it does work:

example (χ : mul_char R R') {a : R} (ha : ¬ is_unit a) : χ (ring.inverse a) = 0 :=
begin
  nontriviality,
  sorry
end

clears the trivial case.

[Michael Stoll]

So it has to do with something in the context?

[Michael Stoll]

I take it back: nontriviality R does not. Without argument, it uses R' :thinking:

[Michael Stoll]

(Same with monoid homomorphism in place of mul_char.)

[Michael Stoll]

So maybe this is a #mwe:

import ring_theory.integral_domain

example {R R'} [comm_ring R] [comm_ring R'] {a : R} (ha : ¬ is_unit a) (f : R →* R') :
  f (ring.inverse a) = 0 :=
begin
  nontriviality R, -- error
end

[Ruben Van de Velde]

Yeah, I can't get nontriviality to work either, but maybe if you add it to docs#tactic.nontriviality_by_assumption

[Michael Stoll]

nontriviality R using [is_unit_of_subsingleton] does not work, either.
What does "it" refer to in your post?

[Michael Stoll]

This works:

example {R R'} [comm_ring R] [comm_ring R'] {a : R} (ha : ¬ is_unit a) (f : R →* R') :
  f (ring.inverse a) = 0 :=
begin
  nontriviality R using [@false.elim (f (ring.inverse a) = 0) (ha (is_unit_of_subsingleton a))],
  sorry
end

in that it does clear the trivial case. But I have to basically spell out the proof anyway here.

[Eric Wieser]

casesI subsingleton_or_nontrivial R is the normal way to handle this kind of thing

[Alex J. Best]

Yeah its a bit of a funny one, seeing as nontriviality is getting a contradiction with the assumption it works best with that assumption reverted:

import ring_theory.integral_domain
.

example {R R'} [comm_ring R] [comm_ring R'] {a : R} (ha : ¬ is_unit a) (f : R →* R') :
  f (ring.inverse a) = 0 :=
begin
  revert ha,
  nontriviality R,
  intro ha,
  sorry
end

[Alex J. Best]

Maybe there is some improvement needed for this tactic

[Alex J. Best]

branch#alexjbest/better-nontriviality, lets see if it builds!

[Eric Rodriguez]

is there any way to let it take extra simp args instead of just doing *? maybe that'll be slow

[Alex J. Best]

It can already take extra simp args, just not targets. I'm not sure about slowness, there are already likely many simp lemmas being tried, so adding a few local hypotheses seems ok, but the additional targets could be a lot.

[Michael Stoll]

Alex J. Best said:

Yeah its a bit of a funny one, seeing as nontriviality is getting a contradiction with the assumption it works best with that assumption reverted:

Thanks. This works fine in my proof.

[Alex J. Best]

Alex J. Best said:

branch#alexjbest/better-nontriviality, lets see if it builds!

Mathlib builds but one of the tests fails, so maybe some more thought is needed. But I think this should be in scope for nontriviality