Zulip Chat Archive

Stream: maths

Topic: computers are smart??


view this post on Zulip Reid Barton (Jun 04 2018 at 15:08):

So I was going along constructing coequalizers in Top, like you do. A coequalizer is a kind of quotient, so I needed to prove that if ZZ is the quotient of YY by a relation, then the quotient map YZY \to Z is continuous, so that it's a morphism in Top.
I was all set to add the lemma for that to my continuity tactic, when I noticed the tactic had already succeeded before I did so! What happened?

view this post on Zulip Reid Barton (Jun 04 2018 at 15:09):

It turns out that continuity of the quotient map YZY \to Z is definitionally equivalent to continuity of the identity map on ZZ, because a set is defined to be open in ZZ if and only if its preimage is open in YY. So the tactic found that it could just apply continuous_id!

view this post on Zulip Johan Commelin (Jun 04 2018 at 17:08):

Wunderbar!

view this post on Zulip Johan Commelin (Jun 05 2018 at 07:42):

In fact, Reid, how did you define the topology on ZZ? Because there is a bunch of stuff on coinduced topologies in mathlib, and that would also give you continuity of the quotient map by definition.

view this post on Zulip Reid Barton (Jun 05 2018 at 11:52):

I did use the coinduced topology (see PR at https://github.com/leanprover/mathlib/pull/155/commits/b60f3687e8692f118c385f958d48d31388593298#diff-1c17754b46d709d0b8e22318f94035cdR903)

view this post on Zulip Johan Commelin (Jun 05 2018 at 11:53):

I see. So your continuity tactic is not in that PR?


Last updated: May 12 2021 at 08:14 UTC