## Stream: general

### Topic: quotients

#### Patrick Massot (Jul 15 2018 at 10:50):

I still don't know much about quotients in Lean. I have the goal {x : completion α × completion α | (g x.1, g x.2) ∈ r} ∈ uniformity.sets. And completion α is the quotient of something, and g is induced by h defined before quotienting. So I'd like to rewrite the left hand side as the image under lam y, (quotient.mk y.1, quotient.mk y.2) of the obvious set where (g x.1, g x.2) becomes (h y.1, h y.2). How can I do that? Should I do that?

#### Chris Hughes (Jul 15 2018 at 11:37):

I proved it, but it's not pretty. I think there's a demand for more advanced versions of cases which can deal with quotients, bound variables, and things like turning f : α → β × β to f₁ f₂ : α → β.

import data.set.basic
variables {α : Type*} {β : Type*} [s : setoid α] (g : quotient s → β) (r : set (β × β))

example (h : α → β) (Hh : h = g ∘ quotient.mk) :
{x : quotient s × quotient s | (g x.1, g x.2) ∈ r} =
(λ a : α × α, (⟦a.1⟧, ⟦a.2⟧)) '' ((λ a : α × α, (h a.1, h a.2)) ⁻¹' r) :=
Hh.symm ▸
set.ext (λ ⟨a₁, a₂⟩, ⟨quotient.induction_on₂ a₁ a₂
(λ a₁ a₂ h, ⟨(a₁, a₂), h, rfl⟩),
λ ⟨⟨b₁, b₂⟩, h₁, h₂⟩, show (g a₁, g a₂) ∈ r, from
have h₃ : ⟦b₁⟧ = a₁ ∧ ⟦b₂⟧ = a₂ := prod.ext_iff.1 h₂,
h₃.1 ▸ h₃.2 ▸ h₁⟩)


#### Mario Carneiro (Jul 15 2018 at 11:39):

induction for quotients is a feature I want in lean 4

#### Chris Hughes (Jul 15 2018 at 11:39):

There's no reason why it can't be done in lean 3 is there?

#### Mario Carneiro (Jul 15 2018 at 11:40):

I'm not sure how replicable induction is

Is it C++?

mostly

#### Chris Hughes (Jul 15 2018 at 11:40):

Isn't it just basically revert, refine quotient.induction_on _ _, intros

#### Chris Hughes (Jul 15 2018 at 11:42):

meta def qindunction (p : parse texpr) (n : parse types.using_ident) : tactic unit :=
do e ← to_expr p,
revert_kdependencies e,
refine (quotient.induction_on %%e _),
intro n,
[intros]


#### Kevin Buzzard (Jul 15 2018 at 11:42):

Here's a really dumb question about quotients. It seems to me that instead of using the quotient type one could just use an inductive type: the quotient of X by r could be {x : set X // I am an equivalence class} and the facts about quotients that don't come for free in type theory could be added as axioms about this subtype. Why is it not done this way?

#### Kevin Buzzard (Jul 15 2018 at 11:42):

Then quotients would be easier to think about

#### Mario Carneiro (Jul 15 2018 at 11:42):

Sure, you can do that

#### Chris Hughes (Jul 15 2018 at 11:42):

Computablity perhaps?

#### Mario Carneiro (Jul 15 2018 at 11:42):

some facts need the axiom of choice

#### Mario Carneiro (Jul 15 2018 at 11:42):

and it's not data when you do that

#### Chris Hughes (Jul 15 2018 at 11:43):

It's very nice to have the definitional reduction of quotient.lift

#### Mario Carneiro (Jul 15 2018 at 11:43):

You can't get that with any construction

#### Mario Carneiro (Jul 15 2018 at 11:44):

and that adds real power - funext is proven using quotients

#### Patrick Massot (Jul 15 2018 at 11:44):

Thank you very much Chris!

#### Patrick Massot (Jul 15 2018 at 11:44):

I hope I'll be able to use that.

#### Mario Carneiro (Jul 15 2018 at 11:45):

In fact, I highly recommend reading the proof of funext. It's quite the mind bender

#### Patrick Massot (Jul 15 2018 at 11:45):

This is explained in TPIL

#### Mario Carneiro (Jul 15 2018 at 11:45):

It's really not obvious why you can't use set-quotients to do the same proof

#### Kevin Buzzard (Jul 15 2018 at 11:45):

oh my goodness Chris is posting meta code. How things move on! Two weeks ago he was asking me what a monad was.

#### Patrick Massot (Jul 15 2018 at 11:46):

Kevin, I don't understand why you'd want this set-theoretic construction. I actually spend quite a lot of time explaining to my students that this construction is a lie. What matter about quotients are the axioms enforced in Lean.

#### Patrick Massot (Jul 15 2018 at 11:47):

To me the set theoretic quotient is the same level of lie as the Kuratowski pair definition

#### Mario Carneiro (Jul 15 2018 at 11:47):

But an obvious question with that is why quotients and not other things?

#### Kevin Buzzard (Jul 15 2018 at 11:48):

Oh that's an interesting comment Patrick. The truth of the matter was that I was watching a school play with one of my kids in, which turned out to be over three hours long, and so I spent most of the last 90 minutes thinking about other ways of doing quotients in my head in the dark

#### Patrick Massot (Jul 15 2018 at 11:49):

Mario, I'm not sure what is "that" in your latest message

#### Mario Carneiro (Jul 15 2018 at 11:49):

Why do quotients get an axiomatic definition but, say, real numbers don't?

#### Mario Carneiro (Jul 15 2018 at 11:50):

is there a sense in which lean's type formers are "complete" with quotients but not without?

#### Patrick Massot (Jul 15 2018 at 11:51):

I think most people in France teach the set-theoretic quotient and never explicitly say it's a lie. Students are expected to magically understand what really matters

#### Kevin Buzzard (Jul 15 2018 at 11:51):

In fact, I highly recommend reading the proof of funext. It's quite the mind bender

Funnily enough I tried this only recently, when I realised that I was going to have to learn how to use quotients.

I have been writing about "the three basic kinds of types", trying to explain them to mathematicians. All this came from my trying to figure out why there were three basic kinds of types at all -- inductive types and pi types sure, and now quotients -- why can't we just do them with inductive types? In some sense Patrick's comments are quite a good answer to this -- I am now thinking that the construction I've known all my working life is just a hack.

#### Mario Carneiro (Jul 15 2018 at 11:51):

That's actually a good question - why are quotients not an inductive type?

#### Patrick Massot (Jul 15 2018 at 11:52):

and I think almost no university seriously teaches the construction of real numbers

#### Kevin Buzzard (Jul 15 2018 at 11:52):

Quotients as sets of sets is the ZFC construction of the object which has the right universal property.

#### Mario Carneiro (Jul 15 2018 at 11:52):

HoTT has an interesting answer to this: they are a "higher inductive type"

#### Mario Carneiro (Jul 15 2018 at 11:52):

The point is that in type theory, set-quotients do not have the right universal property

?

#### Mario Carneiro (Jul 15 2018 at 11:53):

They lack the computation rule

#### Kevin Buzzard (Jul 15 2018 at 11:53):

which one is that?

#### Mario Carneiro (Jul 15 2018 at 11:53):

lift f (mk a) = f a

#### Chris Hughes (Jul 15 2018 at 11:54):

It is true, but not rfl

"lack" :-)

