# Zulip Chat Archive

## Stream: new members

### Topic: field of fractions

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

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

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

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

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

#### Eric Wieser (Dec 18 2020 at 14:41):

Should docs#fraction_map have a coe_to_fun equal to to_map?

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

#### Johan Commelin (Dec 18 2020 at 14:43):

I think `fraction_map`

(and `localization_map`

) should be predicates on `ring_hom`

.

#### Johan Commelin (Dec 18 2020 at 14:43):

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

#### Eric Wieser (Dec 18 2020 at 14:44):

I think the instance may already be there

#### Eric Wieser (Dec 18 2020 at 14:44):

Does it work without to_map?

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

#### Eric Wieser (Dec 18 2020 at 14:57):

It might be that you only need one of the `to_map`

s

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

?

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

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

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

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

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

#### Damiano Testa (Dec 18 2020 at 15:14):

Ah, thanks a lot, Eric! I am not at all familiar with `coe`

stuff, 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.

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

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

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

#### 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' := _ }
```

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

#### Kenny Lau (Dec 19 2020 at 05:03):

You can search `fraction_map ℤ ℚ`

in VSCode

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

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

#### Kenny Lau (Dec 19 2020 at 05:53):

`exact c.2`

#### Damiano Testa (Dec 19 2020 at 05:53):

Seriously! It works, thanks a lot!!

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

#### Johan Commelin (Dec 19 2020 at 08:12):

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

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

#### Damiano Testa (Dec 19 2020 at 08:18):

Something like `assumption`

, except... `subassumption`

?

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

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

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

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

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

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

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

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

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

.

#### Johan Commelin (Dec 19 2020 at 10:08):

If `s : set X`

, then `subtype s`

is

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

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

#### Johan Commelin (Dec 19 2020 at 10:10):

`c.2`

is just shorthand for `c.property`

.

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

.

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

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

#### Damiano Testa (Dec 19 2020 at 10:14):

And it clarifies a lot!

#### Yakov Pechersky (Dec 20 2020 at 00:15):

I bet `suggest`

would give you the proof right away

#### Kevin Buzzard (Dec 20 2020 at 00:36):

`hint`

suggests `cases c`

and then `hint`

again suggests `tauto`

which works :-)

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

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

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

- Is the lemma below already in mathlib? I could not find it.
- 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 }
```

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

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

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

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

.

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

and `eval2`

is.

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

.

#### Adam Topaz (Dec 30 2020 at 15:44):

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

.

#### Adam Topaz (Dec 30 2020 at 15:45):

If you insist on using `eval`

, I suggest using docs#polynomial.eval₂_eq_eval_map

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

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

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

#### Johan Commelin (Dec 30 2020 at 15:51):

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

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

#### Johan Commelin (Dec 30 2020 at 15:54):

probably both, because the proof of `nums_dens_2`

is not a 1-liner.

#### Adam Topaz (Dec 30 2020 at 15:54):

You can also formulate `nums_dens`

with `is_unit (i b)`

.

#### Adam Topaz (Dec 30 2020 at 15:55):

Which I suppose is closer to the localization api.

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

#### Johan Commelin (Dec 30 2020 at 15:56):

That's another argument for `nums_dens`

. It is a lot more flexible.

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

#### Adam Topaz (Dec 30 2020 at 15:56):

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

#### Adam Topaz (Dec 30 2020 at 15:57):

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

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

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

#### 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 : A \to B$ factors through $A \to S^{-1}A$."?

Probably `localization_map.lift`

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

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

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

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

#### Adam Topaz (Dec 30 2020 at 15:59):

Right docs#localization_map.lift

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

.

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

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

#### Adam Topaz (Dec 30 2020 at 16:12):

So essentially, yes :)

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

#### Damiano Testa (Dec 30 2020 at 16:19):

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

!

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

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

#### Kevin Buzzard (Dec 30 2020 at 17:19):

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

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

#### Damiano Testa (Dec 30 2020 at 19:29):

Thank you very much!

#### Adam Topaz (Dec 30 2020 at 19:30):

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

#### Adam Topaz (Dec 30 2020 at 19:30):

This proof should have been `by simp`

.

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

#### Damiano Testa (Dec 30 2020 at 19:34):

In fact, maybe this example should be a `simp`

lemma

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

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

#### Johan Commelin (Dec 30 2020 at 19:48):

I left a review (-;

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

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