Zulip Chat Archive

Stream: condensed mathematics

Topic: finite exact sequences


Johan Commelin (Sep 29 2021 at 06:05):

The following code compiles, but it seems like we can maybe improve the UX a bit:

import algebra.homology.exact

noncomputable theory

open category_theory
open category_theory.limits

universes v u

namespace category_theory
variables (๐’ž : Type u) [category.{v} ๐’ž] [has_zero_morphisms ๐’ž] [has_images ๐’ž] [has_kernels ๐’ž]

inductive exact_seq : list (ฮฃ {A B : ๐’ž}, A โŸถ B) โ†’ Prop
| empty  : exact_seq []
| single : โˆ€ f, exact_seq [f]
| cons   : โˆ€ {A B C : ๐’ž} (f : A โŸถ B) (g : B โŸถ C) (L)
              (hfg : exact f g) (hgL : exact_seq (โŸจ_,_,gโŸฉ :: L)),
              exact_seq (โŸจ_,_,fโŸฉ :: โŸจ_,_,gโŸฉ :: L)

end category_theory

Johan Commelin (Sep 29 2021 at 06:06):

I really don't like the underscores in (โŸจ_,_,fโŸฉ :: โŸจ_,_,gโŸฉ :: L)

Johan Commelin (Sep 29 2021 at 06:06):

