Zulip Chat Archive

Stream: new members

Topic: field of fractions


view this post on Zulip Damiano Testa (Dec 18 2020 at 14:21):

Before I embark in proving the lemma below, could I ask that it is what I think that it is mathematically?

I want to prove that if f : polynomial ℤ and a b : ℤ, then b ^ f.nat_degree * eval f (a / b) is an integer. Is this what the code below generalizes? Is the statement that I want already in Lean?

Thanks!

import ring_theory.localization

open polynomial

variables {R K : Type*} [integral_domain R] [field K] {d : fraction_map R K}

lemma nums_dens (f : polynomial R) (a b : R) (b0 : b  0) :  r : R,
  (((d.to_map b) ^ f.nat_degree * eval₂ d.to_map (d.to_map a / d.to_map b) f) = d.to_map r) :=
begin
  sorry,
end

view this post on Zulip Damiano Testa (Dec 18 2020 at 14:30):

(Also, feel free to suggest any improvements to the statement: I have never used localizations in Lean before.)

view this post on Zulip Johan Commelin (Dec 18 2020 at 14:39):

@Damiano Testa yup, that statement looks right. And I'm sorry that it turns into such a mess.

view this post on Zulip Johan Commelin (Dec 18 2020 at 14:40):

I think we should be able to make this look better... but it will require changes to mathlib

view this post on Zulip Damiano Testa (Dec 18 2020 at 14:40):

Thanks for the confirmation! Since I had not experience of fields of fractions, I wanted to make sure that I was not complicating my life too much by doing it like this!

view this post on Zulip Eric Wieser (Dec 18 2020 at 14:41):

Should docs#fraction_map have a coe_to_fun equal to to_map?

view this post on Zulip Damiano Testa (Dec 18 2020 at 14:42):

So that I understand Eric's comment: this means I would not need to type d.to_map b, but simply d b would suffice?

view this post on Zulip Johan Commelin (Dec 18 2020 at 14:43):

I think fraction_map (and localization_map) should be predicates on ring_hom.

view this post on Zulip Johan Commelin (Dec 18 2020 at 14:43):

But that requires a bunch of refactoring, for which I currently don't have the time

view this post on Zulip Eric Wieser (Dec 18 2020 at 14:44):

I think the instance may already be there

view this post on Zulip Eric Wieser (Dec 18 2020 at 14:44):

Does it work without to_map?

view this post on Zulip Damiano Testa (Dec 18 2020 at 14:51):

I am waiting for Lean to process the file: it takes a really long time.

Earlier, though, I had to put in the .to_map since at some stage it was not working without. However, it was also a stage where I did not have a correctly formed term, so I am not sure that the missing .to_map was the issue.

view this post on Zulip Eric Wieser (Dec 18 2020 at 14:57):

It might be that you only need one of the to_maps

view this post on Zulip Anne Baanen (Dec 18 2020 at 14:58):

Johan Commelin said:

I think fraction_map (and localization_map) should be predicates on ring_hom.

Perhaps fraction_map R K should even be a class extending algebra R K?

view this post on Zulip Damiano Testa (Dec 18 2020 at 15:01):

Finally I could use Lean! It seems to require the .to_map. For instance

lemma nums_dens (f : polynomial R) (a b : R) (b0 : b  0) :  r : R,
  (((d.to_map b) ^ f.nat_degree * eval₂ d.to_map (d.to_map a / d.to_map b) f) = d r) :=
 --function expected at
--  d
--term has type
--  localization_map (non_zero_divisors R) K

whereas

lemma nums_dens (f : polynomial R) (a b : R) (b0 : b  0) :  r : R,
  (((d.to_map b) ^ f.nat_degree * eval₂ d.to_map (d.to_map a / d.to_map b) f) = d.to_map r) :=

works.

view this post on Zulip Anne Baanen (Dec 18 2020 at 15:02):

Damiano Testa said:

Before I embark in proving the lemma below, could I ask that it is what I think that it is mathematically?

I want to prove that if f : polynomial ℤ and a b : ℤ, then b ^ f.nat_degree * eval f (a / b) is an integer. Is this what the code below generalizes? Is the statement that I want already in Lean?

Thanks!

import ring_theory.localization

open polynomial

variables {R K : Type*} [integral_domain R] [field K] {d : fraction_map R K}

lemma nums_dens (f : polynomial R) (a b : R) (b0 : b  0) :  r : R,
  (((d.to_map b) ^ f.nat_degree * eval₂ d.to_map (d.to_map a / d.to_map b) f) = d.to_map r) :=
begin
  sorry,
