Equalizers & Products => Complete

Stream: maths

[Brendan Seamas Murphy]

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

[Brendan Seamas Murphy]

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

[Scott Morrison]

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

[Brendan Seamas Murphy]

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]

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]

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]

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]

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

[Scott Morrison]

Do you know where it is?

[Kevin Buzzard]

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

[Scott Morrison]

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]

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]

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]

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

[Scott Morrison]

(deleted)