Ideally, we would have a way to write exact_seq [f, g, h, f', g', h'] with minimal extra decoration to make it typecheck.

Johan Commelin (Sep 29 2021 at 06:07):

The definition exact_seq doesn't have to make sure that the sources and targets of the morphisms line up.

Johan Commelin (Sep 29 2021 at 06:07):

We could use arrow categories, maybe? But I fear that this mean we need to write arrow.mk all over the place. Which is also bad UX.

Johan Commelin (Sep 29 2021 at 06:16):

@Mario Carneiro Do you have a suggestion how to magically improve our lives here?

Johan Commelin (Sep 29 2021 at 06:25):

Ooh, wow! arrow.mk is available as a coe! Let me try that.

Johan Commelin (Sep 29 2021 at 06:32):

Sweet! This looks pretty nice, I think:

inductive exact_seq : list (arrow ๐’ž) โ†’ Prop
| empty  : exact_seq []
| single : โˆ€ f, exact_seq [f]
| cons   : โˆ€ {A B C : ๐’ž} (f : A โŸถ B) (g : B โŸถ C) (hfg : exact f g) (L) (hgL : exact_seq (g :: L)),
              exact_seq (f :: g :: L)

variable {๐’ž}

lemma exact_iff_exact_seq {A B C : ๐’ž} (f : A โŸถ B) (g : B โŸถ C) :
  exact f g โ†” exact_seq ๐’ž [f, g] :=
begin
  split,
  { intro h, exact exact_seq.cons f g h _ (exact_seq.single _), },
  { rintro (_ | _ | โŸจA, B, C, f, g, hfg, _, _ | _ | _โŸฉ), exact hfg, }
end

Johan Commelin (Sep 29 2021 at 07:47):

I now have

import algebra.homology.exact

noncomputable theory

open category_theory
open category_theory.limits

universes v u

namespace list

variables {ฮฑ : Type*} (a : ฮฑ) (L : list ฮฑ) (m n : โ„•)

/-- Returns the sublist of `L` starting at index `m` of length `n`
(or shorter, if `L` is too short). -/
def extract := (L.drop m).take n

@[simp] lemma extract_nil : [].extract m n = ([] : list ฮฑ) :=
by { cases n, refl, cases m, refl, refl }

@[simp] lemma extract_zero_right : L.extract m 0 = [] := rfl

@[simp] lemma extract_cons_succ_left : (a :: L).extract m.succ n = L.extract m n := rfl

end list

example : [0,1,2,3,4,5,6,7,8,9].extract 4 3 = [4,5,6] := rfl

namespace category_theory
variables (๐’ž : Type u) [category.{v} ๐’ž]
variables [has_zero_morphisms ๐’ž] [has_images ๐’ž] [has_kernels ๐’ž]

/-- A sequence `[f, g, ...]` of morphisms is exact if the pair `(f,g)` is exact,
and the sequence `[g, ...]` is exact.

Recall that the pair `(f,g)` is exact if `f โ‰ซ g = 0`
and the natural map from the image of `f` to the kernel of `g` is an epimorphism
(equivalently, in abelian categories: isomorphism). -/
inductive exact_seq : list (arrow ๐’ž) โ†’ Prop
| nil    : exact_seq []
| single : โˆ€ f, exact_seq [f]
| cons   : โˆ€ {A B C : ๐’ž} (f : A โŸถ B) (g : B โŸถ C) (hfg : exact f g) (L) (hgL : exact_seq (g :: L)),
              exact_seq (f :: g :: L)

variable {๐’ž}

lemma exact_iff_exact_seq {A B C : ๐’ž} (f : A โŸถ B) (g : B โŸถ C) :
  exact f g โ†” exact_seq ๐’ž [f, g] :=
begin
  split,
  { intro h, exact exact_seq.cons f g h _ (exact_seq.single _), },
  { rintro (_ | _ | โŸจA, B, C, f, g, hfg, _, _ | _ | _โŸฉ), exact hfg, }
end

namespace exact_seq

lemma extract : โˆ€ {L : list (arrow ๐’ž)} (h : exact_seq ๐’ž L) (m n : โ„•),
  exact_seq ๐’ž (L.extract m n)
| L (nil)               m     n     := by { rw list.extract_nil, exact nil }
| L (single f)          m     0     := nil
| L (single f)          0     (n+1) := by { cases n; exact single f }
| L (single f)          (m+1) (n+1) := by { cases m; exact nil }
| _ (cons f g hfg L hL) (m+1) n     := extract hL m n
| _ (cons f g hfg L hL) 0     0     := nil
| _ (cons f g hfg L hL) 0     1     := single f
| _ (cons f g hfg L hL) 0     (n+2) := cons f g hfg (L.take n) (extract hL 0 (n+1))

end exact_seq

end category_theory

Johan Commelin (Sep 29 2021 at 07:48):

I hope that we can use this to make talking about pretty explicit finite exact sequences a bit smoother.

Filippo A. E. Nuccio (Sep 29 2021 at 10:53):

Beautiful!

Johan Commelin (Sep 29 2021 at 19:29):

Uh oh... I now need exact_seq.unop which takes an exact sequence in Cแต’แต– and returns the corresponding exact sequence in C.

Johan Commelin (Sep 29 2021 at 19:30):

I don't think we have anything like exact f g โ†” exact g.op f.op so far :sad:

Johan Commelin (Sep 29 2021 at 19:41):

Uggh, we don't even know that the opposite of an abelian category is abelian :crying_cat:

Filippo A. E. Nuccio (Sep 29 2021 at 19:44):

Oh gosh!

Filippo A. E. Nuccio (Sep 29 2021 at 19:46):

https://leanprover-community.github.io/mathlib_docs/category_theory/abelian/opposite.html#category_theory.opposite.abelian

Filippo A. E. Nuccio (Sep 29 2021 at 19:48):

Isn't it what you want?

Johan Commelin (Sep 29 2021 at 19:48):

Nothing an extra import can't fix :tada:

Johan Commelin (Sep 29 2021 at 19:48):

Next question: can we go from arrow Cแต’แต– to arrow C already?

Filippo A. E. Nuccio (Sep 29 2021 at 19:50):

Do you mean the arrow category or simply docs#quiver.hom.op?

Filippo A. E. Nuccio (Sep 29 2021 at 19:52):

And actually, with docs#category_theory.kernel_op_op and docs#category_theory.cokernel_op_op is it really hard to show that the opposite of a SES is a SES?

Johan Commelin (Sep 29 2021 at 19:57):

I meant the actual arrow category.

Johan Commelin (Sep 29 2021 at 19:59):

We'll need something like this:

lemma of_op : โˆ€ {L : list (arrow ๐’œ)}, exact_seq ๐’œแต’แต– (L.reverse.map (ฮป f, sorry)) โ†’
  exact_seq ๐’œ L := sorry

Filippo A. E. Nuccio (Sep 29 2021 at 20:00):

I see... I am now finishing to work on the surjectivity of ฮธ\theta and coming up with the SES we discussed the other day. But I might try to have a look when I am fed up with real numbers...

Filippo A. E. Nuccio (Sep 29 2021 at 20:01):

Although I guess that someone else (you?) will be done before I even start ... :racecar:

Johan Commelin (Sep 29 2021 at 20:01):

I just pushed that sorry. It's in for_mathlib/exact_seq

Johan Commelin (Sep 29 2021 at 20:01):

No, I'm done for the day

Filippo A. E. Nuccio (Sep 29 2021 at 20:01):

You mean you are finally having breakfast, now? :wink:

Adam Topaz (Sep 29 2021 at 20:18):

Johan Commelin said:

Next question: can we go from arrow Cแต’แต– to arrow C already?

I think we might have a general thing about comma categories?


Last updated: Dec 20 2023 at 11:08 UTC