## Stream: homology

### Topic: Getting an iso with ker g from exact f g and mono f

#### Brendan Seamas Murphy (Aug 25 2022 at 20:04):

I have f : X ⟶ Y, g : Y ⟶ Z and I know mono f, exact f g. What's the easiest way to get an isomorphism X ≅ kernel g? I'm depending on LTE in case there's an easy way from the stuff in there that isn't in mathlib

#### Adam Topaz (Aug 25 2022 at 20:12):

Take a look at https://github.com/leanprover-community/lean-liquid/blob/master/src/for_mathlib/exact_lift_desc.lean particularly mono_lift etc

#### Adam Topaz (Aug 25 2022 at 20:13):

that should let you work with X as if it was a kernel already (in the sense that you get the same API)

#### Adam Topaz (Aug 25 2022 at 20:14):

if you want you could construct an isomorphism with kernel g using this API, but the API itself might be enough for your application.

#### Brendan Seamas Murphy (Aug 25 2022 at 20:30):

No I need an actual isomorphism with the kernel, I have an exact sequence 0 -> X -> R^2 -g> R where g(x, y) = x + y and I want to conclude X is free of rank 1. I ended up using exact_iff_image_to_kernel'_is_iso and limits.image_mono_iso_source

#### Brendan Seamas Murphy (Aug 25 2022 at 20:31):

(this is for computing H₁(∂Δ²; R) using the isomorphism H₁(∂Δ²; R) ≅ H₁(Δ¹, ∂Δ¹; R) and the LES of the pair (Δ¹, ∂Δ¹))

#### Markus Himmel (Aug 25 2022 at 20:55):

The usual way to get the isomorphism would be to use docs#category_theory.abelian.is_limit_of_exact_of_mono and docs#category_theory.limits.is_limit.cone_point_unique_up_to_iso

Thanks!

#### Brendan Seamas Murphy (Aug 25 2022 at 21:01):

Actually I think the right way to do what I'm trying to do is to show that a ladder diagram like this with exact rows and the vertical maps isos induces the dotted iso image.png

#### Kevin Buzzard (Aug 25 2022 at 22:56):

@Brendan Seamas Murphy it's great that you're a consumer of the abelian category API! I don't think abelian category formalisation has been attempted before so it will be interesting to see what people need.

#### Brendan Seamas Murphy (Aug 25 2022 at 22:56):

Yeah, I think my singular homology project has been a kind of stress test for it. I'll try to write up something about my experience with it and pain points

#### Brendan Seamas Murphy (Aug 25 2022 at 22:57):

Definitely could use some comprehensive documentation

#### Brendan Seamas Murphy (Aug 25 2022 at 23:07):

Also I am nearly done with my project, I have the iso Hₖ(Δⁿ, ∂Δⁿ) ≅ Hₖ(∂Δⁿ⁺¹) and just need to do an inductive argument to calculate Hₖ(∂Δⁿ). I haven't had much time to work on it until recently because I needed to study for & take my qualifying exams (which I've passed!)

#### Brendan Seamas Murphy (Aug 25 2022 at 23:08):

After this I'll start merging chunks into mathlib

#### Reid Barton (Aug 25 2022 at 23:38):

What kind of homology is this?

#### Brendan Seamas Murphy (Aug 25 2022 at 23:40):

Singular, see https://github.com/Shamrock-Frost/BrouwerFixedPoint

#### Reid Barton (Aug 25 2022 at 23:42):

Nice!

Last updated: Dec 20 2023 at 11:08 UTC