lemmas on int and subsingleton

Stream: new members

[Damiano Testa]

Dear All,

while working on the lean-liquid branch, I found the lemmas below useful and I could not find them in mathlib. If you think that it would be helpful to have some of them in mathlib, let me know and I will be happy to make the relevant PRs!

Thanks!

import algebra.associated

lemma int.nat_abs_eq_iff {n : ℤ} {k : ℕ} : n.nat_abs = k ↔ n = k ∨ n = -k :=
⟨by { rintro rfl, exact int.nat_abs_eq n }, by rintro (rfl | rfl); simp⟩

lemma int.is_unit_plus_minus_one_of {n : ℤ} : is_unit n ↔ n = 1 ∨ n = -1 :=
is_unit_int.trans (int.nat_abs_eq_iff.trans iff.rfl)

lemma function.injective.of_subsingleton {s t : Type*} [hs : subsingleton s] (f : s → t) :
  function.injective f :=
λ a b ab, subsingleton_iff.mp hs a b

lemma function.surjective.to_subsingleton {s t : Type*} [nonempty s] (f : s → t) [subsingleton t] :
  function.surjective f :=
function.surjective_iff_has_right_inverse.mpr ⟨function.inv_fun f, by finish⟩

lemma subsingleton_eq_univ_of_mem {A : Type*} (hA : subsingleton A) (a : A) :
  ({a} : set A) = set.univ :=
le_antisymm (λ a1 ha, set.mem_univ a1)
  (λ x hx, set.mem_singleton_iff.mpr (subsingleton_iff.mp hA x a))

[Johan Commelin]

LGTM.
nonempty s should be a type class assumption (in lemma 4)

[Johan Commelin]

For the last lemma, I wonder whether you want to generalise the LHS to an arbitrary set s with assumption s.nonempty

[Damiano Testa]

Johan, thanks!

lemma4 : I edited the list above and, in the same lemma, went ahead to make subsingleton also a typeclass assumption!

[Damiano Testa]

I am working on a proof of the other suggestion that you made!

[Damiano Testa]

I could almost find the version that Johan suggested with a set:

lemma subsingleton_eq_univ_of_subset {A : Type*} [hA : subsingleton A] (a : set A) [nonempty a] :
  a = set.univ :=
subsingleton.eq_univ_of_nonempty set.nonempty_of_nonempty_subtype

and the same proof works for the earlier lemma:

lemma subsingleton_eq_univ_of_mem {A : Type*} (hA : subsingleton A) (a : A) :
  ({a} : set A) = set.univ :=
subsingleton.eq_univ_of_nonempty set.nonempty_of_nonempty_subtype

I guess that this means that this lemma "is" already in mathlib!

[Eric Wieser]

Is nonempty a (for a : set _) the preferred spelling of set emptiness? That inserts a coercion to sort, which is why it would surprise me if it is!

[Eric Wieser]

Ah, indeed the proof you give translates your spelling to the less surprising one

[Eric Wieser]

I'm pretty sure I've seen int.nat_abs_eq_iff or similar in review recently...

[Johan Commelin]

@Eric Wieser s is a Type. Maybe those letters should be changed to X and Y or \alpha and \beta.

[Eric Wieser]

Ah, I mistakenly assumed the last code snippet agreed with the earlier ones, and didn't scroll sideways to check on mobile!

[Damiano Testa]

Besides the fact that there is one case in which the assumption nonempty is applied to a set, the confusion is probably also caused by the fact that I used s for a Type, whereas often s denotes a subset. I tried to uniformize the notation, in the code below:

namespace int

-- proof provided by Ruben
lemma nat_abs_eq_iff {a : ℤ} {n : ℕ} : a.nat_abs = n ↔ a = n ∨ a = -n :=
by rw [←int.nat_abs_eq_nat_abs_iff, int.nat_abs_of_nat]

lemma is_unit_plus_minus_one_of {a : ℤ} : is_unit a ↔ a = 1 ∨ a = -1 :=
is_unit_int.trans (nat_abs_eq_iff.trans iff.rfl)

