injective.ne

Stream: Is there code for X?

[Damiano Testa]

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]

I usually use mt f_inj.eq

[Mario Carneiro]

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

[Damiano Testa]

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

[Damiano Testa]

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]

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]

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]

"precedence" maybe?

[Damiano Testa]

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]

Just apply mt and then pick up the pieces maybe?

[Damiano Testa]

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]

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

[Mario Carneiro]

that's the identity function

[Mario Carneiro]

I think f0 should be the last argument to mt

[Mario Carneiro]

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

[Damiano Testa]

  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]

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]

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

[Mario Carneiro]

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

[Damiano Testa]

  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]

.2

[Mario Carneiro]

oh hey, injective.ne is a thing

[Damiano Testa]

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]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Damiano Testa]

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]

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]

.1 then

[Mario Carneiro]

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

[Mario Carneiro]

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

[Damiano Testa]

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

[Mario Carneiro]

then why not prove that?

[Mario Carneiro]

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

[Patrick Massot]

What if you start with contrapose! f0?

[Damiano Testa]

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]

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]

this stuff with negations in it looks too specialized

[Damiano Testa]

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]

Isn't this a cleaner state?

[Mario Carneiro]

oh, map_injective is literally the theorem I said

[Damiano Testa]

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

[Mario Carneiro]

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

[Patrick Massot]

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]

docs#ring_hom.injective_iff

[Damiano Testa]

Ah, thanks for ring_hom.injective_iff!

[Patrick Massot]

Cleaner:

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

[Mario Carneiro]

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

[Damiano Testa]

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]

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

[Damiano Testa]

ok, thanks!

[Damiano Testa]

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

[Mario Carneiro]

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]

Thanks! I will learn to use show!

[Patrick Massot]

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]

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

[Damiano Testa]

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]

ok, I will practice with and without show.

[Mario Carneiro]

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

[Damiano Testa]

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]

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]

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

[Kevin Buzzard]

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.