#### Mario Carneiro (Jul 15 2018 at 11:54):

because in type theory definitional equality matters

Yes!

#### Kevin Buzzard (Jul 15 2018 at 11:55):

I understand this much better than I did a few months ago. Perhaps this is obvious to CS people. I think it really needs to be spelt out to mathematicians.

#### Mario Carneiro (Jul 15 2018 at 11:55):

HoTT is of course all about exploring the nontrivial structure of equality, where definitional equality is the equalest equal

#### Kevin Buzzard (Jul 15 2018 at 11:56):

All equalities are equal, but some are more equal than others.

#### Patrick Massot (Jul 15 2018 at 11:56):

Kevin, did you read the first chapter of the HoTT book?

no

You should

#### Mario Carneiro (Jul 15 2018 at 11:56):

It's a really good intro to dependent type theory

#### Kevin Buzzard (Jul 15 2018 at 11:57):

Thanks. I'm always looking for new things to read, even though reading is so 1990s

#### Mario Carneiro (Jul 15 2018 at 11:57):

Also you will find some decent material on HITs there

#### Patrick Massot (Jul 15 2018 at 11:57):

http://saunders.phil.cmu.edu/book/hott-online.pdf

#### Mario Carneiro (Jul 15 2018 at 11:57):

HoTT has some much more exotic HITs than quotients

#### Mario Carneiro (Jul 15 2018 at 11:58):

like "the circle" S1, which is "inductively generated" by base : S1 and loop : base = base

#### Mario Carneiro (Jul 15 2018 at 11:58):

In HoTT you can prove that loop is not rfl

#### Kevin Buzzard (Jul 15 2018 at 11:59):

In HoTT can you define the notion of a finite set? Can you use the axiom of choice?

#### Mario Carneiro (Jul 15 2018 at 12:00):

You can do pretty much everything in classical math

#### Mario Carneiro (Jul 15 2018 at 12:01):

You have to state the axiom of choice carefully to be consistent with univalence (lean's choice is not consistent with univalence), but it is a reasonable interpretation of ZFC-esque axiom of choice

#### Mario Carneiro (Jul 15 2018 at 12:01):

it's not provable though, it's an axiom

#### Mario Carneiro (Jul 15 2018 at 12:02):

there are more details in the HoTT book for how the axiom of choice works

#### Mario Carneiro (Jul 15 2018 at 12:03):

it uses the "propositional truncation" as a substitute for the Prop universe

#### Patrick Massot (Jul 15 2018 at 12:03):

I was not referring to all this. I really mean Chapter one, about type theory, only slightly biased towards exotic stuff that will follow

#### Mario Carneiro (Jul 15 2018 at 12:04):

Yes, of course that's more advanced material and more HoTT-y stuff

#### Kevin Buzzard (Jul 15 2018 at 12:04):

I know you weren't Patrick, but I mentioned to my old university set theory teacher that I was now doing type theory and he asked me if it was HoTT and if so then could I define a finite set (because he'd heard that it was problematic)

