Zulip Chat Archive

Stream: Is there code for X?

Topic: injective.ne


view this post on Zulip Damiano Testa (Dec 31 2020 at 09:47):

Dear All,

I found myself needing the lemmas below, that I could not find in mathlib. Of course, I could replace them by their proofs, when I need them, but it feels like these lemmas might be useful. In particular, injective.ne (a ≠ 0) is used a lot in usual mathematical arguments, since rings have opposites (what an unnatural assumption). Should the lemmas below be imported to mathlib? Should there be a few general statements saying that homs (with appropriate assumptions) are injective if and only if they map non-zero elements to non-zero elements?

import data.polynomial.eval
import data.real.basic

open polynomial

lemma polynomial.injective.ne_of_inj_algebra_map
  {R A : Type*} [comm_semiring R] [semiring A] [algebra R A]
  {f : polynomial R} (f0 : f  0) (h : function.injective (algebra_map R A)) :
  map (algebra_map R A) f  0 :=
begin
  rw  map_zero (algebra_map R A),
  exact (map_injective (algebra_map R A) h).ne f0,
end

lemma polynomial.injective_int_real : function.injective (algebra_map  ) :=
(λ _ _ A, by simpa only [ring_hom.eq_int_cast, int.cast_inj] using A)

lemma polynomial.injective.ne {f : polynomial } (f0 : f  0) : map (algebra_map  ) f  0 :=
polynomial.injective.ne_of_inj_algebra_map f0 polynomial.injective_int_real

view this post on Zulip Mario Carneiro (Dec 31 2020 at 10:13):

I usually use mt f_inj.eq

view this post on Zulip Mario Carneiro (Dec 31 2020 at 10:14):

it seems easier to just use mt rather than make contrapositive versions of everything

view this post on Zulip Damiano Testa (Dec 31 2020 at 10:15):

Thanks for the suggestion! Let me internalize this and see how it works in the lemmas above!

view this post on Zulip Damiano Testa (Dec 31 2020 at 11:04):

I am missing something very basic here: I have been trying to get the contrapositive, but none of mt h, mt h_inj,mt h_inj.eq, mt h.eq works in the first lemma above. After unfolding h, I get the impression that Lean does not like the two variables implicit in h, but I have failed to give them explicitly, even with @h [...].

lemma polynomial.injective.ne_of_inj_algebra_map
  {R A : Type*} [comm_semiring R] [semiring A] [algebra R A]
  {f : polynomial R} (f0 : f  0) (h : function.injective (algebra_map R A)) :
  map (algebra_map R A) f  0 :=
begin
  rw  map_zero (algebra_map R A),
  unfold function.injective at h,
  apply mt @h (map (algebra_map R A) f) (map (algebra_map R A) 0),
--type mismatch at application
--  mt h
--term
--  h
--has type
--  ∀ ⦃a₁ a₂ : R⦄, ⇑(algebra_map R A) a₁ = ⇑(algebra_map R A) a₂ → a₁ = a₂
--but is expected to have type
--  ?m_1 → ?m_2
end

view this post on Zulip Kevin Buzzard (Dec 31 2020 at 11:08):

What you've written can't be right because mt is expecting an input which is a proof of P -> Q, and you're giving it @h which is much more complicated. Do you just need brackets around the (@h ...)?

view this post on Zulip Kevin Buzzard (Dec 31 2020 at 11:09):

mt is a function so will eat the next term it sees as its input -- function application has super-high binding power or priority or whatever it's called -- the BIDMAS thing.

view this post on Zulip Eric Wieser (Dec 31 2020 at 11:10):

"precedence" maybe?

view this post on Zulip Damiano Testa (Dec 31 2020 at 11:12):

Ok, this is part of the issue! The other part is that I probably gave the wrong inputs to h. I will fiddle with this a little longer!

Thanks!

view this post on Zulip Kevin Buzzard (Dec 31 2020 at 11:12):

Just apply mt and then pick up the pieces maybe?

view this post on Zulip Damiano Testa (Dec 31 2020 at 11:15):

ok, I feel very clumsy, but what's below works!

lemma polynomial.injective.ne_of_inj_algebra_map
  {R A : Type*} [comm_semiring R] [semiring A] [algebra R A]
  {f : polynomial R} (f0 : f  0) (h : function.injective (algebra_map R A)) :
  map (algebra_map R A) f  0 :=
begin
  rw  map_zero (algebra_map R A),
  apply mt,
  intros j,
  apply f0,
  apply (map_injective (algebra_map R A) h) j,
  exact not_false,
end

with show_term and some compressing, this is what it becomes:

lemma polynomial.injective.ne_of_inj_algebra_map
  {R A : Type*} [comm_semiring R] [semiring A] [algebra R A]
  {f : polynomial R} (f0 : f  0) (h : function.injective (algebra_map R A)) :
  map (algebra_map R A) f  0 :=
begin
  rw  map_zero (algebra_map R A),
  exact mt (λ j, f0 (map_injective (algebra_map R A) h j)) not_false,
end

