Zulip Chat Archive

Stream: condensed mathematics

Topic: for_mathlib/chain_complex_exact

Kevin Buzzard (Jun 01 2022 at 13:51):

I'm working on the sorries in this file @Adam Topaz @Johan Commelin ; the claim on line 16 is that the whole file is self-contained which is probably an ideal place for me to learn more about this part of the repo.

Adam Topaz (Jun 01 2022 at 14:03):

I think that claim is still true :wink:

Kevin Buzzard (Jun 01 2022 at 17:24):

I've pushed some progress. Let me just ignore the fact that I'm taking a train to Switzerland tomorrow morning and press on.

Kevin Buzzard (Jun 01 2022 at 17:53):

Do we have this:

import category_theory.abelian.exact

open category_theory category_theory.limits

lemma is_zero.exact {𝒞 : Type*} [category 𝒞] [abelian 𝒞] {A B C : 𝒞} {f : A ⟶ B} {g : B ⟶ C}
  (hB : is_zero B) : exact f g :=
begin
  rw abelian.exact_iff,
  split,
  { rw [is_zero.eq_zero_of_tgt hB f, zero_comp], },
  { rw [is_zero.eq_zero_of_tgt hB (kernel.ι g), zero_comp], },
end

?

Adam Topaz (Jun 01 2022 at 17:56):

see for_mathlib/homology_exact

Adam Topaz (Jun 01 2022 at 17:57):

https://github.com/leanprover-community/lean-liquid/blob/0718954bd33fb9455b97d3f9e8c2eb39d85d0849/src/for_mathlib/homology_exact.lean#L46

Kevin Buzzard (Jun 01 2022 at 18:02):

Do we have

lemma exact_of_epi {𝒞 : Type*} [category 𝒞] [abelian 𝒞] {A B C : 𝒞} {f : A ⟶ B} {g : B ⟶ C}
  (hfg : f ≫ g = 0) (hf : epi f) : exact f g :=
sorry

?

Adam Topaz (Jun 01 2022 at 18:03):

yeah it should be somewhere

Adam Topaz (Jun 01 2022 at 18:03):

maybe in for_mathlib/abelian_category?

Adam Topaz (Jun 01 2022 at 18:05):

Oh wait, that's false.

Adam Topaz (Jun 01 2022 at 18:06):

Oh wait, no it's not.

Kevin Buzzard (Jun 01 2022 at 18:06):

Oh is it? Rotten luck :-/ I have got it as far as

hf: epi f
⊢ is_zero (cokernel f)

Is that false too?

Adam Topaz (Jun 01 2022 at 18:08):

No they should both be true

Adam Topaz (Jun 01 2022 at 18:10):

lemma exact_of_epi {A : Type*} [category A] [abelian A]
  (X Y Z : A) (f : X ⟶ Y) (g : Y ⟶ Z) [epi f] (w : f ≫ g = 0) : exact f g :=
begin
  rw abelian.exact_iff,
  use w,
  convert comp_zero,
  apply is_zero.eq_of_tgt,
  library_search -- exact is_zero_cokernel_of_epi f,
end

Adam Topaz (Jun 01 2022 at 18:12):

We might be missing exact_of_epi

Kevin Buzzard (Jun 01 2022 at 18:12):

lemma exact_of_epi {𝒞 : Type*} [category 𝒞] [abelian 𝒞] {A B C : 𝒞} {f : A ⟶ B} {g : B ⟶ C}
  (hfg : f ≫ g = 0) (hf : epi f) : exact f g :=
begin
  rw abelian.exact_iff,
  refine ⟨hfg, _⟩,
  rw [(abelian.epi_iff_cokernel_π_eq_zero _).1 hf, comp_zero],
end

Adam Topaz (Jun 01 2022 at 18:13):

epi is a class

Kevin Buzzard (Jun 01 2022 at 18:13):

I've been avoiding the convert technique recently, it can get really slow; I think it's a bad habit :-)

Adam Topaz (Jun 01 2022 at 18:13):

yeah, I use it sparingly.

Kevin Buzzard (Jun 01 2022 at 18:29):

OK I just pushed one more sorry. I doubt I'll have any more time today. I can finish these off tomorrow hopefully.

Kevin Buzzard (Jun 01 2022 at 19:29):

OK I did one more :-) The last one will have to wait -- anyway it's of a slightly different nature to the rest, so I will need new tricks. I'm done for the day :-)

Kevin Buzzard (Jun 02 2022 at 12:39):

Working on the final sorry in this file.

Kevin Buzzard (Jun 02 2022 at 15:07):

OK so it's now sorry-free. I'm not sure if I missed any tricks. Checking that an additive equivalence of categories preserves and reflects exactness was surprisingly long.

Last updated: Dec 20 2023 at 11:08 UTC