#### Kevin Buzzard (Jul 15 2018 at 12:04):

and I told him that it wasn't and that I had no idea about his question

#### Mario Carneiro (Jul 15 2018 at 12:06):

If you are specifically interested in finite sets in HoTT, I've had a conversation with Floris on that exact topic (he's our resident expert)

#### Mario Carneiro (Jul 15 2018 at 12:06):

Constructively, there are a few variations on what "finite" means

#### Mario Carneiro (Jul 15 2018 at 12:06):

The simplest is something isomorphic to fin n

#### Mario Carneiro (Jul 15 2018 at 12:07):

If we call that one "finite", then "subfinite" means a subset of a finite set

#### Kevin Buzzard (Jul 15 2018 at 12:07):

and equality is undecidable...

#### Mario Carneiro (Jul 15 2018 at 12:08):

and then there is an image of a finite set (I forget what this is called), and a subset of an image of a finite set

#### Kevin Buzzard (Jul 15 2018 at 12:08):

If I assume AC and propext then all these are the same, right?

#### Patrick Massot (Jul 15 2018 at 12:09):

Forget about HoTT Kevin, it's all constructive

#### Patrick Massot (Jul 15 2018 at 12:09):

We have maths to do instead

#### Mario Carneiro (Jul 15 2018 at 12:09):

With LEM, you know that the subset is decidable so subfinite and finite are the same

#### Mario Carneiro (Jul 15 2018 at 12:10):

for images, I guess you can get a section out using AC so that becomes the same as finite too

#### Mario Carneiro (Jul 15 2018 at 12:10):

I don't think you need propext for anything

#### Mario Carneiro (Jul 15 2018 at 12:11):

Actually unique choice might be enough for the section thing, since it's a finite choice

#### Mario Carneiro (Jul 15 2018 at 12:11):

Oh yeah, there's another gradation: "isomorphic to fin n" or "merely isomorphic to fin n"

#### Mario Carneiro (Jul 15 2018 at 12:12):

where "merely" is a HoTT adjective meaning "in Prop" basically

#### Mario Carneiro (Jul 15 2018 at 12:12):

that's like the difference between "fintype" and "finite" in lean

#### Kevin Buzzard (Jul 15 2018 at 12:22):

You can do pretty much everything in classical math

Forget about HoTT Kevin, it's all constructive

?

#### Mario Carneiro (Jul 15 2018 at 12:24):

It's very constructivity-aware, even if there are some classical axioms that are admissible

#### Mario Carneiro (Jul 15 2018 at 12:25):

Lean's choice axiom is much more heavy handed

#### Mario Carneiro (Jul 15 2018 at 12:25):

It's comparable to the status of equality reflection as a type theory axiom

#### Mario Carneiro (Jul 15 2018 at 12:26):

lean doesn't have it, and as a result you have to do all these casts and things

#### Mario Carneiro (Jul 15 2018 at 12:26):

if you have equality reflection then it is much more like working in ZFC, where typing is just a provable property like any other

#### Mario Carneiro (Jul 15 2018 at 12:28):

So even though you can do everything in ZFC in lean, stuff that really doesn't respect types gets messy in lean

#### Mario Carneiro (Jul 15 2018 at 12:28):

(I don't know how helpful this is as an analogy)

#### Reid Barton (Jul 15 2018 at 13:20):

For inducting on quotients, isn't there induction _ using quot.ind?

#### Johan Commelin (Sep 26 2018 at 10:25):

Currently there is quotient_module.quotient and quotient_ring.quotient. They are both defined in terms of _root_.quotient. To me it would make sense to define a quotient_ring as a quotient_module` and then add the extra algebraic structure.

#### Johan Commelin (Sep 26 2018 at 10:25):

Is there a reason why this is not a good idea?

#### Patrick Massot (Sep 26 2018 at 11:09):

Mario is working on module quotient: https://www.twitch.tv/videos/314424360

#### Patrick Massot (Sep 26 2018 at 11:10):

It's exactly how I imagined Mario doing Lean before meeting him in Orsay

No, wait!

#### Patrick Massot (Sep 26 2018 at 11:10):

It seems that first thing was actually a trailer for the Venom movie

#### Patrick Massot (Sep 26 2018 at 11:10):

Now I can see emacs

#### Johan Commelin (Sep 26 2018 at 11:18):

Too bad I'm on a train... I don't think they want me to stream twitch over the train wifi

#### Kevin Buzzard (Sep 26 2018 at 11:18):

The Dutch have free WiFi on every train in the country and then just moan about how slow it is ;-)

#### Johan Commelin (Sep 26 2018 at 11:20):

I'm in Germany now. But yes, there is pretty good wifi coverage on the high speed trains in NL, DE, and FR

#### Johan Commelin (Sep 26 2018 at 11:20):

I don't have experience with other countries

Last updated: May 15 2021 at 00:39 UTC