view this post on Zulip Mario Carneiro (Dec 31 2020 at 11:23):

that looks odd... you shouldn't need not_false

view this post on Zulip Mario Carneiro (Dec 31 2020 at 11:23):

that's the identity function

view this post on Zulip Mario Carneiro (Dec 31 2020 at 11:24):

I think f0 should be the last argument to mt

view this post on Zulip Mario Carneiro (Dec 31 2020 at 11:24):

does mt (map_injective (algebra_map R A) h) f0 work?

view this post on Zulip Damiano Testa (Dec 31 2020 at 11:25):

  refine mt (map_injective (algebra_map R A) h) f0,

type mismatch at application
  mt (map_injective (algebra_map R A) h)
term
  map_injective (algebra_map R A) h
has type
  function.injective (map (algebra_map R A))
but is expected to have type
  map (algebra_map R A) f = map (algebra_map R A) 0  ?m_1

view this post on Zulip Damiano Testa (Dec 31 2020 at 11:26):

I may be making my life complicated by combining the injectivity of hand the injectivity of the induced map on polynomial R, though.

view this post on Zulip Mario Carneiro (Dec 31 2020 at 11:26):

Oh, the {{}} is getting in the way

view this post on Zulip Mario Carneiro (Dec 31 2020 at 11:27):

maybe (map_injective (algebra_map R A) h).eq_iff.1 works?

view this post on Zulip Damiano Testa (Dec 31 2020 at 11:28):

  refine (map_injective (algebra_map R A) h).eq_iff.1,

invalid type ascription, term has type
  map (algebra_map R A) ?m_1 = map (algebra_map R A) ?m_2  ?m_1 = ?m_2
but is expected to have type
  map (algebra_map R A) f  map (algebra_map R A) 0

view this post on Zulip Mario Carneiro (Dec 31 2020 at 11:28):

.2

view this post on Zulip Mario Carneiro (Dec 31 2020 at 11:28):

oh hey, injective.ne is a thing

view this post on Zulip Damiano Testa (Dec 31 2020 at 11:28):

invalid type ascription, term has type
  ?m_1 = ?m_2  map (algebra_map R A) ?m_1 = map (algebra_map R A) ?m_2
but is expected to have type
  map (algebra_map R A) f  map (algebra_map R A) 0

view this post on Zulip Damiano Testa (Dec 31 2020 at 11:29):

yes, I was using injective.ne in my original proof.

view this post on Zulip Mario Carneiro (Dec 31 2020 at 11:29):

still mt (injective_proof).eq_iff.2 f0 I mean

view this post on Zulip Mario Carneiro (Dec 31 2020 at 11:30):

ok if injective.ne exists already then (injective_proof).ne f0 is better

view this post on Zulip Damiano Testa (Dec 31 2020 at 11:31):

injective_proof of the map on rings, right? what is called h, to be clear?

lemma polynomial.injective.ne_of_inj_algebra_map
  {R A : Type*} [comm_semiring R] [semiring A] [algebra R A]
  {f : polynomial R} (f0 : f  0) (h : function.injective (algebra_map R A)) :
  map (algebra_map R A) f  0 :=
begin
  rw  map_zero (algebra_map R A),
  refine mt (h).eq_iff.2 f0, -- does not work
--type mismatch at application
--  mt h.eq_iff.mpr
--term
--  h.eq_iff.mpr
--has type
--  ?m_1 = ?m_2 → ⇑(algebra_map R A) ?m_1 = ⇑(algebra_map R A) ?m_2
--but is expected to have type
--  map (algebra_map R A) f = map (algebra_map R A) 0 → ?m_1
end

view this post on Zulip Mario Carneiro (Dec 31 2020 at 11:31):

But looking at your theorem, it looks like it's just saying injective (algebra_map R A) -> injective (map (algebra_map R A))

view this post on Zulip Mario Carneiro (Dec 31 2020 at 11:32):

.1 then

view this post on Zulip Mario Carneiro (Dec 31 2020 at 11:32):

I just try it both ways and see which one lean likes

view this post on Zulip Mario Carneiro (Dec 31 2020 at 11:32):

you can see in the error that the arrow is going the wrong way

view this post on Zulip Damiano Testa (Dec 31 2020 at 11:33):

Yes, the theorem should be saying that is the map on coefficients is injective, then the map on polynomials is injective.

view this post on Zulip Mario Carneiro (Dec 31 2020 at 11:33):

then why not prove that?

view this post on Zulip Mario Carneiro (Dec 31 2020 at 11:33):

and use injective.ne or injective.eq_iff or whatever on the result

view this post on Zulip Patrick Massot (Dec 31 2020 at 11:34):

What if you start with contrapose! f0?

view this post on Zulip Damiano Testa (Dec 31 2020 at 11:34):

Yes, I am happy with this. I was wondering whether the lemmas above are something that is good to have in mathlib, that's all!
I am happy to learn new ways to prove stuff, though!

view this post on Zulip Mario Carneiro (Dec 31 2020 at 11:35):

Do we have the theorem about injective (algebra_map R A) -> injective (map (algebra_map R A))? That's the version that looks good for mathlib

