# Zulip Chat Archive

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

ing `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 `h`

and 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
```

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

.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))`

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

.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):

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

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

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