Zulip Chat Archive

Stream: general

Topic: quotients


view this post on Zulip 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?

view this post on Zulip 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₁)

view this post on Zulip Mario Carneiro (Jul 15 2018 at 11:39):

induction for quotients is a feature I want in lean 4

view this post on Zulip Chris Hughes (Jul 15 2018 at 11:39):

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

view this post on Zulip Mario Carneiro (Jul 15 2018 at 11:40):

I'm not sure how replicable induction is

view this post on Zulip Chris Hughes (Jul 15 2018 at 11:40):

Is it C++?

view this post on Zulip Mario Carneiro (Jul 15 2018 at 11:40):

mostly

view this post on Zulip Chris Hughes (Jul 15 2018 at 11:40):

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

view this post on Zulip 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]

view this post on Zulip 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?

view this post on Zulip Kevin Buzzard (Jul 15 2018 at 11:42):

Then quotients would be easier to think about

view this post on Zulip Mario Carneiro (Jul 15 2018 at 11:42):

Sure, you can do that

view this post on Zulip Chris Hughes (Jul 15 2018 at 11:42):

Computablity perhaps?

view this post on Zulip Mario Carneiro (Jul 15 2018 at 11:42):

some facts need the axiom of choice

view this post on Zulip Mario Carneiro (Jul 15 2018 at 11:42):

and it's not data when you do that

view this post on Zulip Chris Hughes (Jul 15 2018 at 11:43):

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

view this post on Zulip Mario Carneiro (Jul 15 2018 at 11:43):

You can't get that with any construction

view this post on Zulip Mario Carneiro (Jul 15 2018 at 11:44):

and that adds real power - funext is proven using quotients

view this post on Zulip Patrick Massot (Jul 15 2018 at 11:44):

Thank you very much Chris!

view this post on Zulip Patrick Massot (Jul 15 2018 at 11:44):

I hope I'll be able to use that.

view this post on Zulip Mario Carneiro (Jul 15 2018 at 11:45):

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

view this post on Zulip Patrick Massot (Jul 15 2018 at 11:45):

This is explained in TPIL

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Jul 15 2018 at 11:47):

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

view this post on Zulip 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

view this post on Zulip Patrick Massot (Jul 15 2018 at 11:49):

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

view this post on Zulip Mario Carneiro (Jul 15 2018 at 11:49):

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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Jul 15 2018 at 11:51):

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

view this post on Zulip Patrick Massot (Jul 15 2018 at 11:52):

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

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Jul 15 2018 at 11:52):

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

view this post on Zulip Mario Carneiro (Jul 15 2018 at 11:52):

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

view this post on Zulip Kevin Buzzard (Jul 15 2018 at 11:53):

?

view this post on Zulip Mario Carneiro (Jul 15 2018 at 11:53):

They lack the computation rule

view this post on Zulip Kevin Buzzard (Jul 15 2018 at 11:53):

which one is that?

view this post on Zulip Mario Carneiro (Jul 15 2018 at 11:53):

lift f (mk a) = f a

view this post on Zulip Chris Hughes (Jul 15 2018 at 11:54):

It is true, but not rfl

view this post on Zulip Kevin Buzzard (Jul 15 2018 at 11:54):

"lack" :-)

view this post on Zulip Mario Carneiro (Jul 15 2018 at 11:54):

because in type theory definitional equality matters

view this post on Zulip Kevin Buzzard (Jul 15 2018 at 11:54):

Yes!

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Jul 15 2018 at 11:56):

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

view this post on Zulip Patrick Massot (Jul 15 2018 at 11:56):

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

view this post on Zulip Kevin Buzzard (Jul 15 2018 at 11:56):

no

view this post on Zulip Patrick Massot (Jul 15 2018 at 11:56):

You should

view this post on Zulip Mario Carneiro (Jul 15 2018 at 11:56):

It's a really good intro to dependent type theory

view this post on Zulip Kevin Buzzard (Jul 15 2018 at 11:57):

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

view this post on Zulip Kevin Buzzard (Jul 15 2018 at 11:57):

My kids don't read anything.

view this post on Zulip Kevin Buzzard (Jul 15 2018 at 11:57):

They just google

view this post on Zulip Mario Carneiro (Jul 15 2018 at 11:57):

Also you will find some decent material on HITs there

view this post on Zulip Patrick Massot (Jul 15 2018 at 11:57):

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

view this post on Zulip Mario Carneiro (Jul 15 2018 at 11:57):

HoTT has some much more exotic HITs than quotients

view this post on Zulip Mario Carneiro (Jul 15 2018 at 11:58):

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

view this post on Zulip Mario Carneiro (Jul 15 2018 at 11:58):

In HoTT you can prove that loop is not rfl

view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Jul 15 2018 at 12:00):

You can do pretty much everything in classical math

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Jul 15 2018 at 12:01):

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

view this post on Zulip Mario Carneiro (Jul 15 2018 at 12:02):

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

view this post on Zulip Mario Carneiro (Jul 15 2018 at 12:03):

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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Jul 15 2018 at 12:04):

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

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip Mario Carneiro (Jul 15 2018 at 12:06):

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

view this post on Zulip Mario Carneiro (Jul 15 2018 at 12:06):

The simplest is something isomorphic to fin n

view this post on Zulip Mario Carneiro (Jul 15 2018 at 12:07):

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

view this post on Zulip Kevin Buzzard (Jul 15 2018 at 12:07):

and equality is undecidable...

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Jul 15 2018 at 12:08):

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

view this post on Zulip Patrick Massot (Jul 15 2018 at 12:09):

Forget about HoTT Kevin, it's all constructive

view this post on Zulip Patrick Massot (Jul 15 2018 at 12:09):

We have maths to do instead

view this post on Zulip Mario Carneiro (Jul 15 2018 at 12:09):

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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Jul 15 2018 at 12:10):

I don't think you need propext for anything

view this post on Zulip Mario Carneiro (Jul 15 2018 at 12:11):

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

view this post on Zulip Mario Carneiro (Jul 15 2018 at 12:11):

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

view this post on Zulip Mario Carneiro (Jul 15 2018 at 12:12):

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

view this post on Zulip Mario Carneiro (Jul 15 2018 at 12:12):

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

view this post on Zulip 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

?

view this post on Zulip Mario Carneiro (Jul 15 2018 at 12:24):

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

view this post on Zulip Mario Carneiro (Jul 15 2018 at 12:25):

Lean's choice axiom is much more heavy handed

view this post on Zulip Mario Carneiro (Jul 15 2018 at 12:25):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Jul 15 2018 at 12:28):

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

view this post on Zulip Reid Barton (Jul 15 2018 at 13:20):

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

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Sep 26 2018 at 10:25):

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

view this post on Zulip Patrick Massot (Sep 26 2018 at 11:09):

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

view this post on Zulip Patrick Massot (Sep 26 2018 at 11:10):

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

view this post on Zulip Patrick Massot (Sep 26 2018 at 11:10):

No, wait!

view this post on Zulip Patrick Massot (Sep 26 2018 at 11:10):

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

view this post on Zulip Patrick Massot (Sep 26 2018 at 11:10):

Now I can see emacs

view this post on Zulip 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

view this post on Zulip 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 ;-)

view this post on Zulip 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

view this post on Zulip 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