end int

lemma function.injective.of_subsingleton {α β : Type*} [h : subsingleton α] (f : α → β) :
  function.injective f :=
λ a b ab, subsingleton_iff.mp h a b

lemma function.surjective.to_subsingleton {α β : Type*} (f : α → β) [nonempty α] [subsingleton β] :
  function.surjective f :=
function.surjective_iff_has_right_inverse.mpr ⟨function.inv_fun f, by finish⟩

-- this lemma and the next may be "too close" to results in mathlib: I will probably not PR them,
-- unless there is some explicit interest in them!
lemma subsingleton_eq_univ_of_mem {α : Type*} [subsingleton α] (a : α) :
  ({a} : set α) = set.univ :=
subsingleton.eq_univ_of_nonempty set.nonempty_of_nonempty_subtype

-- here [nonempty s] introduces a coercion mentioned by Eric
lemma subsingleton_eq_univ_of_subset {α : Type*} [h : subsingleton α] (s : set α) [nonempty s] :
  s = set.univ :=
subsingleton.eq_univ_of_nonempty set.nonempty_of_nonempty_subtype

[Ruben Van de Velde]

Alternative proof for the first one:

import algebra.associated
lemma int.nat_abs_eq_iff {n : ℤ} {k : ℕ} : n.nat_abs = k ↔ n = k ∨ n = -k :=
by rw [←int.nat_abs_eq_nat_abs_iff, int.nat_abs_of_nat]

[Damiano Testa]

Ruben, thanks! I will update with your proof, since it seems more direct!

[Eric Wieser]

I think is_unit_plus_minus_one_of is docs#int.units_eq_one_or

[Eric Wieser]

Or at least, it's a more direct proof via that lemma

[Damiano Testa]

Ok, I was actually right now playing with this, since I had also found int.units_eq_one_or, trying to place is_unit_plus_minus_one_of

[Damiano Testa]

I am failing to be able to use int.units_eq_one_or. I would like to apply the conclusion of that lemma to get Lean to ask me to produce a unit. Is there a way to do this?

What is a good way to proceed?

Below is a proof that I would like to see if it can be made to work:

lemma is_unit_plus_neg_one_of {a : ℤ} (h : is_unit a) : a = 1 ∨ a = -1 :=
begin
  apply units_eq_one_or _,
-- of course this does not work, since Lean does not know that `a` is a piece of a unit.
-- How can I get Lean to proceed there?
end

[Eric Wieser]

Also, the word minus should be neg!

[Damiano Testa]

Eric, this last one was easy to fix! :wink:

[Johan Commelin]

is_unit.eq_one_or_neg_one?

[Johan Commelin]

Of course it's a bit weird to put a lemma specific to int in the is_unit namespace

[Johan Commelin]

Do we already have is_unit.eq_one for nat?

[Eric Wieser]

library_search doesn't find either of these:

lemma nat.units_eq_one (a : units ℕ) : a = 1 :=
by library_search

lemma is_unit.eq_one {a : ℕ} (h : is_unit a) : a = 1 :=
by library_search

edit: ah, we have docs#nat.units_eq_one

[Eric Wieser]

And docs#nat.is_unit_iff

[Damiano Testa]

So, should the name be int.is_unit_iff?

[Damiano Testa]

Still, I have not been able to prove the is_unit lemma from the units one.

[Eric Wieser]

lemma is_unit.eq_one_or {a : ℤ} (h : is_unit a) : a = 1 ∨ a = -1 :=
begin
  obtain ⟨x, rfl⟩ := h,
  rw [←units.coe_one, ←units.coe_neg],
  exact (int.units_eq_one_or _).imp (congr_arg coe) (congr_arg coe),
end

[Damiano Testa]

To confuse me further,

theorem is_unit_int {n : ℤ} : is_unit n ↔ n.nat_abs = 1 :=

is in algebra/associated and not in data/int/basic, where the stuff about units in int appears.

[Damiano Testa]

It might be that the reason for this is to not import algebra/associated into data/int/basic.

