free_comm_ring

Stream: general

[Kenny Lau]

(This thread is a continuation of https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews)
So I built the free commutative ring over a type A, which corresponds to the multivariate polynomials with variables indexed by A and coefficients in \Z. There are some differences between free_comm_ring A and mv_polynomial A \Z:
1. you don't need A to have decidable equality for free_comm_ring A to be a ring, but you do need it for mv_polynomial A \Z to be a ring.
2. the coefficients of free_comm_ring are in \Z, so it is a special case of mv_polynomial (polynomial is also a special case and we also allow it in mathlib).
3. free_comm_ring might have faster elaboration speed than mv_polynomial, and it might be caused by the fact that there are less typeclass searches, since it doesn't need either decidable_eq or a ring instance for the coefficients.

[Kenny Lau]

Should we put free_comm_ring in mathlib?

[Kenny Lau]

@Mario Carneiro @Kevin Buzzard @Chris Hughes

[Mario Carneiro]

no ring instance for the coefficients?

[Mario Carneiro]

I agree that mv_polynomial should have decidable_eq removed, but this isn't the only way to achieve that

[Mario Carneiro]

I think finsupp should go fully classical

[Kenny Lau]

I mean, free_comm_ring doesn't have a sense of "coefficients" at all

[Kenny Lau]

so it doesn't need to search for a ring instance of the "coefficients"

[Mario Carneiro]

you claimed that free_comm_ring is equivalent to mv_polynomial. That means it has all the structure of polynomials. Where is it?

[Kenny Lau]

I never claimed that.

[Kenny Lau]

I said free_comm_ring \a is isomorphic to mv_polynomial \a \Z

[Mario Carneiro]

So how does mv_polynomial A B relate to a free construction?

[Kenny Lau]

I don't see the relevance of that question

[Kenny Lau]

but mv_polynomial A B is the free B-algebra generated by A

[Mario Carneiro]

okay, so let's do that

[Mario Carneiro]

I guess that generalizes to all the other free constructions too

[Kenny Lau]

my construction only works for coefficients in Z

[Mario Carneiro]

like ring expressions with constants taken from a ring, or free group expressions with constants in a group

[Mario Carneiro]

and indeterminates from an arbitrary type

[Kenny Lau]

I don't understand

[Kenny Lau]

what's your new plan?

[Kenny Lau]

you want to replace mv_polynomial entirely?

[Mario Carneiro]

I thought that was your plan

[Kenny Lau]

no that wasn't my plan

[Kenny Lau]

my plan is to keep mv_polynomial, and add free_comm_ring

[Mario Carneiro]

As you pointed out, we already have mv_polynomial \a \Z. It just needs a few less typeclass args

[Kenny Lau]

we also have mv_polynomial unit R but polynomial is still in mathlib

[Mario Carneiro]

But probably your version is closer to what someone would expect if they see free_comm_ring

[Mario Carneiro]

I think it is okay to have isomorphic constructions if they represent a different way of dealing with a type, but you need to have tons of lemmas relating the two if you take this route

[Kenny Lau]

it's just the free comm ring. It's what I intended it to be. It's just a coincidence that it's isomorphic to mv_polynomial A \Z

[Kenny Lau]

I don't understand why a fuss is being made over this

[Kenny Lau]

seriously mv_polynomial is so damn slow I don't even want to work with them @Mario Carneiro

[Kenny Lau]

can I not refactor #754

[Mario Carneiro]

Like I said, the decidable_eq instance on finsupp needs to die

[Mario Carneiro]

Okay, go ahead. But the idea behind library building is that you complete the graph of relations between concepts in the library. If you have two isomorphic things there should be a theorem about that

[Kenny Lau]

what do you mean by "go ahead"?

[Kenny Lau]

I would have given up if I hadn't written this in terms of free_comm_ring to begin with

[Kenny Lau]

elaboration of lift took 18.8s

[Kenny Lau]

def lift : direct_limit G f → P :=
by haveI : is_ring_hom (coe : ℤ → P) := int.cast.is_ring_hom; exact
ideal.quotient.lift _ (eval₂ coe $ λ x : Σ i, G i, g x.1 x.2) begin
  haveI : is_ring_hom (eval₂ (coe : ℤ → P) $ λ x : Σ i, G i, g x.1 x.2) := eval₂.is_ring_hom _ _,
  suffices : ideal.span _ ≤ ideal.comap (eval₂ (coe : ℤ → P) $ λ x : Σ i, G i, g x.1 x.2) ⊥,
  { intros x hx, exact (mem_bot P).1 (this hx) },
  rw ideal.span_le, intros x hx,
  rw [mem_coe, ideal.mem_comap, mem_bot],
  rcases hx with ⟨i, j, hij, x, rfl⟩ | ⟨i, rfl⟩ | ⟨i, x, y, rfl⟩ | ⟨i, x, y, rfl⟩;
  simp only [eval₂_sub, eval₂_X, Hg, eval₂_one, eval₂_add, eval₂_mul,
      is_ring_hom.map_one (g i), is_ring_hom.map_add (g i), is_ring_hom.map_mul (g i), sub_self]
end

[Kenny Lau]

do you see how to make it faster?

[Kenny Lau]

original:

def lift : direct_limit G f → P :=
ideal.quotient.lift _ (free_comm_ring.lift $ λ x, g x.1 x.2) begin
  suffices : ideal.span _ ≤
    ideal.comap (free_comm_ring.lift (λ (x : Σ (i : ι), G i), g (x.fst) (x.snd))) ⊥,
  { intros x hx, exact (mem_bot P).1 (this hx) },
  rw ideal.span_le, intros x hx,
  rw [mem_coe, ideal.mem_comap, mem_bot],
  rcases hx with ⟨i, j, hij, x, rfl⟩ | ⟨i, rfl⟩ | ⟨i, x, y, rfl⟩ | ⟨i, x, y, rfl⟩;
  simp only [lift_sub, lift_of, Hg, lift_one, lift_add, lift_mul,
      is_ring_hom.map_one (g i), is_ring_hom.map_add (g i), is_ring_hom.map_mul (g i), sub_self]
end

[Mario Carneiro]

Using ring_hom might help here as well

[Mario Carneiro]

I think that all of the issues you point out which free_comm_ring solves have nothing to do with the definition

[Kenny Lau]

I would appreciate a diagnosis of the slow elaboration time

[Kenny Lau]

Lean doesn't really have good debugging tools

[Kenny Lau]

Using ring_hom might help here as well

so you're saying, I should do a lot of refactoring just to get #754 into mathlib?

[Mario Carneiro]

No, that's what I meant by "go ahead". But I don't think we should despair over mv_polynomial

[Kenny Lau]

thanks

[Kenny Lau]

The correct way to do mv_polynomial A B is free_comm_ring A \otimes B

[Johan Commelin]

Why is that the correct way? Why isn't the correct way free_comm_algebra B A?

[Kenny Lau]

because how are you gonna construct that

[Kenny Lau]

(the two bifunctors are isomorphic anyway)

[Chris Hughes]

@Kenny Lau What would you suggest changing about mv_polynomial in order to make it usable?

[Kenny Lau]

I would suggest better debugging tools in Lean 4

[Chris Hughes]

Does Mario's suggestion of getting rid of any decidability assumptions, and using classical throughout help?

[Kenny Lau]

no idea

[Kevin Buzzard]

But you could find out Kenny, by finding a situation where you have problems with polynomials and then throwing in prop_decidable etc and seeing if it speeds things up.

[Johan Commelin]

@Rob Lewis Here is another thread about issues with polynomials being slow...