field of fractions

Stream: new members

[Damiano Testa]

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]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Damiano Testa]

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]

Should docs#fraction_map have a coe_to_fun equal to to_map?

[Damiano Testa]

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]

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

[Johan Commelin]

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

[Eric Wieser]

I think the instance may already be there

[Eric Wieser]

Does it work without to_map?

[Damiano Testa]

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]

It might be that you only need one of the to_maps

[Anne Baanen]

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]

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]

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]

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]

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]

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]

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]

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]

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]

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]

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]

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]

You can search fraction_map ℤ ℚ in VSCode

[Damiano Testa]

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]

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]

exact c.2

[Damiano Testa]

Seriously! It works, thanks a lot!!

[Damiano Testa]

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

[Johan Commelin]

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

[Damiano Testa]

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

[Damiano Testa]

Something like assumption, except... subassumption?

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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]

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

[Johan Commelin]

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

[Damiano Testa]

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]

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

If s : set X, then subtype s is

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

[Johan Commelin]

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]

c.2 is just shorthand for c.property.

[Johan Commelin]

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

[Johan Commelin]

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]

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

[Damiano Testa]

And it clarifies a lot!

[Yakov Pechersky]

I bet suggest would give you the proof right away

[Kevin Buzzard]

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

[Yakov Pechersky]

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

[Damiano Testa]

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]

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 }

[Damiano Testa]

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]

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]

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]

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

[Damiano Testa]

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]

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

[Adam Topaz]

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

[Adam Topaz]

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

[Damiano Testa]

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

[Damiano Testa]

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]

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]

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

[Damiano Testa]

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]

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

[Adam Topaz]

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

[Adam Topaz]

Which I suppose is closer to the localization api.

[Damiano Testa]

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

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

[Damiano Testa]

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]

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]

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

[Johan Commelin]

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]

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

[Johan Commelin]

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]

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]

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]

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

Right docs#localization_map.lift

[Adam Topaz]

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]

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]

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]

So essentially, yes :)

[Adam Topaz]

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]

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

[Damiano Testa]

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]

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]

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

[Adam Topaz]

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]

Thank you very much!

[Adam Topaz]

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

[Adam Topaz]

This proof should have been by simp.

[Damiano Testa]

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

[Damiano Testa]

In fact, maybe this example should be a simp lemma

[Adam Topaz]

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]

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]

I left a review (-;

[Eric Wieser]

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]

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