## Stream: new members

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

#### Sam Lichtenstein (May 27 2020 at 18:42):

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 (May 27 2020 at 18:43):

I don't think we have anything on torsion.

#### Johan Commelin (May 27 2020 at 18:43):

You want r ≠ 0 in your definition.

#### 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.

#### 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

#### Sam Lichtenstein (May 27 2020 at 18:45):

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

#### Johan Commelin (May 27 2020 at 18:46):

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

#### Johan Commelin (May 27 2020 at 18:46):

That will hopefully fix most of your errors

#### Johan Commelin (May 27 2020 at 18:47):

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

#### 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?

#### Johan Commelin (May 27 2020 at 18:47):

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

#### Johan Commelin (May 27 2020 at 18:47):

tors can't figure out M

#### Johan Commelin (May 27 2020 at 18:47):

You certainly want tors M.

#### 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?

#### 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?

#### Johan Commelin (May 27 2020 at 18:48):

No, the module instance is fine.

#### Sam Lichtenstein (May 27 2020 at 18:48):

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

#### Johan Commelin (May 27 2020 at 18:49):

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

#### Johan Commelin (May 27 2020 at 18:49):

Lean wants you to always be pedantic.

#### 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.

#### 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}


#### Johan Commelin (May 27 2020 at 18:50):

I think that doesn't compile?

#### Johan Commelin (May 27 2020 at 18:50):

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

#### Johan Commelin (May 27 2020 at 18:51):

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

#### 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

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

#### 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


#### 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?

#### 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.

#### 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.

#### Sam Lichtenstein (May 27 2020 at 23:39):

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

#### 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.

#### 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

#### 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.

#### 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?

#### 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.

thank you

#### 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.

#### 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

#### 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.

#### 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 $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 (May 27 2020 at 23:47):

induction x uses the universal property of the quotient

ah ok

#### Kevin Buzzard (May 27 2020 at 23:47):

well, it's a rather silly universal property here

#### Kevin Buzzard (May 27 2020 at 23:48):

It might have been clearer to write induction x with xtilde

#### Sam Lichtenstein (May 27 2020 at 23:48):

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

#### Kevin Buzzard (May 27 2020 at 23:48):

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


#### Kevin Buzzard (May 27 2020 at 23:49):

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

#### Kevin Buzzard (May 27 2020 at 23:50):

I would rather use $0$

aha!

#### Kevin Buzzard (May 27 2020 at 23:50):

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

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


#### Sam Lichtenstein (May 27 2020 at 23:53):

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

#### Mario Carneiro (May 27 2020 at 23:55):

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

#### 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

#### 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

#### 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


#### 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.

#### Sam Lichtenstein (May 28 2020 at 00:01):

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

#### Kevin Buzzard (May 28 2020 at 00:02):

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

#### Kevin Buzzard (May 28 2020 at 00:02):

(in the sense that mathematicians would use the word)

#### Sam Lichtenstein (May 28 2020 at 00:02):

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

#### Kevin Buzzard (May 28 2020 at 00:03):

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

#### 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


#### 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

#### 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

#### 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

#### Kevin Buzzard (May 28 2020 at 00:07):

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

#### 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

#### 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

#### 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


#### 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

#### 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

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


#### 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⟩


#### 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