finite exact sequences

Stream: condensed mathematics

[Johan Commelin]

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]

I really don't like the underscores in (⟨_,_,f⟩ :: ⟨_,_,g⟩ :: L)

[Johan Commelin]

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]

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

[Johan Commelin]

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]

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

[Johan Commelin]

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

[Johan Commelin]

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]

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]

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

[Filippo A. E. Nuccio]

Beautiful!

[Johan Commelin]

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]

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

[Johan Commelin]

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

[Filippo A. E. Nuccio]

Oh gosh!

[Filippo A. E. Nuccio]

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

[Filippo A. E. Nuccio]

Isn't it what you want?

[Johan Commelin]

Nothing an extra import can't fix :tada:

[Johan Commelin]

Next question: can we go from arrow Cᵒᵖ to arrow C already?

[Filippo A. E. Nuccio]

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

[Filippo A. E. Nuccio]

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]

I meant the actual arrow category.

[Johan Commelin]

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]

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]

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

[Johan Commelin]

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

[Johan Commelin]

No, I'm done for the day

[Filippo A. E. Nuccio]

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

[Adam Topaz]

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?