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

Stream: new members

[Sam Lichtenstein]

Suppose I define the notion of the $R$-torsion submodule of an $R$-module $M$ (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 $R$-torsion free for $R$-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!

[Johan Commelin]

I don't think we have anything on torsion.

[Johan Commelin]

You want r ≠ 0 in your definition.

[Johan Commelin]

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

[Sam Lichtenstein]

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

[Sam Lichtenstein]

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

[Johan Commelin]

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

[Johan Commelin]

That will hopefully fix most of your errors

[Johan Commelin]

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

[Sam Lichtenstein]

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

[Johan Commelin]

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

[Johan Commelin]

tors can't figure out M

[Johan Commelin]

You certainly want tors M.

[Sam Lichtenstein]

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?

[Johan Commelin]

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?

[Johan Commelin]

No, the module instance is fine.

[Sam Lichtenstein]

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

[Johan Commelin]

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

[Johan Commelin]

Lean wants you to always be pedantic.

[Johan Commelin]

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.

[Sam Lichtenstein]

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}

[Johan Commelin]

I think that doesn't compile?

[Johan Commelin]

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

[Johan Commelin]

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

[Sam Lichtenstein]

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

[Sam Lichtenstein]

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/M^{tors}$ is torsion-free, this didn't seem like a natural approach to me, but I suppose YMMV.)

[Kevin Buzzard]

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

[Sam Lichtenstein]

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?

[Kevin Buzzard]

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

[Kevin Buzzard]

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.

[Sam Lichtenstein]

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

[Sam Lichtenstein]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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.

[Sam Lichtenstein]

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?

[Kevin Buzzard]

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.

[Sam Lichtenstein]

OK that's helpful.

[Sam Lichtenstein]

thank you

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Sam Lichtenstein]

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.

[Kevin Buzzard]

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 $p$ is a submodule of $M$, $x\in M$, $\overline{x} = 0$ in $M/p$ and the goal is to find some $m\in p$ such that $\overline{m}=\overline{x}$.

[Kevin Buzzard]

induction x uses the universal property of the quotient

[Sam Lichtenstein]

ah ok

[Kevin Buzzard]

well, it's a rather silly universal property here

[Kevin Buzzard]

It might have been clearer to write induction x with xtilde

[Sam Lichtenstein]

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

[Kevin Buzzard]

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

[Sam Lichtenstein]

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

[Kevin Buzzard]

I think you're going round in circles if you use $x$

[Kevin Buzzard]

I would rather use $0$

[Sam Lichtenstein]

aha!

[Kevin Buzzard]

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

[Sam Lichtenstein]

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
⊢ _ = _

[Sam Lichtenstein]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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.

[Sam Lichtenstein]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

(in the sense that mathematicians would use the word)

[Sam Lichtenstein]

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

[Kevin Buzzard]

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

[Mario Carneiro]

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

[Kevin Buzzard]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Kevin Buzzard]

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

[Mario Carneiro]

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

[Kevin Buzzard]

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

[Mario Carneiro]

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

[Kevin Buzzard]

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

[Mario Carneiro]

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

[Mario Carneiro]

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 := ...

[Mario Carneiro]

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⟩

[Johan Commelin]

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.