Zulip Chat Archive

Stream: maths

Topic: semimodules nein danke


view this post on Zulip Kevin Buzzard (Sep 13 2018 at 21:34):

tactic.mk_instance failed to generate instance for
  module (polynomial R) (polynomial R)

That didn't used to happen.

From algebra/module.lean:

instance semiring.to_semimodule [r : semiring α] : semimodule α α := [stuff]

instance ring.to_module [r : ring α] : module α α :=
{ ..semiring.to_semimodule }

Is this definitely OK? My rings are no longer modules over themselves for some reason.

view this post on Zulip Kenny Lau (Sep 13 2018 at 21:35):

nein danke

view this post on Zulip Kevin Buzzard (Sep 13 2018 at 21:48):

import data.polynomial algebra.module

example (R) [nonzero_comm_ring R] (I : set (polynomial R)) [is_submodule I] : 1 = 1 := by simp

/-

failed to synthesize type class instance for
R : Type ?,
_inst_1 : nonzero_comm_ring R,
I : set (polynomial R)
⊢ module ?m_1 (polynomial R)

-/

Am I just making a rookie error? I thought this used to work?

view this post on Zulip Kevin Buzzard (Sep 13 2018 at 21:49):

Oh -- I am -- this is not the problem. I need decidable equality. I'll keep looking for the problem.

view this post on Zulip Mario Carneiro (Sep 13 2018 at 21:51):

FYI I'm currently working on a big rewrite of most of this, so stay tuned.

view this post on Zulip Kevin Buzzard (Sep 13 2018 at 21:55):

Oh Ok. I just pulled again and the errors moved to different places, so I guess that's progress.

view this post on Zulip Kevin Buzzard (Sep 13 2018 at 22:01):

Oh I still have (in the middle of some code)

      letI : comm_ring (polynomial R) := by apply_instance, -- works fine
      letI : module (polynomial R) (polynomial R) := by apply_instance, -- fails to generate instance

but if you're changing stuff then perhaps I will just leave things for now.

view this post on Zulip Kevin Buzzard (Sep 14 2018 at 08:44):

import data.polynomial algebra.module linear_algebra.submodule

local attribute [instance, priority 1] classical.prop_decidable

open polynomial

#print ring.to_module
/-

@[instance]
protected def ring.to_module : Π {α : Type u} [r : ring α], module α α := ...

-/

lemma leading_term_bdd_deg_ideal {R} [nonzero_comm_ring R] (I : set (polynomial R)) [is_submodule I] (n : ) :
submodule R R :=
{c : R |  f, f  I  degree f  n  leading_coeff f = c},{
  zero_ := 0,is_submodule.zero,lattice.bot_le,rfl,
  add_ := λ a b f, Hf g, Hg, begin
    letI : ring (polynomial R) := by apply_instance, -- works
    letI : module (polynomial R) (polynomial R) := by apply_instance, -- fails
  sorry, end,
  smul := sorry,
}

There's a fairly minimal working example of something which is stopping me from doing anything on Hilbert basis at the minute. Type class inference can find the ring instance, and the ring to module instance is there, but type class inference can't find the module instance.

view this post on Zulip Kevin Buzzard (Sep 14 2018 at 08:46):

I can't add the instance explictly -- well, I can -- but then I get weird diamond errors later on. I am going to put Hilbert basis on hold for a while until I can understand what is going on here -- currently my understanding is that this is not user error and I should just wait, and of course I'm happy to wait.

view this post on Zulip Johan Commelin (Sep 14 2018 at 08:52):

@Kevin Buzzard You could use the explicit
letI : module (polynomial R) (polynomial R) := @ring.to_module (polynomial R) _,

view this post on Zulip Johan Commelin (Sep 14 2018 at 08:52):

It is a bit ugly, but maybe it would unblock you?

view this post on Zulip Kevin Buzzard (Sep 14 2018 at 09:01):

No because then I get diamond issues with exactly the instances that Mario is currently refactoring

view this post on Zulip Kevin Buzzard (Sep 14 2018 at 09:03):

I just thought I'd post this example because either it's something which seems to be to be currently broken or I've made a mistake and it doesn't work for a good reason (note that I go from term mode to tactic mode and for all I know this has consequences for type class inference). If I've not made a mistake then it's something that should work after the refactoring

view this post on Zulip Johan Commelin (Sep 14 2018 at 09:04):

Hmmm... that's crazy.

view this post on Zulip Kevin Buzzard (Sep 14 2018 at 09:17):