end

Equivalent, but nicer, should be to have the conclusion d.is_integer ((((d.to_map b) ^ f.nat_degree * eval₂ d.to_map (d.to_map a / d.to_map b) f)) (see docs#localization_map.is_integer).

view this post on Zulip Anne Baanen (Dec 18 2020 at 15:04):

Damiano Testa said:

So that I understand Eric's comment: this means I would not need to type d.to_map b, but simply d b would suffice?

It would be nice, but isn't possible at the moment. So you'll have to write d.to_map b always, unfortunately.

view this post on Zulip Damiano Testa (Dec 18 2020 at 15:05):

Anne, thanks for the suggestion! I will use .is_integer! Also, no worries about the .to_map: it had not even occurred to me that it might be possible to not have to type it!

view this post on Zulip Eric Wieser (Dec 18 2020 at 15:12):

This works:

import ring_theory.localization

open polynomial

variables {R K : Type*} [integral_domain R] [field K]{d : fraction_map R K}

instance : has_coe (fraction_map R K) (R →+* K) := localization_map.to_ring_hom

lemma nums_dens (f : polynomial R) (a b : R) (b0 : b  0) :
  d.is_integer (d b ^ f.nat_degree * eval₂ d (d a / d b) f) :=
begin
  sorry,
end

If it doesn't cause too much pain, that has_coe instance could be added back to mathlib later.

view this post on Zulip Damiano Testa (Dec 18 2020 at 15:14):

Ah, thanks a lot, Eric! I am not at all familiar with coestuff, but I am happy to use what you proposed!

In any case, I will start proving this result in a bit: I first need to set up an inductive argument.

view this post on Zulip Eric Wieser (Dec 18 2020 at 15:15):

I'd probably try to prove the to_map version first, and then see what breaks if you use the has_coe instead one you already have the proof

view this post on Zulip Anne Baanen (Dec 18 2020 at 15:19):

If we later decide to add the has_coe, we should not forget to also add a has_coe_to_fun, as explained in the function coercion library note.

view this post on Zulip Damiano Testa (Dec 18 2020 at 18:00):

In case anyone is interested, want to golf the proofs or has comments of any form, below is a proof of the initial lemma!

import data.polynomial.erase_lead
import ring_theory.localization

open polynomial finset

lemma erase_lead_card_support_eq {R : Type*} [semiring R] {c : } {f : polynomial R}
  (f0 : f.support.card = c.succ) :
  f.erase_lead.support.card = c :=
begin
  rw [erase_lead_support, card_erase_of_mem],
  { exact nat.pred_eq_of_eq_succ f0 },
  { rw nat_degree_eq_support_max',
    refine f.support.max'_mem (nonempty_support_iff.mpr _),
    { rintro rfl,
      rw [support_zero, card_empty] at f0,
      exact (not_le.mpr (nat.succ_pos c)) (eq.ge f0) } }
end

lemma Pind {R : Type*} [semiring R] {P : polynomial R  Prop} (N : )
  (P_0 : P 0)
  (P_C_mul_pow :  n : ,  r : R, r  0  n  N  P (C r * X ^ n))
  (P_C_add :  f g : polynomial R, f.nat_degree  N  g.nat_degree  N  P f  P g  P (f + g)) :
   f : polynomial R, f.nat_degree  N  P f :=
begin
  intros f df,
  generalize' hd : card f.support = c,
  revert f,
  induction c with c hc,
  { refine λ f df f0, by rwa (finsupp.support_eq_empty.mp (card_eq_zero.mp f0)) },
  { intros f df f0,
    rw  erase_lead_add_C_mul_X_pow f,
    apply P_C_add _ _ (le_trans erase_lead_nat_degree_le df),
    { apply le_trans (nat_degree_C_mul_X_pow_le (leading_coeff f) (nat_degree f)) df },
    { exact hc _ (le_trans erase_lead_nat_degree_le df) (erase_lead_card_support_eq f0) },
    { apply P_C_mul_pow _ _ _ df,
      rw [ne.def, leading_coeff_eq_zero],
      rintro rfl,
      exact (not_le.mpr (nat.succ_pos c)) (eq.ge f0) } },
end

variables {R K : Type*} [integral_domain R] [field K] {d : fraction_map R K}

lemma P_0 (N : ) (a b : R) (b0 : b  0) :
  d.is_integer (d.to_map b ^ N * eval₂ d.to_map (d.to_map a / d.to_map b) 0) :=
begin
  rw [eval₂_zero, mul_zero],
  exact 0, d.to_map.map_zero⟩,
end

lemma P_C_mul_pow (N : ) (a b : R) (b0 : b  0) :
   (n : ) (r : R), r  0  n  N 
    d.is_integer (d.to_map b ^ N * eval₂ d.to_map (d.to_map a / d.to_map b) (C r * X ^ n)) :=
begin
  intros n r r0 nN,
  refine r * a ^ n * b ^ (N - n), _⟩,
  have : (C r * X ^ n).nat_degree = n,
  { rw C_mul_X_pow_eq_monomial,
    exact nat_degree_monomial _ _ r0 },
  simp only [eval₂_X_pow, div_pow, eval₂_C, eval₂_mul, ring_hom.map_pow, ring_hom.map_mul],
  rw [ mul_assoc, mul_comm _ (d.to_map r), mul_assoc, mul_assoc, mul_eq_mul_left_iff],
  left,
  rw [ mul_div_assoc, mul_comm, mul_div_assoc,  mul_div_comm, mul_comm],
  simp only [mul_eq_mul_left_iff],
  left,
  symmetry,
  rw [div_eq_iff,  pow_add, nat.sub_add_cancel nN],
  intro l0,
  apply b0,
  apply pow_eq_zero,
  apply localization_map.injective d le_rfl,
  simpa only [ring_hom.map_pow, ring_hom.map_zero, localization_map.injective d le_rfl],
end

lemma P_C_add (N : ) (a b : R) (b0 : b  0) :
   (f g : polynomial R), f.nat_degree  N  g.nat_degree  N 
    d.is_integer (d.to_map b ^ N * eval₂ d.to_map (d.to_map a / d.to_map b) f) 
    d.is_integer (d.to_map b ^ N * eval₂ d.to_map (d.to_map a / d.to_map b) g) 
    d.is_integer (d.to_map b ^ N * eval₂ d.to_map (d.to_map a / d.to_map b) (f + g)) :=
begin
  rintros f g fN gN f1, hf g1, hg⟩,
  refine f1 + g1, _⟩,
  simp only [mul_add, eval₂_add, hf, hg, ring_hom.map_add]
end

lemma is_integer_N (N : ) (a b : R) (b0 : b  0) :  (f : polynomial R), f.nat_degree  N 
d.is_integer (((d.to_map b) ^ N * eval₂ d.to_map (d.to_map a / d.to_map b) f)) :=
Pind N (P_0 N a b b0) (P_C_mul_pow N a b b0) (P_C_add N a b b0)

lemma nums_dens (f : polynomial R) (a b : R) (b0 : b  0) :
  d.is_integer (((d.to_map b) ^ f.nat_degree * eval₂ d.to_map (d.to_map a / d.to_map b) f)) :=
is_integer_N (nat_degree f) a b b0 f le_rfl

view this post on Zulip Damiano Testa (Dec 19 2020 at 04:42):

A follow up question: is the definition below already in mathlib? Thanks!

def zq : fraction_map   := { to_fun := (λ z, z),
  map_one' := _,
  map_mul' := _,
  map_zero' := _,
  map_add' := _,
  map_units' := _,
  surj' := _,
  eq_iff_exists' := _ }

view this post on Zulip Damiano Testa (Dec 19 2020 at 04:51):

Found it!

/-- The cast from `int` to `rat` as a `fraction_map`. -/
def int.fraction_map : fraction_map   :=
{ to_fun := coe,
  map_units' :=
  begin
    rintro x, hx⟩,
    rw [submonoid.mem_carrier, mem_non_zero_divisors_iff_ne_zero] at hx,
    simpa only [is_unit_iff_ne_zero, int.cast_eq_zero, ne.def, subtype.coe_mk] using hx,
  end,
  surj' :=
  begin
    rintro n, d, hd, h⟩,
    refine ⟨⟨n, d, _⟩⟩, rat.mul_denom_eq_num⟩,
    rwa [submonoid.mem_carrier, mem_non_zero_divisors_iff_ne_zero, int.coe_nat_ne_zero_iff_pos]
  end,
  eq_iff_exists' :=
  begin
    intros x y,
    rw [int.cast_inj],
    refine by { rintro rfl, use 1 }, _⟩,
    rintro ⟨⟨c, hc⟩, h⟩,
    apply int.eq_of_mul_eq_mul_right _ h,
    rwa [submonoid.mem_carrier, mem_non_zero_divisors_iff_ne_zero] at hc,
  end,
  ..int.cast_ring_hom  }

view this post on Zulip Kenny Lau (Dec 19 2020 at 05:03):

You can search fraction_map ℤ ℚ in VSCode

view this post on Zulip Damiano Testa (Dec 19 2020 at 05:16):

Ah, thanks for the pointer! I still had not realized that there was a search tool across all the repository! I had created my own using grep on the command line!

view this post on Zulip Damiano Testa (Dec 19 2020 at 05:50):

Once more, how can I prove this fact? I cannot get the coercion to more from the submonoid to the element.

import ring_theory.non_zero_divisors

example {Z : Type*} [integral_domain Z] (c : (non_zero_divisors Z)) :
  c  non_zero_divisors Z :=
begin
  sorry,
end

view this post on Zulip Kenny Lau (Dec 19 2020 at 05:53):

exact c.2

view this post on Zulip Damiano Testa (Dec 19 2020 at 05:53):

Seriously! It works, thanks a lot!!

view this post on Zulip Damiano Testa (Dec 19 2020 at 08:05):

Is there a way of finding out such proofs automatically? Library_search does not seem to try the components of assumptions.

view this post on Zulip Johan Commelin (Dec 19 2020 at 08:12):

Which is weird, because this is just shorthand for subtype.property c

view this post on Zulip Damiano Testa (Dec 19 2020 at 08:17):

Is there a tactic that tries out exact h.i where h is a hypothesis and i an index?

view this post on Zulip Damiano Testa (Dec 19 2020 at 08:18):

Something like assumption, except... subassumption?

view this post on Zulip Kevin Buzzard (Dec 19 2020 at 08:20):

A tactic like library_search is to find proofs when you don't know where they are. Here it's clear where the proof is, all you need to learn is the simple technique for getting it out.

view this post on Zulip Kevin Buzzard (Dec 19 2020 at 08:25):

Re subassumption -- if you've spent some time playing with pp.all true you will discover how absolutely gigantic some terms are!

view this post on Zulip Kevin Buzzard (Dec 19 2020 at 08:26):

That, together with the fact that figuring out if two terms have the same type is noncomputable, indicates that it might be better off just learning the trick

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

Ok, in this case, I had no idea that c.2 was my assumption, but I take your points!

view this post on Zulip Kevin Buzzard (Dec 19 2020 at 08:39):

If you don't understand what c is or how to work with it, you should right click on non_zero_divisors and jump to definition, where you will see how it's defined and examples of how to use it plus the basic API (the lemmas proved just after the definition).

view this post on Zulip Kevin Buzzard (Dec 19 2020 at 08:40):

Inside a tactic proof you can also do cases c if you want to see what it's hiding

view this post on Zulip Johan Commelin (Dec 19 2020 at 08:45):

But in this case clicking on non_zero_divisors wouldn't help. It's the coe_to_sort that was hiding something

view this post on Zulip Damiano Testa (Dec 19 2020 at 10:04):

Thank you both! I had looked at non_zero_divisors and I tried to exact it a lot, but did not think of it having fields. A rookie mistake!

view this post on Zulip Johan Commelin (Dec 19 2020 at 10:08):

@Damiano Testa non_zero_divisors is a set. But sets can be coerced into types (using coe_to_sort). This coercion sends a set s to subtype s = {x // x \in s}.

view this post on Zulip Johan Commelin (Dec 19 2020 at 10:08):

If s : set X, then subtype s is

{ val : X,
  property : val \in s }

view this post on Zulip Johan Commelin (Dec 19 2020 at 10:10):

So if you have a term c : non_zero_divisors, then c.val is the raw element, and c.property is the proof witness that c.val is in fact a nonzero divisor.

view this post on Zulip Johan Commelin (Dec 19 2020 at 10:10):

c.2 is just shorthand for c.property.

view this post on Zulip Johan Commelin (Dec 19 2020 at 10:10):

But my main point is that .val and .property have nothing to do with non_zero_divisor. They come from subtype.

view this post on Zulip Johan Commelin (Dec 19 2020 at 10:11):

And the subtype showed up by some hidden Lean trick, because non_zero_divisor was being treated as a Type instead of as a set.

view this post on Zulip Damiano Testa (Dec 19 2020 at 10:14):

Thank you very much for the explanation! I am now just competent enough to understand what you are saying!

view this post on Zulip Damiano Testa (Dec 19 2020 at 10:14):

And it clarifies a lot!

view this post on Zulip Yakov Pechersky (Dec 20 2020 at 00:15):

I bet suggest would give you the proof right away

view this post on Zulip Kevin Buzzard (Dec 20 2020 at 00:36):

hint suggests cases c and then hint again suggests tauto which works :-)

view this post on Zulip Yakov Pechersky (Dec 20 2020 at 00:44):

Ah. That's too bad! Is there any way to add subtype.property to the suggest list?

view this post on Zulip Damiano Testa (Dec 20 2020 at 05:16):

Thanks for the suggestion of using cases! I do not use cases enough, I think. Once that step made its way in its final form, it is included in the line

exact false.rec _ (not_not.mpr ze (mem_non_zero_divisors_iff_ne_zero.mp c.property))

view this post on Zulip Damiano Testa (Dec 20 2020 at 05:33):

Below is a proof that you can obtain a fraction_map out of an injective ring homomorphism such that every element of the target is the ratio of two elements of the source. This is not much longer than the proof of int.fraction_map and you can recover int.fraction_map from this in 4 lines.

  1. Is the lemma below already in mathlib? I could not find it.
  2. Does it seem like a valuable addition?
lemma fraction_map_of_inj_frac {Z Q : Type*} [integral_domain Z] [field Q] (i : Z →+* Q)
  (inj : function.injective i)
  (gen :  q : Q,  a b : Z, b  0  q * i b = i a) :
  fraction_map Z Q :=
{ to_fun := (λ z, i z),
  map_one' := ring_hom.map_one i,
  map_mul' := ring_hom.map_mul i,
  map_zero' := ring_hom.map_zero i,
  map_add' := ring_hom.map_add i,
  map_units' := begin
    rintros y, z⟩,
    rw [submonoid.mem_carrier, mem_non_zero_divisors_iff_ne_zero] at z,
    refine ⟨{val := i y, inv := (i y)⁻¹, val_inv := _, inv_val := _}, rfl;
    { try { rw mul_inv_cancel },
      try { rw inv_mul_cancel },
      rw  ring_hom.map_zero i,
      exact function.injective.ne inj z },
  end,
  surj' := begin
    intro z,
    obtain a, b, b0, H := gen z,
    exact ⟨⟨a, b, mem_non_zero_divisors_iff_ne_zero.mpr b0⟩⟩, H⟩,
  end,
  eq_iff_exists' := begin
    intros x y,
    simp_rw [function.injective.eq_iff inj, mul_eq_mul_right_iff],
    refine λ h, 1, or.inl h⟩, λ h, _⟩,
    rcases h with c, rfl | ze⟩,
    { refl },
    { exact false.rec _ (not_not.mpr ze (mem_non_zero_divisors_iff_ne_zero.mp c.property)) },
 end }

view this post on Zulip Damiano Testa (Dec 20 2020 at 05:36):

And below is the proof of int.fraction_map, given the lemma above.

noncomputable def ZQ_alg : fraction_map   :=
fraction_map_of_inj_frac (algebra_map  )
  (id (λ a b h, (@int.cast_inj  _ _ _ a b).mp (by rwa ring_hom.eq_int_cast at h)))
  (λ q, q.1, q.2, by { norm_cast, exact rat.denom_ne_zero q },
    (by rw [ring_hom.eq_int_cast, ring_hom.eq_int_cast, int.cast_coe_nat, rat.mul_denom_eq_num] )⟩)

together with a proof that it coincides with the earlier definition:

lemma comp : ZQ_alg = fraction_map.int.fraction_map :=
by { ext1, simp only [ring_hom.eq_int_cast] }

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

Dear All,

in the process of cleaning up, I now have two almost identical proofs of essentially the same statement. One assumes that you start with a semiring/comm_ring pair, the other with an integral_domain/field pair. I would like to obtain the integral_domain/field result as an application of the semiring/comm_ring one. However, I seem to be steering Lean to proving something that is not true. Can anyone help me with the second sorry below, please? Thank you very much!

import ring_theory.localization

open polynomial

section semiring

variables {R K : Type*} [semiring R] [comm_semiring K] {i : R →+* K}
variables {a b : R} {bi : K} {bu : bi * i b = 1}

lemma nums_dens  -- this is the lemma that I can prove
  (i : R →+* K)
  (f : polynomial R) (a b : R) (bi : K) (bu : bi * i b = 1) :
  ( D : R, i D = (i b ^ f.nat_degree * eval (i a * bi) (polynomial.map i f))) :=
sorry  -- I have a full proof of this fact

end semiring

section fractions_map

variables {R K : Type*} [integral_domain R] [field K] {d : fraction_map R K}

-- this is the "special case" of the previous one that I can only prove by reproving it along
-- the same lines as the lemma above
lemma nums_dens_2 (f : polynomial R) (a : R) {b : R} (b0 : b  0) :
  d.is_integer (((d.to_map b) ^ f.nat_degree * eval₂ d.to_map (d.to_map a / d.to_map b) f)) :=
begin
  convert nums_dens d.to_map f a b (1 / d.to_map b) _,
  unfold eval, -- here you can see that Lean is following different paths that seem to diverge
  sorry, -- I can see that Lean went to try to prove something that is not necessarily true
  -- but how can I get it to prove what actually is true?
  apply one_div_mul_cancel,
  rw  (localization_map.to_map d).map_zero,
  exact function.injective.ne (fraction_map.injective d) b0,
end

end fractions_map

view this post on Zulip Adam Topaz (Dec 30 2020 at 15:24):

import ring_theory.localization
import tactic.field_simp

open polynomial

section semiring

variables {R K : Type*} [semiring R] [comm_semiring K] {i : R →+* K}
variables {a b : R} {bi : K} {bu : bi * i b = 1}

lemma nums_dens  -- this is the lemma that I can prove
  (i : R →+* K)
  (f : polynomial R) (a b : R) (bi : K) (bu : bi * i b = 1) :
  ( D : R, i D = (i b ^ f.nat_degree * eval₂ i (i a * bi) f)) :=
sorry  -- I have a full proof of this fact

end semiring

section fractions_map

variables {R K : Type*} [integral_domain R] [field K] {d : fraction_map R K}

-- this is the "special case" of the previous one that I can only prove by reproving it along
-- the same lines as the lemma above
lemma nums_dens_2 (f : polynomial R) (a : R) {b : R} (b0 : b  0) :
  d.is_integer (((d.to_map b) ^ f.nat_degree * eval₂ d.to_map (d.to_map a / d.to_map b) f)) :=
begin
  convert nums_dens d.to_map f a b (1 / d.to_map b) _,
  field_simp,
  apply one_div_mul_cancel,
  rw  (localization_map.to_map d).map_zero,
  exact function.injective.ne (fraction_map.injective d) b0,
end

end fractions_map

Note that I changed eval to eval\_2 in the first lemma.

view this post on Zulip Adam Topaz (Dec 30 2020 at 15:26):

I don't know how important it is for you to have eval as opposed to eval_2.

view this post on Zulip Damiano Testa (Dec 30 2020 at 15:42):

Ah, thank you! I will try to see how it plays out: to be honest, I do not know what the difference betweeneval and eval2 is.

view this post on Zulip Adam Topaz (Dec 30 2020 at 15:44):

As I understand it, eval_2 takes a polynomial over R and a morphism R -> S and evaluates the polynomial in S.

view this post on Zulip Adam Topaz (Dec 30 2020 at 15:44):

So it looks like that's exactly what you're trying to do in nums_dens.

view this post on Zulip Adam Topaz (Dec 30 2020 at 15:45):

If you insist on using eval, I suggest using docs#polynomial.eval₂_eq_eval_map

view this post on Zulip Damiano Testa (Dec 30 2020 at 15:47):

Thanks for the conversion between eval and eval2: it seems that everything might be a simple rw away!

view this post on Zulip Damiano Testa (Dec 30 2020 at 15:50):

Indeed: below is a proof of the literal statements that I wrote before!

lemma nums_dens_2 (f : polynomial R) (a : R) {b : R} (b0 : b  0) :
  d.is_integer (((d.to_map b) ^ f.nat_degree * eval₂ d.to_map (d.to_map a / d.to_map b) f)) :=
begin
  convert wfs.nums_dens d.to_map f a b (1 / d.to_map b) _,
  rw [eval₂_eq_eval_map, mul_one_div],
  apply one_div_mul_cancel,
  rw  (localization_map.to_map d).map_zero,
  exact function.injective.ne (fraction_map.injective d) b0,
end

Thank you very much!

view this post on Zulip Johan Commelin (Dec 30 2020 at 15:50):

Right, there are 3 ways of evaluating polynomials. If you have f : polynomial R, then you can use

  • eval to evaluate f on elements of R,
  • eval2 to evaluate f on elements of S, but you have to provide a ring hom R -> S
  • aeval to evaluate f on elements of A, if there is an instance [algebra R A] available.

view this post on Zulip Johan Commelin (Dec 30 2020 at 15:51):

(and some of this will assume various rings are commutative)

view this post on Zulip Damiano Testa (Dec 30 2020 at 15:51):

Thank you both!

I personally prefer the initial version nums_dens. However, it does not use the localization theory. I would like to PR either one/both of these to mathlib: is there any preference?

view this post on Zulip Johan Commelin (Dec 30 2020 at 15:54):

probably both, because the proof of nums_dens_2 is not a 1-liner.

view this post on Zulip Adam Topaz (Dec 30 2020 at 15:54):

You can also formulate nums_dens with is_unit (i b).

view this post on Zulip Adam Topaz (Dec 30 2020 at 15:55):

Which I suppose is closer to the localization api.

view this post on Zulip Damiano Testa (Dec 30 2020 at 15:55):

(I meant, PR these with a full proof! My preference would be to prove nums_dens and maybe or maybe not include also the proof above of nums_dens_2. Since I do not have much experience with localizations in mathlib, I had worked with the initial version. I do use the freedom of having a target field that is larger than the field of fractions. In my intended application, the rings in question are ℤ and ℝ, rather than ℚ.)

view this post on Zulip Johan Commelin (Dec 30 2020 at 15:56):

That's another argument for nums_dens. It is a lot more flexible.

view this post on Zulip Damiano Testa (Dec 30 2020 at 15:56):

Ok, so I will PR the statement without localizations and merge it in some file. Then, once this one is in, I will add the proof of nums_dens_2 in the localization file. Of course, the names will have to be better!

view this post on Zulip Adam Topaz (Dec 30 2020 at 15:56):

Don't we have something in mathlib which says "This morphism of rings f:ABf : A \to B factors through AS1AA \to S^{-1}A."?

view this post on Zulip Adam Topaz (Dec 30 2020 at 15:57):

I.e. \forall s, is_unit (f s)

view this post on Zulip Johan Commelin (Dec 30 2020 at 15:57):

Hmm, maybe just PR only nums_dens. We'll see if nums_dens_2 is useful in the end. Maybe if we refactor localization to make localization_map a predicate, then the proof of nums_dens_2 will be a 1-liner.

view this post on Zulip Johan Commelin (Dec 30 2020 at 15:57):

If nobody gets to it before me, I hope to do this refactor 2nd half of Feb

view this post on Zulip Johan Commelin (Dec 30 2020 at 15:58):

Adam Topaz said:

Don't we have something in mathlib which says "This morphism of rings f:ABf : A \to B factors through AS1AA \to S^{-1}A."?

Probably localization_map.lift or something like that. I'm sure it's there.

view this post on Zulip Damiano Testa (Dec 30 2020 at 15:58):

Ok, I will do so! As an idea, I like the localization idea, however, the possibility of working with a "possibly larger than the localization" target ring can be useful.

view this post on Zulip Adam Topaz (Dec 30 2020 at 15:59):

Yeah, I agree. That's why I suggested the is_unit thing, because I assumed the api for localization used it... I'm looking in mathlib now...

view this post on Zulip Damiano Testa (Dec 30 2020 at 15:59):

(I still do not have a good application in mind for the semiring stuff, so, although it is true with these very limited hypotheses, it is not this that sells it to me!)

view this post on Zulip Adam Topaz (Dec 30 2020 at 15:59):

Right docs#localization_map.lift

view this post on Zulip Adam Topaz (Dec 30 2020 at 16:00):

So, I think if you can phrase your nums_dens using is_unit, it should be easy to relate it to localization via the universal property using localization_map.lift.

view this post on Zulip Damiano Testa (Dec 30 2020 at 16:06):

Just to emphasize what you have all been saying: I had no use for this in this context, however, I would also find it useful to have the freedom in localization to work with the localization of a quotient. If I understand correctly, this is where the localization_map.lift comes in.

view this post on Zulip Adam Topaz (Dec 30 2020 at 16:12):

Well, what I'm saying is that the condition is_unit (i b) is equivalent to the assertion that the moprhism i factors through the localization at the element b. And the part of the localization api which lets you obtain the map from the localization at b is coming from localization_map.lift, where the assumption is \forall s, is_unit (i s) (or something similar...).

view this post on Zulip Adam Topaz (Dec 30 2020 at 16:12):

So essentially, yes :)

view this post on Zulip Adam Topaz (Dec 30 2020 at 16:17):

Here's a skeleton :)

import ring_theory.localization
import algebra.group.units
import tactic.field_simp

open polynomial

section semiring

variables {R K : Type*} [semiring R] [comm_semiring K] {i : R →+* K}
variables {a b : R}

lemma nums_dens  -- this is the lemma that I can prove
  (i : R →+* K)
  (f : polynomial R) (a b : R) (hb : is_unit (i b)) :
  ( D : R, i D = (i b ^ f.nat_degree * eval₂ i (i a * hb.unit.inv) f)) :=
sorry  -- I have a full proof of this fact

end semiring

view this post on Zulip Damiano Testa (Dec 30 2020 at 16:19):

Thanks! I was trying to see how to extract the inverse from is_unit!

view this post on Zulip Damiano Testa (Dec 30 2020 at 16:56):

I am failing to make progress: how do I access the fact that is_unit implies that there is an inverse? Below is a #mwe that I am not able to solve.

import algebra.group.units
import algebra.ring.basic

example {R : Type*} [semiring R] {K : Type*} [comm_semiring K]
  {i : R →+* K} (b : R) (iub : is_unit (i b)) :
  iub.unit.inv * i b = 1 :=
begin
  admit,
end

view this post on Zulip Patrick Massot (Dec 30 2020 at 17:00):

Johan Commelin said:

Right, there are 3 ways of evaluating polynomials. If you have f : polynomial R, then you can use

  • eval to evaluate f on elements of R,
  • eval2 to evaluate f on elements of S, but you have to provide a ring hom R -> S
  • aeval to evaluate f on elements of A, if there is an instance [algebra R A] available.

Is this in a module docstring somewhere? If not then it should be added.

view this post on Zulip Kevin Buzzard (Dec 30 2020 at 17:19):

Are the three ways to do arbitrary unions, each with their own specific notation, documented somewhere?

view this post on Zulip Adam Topaz (Dec 30 2020 at 19:25):

Damiano Testa said:

I am failing to make progress: how do I access the fact that is_unit implies that there is an inverse? Below is a #mwe that I am not able to solve.

Here's a proof (that can probably be golfed a bit):

import algebra.group.units
import algebra.ring.basic

-- This should really be a simp lemma for `is_unit` itself...
example {R : Type*} [semiring R] {K : Type*} [comm_semiring K]
  {i : R →+* K} (b : R) (iub : is_unit (i b)) :
  iub.unit.inv * i b = 1 :=
begin
  convert iub.unit.inv_val,
  change _ = (iub.unit),
  simp [iub.unit_spec],
end

view this post on Zulip Damiano Testa (Dec 30 2020 at 19:29):

Thank you very much!

view this post on Zulip Adam Topaz (Dec 30 2020 at 19:30):

It really looks like mathlib is missing some simp lemmas here...

view this post on Zulip Adam Topaz (Dec 30 2020 at 19:30):

This proof should have been by simp.

view this post on Zulip Damiano Testa (Dec 30 2020 at 19:33):

Yes, even with your solution, I am finding it very difficult to navigate with the is_unit command...

view this post on Zulip Damiano Testa (Dec 30 2020 at 19:34):

In fact, maybe this example should be a simp lemma

view this post on Zulip Adam Topaz (Dec 30 2020 at 19:36):

This is a bit better:

import algebra.group.units
import algebra.ring.basic

-- rename this...
@[simp] lemma unit_val_eq_coe {M : Type*} [monoid M] (u : units M) : u.val = u := rfl

-- rename this too...
@[simp] lemma is_unit_mul {M : Type*} [monoid M] {x : M}
  (hx : is_unit x) : hx.unit.inv * x = 1 :=
begin
  convert hx.unit.inv_val,
  simp [hx.unit_spec],
end

example {R : Type*} [semiring R] {K : Type*} [comm_semiring K]
  {i : R →+* K} (b : R) (iub : is_unit (i b)) :
  iub.unit.inv * i b = 1 := by simp

view this post on Zulip Damiano Testa (Dec 30 2020 at 19:43):

I am off for the day, but will take a look at this soon! I have PR #5529 with a single lemma waiting to be approved, before I will make a PR with the stuff about denominators!

view this post on Zulip Johan Commelin (Dec 30 2020 at 19:48):

I left a review (-;

view this post on Zulip Eric Wieser (Dec 31 2020 at 12:24):

A golf of @Adam Topaz's second lemma,

@[simp] lemma is_unit.inv_mul {M : Type*} [monoid M] {x : M}
  (hx : is_unit x) : hx.unit.inv * x = 1 :=
units.inv_mul_of_eq hx.unit_spec

or possible more simp-normal,

@[simp] lemma is_unit.inv_mul {M : Type*} [monoid M] {x : M}
  (hx : is_unit x) : (hx.unit⁻¹) * x = 1 :=
units.inv_mul_of_eq hx.unit_spec

which parallels the theorem statement of docs#unit.inv_mul

view this post on Zulip Damiano Testa (Jan 03 2021 at 10:03):

I created PR #5587 including the stuff about clearing denominators. I still did not include the is_unit stuff, though.


Last updated: May 15 2021 at 00:39 UTC