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

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

#### 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) :
begin
{ 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,
{ apply le_trans (nat_degree_C_mul_X_pow_le (leading_coeff f) (nat_degree f)) df },
{ apply P_C_mul_pow _ _ _ df,
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,
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, _⟩,
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_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.

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_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 betweeneval 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):

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