Zulip Chat Archive

Stream: new members

Topic: how to "access" the module instance on submodule quotient?


view this post on Zulip Sam Lichtenstein (May 27 2020 at 18:42):

Suppose I define the notion of the RR-torsion submodule of an RR-module MM (I couldn't find this in mathlib but maybe I missed it):

import linear_algebra.basic algebra.direct_sum tactic

open submodule

variables {R : Type*} {M : Type*}
variables [comm_ring R] [add_comm_group M] [module R M]

def tors : submodule R M :=
{ carrier := {v |  (r:R), r  v = 0},
  zero :=  by {simp at *},
  add := begin intros x y hx hy, simp only [set.mem_set_of_eq] at *,
               cases hx with rx hrx, cases hy with ry hry,
               use rx * ry, rw [smul_add _, mul_smul, mul_smul, smul_comm, hrx, hry],
               simp at * end,
  smul := begin intros r m h, simp only [set.mem_set_of_eq] at *,
                cases h with s hs, use s, rw [smul_comm, hs], simp at *
                end}

#check @tors R M _ _ _

I can also define the property of being RR-torsion free for RR-modules, i.e. no nonzero elements are annihilated by a non-zerodivisor:

def torsion_free {N: Type*}[add_comm_group N][module R N] :=
    (n : N), n  0   (r : R), ((s : R),  s   0  r * s  0)  r  n  0

(Probably there are less awkward ways to make the definition above, but that's not necessarily germane to my question here.)

My first question is how to state "the quotient of a module by its torsion submodule is torsion free"?

I tried torsion_free (submodule.quotient tors) and got an error: switched to simple application elaboration procedure because failed to use expected type to elaborate it, error message.

If I do @torsion_free _ _ (submodule.quotient tors) _ _, I get don't know how to synthesize placeholder errors, so my hypothesis is that I need to invoke some sort of incantation to tell Lean to use the "obvious" R-module structure on the quotient in question, which is defined in linear_algebra/basic.lean: line 897.

Part of the issue here may have to do with leaning on type inference (or is the right thing to say "elaboration"?) unnecessarily, when I could be explicit instead?

I tried to make an alternate definition of tors with the dependence on M (and/or R) made explicit via () instead of the implicit variable {M : Type*}:

def tors' {S : Type*}[comm_ring S]
    (N : Type*)[add_comm_group N][module S N] : submodule S N := sorry

But when I tried to construct the submodule structure, it seemed to go horribly wrong, e.g. zero := by {simp at *} no longer worked.

Can anyone shed light on my confusion here? What is the "right" way to define tors? Thanks!

view this post on Zulip Johan Commelin (May 27 2020 at 18:43):

I don't think we have anything on torsion.

view this post on Zulip Johan Commelin (May 27 2020 at 18:43):

You want r ≠ 0 in your definition.

view this post on Zulip Johan Commelin (May 27 2020 at 18:44):

@Sam Lichtenstein Note that with rcases you can merge the intros and cases lines, if you want.

view this post on Zulip Sam Lichtenstein (May 27 2020 at 18:44):

sorry, I fixed the part that supposedly asserted r was a nonzerodivisor, so it now implies r != 0

view this post on Zulip Sam Lichtenstein (May 27 2020 at 18:45):

oh whoops, you mean in the carrier
yeah that's a mistake

view this post on Zulip Johan Commelin (May 27 2020 at 18:46):

@Sam Lichtenstein Change {R} and {M} to (R) and (M) in your variables

view this post on Zulip Johan Commelin (May 27 2020 at 18:46):

That will hopefully fix most of your errors

view this post on Zulip Johan Commelin (May 27 2020 at 18:47):

If you write {R}, you're telling Lean: "Hey, figure out this argument by yourself"

view this post on Zulip Sam Lichtenstein (May 27 2020 at 18:47):

But this does seem like a case where Lean should be able to figure stuff out for itself?

view this post on Zulip Johan Commelin (May 27 2020 at 18:47):

With (R), you say: "I'll supply this argument, everytime I use this def/lemma"

view this post on Zulip Johan Commelin (May 27 2020 at 18:47):

tors can't figure out M

view this post on Zulip Johan Commelin (May 27 2020 at 18:47):

You certainly want tors M.

view this post on Zulip Sam Lichtenstein (May 27 2020 at 18:48):

If I declare (M) in variables at the top, do I need to make the R-module instance on M explicit in the "hypotheses" of the tors definition?

view this post on Zulip Johan Commelin (May 27 2020 at 18:48):

But then Lean will still complain, and say: look M is supposed to be a module, but over which ring? It's a module over Z, but maybe you want another ring?

view this post on Zulip Johan Commelin (May 27 2020 at 18:48):

No, the module instance is fine.

view this post on Zulip Sam Lichtenstein (May 27 2020 at 18:48):

Because [module R M] is in the variables at the top?

view this post on Zulip Johan Commelin (May 27 2020 at 18:49):

In usual maths, if you are pedantic, you would write TorsR(M)\mathrm{Tors}_R(M), with both R and M explicit

view this post on Zulip Johan Commelin (May 27 2020 at 18:49):

Lean wants you to always be pedantic.

view this post on Zulip Johan Commelin (May 27 2020 at 18:50):

The rest of the variables are fine. [comm_ring R] means: Hey Lean, I'll tell you about R, which is a random type. I expect you to figure out a ring structure on R.

view this post on Zulip Sam Lichtenstein (May 27 2020 at 18:50):

So you're suggesting the following should work (modulo the r!=0 issue in the carrier)?

variables (R : Type*) (M : Type*)
variables [comm_ring R] [add_comm_group M] [module R M]

def tors (R) (M) : submodule R M :=
{ carrier := {v |  (r:R), r  v = 0},
  zero :=  by {simp at *},
  add := begin intros x y hx hy, simp only [set.mem_set_of_eq] at *,
               cases hx with rx hrx, cases hy with ry hry,
               use rx * ry, rw [smul_add _, mul_smul, mul_smul, smul_comm, hrx, hry],
               simp at * end,
  smul := begin intros r m h, simp only [set.mem_set_of_eq] at *,
                cases h with s hs, use s, rw [smul_comm, hs], simp at *
                end}

view this post on Zulip Johan Commelin (May 27 2020 at 18:50):

I think that doesn't compile?

view this post on Zulip Johan Commelin (May 27 2020 at 18:50):

You can leave out the (R) and (M) from the def of tors

view this post on Zulip Johan Commelin (May 27 2020 at 18:51):

I meant that you should just change the parens in the variables line.

view this post on Zulip Sam Lichtenstein (May 27 2020 at 18:52):

OK thanks, I have to take care of something else, but I will try again later this afternoon

view this post on Zulip Sam Lichtenstein (May 27 2020 at 23:32):

Alright, I have distilled my next question down the following:

1) What on earth is going on in this proof?

import linear_algebra.basic tactic

variables {R : Type*} {M : Type*}
variables [comm_ring R] [add_comm_group M] [module R M]

open submodule

lemma lem (p : submodule R M) (x : submodule.quotient p) :
        x = 0   (m : M), m  p  quotient.mk' m = x  :=
begin
split, intro h, simp only [quotient.mk'_eq_mk] at *, induction x,
finish, tauto, intro h, cases h with m hm, cases hm with hm₁ hm₂,
simp only [quotient.mk'_eq_mk] at *, rw  hm₂, induction hm₂, finish,
end

2) What's wrong with the superficially similar (mk instead of mk') variant, which raises errors synthesized type class instance is not definitionally equal to expression inferred by typing rules, ...:

lemma lem (p : submodule R M) (x : submodule.quotient p) :
        x = 0   (m : M), m  p  quotient.mk m = x  := sorry -- the lemma's statement doesn't work

3) Shouldn't there be some version of this lemma whose proof is "by {tauto}", or at least "by {simp at *}"?