[Eric Wieser]

Or a shorter proof,

lemma is_unit.eq_one_or' {a : ℤ} : is_unit a → a = 1 ∨ a = -1
| ⟨x, hx⟩ := hx ▸ (int.units_eq_one_or _).imp (congr_arg coe) (congr_arg coe)

[Eric Wieser]

If that proof can be moved to data/int/basic, it probably should be

[Damiano Testa]

At the moment, it cannot, since the proof uses lemmas in algebra/associated, but I am sure that I can prove this lemma from what is in data/int/basic, since we already know that units in int are 1 and -1! :upside_down:

[Ruben Van de Velde]

Should it be an iff, though?

[Damiano Testa]

Ruben, I took Erics suggestion to mean the following:

lemma is_unit.eq_one_or' {a : ℤ} : is_unit a → a = 1 ∨ a = -1
| ⟨x, hx⟩ := hx ▸ (int.units_eq_one_or _).imp (congr_arg coe) (congr_arg coe)

lemma is_unit_iff {a : ℤ} : is_unit a ↔ a = 1 ∨ a = -1 :=
begin
  refine ⟨λ h, is_unit.eq_one_or' h, λ h, _⟩,
  rcases h with rfl | rfl,
  { exact is_unit_one },
  { exact is_unit_of_mul_eq_one _ (- 1 : ℤ) (neg_one_mul _) }
end

[Eric Wieser]

Note the ' was just to distinguish it from my previous lemma, there's no need for ' if you PR that

[Damiano Testa]

How do people feel about making is_unit_iff a simp lemma?

[Damiano Testa]

Should the iff version of units be there as well?
Hmm, I had not given enough TT thought about this: the units lemma is tricky to convert into an iff, right?

[Damiano Testa]

Also as a simp lemma?

[Eric Wieser]

Looks like you could do with an is_unit.neg lemma there too:

lemma is_unit.neg {α : Type*} [ring α] {a : α} (h : is_unit a) : is_unit (-a) :=
begin
  obtain ⟨x, rfl⟩ := h,
  exact (-x).is_unit,
end

lemma is_unit_iff {a : ℤ} : is_unit a ↔ a = 1 ∨ a = -1 :=
begin
  refine ⟨is_unit.eq_one_or, λ h, _⟩,
  rcases h with rfl | rfl,
  { exact is_unit_one },
  { exact is_unit_one.neg }
end

[Eric Wieser]

I think that might be a bad idea as a simp lemma

[Damiano Testa]

With the changes above, the lemma below now fits in data/int/basic and is no longer needed in algebra/associated:

theorem is_unit_int {n : ℤ} : is_unit n ↔ n.nat_abs = 1 :=
by simp [nat_abs_eq_iff, is_unit_iff]

[Damiano Testa]

Ok, I will remove the simp attribute!

[Damiano Testa]

I was thinking about the is_unit.neg, but it probably does not belong to any file that is already imported into data/int/basic, right?

[Damiano Testa]

I am happy to prove that the opposite of a unit is again a unit, though it would probably be a different PR!

[Ruben Van de Velde]

I had

variables {α : Type*} [ring α]

lemma is_unit.neg (u : α) : is_unit (-u) ↔ is_unit u :=
begin
  split;
  { rintro ⟨u', hu⟩,
    use -u',
    simp only [hu, neg_neg, units.coe_neg] }
end

[Damiano Testa]

PR #7058

[Yakov Pechersky]

Any is_unit lemma is also a lemma about units. And units are a group/subgroup depending on how you approach it. The neg one is just a special case of a mul_hom

[Eric Wieser]

Sure, but we have is_unit.mul and is_unit.inv, so we may as well add versions for the other operators for convenience

[Eric Wieser]

Do we have the fact that units are a subgroup?

[Damiano Testa]

In case it helps, this is the part of the code where opposites interact with is_unit in the PR:

https://github.com/leanprover-community/mathlib/blob/042166150bc51f7976161ff8642f3b408a823f07/src/algebra/ring/basic.lean#L627