invalid type ascription, term has type
  @is_submodule R (@polynomial R (@comm_ring.to_comm_semiring R (@nonzero_comm_ring.to_comm_ring R _inst_1)))
    (@comm_ring.to_ring R (@nonzero_comm_ring.to_comm_ring R _inst_1))
    (@polynomial.module R (λ (a b : R), classical.prop_decidable (a = b)) (@nonzero_comm_ring.to_comm_ring R _inst_1))
    I
but is expected to have type
  @is_submodule (@polynomial R (@comm_ring.to_comm_semiring R (@nonzero_comm_ring.to_comm_ring R _inst_1)))
    (@polynomial R (@comm_ring.to_comm_semiring R (@nonzero_comm_ring.to_comm_ring R _inst_1)))
    (@comm_ring.to_ring (@polynomial R (@comm_ring.to_comm_semiring R (@nonzero_comm_ring.to_comm_ring R _inst_1)))
       _inst)
    _inst_3
    I

for what it's worth. Oh! What is this polynomial.module?? That's the statement that R[X] is a module over R. Is that relevant? Anyway, this is not the point -- the point is that either my original thing should work and it doesn't (in which case I should stop, because I am using modules all over the place and will surely see other problems later, even though no module actually occurs in the proofs, only ideals, and part of me wants to define ideals as subsets of rings plus blah because we all know that type classes for modules have problems, whereas type classes for ideals will probably work fine), or I've made a mistake (in which case I need help because I can't see it).

view this post on Zulip Johan Commelin (Sep 14 2018 at 09:32):

@Kevin Buzzard So the math strategy would be something like "wlog we have deg(f) ≤ deg(g), now look at X^(degree g - degree f) * f + g. Done."

view this post on Zulip Johan Commelin (Sep 14 2018 at 09:33):

I don't know how to do wlog in Lean, so I'll just do cases on have H := le_or_gt f.degree g.degree,

view this post on Zulip Johan Commelin (Sep 14 2018 at 09:33):

The next step fails, because Lean doesn't know how to subtract with_bot ℕ thingies. Is that intended? Or should we use nat_degree?

view this post on Zulip Kevin Buzzard (Sep 14 2018 at 09:41):

Oh I've done all this bit -- you should look at the kmb_hilbert_basis branch of community mathlib.

view this post on Zulip Johan Commelin (Sep 14 2018 at 09:44):

why are you making me commit just becuase I want to change branch

git stash

view this post on Zulip Kevin Buzzard (Sep 14 2018 at 10:03):

Oh that's what it's for!

view this post on Zulip Johan Commelin (Sep 14 2018 at 10:38):

unexpected occurrence of recursive function
Did I unlock something?

view this post on Zulip Johan Commelin (Sep 14 2018 at 10:38):

@Kevin Buzzard I tried using wlog:

-- zero ring a special case so let's deal with it separately
theorem hilbert_basis_zero_ring {R} [comm_ring R] (h : (0 : R) = 1) :
is_noetherian_ring (polynomial R) :=
begin
  apply ring.is_noetherian_of_zero_eq_one,
  rw polynomial.ext,
  intro n,
  repeat {rw semiring.zero_of_zero_eq_one h (coeff _ n)}
end

theorem hilbert_basis {R} [comm_ring R] (hR : is_noetherian_ring R) : is_noetherian_ring (polynomial R) :=
begin
  -- deal with zero ring first
  by_cases h01 : (0 : R) = 1,
    exact hilbert_basis_zero_ring h01,
  letI : nonzero_comm_ring R := comm_ring.non_zero_of_zero_ne_one h01,
  let L : set R := set.range leading_coeff,
  have HL : is_ideal L := {
    zero_ := 0,rfl,
    add_ := λ a b f,Hf g,Hg, begin
      by_cases h0 : a + b = 0, rw h0, exact 0, rfl,
      by_cases hf : f = 0, rw [Hf, Hg, hf, leading_coeff_zero, zero_add], exact g,rfl,
      by_cases hg : g = 0, rw [Hf, Hg, hg, leading_coeff_zero, add_zero], exact f,rfl,
      wlog hd : nat_degree f  nat_degree g using [f g, g f],
      { exact or.cases_on (le_or_lt (nat_degree f) (nat_degree g)) (assume H, or.inl H) (assume H, or.inr (le_of_lt H)) },
      { let h := f * X ^ (nat_degree g - nat_degree f) + g,
        have Htemp : leading_coeff f * leading_coeff (X ^ (nat_degree g - nat_degree f))  0,
          rw [leading_coeff_X_pow,mul_one],
          exact (λ h, hf $ leading_coeff_eq_zero.1 h),
        have Ha : a = leading_coeff (f * X ^ (nat_degree g - nat_degree f)),
          rw [leading_coeff_mul' Htemp,leading_coeff_X_pow,mul_one,Hf],
        exact h, begin convert leading_coeff_add_of_degree_eq _ _, exact Hg.symm,
                      rw degree_mul_eq' Htemp,
                      rw degree_X_pow,
                      rw degree_eq_nat_degree hf,
                      rw degree_eq_nat_degree hg,
                      rw with_bot.coe_add,
                      rw with_bot.coe_eq_coe,
                      exact nat.add_sub_cancel' hd,
                    rwa [Ha,Hg],
                  end },
    end,
    smul := sorry
  },
  sorry,
end

view this post on Zulip Johan Commelin (Sep 14 2018 at 10:39):

I also proved hilbert_basis_zero_ring

view this post on Zulip Reid Barton (Sep 14 2018 at 10:43):

I wonder whether Hilbert ever proved it

view this post on Zulip Johan Commelin (Sep 14 2018 at 10:45):

Lol...

view this post on Zulip Johan Commelin (Sep 14 2018 at 10:45):

Do you have any idea how I managed to get into this recursive function? Is this a bug in wlog?

view this post on Zulip Reid Barton (Sep 14 2018 at 11:02):

Usually when I get that recursive function error it's because I have some _fun_match or similar thing among my hypotheses and some tactic tried to apply it

view this post on Zulip Reid Barton (Sep 14 2018 at 11:03):

Is that the whole error message?
Guessing from previous discussion here I can't run your code that easily

view this post on Zulip Reid Barton (Sep 14 2018 at 11:04):

The add := λ a b ⟨f,Hf⟩ ⟨g,Hg⟩, looks possibly to blame, if that is the cause

view this post on Zulip Johan Commelin (Sep 14 2018 at 11:07):

There are indeed _fun_match hypotheses in the context.

view this post on Zulip Reid Barton (Sep 14 2018 at 11:08):

see if moving that lambda stuff to an rintros tactic helps

view this post on Zulip Johan Commelin (Sep 14 2018 at 11:08):

Ok, I'll try

view this post on Zulip Johan Commelin (Sep 14 2018 at 11:08):

wlog is too good to miss out on

view this post on Zulip Reid Barton (Sep 14 2018 at 11:11):

Hilbert (1890) proved the theorem (for the special case of polynomial rings over a field)

view this post on Zulip Johan Commelin (Sep 14 2018 at 11:11):

And here we are, about 130 years later, proving it for the zero ring!

view this post on Zulip Kevin Buzzard (Sep 14 2018 at 11:13):

Maybe you don't have my most recent commits. I have more than this. I gave up on wlog for exactly the reason you posted

view this post on Zulip Johan Commelin (Sep 14 2018 at 11:15):

Hmmm, too bad.

view this post on Zulip Reid Barton (Sep 14 2018 at 11:18):

I feel like you could avoid this zero ring stuff if you worked at it. For example, instead of the ideal of all leading coefficients, take the ideal { coeff f i | coeff f j = 0 for all j > i }. Probably not worth it though.

view this post on Zulip Johan Commelin (Sep 14 2018 at 11:20):

Hmm, I don't know. Doesn't that lead to rather clean proofs?

view this post on Zulip Kevin Buzzard (Sep 14 2018 at 11:20):

I honestly don't think that trying to write proofs that work with the zero ring is worth it. Every third step you need to check that something is non-zero. To prove that if I is an ideal of R[X] then the set of leading terms of polynomials in I is an ideal involves so many edge cases; leading term f non-zero, leading term g non-zero, leading term f + g non-zero, and this is all in the case R non-zero. The proof is edge case after edge case and edge case 1 is very naturally R = 0.

view this post on Zulip Johan Commelin (Sep 14 2018 at 11:20):

You need a little lemma saying coeff f j = 0 for all j > degree f.

view this post on Zulip Kevin Buzzard (Sep 14 2018 at 11:22):

Loads of the lemmas about how leading coefficients of polynomials behave rely on terms being non-zero, e.g. you use f*X^(deg g - deg f) to get degree of f up to that of g, and to compute the degree of this you need degree of X is 1 and this demands a proof that 1 isn't 0

view this post on Zulip Kevin Buzzard (Sep 14 2018 at 11:23):

Oh I see -- you mean avoid leading terms completely? But we also need the ideal of leading terms of polys of degree at most n. Maybe you're right and there's some way of doing it.

view this post on Zulip Kevin Buzzard (Sep 14 2018 at 11:23):

PS I pushed some more commits

view this post on Zulip Kevin Buzzard (Sep 14 2018 at 11:24):

the j thing -- you have to be careful because degree is not a nat, it's a with_bot nat, and coeff takes a nat

view this post on Zulip Reid Barton (Sep 14 2018 at 11:24):

I think if you avoid ever saying the word "degree", and unravel its definition everywhere, then possibly all the "R is not zero" steps disappear.

view this post on Zulip Reid Barton (Sep 14 2018 at 11:25):

(But they may be replaced by having to do more other work, and in any case it's a bit unnatural.)

view this post on Zulip Reid Barton (Sep 14 2018 at 11:29):

Apparently they proved this in Mizar

Let RR be a Noetherian Abelian add-associative right zeroed right complementable associative distributive well unital commutative non empty double loop structure. One can verify that Polynom-Ring RR is Noetherian.

view this post on Zulip Kevin Buzzard (Sep 14 2018 at 12:41):

You need to talk about degrees because given an ideal II of R[X]R[X] you need to consider the ideal JkJ_k (kk a natural) comprising of 0 and the leading terms of the polynomials in II of degree kk. But I agree there might be tricks. Here's another example of an edge case -- if ff has degree kk and leading term aa, and cc is in RR then you want to prove that aca*c is in RR, but cfc*f might not have degree kk any more and you have to deal with that case separately. It's quite an annoying proof to formalise :-)

view this post on Zulip Kevin Buzzard (Sep 14 2018 at 16:09):

Aah! I found my type class problem!

import data.polynomial algebra.module linear_algebra.submodule

local attribute [instance, priority 1] classical.prop_decidable

open polynomial

set_option pp.all true

universe u

-- Maths :  "Let I be an ideal of R[X]"

definition ABC (R : Type u) [comm_ring R] (I : set (polynomial R)) [is_submodule I] : false :=
begin

-- ...but I is not an ideal of (polynomial R)!

/-

_inst_2 :
  @is_submodule.{u u} R (@polynomial.{u} R (@comm_ring.to_comm_semiring.{u} R _inst_1))
    (@comm_ring.to_ring.{u} R _inst_1)
    (@polynomial.module.{u} R (λ (a b : R), classical.prop_decidable (@eq.{u+1} R a b)) _inst_1)

-/

-- I is an R-submodule :-/

sorry
end

There's an instance making (polynomial R) an R-module, and another instance making it a (polynomial R)-module, and is_submodule chooses the one I don't want. @Chris Hughes @Mario Carneiro is there a coherent strategy to deal with this? Any time a ring is a module over another ring (and this happens all the time in commutative ring theory) we will have instances of module R M for fixed M and lots of R. I propose scrapping stuff like is_submodule M and replacing it with is_submodule R M. What do you think?

view this post on Zulip Kevin Buzzard (Sep 14 2018 at 16:18):

It's probably worth saying that it is not uncommon at all to hear mathematicians saying "let N be an A-submodule of B" or "let W be a k-subspace of V".

view this post on Zulip Kevin Buzzard (Sep 14 2018 at 19:56):

-- Maths :  "Let I be an ideal of R[X]"

-- Lean
example {R} [comm_ring R] (I : set (polynomial R)) [@is_submodule (polynomial R) _ _ (ring.to_module) I]

view this post on Zulip Kevin Buzzard (Sep 14 2018 at 19:57):

Lean currently has to be told that the ring polynomial R is a module over itself.

view this post on Zulip Kevin Buzzard (Sep 14 2018 at 20:09):

import data.polynomial algebra.module linear_algebra.submodule

local attribute [instance, priority 1] classical.prop_decidable

open polynomial

universe u

-- Maths :  "Let I be an ideal of R[X]. Then 0 ∈ I. "

definition ABC (R : Type u) [comm_ring R] (I : set (polynomial R)) [is_submodule I] : (0 : polynomial R)  I :=
is_submodule.zero -- fails

/-

function expected at
  is_submodule.zero
term has type
  ?m_1 0
Additional information:
/home/buzzard/lean-projects/mathlib-community/tests/scratch.lean:16:0: context: switched to simple application elaboration procedure because failed to use expected type to elaborate it, error message
  too many arguments

-/

Does anyone know what too many arguments means in this context and why it happened?

definition ABC (R : Type u) [comm_ring R] (I : set (polynomial R)) [@is_submodule (polynomial R) _ _ (ring.to_module) I] : (0 : polynomial R)  I :=
is_submodule.zero -- also fails

view this post on Zulip Kevin Buzzard (Sep 14 2018 at 20:23):

definition ABC (R : Type u) [comm_ring R]
  (I : set (polynomial R)) [@is_submodule (polynomial R) _ _ (ring.to_module) I] :
(0 : polynomial R)  I := @is_submodule.zero _ (polynomial R) _ (ring.to_module) I _

Zero is in an ideal of a polynomial ring! Why am I so bad at this? Is it broken or am I just overlooking something simple?

view this post on Zulip Kevin Buzzard (Sep 14 2018 at 20:24):

@Kenny Lau how do you prove zero is in an ideal of the ring R[X]R[X]?

view this post on Zulip Kenny Lau (Sep 14 2018 at 20:24):

I don't

view this post on Zulip Kevin Buzzard (Sep 14 2018 at 20:25):

Why not?

view this post on Zulip Kevin Buzzard (Sep 14 2018 at 20:26):

You want algebraic closure to finish your rigorous formulation of the statement of the local Langlands conjectures for all abelian algebraic groups, a theorem of Langlands. More mathematicians will be interested in Lean if you do that. Tom Hales has already mentioned it in a talk of his -- did you see?

view this post on Zulip Kevin Buzzard (Sep 14 2018 at 20:27):

and for algebraic closure you're going to have to use ideals in polynomial rings quite a lot.

view this post on Zulip Kevin Buzzard (Sep 14 2018 at 20:28):

What is the current status of your formulation project?

view this post on Zulip Kenny Lau (Sep 14 2018 at 20:30):

I mean, aren't we waiting for the refactoring?

view this post on Zulip Kevin Buzzard (Sep 14 2018 at 20:31):

The Langlands philosophy is notorious for being a "philosophy", a vague web of general ideas that it's hard to make rigorous, which occasionally specialise down to very explicit conjectures but sometimes are not actually rigorous mathematical statements. If you get stuck formulating them in general then you can start asking experts in number theory how they actually formulate their grand conjectures. I think it would be really cool. Toby Gee and I spent several years of our lives trying to formulate an actual rigorous conjecture which could rightly be given the name of "Langlands' Reciprocity Conjecture for a general connected reductive group" and we still do not have a general conjecture which encompasses everything.

view this post on Zulip Kevin Buzzard (Sep 14 2018 at 20:32):

https://arxiv.org/abs/1009.0785

view this post on Zulip Kenny Lau (Sep 14 2018 at 20:32):

You want algebraic closure to finish your rigorous formulation of the statement of the local Langlands conjectures for all abelian algebraic groups, a theorem of Langlands. More mathematicians will be interested in Lean if you do that. Tom Hales has already mentioned it in a talk of his -- did you see?

in fact I saw it recently while searching for myself

view this post on Zulip Kevin Buzzard (Sep 14 2018 at 20:35):

I believe that our conjecture can be formalised in Lean and I am not sure that Langlands' philosophy can, not in a way that everyone would find satisfactory at least. What if someone claimed it was the existence of some Global Langlands Group with some properties and then someone like Reid Barton or you just observed that such a group with these properties trivially exists because it's just some pullback. The "ultimate conjecture" is extremely vague. It says that the global Langlands group should be constructed in some way using some generalisation of Galois theory that we don't actually have.

view this post on Zulip Kevin Buzzard (Sep 14 2018 at 20:37):

If you just say that it's some "Galoisish" group whose representation theory looks like the set of automorphic representations in some vague way, and then you try to formalise what you mean, then you're in danger of someone just building a group whose representation theory has this property for trivial reasons.

view this post on Zulip Kevin Buzzard (Sep 14 2018 at 20:42):

Jim Arthur wrote a paper about this many years ago and I wish I understood that paper better. http://www.claymath.org/library/cw/arthur/pdf/automorphic-langlands-group.pdf

view this post on Zulip Kevin Buzzard (Sep 14 2018 at 21:51):

@Reid Barton I thought a bit more about your suggestion and of course you're right. One wants a new subtype deg_le n of polynomials of degree at most n, we want to prove that this is an R-module, and we want to define these increasing ideals as the projection map given by the n'th coefficient. That way we should still to the construction of the finite generating set for the ideal. There's then an induction to go but it looks really easy in this optic.

view this post on Zulip Kevin Buzzard (Sep 14 2018 at 21:53):

No need to assume R is non zero

view this post on Zulip Kevin Buzzard (Sep 14 2018 at 21:55):

We just need deg (f + g) <= max(deg f,deg g) and deg r*f <= deg f, both of which are true unconditionally

view this post on Zulip Kevin Buzzard (Sep 14 2018 at 21:55):

@Chris Hughes these are the nice statements about degrees of polynomials.

view this post on Zulip Kevin Buzzard (Sep 14 2018 at 21:57):

In some sense I'm back to square 1 with my proof but this time it's going to be far more mathlib-ready!

view this post on Zulip Kevin Buzzard (Sep 14 2018 at 22:27):

Dumb question: if R is a ring considered as a semiring and M is a semimodule over the semiring R, is then M a module over the ring R?

view this post on Zulip Reid Barton (Sep 14 2018 at 22:48):

Yes because mmm \mapsto -m is provided by multiplication by 1R-1 \in R and it satisfies the expected equation by distributivity 0=(1+(1))m=mm0 = (1 + (-1)) m = m - m.

view this post on Zulip Mario Carneiro (Sep 14 2018 at 23:17):

I've been too busy to respond today but I see you have converged on the same solution as I have for the ideal of degree <= n polynomials :)

view this post on Zulip Kevin Buzzard (Sep 14 2018 at 23:22):

it's not an ideal :-/

view this post on Zulip Kevin Buzzard (Sep 14 2018 at 23:23):

this is exactly the difference between an ideal and a submodule :-) It's a submodule for one module structure but not for the other.

view this post on Zulip Kevin Buzzard (Sep 14 2018 at 23:36):

def coeff_zero_iff_deg_le {R} [comm_semiring R] (f : polynomial R) (n : with_bot ) :
degree f  n   m : , n < m  coeff f m = 0 :=
begin
  split,
  { intros H m Hm,
    unfold degree at H,
    have : m  f.support,
      intro H2,
      rw finset.sup_le_iff at H,
      have H3 := H m H2,
      revert Hm,
      show ¬ (n < m),
      apply not_lt_of_ge,
      exact H3,
      rw decidable.not_not_iff (coeff f m = 0),
      intro H4,
      apply this,
      rw finsupp.mem_support_to_fun,
      exact H4},
  { intro H,
--    have H2 := H (with_bot_succ n) (with_bot_lt_succ n),
    unfold degree,
    refine finset.sup_le _,
    intros b Hb,
    rw finsupp.mem_support_to_fun at Hb,
    change coeff f b  0 at Hb,
    apply decidable.of_not_not _, apply_instance,
    intro Hn,
    replace Hn := lt_of_not_ge Hn,
    apply Hb,
    apply H,
    exact Hn,
  }
end

This is with the poly_coeffs branch of community mathlib, with Kenny's coeff commands. I think that it might be possible to golf that a bit.

view this post on Zulip Kevin Buzzard (Sep 15 2018 at 07:28):

def coeff_zero_iff_deg_le {R} [comm_semiring R] (f : polynomial R) (n : with_bot ) :
degree f  n   m : , n < m  coeff f m = 0 :=
⟨λ (H : finset.sup (f.support) some  n) m (Hm : n < (m : with_bot )), decidable.of_not_not $ λ H4,
  have H1 : m  f.support,
    from λ H2, not_lt_of_ge ((finset.sup_le_iff.1 H) m H2 : ((m : with_bot )  n)) Hm,
  H1 $ (finsupp.mem_support_to_fun f m).2 H4,
λ H, finset.sup_le $ λ b Hb, decidable.of_not_not $ λ Hn,
  (finsupp.mem_support_to_fun f b).1 Hb $ H b $ lt_of_not_ge Hn

That'a a bit better

view this post on Zulip Kevin Buzzard (Sep 15 2018 at 10:24):

This code seems to demonstrate various things which are currently not optimal:

lemma leading_term_bdd_deg_ideal {R} [decidable_eq R] [nonzero_comm_ring R]
  (I : set (polynomial R)) [@is_submodule R _ _ _ I] (n : ) :
submodule R R :=
submodule.map (λ f : polynomial R, coeff f n) (@coeff_is_linear R _ _ n)
  (I,by apply_instance  deg_le R n,by apply_instance)

I has type set S for S a ring which is hence an SS-module and an RR-module. I want to prove a relatively straightforward theorem about a sub-RR-module of SS. I could have proved it for sub-SS-modules but it's true for sub-RR-modules so I have written it in the correct generality. Of course I now want to immediately apply it to a sub-SS-module and type class inference is going to struggle with that because there is some content there (the lemma that the RR-module structure on SS is induced by a ring map RSR\to S and hence any SS-module is naturally an RR-module, and that all these RR-module structures are the same). I also have a problem with intersections of submodules. I carry around the sets, because the proofs that they are submodules are known to type class inference. However when I want to construct their intersection using the lattice structure I find myself having to explicitly magic up the instances to turn the sets into modules. @Mario Carneiro this is real-world module usage -- in general I want to know that if ABA\to B is a map of rings then a BB-module "is" an AA-module. It does not sound to me like this is appropriate for type class inference. Is it? If I have to make the instances explicitly then is this an indication that modules shouldn't be typeclasses at all, or that some other sort of rethink is needed?

view this post on Zulip Mario Carneiro (Sep 15 2018 at 21:10):

I will not start on this until I've finished the current refactoring, but I think it is the right time to bring this up. I think that we should drop the out_param on the scalar field of a module. Downsides:

1. linear_map, submodule, module and other such types will require an explicit ring argument
2. a • x will not typecheck if the type of a is not specified
3. add_comm_group B cannot be a parent of module A B

I think (1) is mainly a problem for notation, i.e. something like M1 ->l M2 won't work since you have to shove R in the notation somewhere. (2) is possibly a problem if we are leaving off the type in pis or such but I can't see it having a big effect. (3) is the biggest problem, since it will add to the things you have to say about modules in proofs, but I'm already testing this change with the current refactoring. Upsides:

1. no more mysterious module typeclass timeout problems
2. no more questions about what to have implicit and what to have typeclass implicit
3. you can freely use modules over different rings, even in the same proof or statement
4. we can fill out the module typeclass hierarchy, rather than hiding some instances that have bad behavior like the endomorphism ring

I think that on the whole the benefits outweigh the downsides. The contract of an out_param is that you should only have one instance for module ? B for fixed B. This is just not true in advanced math. Indeed it's false even in the most trivial case, since you can always restrict the ring to a subring. @Johannes Hölzl @Kevin Buzzard Thoughts?

view this post on Zulip Kenny Lau (Sep 15 2018 at 21:16):

will it be finally possible to tell Lean that every abelian group is a Z-module? :D

view this post on Zulip Mario Carneiro (Sep 15 2018 at 21:17):

yes

view this post on Zulip Kenny Lau (Sep 15 2018 at 21:17):

yay

view this post on Zulip Mario Carneiro (Sep 15 2018 at 21:18):

it is very similar to the removal of out_param for ^

view this post on Zulip Mario Carneiro (Sep 15 2018 at 21:19):

now we can have has_pow instances for monoid, nat, group, int, and cardinal, cardinal all at the same time

view this post on Zulip Kevin Buzzard (Sep 15 2018 at 21:34):

I don't think I am competent enough to understand the ramifications of what you are suggesting, but I am all for changing things if you think it's a good idea, and will report back if I find any problems -- when things have settled down I will simply just go back to Hilbert and see what happens.

view this post on Zulip Kevin Buzzard (Sep 15 2018 at 21:35):

All I can say is that I have now seen with my own eyes that I want subsets of M to be either A-submodules or B-submodules and I am happy to say which.

view this post on Zulip Mario Carneiro (Sep 15 2018 at 21:36):

are you comfortable saying which in all circumstances, even when there is only one reasonable choice?

view this post on Zulip Kevin Buzzard (Sep 15 2018 at 21:40):

I am going to say yes I'm happy doing this. It doesn't feel unnatural to say "R-submodule" everywhere even if there is only one ring R -- after all, the axioms for a submodule really do depend on R.

view this post on Zulip Mario Carneiro (Sep 15 2018 at 21:41):

and now ideal actually has some work to do - ideal of R means R-submodule of R

view this post on Zulip Kevin Buzzard (Sep 15 2018 at 21:41):

Of course others might not be so happy but I think that even when I teach students about vector spaces over k I might even say "k-subspace" a lot.

view this post on Zulip Kevin Buzzard (Sep 15 2018 at 21:42):

Oh but actually this is now better, because for ideals I would get annoyed.

view this post on Zulip Kevin Buzzard (Sep 15 2018 at 21:42):

For ideals there's only one choice.

view this post on Zulip Mario Carneiro (Sep 15 2018 at 21:42):

Although subspace is still being useless

view this post on Zulip Kevin Buzzard (Sep 15 2018 at 21:43):

but that's Ok I think. I like the sound of this.

view this post on Zulip Johannes Hölzl (Sep 15 2018 at 22:21):

I don't understand why module A B cannot have add_comm_group as parent? What is the problem?
For me Point 3 (a type often has multiple different modules for different rings) is the main reason. I think everything else could be worked around eventually (maybe in Lean 4). And it looks we were already running into problems with the field instance for vector spaces. So I think this is a very good change!

view this post on Zulip Mario Carneiro (Sep 16 2018 at 04:33):

If module A B requires both A and B before being synthesized, as would happen if A was no longer marked an out_param, but it had a parent coercion to add_comm_group B, then you could not resolve a goal like has_zero B. It would climb the hierarchy to add_comm_group B, but then the parent coercion \all A B [ring A] [module A B], add_comm_group B would not be triggered since A is not yet known. Indeed this is a classic example of an unusable instance, since it has dependencies that don't appear in the target type.

view this post on Zulip Ali Sever (Sep 16 2018 at 08:36):

Is there a place where I can find all the classes (like linear_order or module)? I think my distances are a semi module, but I don't know where they are, and they might even be something stronger.

view this post on Zulip Kevin Buzzard (Sep 16 2018 at 08:38):

git grep says there are about 200 classes

view this post on Zulip Kevin Buzzard (Sep 16 2018 at 08:38):

but probably there's a bunch of false positives. What do you want to do with them now? Just look at them?

view this post on Zulip Ali Sever (Sep 16 2018 at 08:40):

I don't think I could sift through 200

view this post on Zulip Kevin Buzzard (Sep 16 2018 at 08:40):

If you're now assuming the parallel postulate then you can divide by a positive integer, so your distances are now probably a semi vector space over the semi field Q_{>=0}. But I am not sure that these concepts exist or are useful

view this post on Zulip Kevin Buzzard (Sep 16 2018 at 08:41):

Hmm, I guess Q\mathbb{Q} is a semi-module over Q+\mathbb{Q}^+ with no basis, so there will be no theorem of the form that every semimodule over Q+\mathbb{Q}^+ has a basis (in contrast to the theory of fields, where every vector space has a basi).

view this post on Zulip Ali Sever (Sep 16 2018 at 08:42):

I have a linear_order, with a 0. My angles have a maximum in addition to that, but I plan to turn them into mod 360 (or 2*pi).

view this post on Zulip Kevin Buzzard (Sep 16 2018 at 08:42):

Your angles currently are [0,180] basically, right? Or (0,180) or something.

view this post on Zulip Ali Sever (Sep 16 2018 at 08:43):

inclusive, but I don't need to make those at the moment. But I would like to have a linear order and a minimum (which is 0).

view this post on Zulip Kevin Buzzard (Sep 16 2018 at 08:45):

The point of this thread was for me to whinge about modules and ideals and things, but mathlib is currently undergoing a bit of a transition in the way it handles this stuff. So introducing semimodules into your work might mean that you have to rewrite later. As you might have seen from yesterday, there seems to be still some discussion about exactly how the semiring will be mentioned (or perhaps decisions have been made but not implemented yet).

view this post on Zulip Ali Sever (Sep 16 2018 at 08:46):

Ok, I guess I'll just have a linear_order, and a theorem that says everything is bigger than 0.

view this post on Zulip Kevin Buzzard (Sep 16 2018 at 08:47):

well you can certainly have a linear order. I don't think looking through all of Lean trying to spot classes is the way to see what's there. I think you should look through mathlib, spot a directory or a file which looks relevant to you like order/basic.lean and then take a look at the types and typeclasses being used in that file. Right click on something like preorder to find where it's defined (a preorder is another example of something which is used a lot in Lean but which is hardly ever defined or used in a maths UG degree, we see partial orders but this is even weaker) and then just poke around. I just tried this and ending up finding my way to core Lean's init/algebra/order.lean very quickly. I think doing stuff like this can be pretty instructive.

view this post on Zulip Kenny Lau (Nov 08 2018 at 09:02):

will it be finally possible to tell Lean that every abelian group is a Z-module? :D

@Mario Carneiro do you think we're ready to teach Lean this fact?


Last updated: May 12 2021 at 07:17 UTC