Zulip Chat Archive

Stream: maths

Topic: Equalizers & Products => Complete


view this post on Zulip Brendan Seamas Murphy (Sep 04 2019 at 02:26):

Is this proven in the category theory lib anywhere? I'm having trouble finding it

view this post on Zulip Brendan Seamas Murphy (Sep 04 2019 at 02:29):

Nevermind, looks like this is in a later version of mathlib than I have

view this post on Zulip Scott Morrison (Sep 04 2019 at 02:53):

Hi @Brendan Seamas Murphy, it just arrived two days ago! I'm curious what you're wanting it for.

view this post on Zulip Brendan Seamas Murphy (Sep 04 2019 at 02:57):

I was curious about formulating basic group theory in terms of short exact sequences, and was looking for a good way to state a version of the second isomorphism theorem, that for A, B normal in G, AB/B is iso to A/(A \cap B)

view this post on Zulip Brendan Seamas Murphy (Sep 04 2019 at 02:57):

But instead of working with subgroups I have

structure SES (A B C : Group) :=
(f : A ⟶ B) (g : B ⟶ C)
(f_inj : function.injective f)
(g_surj : function.surjective g)
(im_f_eq_ker_g : set.range f = is_group_hom.ker g)

view this post on Zulip Brendan Seamas Murphy (Sep 04 2019 at 02:59):

Given S : SES A G K and S' : SES B G K', I can get an injective map pullback S.f S'.f -> G, which is easier to work with than the intersection of the images of S.f and S'.f

view this post on Zulip Brendan Seamas Murphy (Sep 04 2019 at 03:01):

I could just construct the pullback manually but I figured I might check if Lean had them already, and then I was wondering if I could avoid doing pullbacks and instead do products and equalizers

view this post on Zulip Kevin Buzzard (Sep 04 2019 at 03:44):

@Sian Carey proved the correspondence theorem using bundled subgroups and group homs.

view this post on Zulip Scott Morrison (Sep 04 2019 at 03:48):

Do you know where it is?

view this post on Zulip Kevin Buzzard (Sep 04 2019 at 03:49):

I believe it's currently private. I'll email her.

view this post on Zulip Scott Morrison (Sep 04 2019 at 03:49):

Also, more generally, I think it's best when constructing (co)limits in algebraic examples to just do the most general construction that works in that setting, and then let typeclass inference provide you with special shapes (pullbacks, equalizers, etc).

view this post on Zulip Scott Morrison (Sep 04 2019 at 03:51):

We don't have arbitrary limits set up in Grp yet (or indeed the definition of Grp), but it should be an easy exercise copying what is in the file algebra/CommRing/limits.lean.

view this post on Zulip Scott Morrison (Sep 04 2019 at 03:51):

I have been holding off providing all these has_limits constructions in all the different algebraic examples, in the hope of doing them uniformly with the help of some tactics, but maybe it's best to just make them all, and we can refactor them later.

view this post on Zulip Kevin Buzzard (Sep 10 2019 at 07:21):

https://github.com/ImperialCollegeLondon/lean-groups

view this post on Zulip Scott Morrison (Sep 10 2019 at 07:24):

(deleted)


Last updated: May 11 2021 at 16:22 UTC