4) Apparently it is a Bad Idea to try to work with quotient representatives using @quotient.exists_rep _ (submodule.quotient_rel p), because this gives things of the form quot.mk setoid.r m, which seem surprisingly difficult to turn into things of the form quotient.mk m, despite the theorem quotient.quot_mk_eq_mk. But what is the "right" way to work with lifts of elements of quotients?

(I suppose a possible answer to #4 is "don't" -- instead try to formulate results using the universal property of the quotient in question. At least in the context of showing that M/MtorsM/M^{tors} is torsion-free, this didn't seem like a natural approach to me, but I suppose YMMV.)

view this post on Zulip Kevin Buzzard (May 27 2020 at 23:35):

What do you even mean by Q1?

lemma lem (p : submodule R M) (x : submodule.quotient p) :
        x = 0   (m : M), m  p  quotient.mk' m = x  :=
begin
  split,
  { intro h,
    --simp only [quotient.mk'_eq_mk] at *, -- doesn't do anything
    induction x,
    finish,
    tauto},
  { --intro h,
    --cases h with m hm,
    --cases hm with hm₁ hm₂,
    rintro m, hm₁, hm₂, -- the same
    simp only [quotient.mk'_eq_mk] at *,
    rw  hm₂,
    induction hm₂,
    finish},
end

view this post on Zulip Sam Lichtenstein (May 27 2020 at 23:37):

Well, I agree that I could have organized that proof better. But I found it by more or less blindly following suggestions from hint. I guess what I'm wondering is where do I learn about the yoga of mk vs mk' and all that, and I suppose how I should think of quotients as inductive types. Is this explained clearly somewhere?

view this post on Zulip Kevin Buzzard (May 27 2020 at 23:37):

Q2: quotient.mk works when the equivalence relation on M is known to the type class inference system. It's a long story.

view this post on Zulip Kevin Buzzard (May 27 2020 at 23:39):

There are three kinds of brackets for function inputs in Lean. The () ones are inputs which the user supplies. The {} ones are ones which a C++ algorithm called Lean's unification system supplies. The [] ones are ones which a different C++ algorithm called Lean's type class system supplies.

view this post on Zulip Sam Lichtenstein (May 27 2020 at 23:39):

Put differently, what is going on in the finishes after induction xyz?

view this post on Zulip Sam Lichtenstein (May 27 2020 at 23:40):

Yes, I am feeling a bit better about the various types of brackets now. I've moved on to being confused about quotients.

view this post on Zulip Kevin Buzzard (May 27 2020 at 23:41):

It took me a long time to get the hang of the [] system. The way it works is that the user puts things into the [] system (e.g. you put into the system the fact that R is a commutative ring) and then the system does magic behind the scenes, e.g. if you write r + s with r : R and s : R then the typeclass system will magic up + from the fact that it knows R is a ring and that rings have addition

view this post on Zulip Kevin Buzzard (May 27 2020 at 23:41):

But you didn't put the equivalence relation defining R/M into the typeclass system, so quotient.mk, which runs on [], can't get it out.

view this post on Zulip Sam Lichtenstein (May 27 2020 at 23:41):

Oh I see -- you're saying that in general I'm probably always going to want mk' because typically when working with many inferred things floating around, the type class inference system won't be able to handle mk?

view this post on Zulip Kevin Buzzard (May 27 2020 at 23:42):

The type class system can "handle" a quotient if and only if you've told it about the quotient, and if you're dealing with quotient modules then the unification system can handle it fine.

view this post on Zulip Sam Lichtenstein (May 27 2020 at 23:43):

OK that's helpful.

view this post on Zulip Sam Lichtenstein (May 27 2020 at 23:43):

thank you

view this post on Zulip Kevin Buzzard (May 27 2020 at 23:43):

quotients aren't inductive types, they're quotient types. There are inductive types (structures), pi types (functions), quotient types, and that's it.

view this post on Zulip Kevin Buzzard (May 27 2020 at 23:44):

After induction x, the goal which finish is closing is ⊢ ∃ (m : M), m ∈ p ∧ quotient.mk' m = quot.mk setoid.r x

view this post on Zulip Sam Lichtenstein (May 27 2020 at 23:46):

So a natural question (logically prior to my previous question about the finishes after induction x) is what induction x means when x : X for a quotient (rather than inductive) type X. Which I suppose I will now try to look up.

view this post on Zulip Kevin Buzzard (May 27 2020 at 23:46):

The local context in full is this:

p : submodule R M,
x : M,
h : quot.mk setoid.r x = 0
  (m : M), m  p  quotient.mk' m = quot.mk setoid.r x

so pp is a submodule of MM, xMx\in M, x=0\overline{x} = 0 in M/pM/p and the goal is to find some mpm\in p such that m=x\overline{m}=\overline{x}.

view this post on Zulip Kevin Buzzard (May 27 2020 at 23:47):

induction x uses the universal property of the quotient

view this post on Zulip Sam Lichtenstein (May 27 2020 at 23:47):

ah ok

view this post on Zulip Kevin Buzzard (May 27 2020 at 23:47):

well, it's a rather silly universal property here

view this post on Zulip Kevin Buzzard (May 27 2020 at 23:48):

It might have been clearer to write induction x with xtilde

view this post on Zulip Sam Lichtenstein (May 27 2020 at 23:48):

ok so going back to unpacking finish, the first step is clearly use x

view this post on Zulip Kevin Buzzard (May 27 2020 at 23:48):

and what is happening at that point is that Lean replaces all occurences of xM/px\in M/p with x~\overline{\tilde{x}} where x~M\tilde{x}\in M reduces to xx

view this post on Zulip Sam Lichtenstein (May 27 2020 at 23:49):

which gets us to :

p : submodule R M,
x : M,
h : quot.mk setoid.r x = 0
 x  p  quotient.mk x = quot.mk setoid.r x

view this post on Zulip Kevin Buzzard (May 27 2020 at 23:49):

I think you're going round in circles if you use xx

view this post on Zulip Kevin Buzzard (May 27 2020 at 23:50):

I would rather use 00

view this post on Zulip Sam Lichtenstein (May 27 2020 at 23:50):

aha!

view this post on Zulip Kevin Buzzard (May 27 2020 at 23:50):

I have no idea what finish used -- of course x~\tilde{x} would also work

view this post on Zulip Sam Lichtenstein (May 27 2020 at 23:52):

So after induction x, use 0, split, simp only [zero_mem], rw h, rw quotient.mk_zero I am left with a mysterious tautology:

p : submodule R M,
x_a x_b : M,
p : setoid.r x_a x_b
 _ = _

view this post on Zulip Sam Lichtenstein (May 27 2020 at 23:53):

I don't find this too troubling, but it seems a bit odd?

view this post on Zulip Mario Carneiro (May 27 2020 at 23:55):

I think the easiest way to prove this is to use submodule.mk_eq_zero

view this post on Zulip Mario Carneiro (May 27 2020 at 23:56):

that's probably an equality of proofs (you can turn on proof printing with set_option pp.proofs true) and so refl will close it

view this post on Zulip Mario Carneiro (May 27 2020 at 23:57):

It probably appeared because you applied things in a weird order and something was a metavariable when the subgoal would have normally been discharged

view this post on Zulip Kevin Buzzard (May 27 2020 at 23:59):

lemma lem (p : submodule R M) (x : submodule.quotient p) :
        x = 0   (m : M), m  p  quotient.mk' m = x  :=
begin
  split,
  { rintro rfl,
    use 0, simp,
  },
  { rintro m, hm₁, hm₂,
    rw [quotient.mk_eq_zero, quotient.mk'_eq_mk] at hm₁,
    cc
  }
end

view this post on Zulip Kevin Buzzard (May 28 2020 at 00:00):

Quotients are difficult to steer in general. You need to understand the API properly before you can use them effectively. I'm not really sure I understand the API properly, in some sense.

view this post on Zulip Sam Lichtenstein (May 28 2020 at 00:01):

LOL I am not sure whether to be comforted by that or not.

view this post on Zulip Kevin Buzzard (May 28 2020 at 00:02):

The main thing to learn is that quotient.lift is about descending, not lifting.

view this post on Zulip Kevin Buzzard (May 28 2020 at 00:02):

(in the sense that mathematicians would use the word)

view this post on Zulip Sam Lichtenstein (May 28 2020 at 00:02):

right, I did figure out it wasn't what I initial thought

view this post on Zulip Kevin Buzzard (May 28 2020 at 00:03):

The whole mk_eq_mk' thing is a shame, it makes things much messier

view this post on Zulip Mario Carneiro (May 28 2020 at 00:04):

lemma lem (p : submodule R M) (x : submodule.quotient p) :
        x = 0   (m : M), m  p  quotient.mk' m = x  :=
begin
  refine quotient.induction_on' x (λ m, _),
  change (quotient.mk':M  quotient p) with submodule.quotient.mk,
  split,
  { rw [quotient.mk_eq_zero],
    intro h, exact ⟨_, h, rfl },
  { rintro m', hm', e,
    rwa [ e, quotient.mk_eq_zero] }
end

view this post on Zulip Kevin Buzzard (May 28 2020 at 00:05):

Mario is using the quotient interface correctly. It always takes me forever to find that first line

view this post on Zulip Mario Carneiro (May 28 2020 at 00:05):

I think there is a missing theorem for induction_on for submodule.quotient, which would allow you to skip the change line

view this post on Zulip Mario Carneiro (May 28 2020 at 00:06):

I'm using the induction_on for quotient', which is okay but gives you the wrong mk

view this post on Zulip Kevin Buzzard (May 28 2020 at 00:07):

I wrote something about how to make Z/37Z\mathbb{Z}/37\mathbb{Z} in Lean once, maybe I should re-read it.

view this post on Zulip Mario Carneiro (May 28 2020 at 00:07):

If you use induction x, I think it will use quotient.induction_on, which gives you yet another version of mk that you would have to rewrite away more painfully

view this post on Zulip Kevin Buzzard (May 28 2020 at 00:09):

The line local attribute [instance] Zmod37.setoid is inserting it as an instance into the typeclass system, so I can use the unprimed versions of everything all the way through

view this post on Zulip Mario Carneiro (May 28 2020 at 00:09):

lemma lem (p : submodule R M) (x : submodule.quotient p) :
        x = 0   (m : M), m  p  quotient.mk' m = x  :=
begin
  induction x,
  { change (quot.mk (@setoid.r _ (quotient_rel _)):M  quotient p) with submodule.quotient.mk,
    change (quotient.mk':M  quotient p) with submodule.quotient.mk,
    split,
    { rw [quotient.mk_eq_zero],
      intro h, exact ⟨_, h, rfl },
    { rintro m', hm', e,
      rwa [ e, quotient.mk_eq_zero] } },
  refl
end

view this post on Zulip Kevin Buzzard (May 28 2020 at 00:10):

My Mario expansion factor used to be something like 10, it's comforting to see him coming up with proofs which are the same size as mine occasionally

view this post on Zulip Mario Carneiro (May 28 2020 at 00:12):

the final refl, discharging that funny _ = _ goal, is apparently tossed up by induction x. I think it is using the dependent recursor for the quotient, which is basically a combination of quotient.induction_on and quotient.lift, and so has a side goal saying that the function that you constructed in the first part doesn't depend on the representative of the equivalence class. For proofs this is always trivial, which is why induction_on exists in the first place

view this post on Zulip Mario Carneiro (May 28 2020 at 00:13):

If you #print lem, you will see that the first theorem it uses is indeed quot.rec, which looks like this:

set_option pp.proofs true
#print quot.rec
@[elab_as_eliminator, elab_strategy, reducible]
protected def quot.rec : Π {α : Sort u} {r : α  α  Prop} {β : quot r  Sort v} (f : Π (a : α), β (quot.mk r a)),
  ( (a b : α) (p : r a b), eq.rec (f a) (quot.sound p) = f b)  Π (q : quot r), β q := ...

view this post on Zulip Mario Carneiro (May 28 2020 at 00:21):

Kevin Buzzard said:

My Mario expansion factor used to be something like 10, it's comforting to see him coming up with proofs which are the same size as mine occasionally

Challenge accepted:

lemma lem (p : submodule R M) (x : submodule.quotient p) :
        x = 0   (m : M), m  p  quotient.mk' m = x  :=
⟨λ h, ⟨_, zero_mem _, h.symm, by rintro m, h, rfl⟩; exact (quotient.mk_eq_zero p).2 h

view this post on Zulip Johan Commelin (May 28 2020 at 05:44):

I think the takeaway is that we just need to flesh out the api of quotient modules/rings/groups a bit more... currently they are written with a POV that you should fall back to the underlying quotient API, but I think that is quite confusing.


Last updated: May 14 2021 at 11:10 UTC