view this post on Zulip Mario Carneiro (Dec 31 2020 at 11:35):

this stuff with negations in it looks too specialized

view this post on Zulip Damiano Testa (Dec 31 2020 at 11:36):

with contrapose! f=0, this is the state:

R: Type u_1
A: Type u_2
_inst_1: comm_semiring R
_inst_2: semiring A
_inst_3: algebra R A
f: polynomial R
h: function.injective (algebra_map R A)
f0: map (algebra_map R A) f = 0
 f = 0

view this post on Zulip Patrick Massot (Dec 31 2020 at 11:37):

Isn't this a cleaner state?

view this post on Zulip Mario Carneiro (Dec 31 2020 at 11:37):

oh, map_injective is literally the theorem I said

view this post on Zulip Damiano Testa (Dec 31 2020 at 11:37):

Yes, and it is also the one whose contrapositive I was trying to prove!

view this post on Zulip Mario Carneiro (Dec 31 2020 at 11:38):

There should be a theorem that a function is injective iff f x = 0 -> x = 0 and variations on that

view this post on Zulip Patrick Massot (Dec 31 2020 at 11:38):

lemma polynomial.injective.ne_of_inj_algebra_map
  {R A : Type*} [comm_semiring R] [semiring A] [algebra R A]
  {f : polynomial R} (f0 : f  0) (h : function.injective (algebra_map R A)) :
  map (algebra_map R A) f  0 :=
begin
  contrapose! f0,
  rw   map_zero (algebra_map R A) at f0,
  exact map_injective _  h f0
end

view this post on Zulip Mario Carneiro (Dec 31 2020 at 11:39):

docs#ring_hom.injective_iff

view this post on Zulip Damiano Testa (Dec 31 2020 at 11:40):

Ah, thanks for ring_hom.injective_iff!

view this post on Zulip Patrick Massot (Dec 31 2020 at 11:41):

Cleaner:

begin
  contrapose! f0,
  exact map_injective _  h (by simp [f0])
end

view this post on Zulip Mario Carneiro (Dec 31 2020 at 11:42):

by simpa using (map_injective (algebra_map R A) h).ne f0

view this post on Zulip Damiano Testa (Dec 31 2020 at 11:44):

So, if I wanted to use the proof with simpa in the middle of another proof, how should I do to avoid a "non-terminal simp"?

view this post on Zulip Mario Carneiro (Dec 31 2020 at 11:44):

have : map (algebra_map R A) f ≠ 0 := by simpa using (map_injective (algebra_map R A) h).ne f0

view this post on Zulip Damiano Testa (Dec 31 2020 at 11:44):

ok, thanks!

view this post on Zulip Damiano Testa (Dec 31 2020 at 11:44):

for some reason, I do not like have, but this is just me!

view this post on Zulip Mario Carneiro (Dec 31 2020 at 11:45):

apply theorem foo bar (show map (algebra_map R A) f ≠ 0, by simpa using (map_injective (algebra_map R A) h).ne f0)

view this post on Zulip Damiano Testa (Dec 31 2020 at 11:46):

Thanks! I will learn to use show!

view this post on Zulip Patrick Massot (Dec 31 2020 at 11:46):

That's funny because have is the only tactic we constantly use on paper. I still dream of getting to the point where, as in Isabelle, a (nontrivial) Lean proof would only be a sequence of have : ..., by auto.

view this post on Zulip Mario Carneiro (Dec 31 2020 at 11:47):

you may not need show depending on how much context lean has in theorem foo bar _

view this post on Zulip Damiano Testa (Dec 31 2020 at 11:47):

I think with have, but when I write lean arguments, I find that it slows down quite a bit and refine works much better!

view this post on Zulip Damiano Testa (Dec 31 2020 at 11:48):

ok, I will practice with and without show.

view this post on Zulip Mario Carneiro (Dec 31 2020 at 11:48):

with refine, refine foo bar _, {simpa ...}, ...

view this post on Zulip Damiano Testa (Dec 31 2020 at 11:49):

Thank you all for the suggestions! Even though many of these bits and pieces were already in my mind, seeing them come together in this simple example is really useful!

view this post on Zulip Damiano Testa (Dec 31 2020 at 11:50):

I am starting to understand the difference between refine and apply. If I understand correctly, the use of the underscore may make a difference in the last suggestion refine foo bar _, {simpa ...}, ..., right?

view this post on Zulip Damiano Testa (Dec 31 2020 at 11:51):

e.g. apply foo bar _, {simpa ...}, ... may not generate the goal to be solved with {simpa ...}, correct?

view this post on Zulip Kevin Buzzard (Dec 31 2020 at 12:01):

refine is cooler than apply because it knows the goals of every underscore. apply is just refine without underscores and it doesn't always work because of (a) the apply bug and (b) apply F (by simp) doesn't always work because Lean might not know what it's supposed to be proving by simp because of elaboration issues. refine F (by simp) _ _ _ will work.


Last updated: May 17 2021 at 15:13 UTC