## Stream: maths

### Topic: Equalizers & Products => Complete

#### Brendan Seamas Murphy (Sep 04 2019 at 02:26):

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

#### Brendan Seamas Murphy (Sep 04 2019 at 02:29):

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

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

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

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


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

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

#### Kevin Buzzard (Sep 04 2019 at 03:44):

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

#### Scott Morrison (Sep 04 2019 at 03:48):

Do you know where it is?

#### Kevin Buzzard (Sep 04 2019 at 03:49):

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

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

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

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

#### Kevin Buzzard (Sep 10 2019 at 07:21):

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

#### Scott Morrison (Sep 10 2019 at 07:24):

(deleted)

Last updated: May 11 2021 at 16:22 UTC