## Stream: Is there code for X?

### Topic: injective.ne

#### 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


#### Mario Carneiro (Dec 31 2020 at 10:13):

I usually use mt f_inj.eq

#### Mario Carneiro (Dec 31 2020 at 10:14):

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

#### 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!

#### 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


#### 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 ...)?

#### 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.

#### Eric Wieser (Dec 31 2020 at 11:10):

"precedence" maybe?

#### 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!

#### Kevin Buzzard (Dec 31 2020 at 11:12):

Just apply mt and then pick up the pieces maybe?

#### 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


#### Mario Carneiro (Dec 31 2020 at 11:23):

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

#### Mario Carneiro (Dec 31 2020 at 11:23):

that's the identity function

#### Mario Carneiro (Dec 31 2020 at 11:24):

I think f0 should be the last argument to mt

#### Mario Carneiro (Dec 31 2020 at 11:24):

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

#### 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


#### 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.

#### Mario Carneiro (Dec 31 2020 at 11:26):

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

#### Mario Carneiro (Dec 31 2020 at 11:27):

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

#### 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


.2

#### Mario Carneiro (Dec 31 2020 at 11:28):

oh hey, injective.ne is a thing

#### 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


#### Damiano Testa (Dec 31 2020 at 11:29):

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

#### Mario Carneiro (Dec 31 2020 at 11:29):

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

#### Mario Carneiro (Dec 31 2020 at 11:30):

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

#### 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


#### 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))

.1 then

#### Mario Carneiro (Dec 31 2020 at 11:32):

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

#### Mario Carneiro (Dec 31 2020 at 11:32):

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

#### 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.

#### Mario Carneiro (Dec 31 2020 at 11:33):

then why not prove that?

#### Mario Carneiro (Dec 31 2020 at 11:33):

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

#### Patrick Massot (Dec 31 2020 at 11:34):

What if you start with contrapose! f0?

#### 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!

#### 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

#### Mario Carneiro (Dec 31 2020 at 11:35):

this stuff with negations in it looks too specialized

#### 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


#### Patrick Massot (Dec 31 2020 at 11:37):

Isn't this a cleaner state?

#### Mario Carneiro (Dec 31 2020 at 11:37):

oh, map_injective is literally the theorem I said

#### Damiano Testa (Dec 31 2020 at 11:37):

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

#### 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

#### 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


#### Mario Carneiro (Dec 31 2020 at 11:39):

docs#ring_hom.injective_iff

#### Damiano Testa (Dec 31 2020 at 11:40):

Ah, thanks for ring_hom.injective_iff!

#### Patrick Massot (Dec 31 2020 at 11:41):

Cleaner:

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


#### Mario Carneiro (Dec 31 2020 at 11:42):

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


#### 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"?

#### 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

ok, thanks!

#### Damiano Testa (Dec 31 2020 at 11:44):

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

#### 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)

#### Damiano Testa (Dec 31 2020 at 11:46):

Thanks! I will learn to use show!

#### 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.

#### Mario Carneiro (Dec 31 2020 at 11:47):

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

#### 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!

#### Damiano Testa (Dec 31 2020 at 11:48):

ok, I will practice with and without show.

#### Mario Carneiro (Dec 31 2020 at 11:48):

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

#### 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!

#### 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?

#### 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?

#### 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