Getting an iso with ker g from exact f g and mono f

Stream: homology

[Brendan Seamas Murphy]

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]

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]

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]

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]

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]

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

[Markus Himmel]

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

[Brendan Seamas Murphy]

Thanks!

[Brendan Seamas Murphy]

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

[Brendan Seamas Murphy]

I can do this directly using the API Adam linked

[Kevin Buzzard]

@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]

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]

Definitely could use some comprehensive documentation

[Brendan Seamas Murphy]

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]

After this I'll start merging chunks into mathlib

[Reid Barton]

What kind of homology is this?

[Brendan Seamas Murphy]

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

[Reid Barton]

Nice!