complexes, d, dtt

Stream: condensed mathematics

[Johan Commelin]

Here's a pretty heretical proposal, that takes ideas from Floris, Scott, and Sebastien:

import category_theory.limits.shapes.zero

open category_theory category_theory.limits

class has_succ (α : Type*) := (succ : α → α)

-- fix this to something better?
notation `Ş` := has_succ.succ

-- do we want this for every semiring??
instance : has_succ ℕ := ⟨λ n, n + 1⟩
instance : has_succ ℤ := ⟨λ n, n + 1⟩

structure differential_object_aux (ι : Type) (S₀ S₁ : ι → ι) (V : Type*)
  [category V] [has_zero_morphisms V] :=
(X : ι → V)
(differential : Π i, X (S₀ i) ⟶ X (S₁ i))
(differential2 : ∀ i j (h : S₁ i = S₀ j),
  differential i ≫ eq_to_hom (show X (S₁ i) = X (S₀ j), by rw h) ≫ differential j = 0)

variables (ι : Type) (V : Type*) {cov : bool}
variables [has_succ ι] [category V] [has_zero_morphisms V]

def differential_object : bool → Type*
| tt := differential_object_aux ι id Ş V
| ff := differential_object_aux ι Ş id V

abbreviation chain_complex := differential_object ι V ff

abbreviation cochain_complex := differential_object ι V tt

namespace differential_object

variables {ι V}

def X : Π {cov : bool} (C : differential_object ι V cov), ι → V
| tt := differential_object_aux.X
| ff := differential_object_aux.X

variable [decidable_eq ι]

def d : Π {cov : bool} (C : differential_object ι V cov) (i j : ι), C.X i ⟶ C.X j
| tt C i j :=
if h : Ş i = j
then differential_object_aux.differential C i ≫ eq_to_hom (show C.X (Ş i) = C.X j, by rw h)
else 0
| ff C i j :=
if h : i = Ş j
then eq_to_hom (show C.X i = C.X (Ş j), by rw h) ≫ differential_object_aux.differential C j
else 0

lemma d_comp_d (C : differential_object ι V cov) (i j k : ι) :
  C.d i j ≫ C.d j k = 0 :=
begin
  cases cov,
  all_goals
  { dsimp [d], split_ifs with h1 h2,
    { subst h1, subst h2,
      simpa using differential_object_aux.differential2 C _ _ rfl },
    all_goals { simp only [zero_comp, comp_zero] } }
end

end differential_object

[Johan Commelin]

This allows us to work with chain/cochain complexes indexed by $\Z$, $\N$, $\N \times \{0,1,2\}$ etc...

[Johan Commelin]

d_comp_d is true without any proof obligations

[Johan Commelin]

d i j is a map from C.X i to C.X j, for all i and j

[Johan Commelin]

It solves (read: sidesteps) the issue of whether d i : C.X i -> C.X (i-1) or d i : C.X (i+1) -> C.X i.
As @Scott Morrison points out in #6260, both conventions are used in maths literature.

With this proposal d i j : C.X i -> C.X j, you just need to provide both i and j, so that issue doesn't occure :sweat_smile: :relieved: :see_no_evil:

[Johan Commelin]

So far for the immediate advantages that I see.
Downsides:

• We get no type checker guarantees that d makes sense.
• We get no type inference for d _ _ x, we have to always remind Lean about the target of d
• Readability might be hampered by having all those i and js explicit.

[Kevin Buzzard]

What is wrong with just asking for d {i} {j} (h : j = i + 1)? Didn't this work fine?

I personally think that to make some sense of what is happening here, we need an explicit "challenge problem" which can be a test case for any method? e.g. "implement chain complexes and then prove lemma X"? Do you have a good test case in mind Johan? We can try all methods against it, and of course we can make a list of challenge problems if necessary.

[Johan Commelin]

soft_truncation.lean is a nice test case

[Kevin Buzzard]

Can you be more explicit? Where do I look? I've been very busy for the past few days.

[Kevin Buzzard]

(but I feel very free right now :-) although I have a large document to read for an 11am meeting...but it's not 9am yet :P )

[Johan Commelin]

It's in src/

[Johan Commelin]

and full of sorrys

[Johan Commelin]

The downside with your proposal is that we'll have to prove h : j = i + 1 a lot, really a lot.

[Johan Commelin]

And those proofs are all boring and distracting

[Johan Commelin]

But on the other hand, it does give some coherence for the type checker to hang on to.

[Johan Commelin]

So I feel like we have to choose between two evils (-;

[Kevin Buzzard]

I am not saying the h way is better. I think we just need to experiment with both because we are not working on lean-liquid here, we are making some big decision about how to implement chain complexes in Lean so it's definitely worth some thought. I just think that rather than a bunch of people posting random code we need an explicit "test suite" somehow.

[Kevin Buzzard]

I am still very unclear about what I am supposed to be doing with my "rival" proposal. You are using cochain_complex which apparently is already in mathlib. Is one of the rules that we must stick to mathlib's cochain_complex? And the challenge is an explicit question about NormedGroup?

[Johan Commelin]

No! I'm not using mathlibs version

[Johan Commelin]

Sorry for the confusion

[Johan Commelin]

In the top post I propose a rival to mathlib's version

[Kevin Buzzard]

Am I looking at the right file? src/system_of_complexes/soft_truncation.lean?

[Johan Commelin]

Yes

[Johan Commelin]

but it doesn't use my top post yet

[Johan Commelin]

I'm currently viewing LTE as the test suite. Working on converting to my proposal, to see how it works

[Kevin Buzzard]

So is the situation the following:

CHALLENGE: create a definition of cochain complex of NormedGroups, define the soft truncation of a cochain complex of normed groups, and give a complete proof of the assertion that the soft truncation is (k,K)-exact in degrees <= m for c>= c0 iff the original complex is (k,K)-exact in degrees <= m for c>= c0.

And right now we have
Incomplete entry 1: src/system_of_complexes/soft_truncation.lean
Incomplete entry 2: Johan's post above
Non-existent entry 3: my d idea.

Is this an accurate description of what is going on? I might well have some time today to hack on this and my understanding (correct me if I'm wrong) is that yesterday you and Adam decided that this is really becoming the key question.

Have I got the statement of the challenge right?

[Kevin Buzzard]

And we are to use the definition of NormedGroup in the liquid repo but we can use any definition of cochain complex that we like, although we will have to come up with our own definition of is_bounded_exact for that definition?

[Kevin Buzzard]

Wait, the challenge isn't even true, because you can have terms of negative degree which mess things up.

I would really appreciate guidance towards what the challenge is so I can work on this this afternoon.

[Sebastien Gouezel]

One advantage of not having to prove j = i + 1 is for the 0 case in $\N$-indexed complexes: the cohomology is always (d i (i+1).ker) / (d (i-1) i).im, regardless of whether i = 0 or not (and j = i + 1 in this case is just not true).

Also, regarding the fact that there would be too many i and j everywhere, one can register d' {i} (x : C i) = d i (i+1) x and use d' in most situations, and d when one has to do something nontrivial with the indices (or exchange the two notations maybe).

[Johan Commelin]

@Kevin Buzzard yes, that challenge sounds about right

[Johan Commelin]

but it could be extended to a full proof of normed_snake and normed_spectral

[Johan Commelin]

If those work smoothly, that is pretty good evidence that we found a workable definition

[Johan Commelin]

@Sebastien Gouezel I agree that we could use some notation to get rid of some of the is or js

[Johan Commelin]

(But d' is taken because we have differentials in the horizontal and vertical direction (-;

[Johan Commelin]

Kevin Buzzard said:

Wait, the challenge isn't even true, because you can have terms of negative degree which mess things up.

I would really appreciate guidance towards what the challenge is so I can work on this this afternoon.

I think for me the challenge includes to have something that gracefully handles nat-indexed and int-indexed complexes.

[Kevin Buzzard]

What is normed_snake? I see weak_normed_snake in src/normed_snake but this looks like it is proved. I am still unclear about what the challenge is. So far I said something which is definitely unprovable (i.e. false) and you said "that challenge sounds about right", and you are saying things which I don't understand in the sense that I am not sure which formal statement you are talking about.

[Johan Commelin]

But designing a good test suite is hard

[Kevin Buzzard]

I just want an explicit sorry, that's all.

[Johan Commelin]

Kevin Buzzard said:

What is normed_snake? I see weak_normed_snake in src/normed_snake but this looks like it is proved. I am still unclear about what the challenge is. So far I said something which is definitely unprovable (i.e. false) and you said "that challenge sounds about right", and you are saying things which I don't understand in the sense that I am not sure which formal statement you are talking about.

It's proved using mathlibs definition of chain_complex.

[Kevin Buzzard]

And it worked? So what is the problem?

[Johan Commelin]

Well, it "worked". We've had quite some discussions to get past that hurdle

[Kevin Buzzard]

I don't understand what you mean.

[Kevin Buzzard]

I am trying to work out what the ACTUAL QUESTION is.

[Johan Commelin]

Well, we needed Mario to get us past several DTT hurdles, right?

[Kevin Buzzard]

I don't know.

[Kevin Buzzard]

All I know is that I have three hours this afternoon to try and be helpful and I am trying to figure out right now what I can do before admin kicks in in 5 minutes.

[Johan Commelin]

I understand

[Johan Commelin]

But maybe I don't have a clear problem description...

[Kevin Buzzard]

OK then maybe I am asking for too much.

[Johan Commelin]

When we tried to unsorry soft_truncation we quickly ran into DTT issues.

[Johan Commelin]

We could solve them with a lot of eq_to_hom, but that's just ugly.

[Kevin Buzzard]

OK so let's go back to that file.

[Johan Commelin]

So I want something better.

[Johan Commelin]

But Floris reminded us that we also want to support long exact sequences. Which are indexed by nat x (fin 3) or something like that

[Johan Commelin]

So I'm trying to be so general that it also captures that

[Kevin Buzzard]

I think that if you want them to start correctly you might want int x (fin 3)

[Kevin Buzzard]

otherwise you have to say "my first map is injective" explicitly.

[Kevin Buzzard]

Tate's cohomology theory for finite groups has H^n for all integers n :-/

[Johan Commelin]

Right, but the main point is that we maybe don't want to assume that int x (fin 3) has an add_comm_group instance that provided the i -> i + 1 structure

[Johan Commelin]

Instead we should have a generic succ : I -> I on the indexing type

[Kevin Buzzard]

OK so I will simply have a look at soft_truncation from the d {i} {j} (h) viewpoint. I know that you and others have thought about it a lot more than me but I would like to try it myself so I can understand the issues other people have with this idea better.

[Kevin Buzzard]

I agree that the succ idea is brilliant.

[Johan Commelin]

Yes, please test it. I haven't tested that idea nearly enough.

[Kevin Buzzard]

If the idea you're talking about is succ then I think Floris tested it a lot in his thesis :-)

[Kevin Buzzard]

I am still confused about soft_truncation'_is_bounded_exact_iff. What if C is a complex with a poorly behaved term in degree -37 stopping is_bounded_exact from being true. Then it's not bounded_exact, but its soft truncation might be. In system_of_complexes/soft_truncation the lemma is stated as an iff.

[Mario Carneiro]

I think I'm in a similar position to Kevin. I'd like to try out these problems but I have no idea what the problem statement is, much less the informal proof

[Mario Carneiro]

I'm on board with the "theme" of dealing with chain complexes, but I guess there's a particular theorem in mind?

[Johan Commelin]

Did I forget to add the assumption that C is bounded exact in negative degrees?

[Johan Commelin]

I had it in a TODO at some point, but it may have been lost in some process

[Johan Commelin]

@Mario Carneiro What do you mean with "particular theorem"?

[Johan Commelin]

API theorems? Or the big goal?

[Mario Carneiro]

Something that has DTT hell issues

[Mario Carneiro]

probably not the big goal

[Johan Commelin]

Ok, soft_truncation has those

[Johan Commelin]

Let me see if I can find the code for the first sorry, which is what Adam wrote (on some branch?)

[Johan Commelin]

@Mario Carneiro Aah, on master the first def is already complete now

[Johan Commelin]

And the second def has sorry -- annoying )-;, so there you go :grinning:

[Mario Carneiro]

Complete proofs are fine, especially if the result is unsatisfactory

[Mario Carneiro]

link?

[Johan Commelin]

First sorry is on line 37 :rofl:

[Johan Commelin]

https://github.com/leanprover-community/lean-liquid/blob/master/src/system_of_complexes/soft_truncation.lean#L37

[Johan Commelin]

Small success story:

before

lemma of_shift  {k K : ℝ≥0} {m : ℤ} [hk : fact (1 ≤ k)] {c₀ : ℝ≥0}
  (H : ∀ c ≥ c₀, ∀ i < m - 1, ∀ x : C (k * c) (i + 1 + 1),
   ∃ y : C c (i + 1), ∥res x - d y∥ ≤ K * ∥d x∥) :
   C.is_bounded_exact k K m c₀ :=
begin
  intros c hc i hi x,
  specialize H c hc (i-1) (by linarith),
  rw [sub_add_cancel] at H,
  exact H x,
end

lemma to_exact (hC : C.is_weak_bounded_exact k K m c₀) {δ : ℝ≥0} (hδ : 0 < δ)
  (H : ∀ c ≥ c₀, ∀ i < m - 1, ∀ x : C (k * c) (i + 1 + 1),
    d x = 0 → ∃ y : C c (i + 1), res x = d y) : C.is_bounded_exact k (K + δ) m c₀ :=
begin
  apply is_bounded_exact.of_shift,
  intros c hc i hi x,
  by_cases hdx : d x = 0,
  { rcases H c hc i hi x hdx with ⟨y, hy⟩,
    exact ⟨y, by simp [hy, hdx]⟩ },
  { have : ((K + δ : ℝ≥0) : ℝ) * ∥d x∥ = K * ∥d x∥ + δ * ∥d x∥, apply_mod_cast add_mul,
    simp_rw this,
    apply hC c hc _ _ x (δ*∥d x∥) (mul_pos (by exact_mod_cast hδ) $ norm_pos_iff.mpr hdx), linarith },
end

[Johan Commelin]

after

lemma to_exact (hC : C.is_weak_bounded_exact k K m c₀) {δ : ℝ≥0} (hδ : 0 < δ)
  (H : ∀ c ≥ c₀, ∀ i ≤ m, ∀ x : C (k * c) i,
    C.d _ (i+1) x = 0 → ∃ y : C c (i-1), res x = C.d _ _ y) :
  C.is_bounded_exact k (K + δ) m c₀ :=
begin
  intros c hc i hi x,
  by_cases hdx : C.d _ (i+1) x = 0,
  { rcases H c hc i hi x hdx with ⟨y, hy⟩,
    exact ⟨y, by simp [hy, hdx]⟩ },
  { have : ((K + δ : ℝ≥0) : ℝ) * ∥C.d _ (i+1) x∥
      = K * ∥C.d _ (i+1) x∥ + δ * ∥C.d _ (i+1) x∥, apply_mod_cast add_mul,
    rw this,
    exact hC c hc _ hi x (δ*∥C.d _ (i+1) x∥) (mul_pos (by exact_mod_cast hδ) $ norm_pos_iff.mpr hdx) },
end

[Johan Commelin]

In particular the entire of_shift lemma is no longer needed

[Johan Commelin]

Also, the statements aren't about i + 1 + 1, but just about i and i-1, as you would do on paper.

[Johan Commelin]

---

system_of_complexes/basic works again, I pushed to jmc-complex

[Riccardo Brasca]

If you want to test a new approach to the problem I am not so sure that adapting the proof of the (weak) snake lemma is a good test. The proof is not very short, but there are no DTT issues, at least in the first version I wrote. The only thing I did was to let Lean take care of all the indexes, and I never wrote i + 1 + 1 + 1, only _, and it worked like a charm (there are no i - 1 in the proof). The same for the the real numbers, I started with k * (k * (k * c)) instead of k ^ 3 * c and I forgot about it.

[Johan Commelin]

hmm, maybe the DTT issues were not in normed_snake but in the lemma that Patrick was trying to prove

[Johan Commelin]

Namely going from weak exactness to strong exactness

[Riccardo Brasca]

yes, in that lemma there are some i-1

[Kevin Buzzard]

I think that Sebastien's question about nat can be phrased in the following way: should succ : \a \to \a be beefed up to an equiv? I think he says no but I am thinking yes.

[Johan Commelin]

No, I agree with Sebastien

[Johan Commelin]

There are many reasons to keep nat available as long as possible.

[Johan Commelin]

See also #6260 by Scott, where he basically duplicates the entire api to nat.

[Kevin Buzzard]

There will be two definitions of "exact" if we keep nat, one saying A 0 -> A 1 -> A 2 -> ... is exact if it's exact from A1, and a second one saying "and furthermore A0 -> A1 is injective".

[Kevin Buzzard]

We need with_neg_one_nat ;-)

[Sebastien Gouezel]

By exact, you mean zero cohomology, i.e., (d (i-1) i).im = (d i (i+1)).ker for all i, right? This definition already contains the fact that the first arrow is injective, by taking i = 0 :-)

[Kevin Buzzard]

My understanding is that the definition of "A -> B -> C -> D is exact" means "exactness at B and C only". So no, I don't mean this -- I think "A 0 -> A 1 -> A 2 -> ... exact" doesn't imply injectivity of A 0 -> A 1. Or at least I thought that the standard definition didn't mean this. I thought that this was why for short exact sequences we write "0 -> A -> B -> C -> 0" and not just "A -> B -> C" -- exactness of the latter is just exactness at B. But honestly I cannot see this being a problem, as long as people are careful to spell out in docstrings what everything means. It might be a situation where a mathematician can misunderstand a claim being made in Lean but this can be fixed with docstrings.

[Kevin Buzzard]

Here is my effort so far with the "feed in the proofs" variant. It is going well -- I have got further than Johan:

import system_of_complexes.basic
import for_mathlib.normed_group_quotient

/-!
# Soft truncation

In this file we define soft truncation functors
for (systems of) complexes of normed groups.

We call these `soft_truncation'` to distinguish them from the usual soft truncation functors.
The difference is solely in the definition of the object in degree `0`.
Usually this object is defined as `C 0` modulo the kernel of `d : C 0 ⟶ C 1`.
Instead, we define it as `C 0` modulo the image of `d : C (-1) ⟶ C 0`.
Hence the two definitions agree iff `C` is exact in degree `0`.

-/

noncomputable theory
open_locale nnreal

open category_theory category_theory.limits

section has_succ

class has_succ (α : Type*) := (succ : α → α)

-- I can't find that Turkish(?) symbol on my keyboard :-(
notation `Sc` := has_succ.succ

def int.has_succ : has_succ ℤ := ⟨λ z, z + 1⟩

local attribute [instance] int.has_succ

def dsource (n : ℤ) : Sc n = n + 1 := rfl
def dtarget (n : ℤ) : Sc (n - 1) = n := sub_add_cancel n 1

end has_succ

section cochain_complex'

universes v u

structure cochain_complex' (𝒞 : Type u) [category.{v} 𝒞] [has_zero_morphisms 𝒞]
  (α : Type*) [has_succ α] :=
(X : α → 𝒞)
(d {i j : α} (h : Sc i = j) : X i ⟶ X j)
(d_squared' {i j k : α} (hij : Sc i = j) (hjk : Sc j = k) : (d hij) ≫ (d hjk) = 0)

local attribute [instance] int.has_succ

variables {𝒞 : Type u} [category.{v} 𝒞] [has_zero_morphisms 𝒞]
  (C : cochain_complex' 𝒞 ℤ)

lemma d_squared_left (n : ℤ) : C.d (dsource n) ≫ C.d (dsource (n + 1)) = 0 :=
C.d_squared' (dsource n) (dsource (n + 1))

lemma d_squared_middle (n : ℤ) : C.d (dtarget n) ≫ C.d (dsource n) = 0 :=
C.d_squared' (dtarget n) (dsource n)

lemma d_squared_right (n : ℤ) : C.d (dtarget (n - 1)) ≫ C.d (dtarget n) = 0 :=
C.d_squared' (dtarget (n - 1)) (dtarget n)

end cochain_complex'

namespace NormedGroup
open quotient_add_group

namespace soft_truncation'

local attribute [instance] int.has_succ

def X (C : cochain_complex' NormedGroup ℤ) : ℤ → NormedGroup
| -[1+n]  := 0
| 0       := coker (C.d (dtarget 0))
| (n+1:ℕ) := C.X (n+1)

def d (C : cochain_complex' NormedGroup ℤ) : ∀ {i j : ℤ} (h : Sc i = j), X C i ⟶ X C j
| -[1+n] _ _ := 0
| 0 1 rfl := coker.lift (d_squared_right C 1)
| (n+1 : ℕ) (m+1 : ℕ) h := C.d h

lemma d_squared' (C : cochain_complex' NormedGroup ℤ) :
  ∀ (i j k:ℤ) (hij : Sc i = j) (hjk : Sc j = k), d C hij ≫ d C hjk = 0
| -[1+n] _ _ _ _ := show 0 ≫ _ = 0, by rw zero_comp
| 0 1 2 rfl rfl := show coker.lift (d_squared_right C 1) ≫ C.d (dsource 1) = 0, from sorry -- provable
| (n+1:ℕ) (p+1:ℕ) (q+1:ℕ) hij hjk := C.d_squared' hij hjk

The equation compiler is doing some extraordinary things.

[Kevin Buzzard]

By "further than Johan" I just mean that I got the analogue of his line 37 sorry :-)

[Johan Commelin]

hah! that looks quite nice!

[Kevin Buzzard]

Should I press on or try to figure out how to prove this stuff like coker.lift >> f = 0?

[Kevin Buzzard]

Mathematically my sorry is this: we have C-1 -> C0 -> C1 exact, so we get a map coker(C-1->C0)->C1, and we want to prove that if you compose with C1 -> C2 you get zero. This follows because if you start with something in the coker you can compute its image in C1 by lifting to C0 and applying d, so the result follows from C0 -> C1 -> C2 being zero.

[Kevin Buzzard]

In short, the composite map (coker C-1 -> C0) -> C2 is zero because it is the lift of C0 -> C2 which is 0, so the result follows from uniqueness of lifts. Do we have this sort of thing?

[Kevin Buzzard]

Oh, I see exactly what we have, it's all in our repo, I had assumed it was in mathlib. Thanks Adam and Riccardo!

[Johan Commelin]

src/system_of_complexes/completion.lean now also compiles again on my experiment.
We might want to have a friendly wrapper for

 obtain ⟨i, rfl⟩ : ∃ i', i = i' + 1 := ⟨i-1, by linarith⟩, -- lowers `i` by one

[Johan Commelin]

I'm off to bed. If anyone wants to play around with jmc-complex, please go ahead. Despite the initials, I don't claim that branch (-;

[Adam Topaz]

I filled in one sorry, and I added the lemma that @Kevin Buzzard mentioned earlier (I hope I didn't duplicate Kevin's work here).

[Adam Topaz]

The lemma is here: https://github.com/leanprover-community/lean-liquid/blob/ed4cdd6bb95a9c491fb65f2b7bdf9cd24a68535c/src/normed_group/NormedGroup.lean#L183

and the filled sorry is here: https://github.com/leanprover-community/lean-liquid/blob/ed4cdd6bb95a9c491fb65f2b7bdf9cd24a68535c/src/system_of_complexes/soft_truncation.lean#L43

[Kevin Buzzard]

oh nice! I'm about to start on

/-
If this commutes
    A ----> B ---> E
    |       |      |
    |       |      |
   \/      \/      \/
    C ----> D ---> F

then so does this

coker (A → B) ----> E
   |                |
   | coker.map      |
   |                |
   \/               \/
coker (C → D) ----> F
-/
theorem domino {E F : NormedGroup.{u}}{fab : A ⟶ B} {fbd : B ⟶ D} {fac : A ⟶ C} {fcd : C ⟶ D}
  (h : fab ≫ fbd = fac ≫ fcd) {fbe : B ⟶ E} {fdf : D ⟶ F} {fef : E ⟶ F}
  (h2 : fbe ≫ fef = fbd ≫ fdf) : sorry := sorry

[Kevin Buzzard]

@Adam Topaz this is for the sorry in map_comm. I'm writing my own soft_truncation.lean in branch proof_that_succ_i_equals_j using a different definition of cochain_complex. But if it's not hard to fill in the sorrys in master's cochain_complex then we still don't really know which is best.

[Adam Topaz]

Oh, I jsut pushed that proof too :)

[Kevin Buzzard]

oh great!

[Adam Topaz]

https://github.com/leanprover-community/lean-liquid/blob/4151ab41f819db023b285bbfe202d79ce89a9022/src/normed_group/NormedGroup.lean#L183

[Adam Topaz]

Note the comment...

[Adam Topaz]

And now there are no sorry's in the soft truncation definition in Johan's branch

[Kevin Buzzard]

Oh nice! So it works!

[Adam Topaz]

Yeah, it works :)

[Adam Topaz]

Err, sorry I lied.

[Adam Topaz]

I didn't finish soft_truncation, just the inductive definitions above it

[Adam Topaz]

Well, all the "data" is there at least.

[Adam Topaz]

The proofs I gave for these coker lemmas are not very categorical. I'm using the fact that there are actually elements around (by using this coker.\pi_surjective trick)

[Adam Topaz]

Oh, and I just realized that this soft_truncationfile now has some universe-related errors at the bottom :(

[Kevin Buzzard]

I was going to ask that you took a look at the proofs I pushed, in case you could see any shortcuts or tidying.

[Adam Topaz]

Oh sure.

[Kevin Buzzard]

I've pushed the NormedGroup stuff to master, because we'll need it whatever design decisions are made about complexes, right? I'm assuming this soft_truncation thing is actually important?

[Adam Topaz]

I might try to refactor these with the epimorphism instance for coker.\pi that I just added. I like your proofs much more than mine, by the way!

[Adam Topaz]

But somehow this argument using surjectivity of \pi should be encapsulated in the epimorphism property.

[Kevin Buzzard]

OK so here is what the soft_truncation looks like with d {i} {j} (h : Succ i = j). I was really surprised by the equation compiler -- I was expecting to have far more cases to deal with. It's sorry-free but to go any further would require changing more definitions -- I've already written my own cochain_complex to get this far.

[Kevin Buzzard]

@Adam Topaz I filled in two sorries in the jmc-complex branch because the proofs were the same as the ones in my branch -- tidy found them for me and then I tidied them up. The last two sorrys in the file are I believe unprovable right now because as far as I can see there's nothing stopping a general complex misbehaving in negative degrees, which will stop it being <=k-exact in degrees <= m but won't stop the truncation being exact.

[Adam Topaz]

Yeah I think you're right. I guess the backward implication should be true (and the one we care about?)

[Adam Topaz]

Does tidy solve soft_truncation'_d_neg?

[Adam Topaz]

Or even rfl?

[Kevin Buzzard]

No, the definition of these things is by cases on the constructor for int so nothing unfolds until you have done cases on the int. Surely you need to start with something like this:

lemma soft_truncation'_d_neg (c : ℝ≥0) (i j : ℤ) (hi : i < 0) :
  ((soft_truncation'.obj C).d i j : (soft_truncation'.obj C) c i ⟶ _) = 0 :=
begin
  cases i,
  { exfalso, simp at hi, linarith },
  sorry
end

[Adam Topaz]

Oh, I see what's going on now. Yes it's more complicated since there's both an i and jinvolved and j can very well be positive.

[Kevin Buzzard]

I don't know anything about these systems of complexes, I didn't use them today.

[Adam Topaz]

If I recall correctly, d here is defined as the usual d if j is i+1 and 0 otherwise.

[Kevin Buzzard]

I couldn't find the exact form of that definition so I gave up :-)

[Kevin Buzzard]

I wanted to definitionally unwind everything but in the end I got lost trying to chase everything back

[Adam Topaz]

This is the definition:
https://github.com/leanprover-community/lean-liquid/blob/4e4f7d630e53a3f4ea08d6ef1359e5ecd2cbcece/src/system_of_complexes/complex.lean#L137

[Adam Topaz]

But it looks a bit complicated because Johan made one definition for both chain complexes and cochain complexes with this coherent_indices gadget

[Johan Commelin]

Thanks a lot for your help.

[Johan Commelin]

As far as I can see, everything works again, apart from normed_snake.lean

[Johan Commelin]

I'm getting some crazy timeouts there. We should probably split that proof into 3 or 4 pieces, if possible.

[Johan Commelin]

Everything compiles again!

[Johan Commelin]

I pushed to jmc-complex

[Kevin Buzzard]

I just want to remark that the coker stuff I pushed to master might result in a rather trivial conflict with that branch because I cut and pasted a lemma about maps between cokers commuting and gave it a docstring

[Johan Commelin]

I already merged it

[Kevin Buzzard]

I'm still very unclear about what the question is, or even if there is a question. It seems that both the jmc-conplex branch and the proof branch work fine

[Johan Commelin]

@Floris van Doorn I would be very interested in your feedback on https://github.com/leanprover-community/lean-liquid/blob/jmc-complex/src/system_of_complexes/complex.lean

[Kevin Buzzard]

I notice that in my complexes I had the following condition for d^2=0: I took as inputs i, j, k, a proof hij that j=succ(i) and a proof hjk that k=succ(j), and then I just asked that d hij o d hjk = 0, so I avoided eq_to_hom completely. Your differential objects need them. I am nervous about differential_object.differential because you don't have the flexibility to do this kind of thing.

[Kevin Buzzard]

On a related matter, I would like to have the following statement: a short exact sequence of complexes gives us a long exact sequence of cohomology, for R-modules. This is needed for flatness, it's needed for Amelia's MSc, and some variant is presumably needed for this project. Is the issue that we are still trying to figure out how best to state this?

[Adam Topaz]

Didn't Amelia (or another student of yours) define trinagulated categories? This might be the way to go.

[Kevin Buzzard]

Aah! Reading further ahead I see that your coherent_indices trick avoids the problem by asking for a proof that i = succ j, so I am much happier :-) Yes, someone else I think even made a PR for triangles in a category!

[Kevin Buzzard]

#6539 -- this is Luke's coursework for my course.

[Adam Topaz]

It should be fairly straightforward to define the homotopy category of chain complexes, and that's trinagulated.

[Adam Topaz]

(once we decide on the "correct" definition of chain complexes, of course!)

[Johan Commelin]

Kevin Buzzard said:

I notice that in my complexes I had the following condition for d^2=0: I took as inputs i, j, k, a proof hij that j=succ(i) and a proof hjk that k=succ(j), and then I just asked that d hij o d hjk = 0, so I avoided eq_to_hom completely. Your differential objects need them. I am nervous about differential_object.differential because you don't have the flexibility to do this kind of thing.

I agree that we might want to have some other constructors that give more flexibility, specially for chain_complex and cochain_complex.

[Johan Commelin]

This definition is made in such a way that those two specializations have a common backend, which allows us to prove things just once.

[Johan Commelin]

Kevin Buzzard said:

#6539 -- this is Luke's coursework for my course.

Wow, this is cool. Let's review this and build upon it!

[Floris van Doorn]

@Johan Commelin I'm worried about the explicit mention of eq_to_hom in the definition of differential_object. I see that you have to do quite some rewriting with properties about eq_to_hom, and I think that will get annoying quickly. Oh, but as you said, you could write constructors for differential_object specific to chain_complex or cochain_complex.

You will also have to deal with the fact that e.g. differential_object ℤ (+1) 0 and differential_object ℤ 0 (-1) are isomorphic but not equal. But I think you will have to deal with that in any definition. Even if a definition doesn't really see the distinction, like in Kevin's definition in his example earlier this thread, or in my Lean 2 definition, you still have to deal with it. You might start with a family of maps that naturally go from X n -> X (n-1) or another family of maps that is defined so that it has type X (n+1) -> X n, and you have to put them both in the definition of differential_object. In Lean 2, I did this my defining different kind of constructors, depending on the type of the maps (https://github.com/cmu-phil/Spectral/blob/master/algebra/graded.hlean#L106-L122).

I like the trick you do with coherent_indices, that might be a nice way to deal with the fact that you don't have to provide proofs of equality every time (at least, in the statement of theorems).

This looks like a fine way of doing it, and something we can build enough bells and whistles (constructors, computation rules) around that makes working with it possible. I also like Kevin's definition in this thread, but it might be nicer to work with the coherent_indices predicate, so that we don't have to apply each differential to an equality.

Question: is there a reason why you things in terms of differential_object' instead of the more general differential_object (without a prime)? That last one is more general, and would be useful because it also captures the notion of graded objects / graded morphism of degrees other than +1/-1, right?

[Kevin Buzzard]

@Floris van Doorn
Right now mathematically a major thing we are missing is complexes of R-modules indexed by the integers. If we have a working theory for these, and also for the theory of complexes of R-modules indexed by the naturals, and also for the theory of complexes of R-modules indexed by fin 3 x int then we will be able to do a lot of new stuff, starting with the statement of the long exact sequence of cohomology associated to a short exact sequence of complexes. More generally we would like all these for abelian categories, but I am unclear about whether this is too much to ask right now because diagram chasing (i.e. the actual proof) in a non-concrete category is hard right now because we don't have this Freyd representation theorem saying that every abelian category is a full subcategory of an appropriate concrete category (usually R-modules or Ab) and apparently we lack the tactics/infrastructure to work directly with the axioms of an abelian category.

[Scott Morrison]

Regarding working directly with an abelian category, it might be worth having at look at #6308 (constructing the normalized Moore complex from a simplicial object in an abelian category). It works with intersections of kernels of a bunch of maps, and I think is fairly ergonomic. Of course it is not an example of a diagram-chase argument.

[Johan Commelin]

@Floris van Doorn Thanks a lot for all the feedback. Regarding the final question: I didn't see how to generalise to differential_object, so I worked with differential_object' instead.

[Johan Commelin]

I'm thinking about the following renames:

differential_object  -> predifferential_object
differential_object' -> differential_object

[Johan Commelin]

How do people feel about merging this branch into master?

[Johan Commelin]

I personally think that the experiment is 100% over, but on the other hand, further experimentation can be done on master

[Johan Commelin]

And I don't really want to start making progress on 9.6 on this branch, because that's not the purpose of this branch

[Kevin Buzzard]

If you're happy with it, let's merge. We can go on forever coming up with new tests or alternative ways of doing things. The big question with any definition is "is it possible to make enough basic API for mathematicians to be able to take over?" and once you've found a set-up for which the answer is "yes", this will do.

[Johan Commelin]

Ok, I merged the branch

[Johan Commelin]

So jmc-complex is now officially EOL

[Johan Commelin]

As things go... after merging I realised what the correct :tm: definition is.

[Johan Commelin]

I claim that this is the underlying structure that we want to prove a lot of things about:

structure differential_object (ι : Type) (V : Type*) [category V] [has_zero_morphisms V] :=
(X : ι → V)
(d : Π i j, X i ⟶ X j)
(d_comp_d : ∀ i j k, d i j ≫ d j k = 0)

[Johan Commelin]

Difference with the previous def:

• no mention of S0 or S1
• no eq_to_hom
• this d can be used immediately, no sugar on top

[Johan Commelin]

This even allows us to use $\Z \times \Z$ as indexing object, and get double complexes out of it.

[Johan Commelin]

No mention of succ or pred or whatever

[Johan Commelin]

Ooh, wait, I retract the comment about double complexes

[Johan Commelin]

Because d_comp_d is false there

[Johan Commelin]

So maybe I will remove that axiom!

[Johan Commelin]

We can add it on top later, when we specialize to subcategories of (co)chain complexes etc

[Sebastien Gouezel]

If instead you use

structure differential_object {ι : Type} (V : Type*) (X : ι → V) [category V] [has_zero_morphisms V] :=
(d : Π i j, X i ⟶ X j)
(d_comp_d : ∀ i j k, d i j ≫ d j k = 0)

then a double complex would share the same V and X, but it would have two ds, the horizontal one and the vertical one, and each of these would satisfy the d_comp_d axiom.

[Johan Commelin]

@Sebastien Gouezel that is true, but then it is unbundled. Not sure what's best

[Sebastien Gouezel]

Right. I'd say it's probably best to do bundled, because things like spectral sequences will be much easier like that.

[Kevin Buzzard]

I was just considering the Hochschild-Serre spectral sequence when preparing my workshop for this week, which is going to be on group cohomology. I honestly think that group cohomology is a wonderful test case for complexes (and right now I am even wondering if it all works for monoid cohomology). I know exactly how to set it up having supervised two projects in the area and learnt from my mistakes. I will be doing the "low degree" version on Thursday which does not need complexes, but the "general degree" version does and it seems to me like a very natural goal. When my talk is done I might spend some time making one of those GitHub projects in order to flesh out my ideas.

[Filippo A. E. Nuccio]

@Kevin Buzzard Will you be broadcasting the workshop? On Discord?

[Kevin Buzzard]

Yes, it's 1600-1800 London time on the Discord

[Johan Commelin]

I just merged another refactor of complexes. Hopefully this doesn't establish a pattern...

[Johan Commelin]

But this time, there are very few eq_to_homs, even under the hood.

[Johan Commelin]

@Scott Morrison @Floris van Doorn If you could take another look, that would be great. If you like this design, I think we should move it to mathlib.

[Scott Morrison]

@Johan Commelin,

Let me see if I have this right. In this definition of differential_object, we have a d i j from X i to X j, for every i j. Moreover we ask immediately that d i j \gg d j k = d i k.

(First of all, it definitely needs a different name: differential_object is a standard name in real maths.)

This gadget is almost, but not quite, a functor from indiscrete I to the target category, where indiscrete is a not-yet-existing type synonym that puts a single morphism between every pair of objects. The reason it isn't a functor is that we don't want to insist that d i i is the identity. So it's only a semifunctor between semicategorys.

As a second step, when we want to define chain_complex or cochain_complex (either nat or int indexed), we pass to the full subcategory of differential_object where some specified collection of the d i j are zero (e.g. only if j = i + 1 can it be nonzero).

I don't really understand what @Kevin Buzzard has been doing on ses_to_les. Showing that differential_object has equalizers or images or something doesn't seem to serve much purpose: because you'll still need to do separate work to build these again in the subcategory; possibly the main bit of the work?

(That said, I suspect that a big chunk of the theory of limits works perfectly well for semicategories, and it even seems plausible that if V has limits, semifunctors J \func V does too...?)

It seemed like there was a proposal to define the homology functor right at the level of differential_object, but I don't see what the intention is here. You can talk about the intersections of all the kernels of d i j as j varies, and the union of all the images of d k i as k varies, but the image union won't sit in the kernel intersection.

Help?

[Kevin Buzzard]

I don't think d i j >> d j k is defined to be anything initially. Very early on we define it to be 0. The idea is that all d i j if j isn't i + 1 are supposed to be 0 (including d i i).

[Kevin Buzzard]

In an abelian category you could talk about the join of all the images. But I'm not sure this is the way to go. I think I've understood all this a bit better now -- I started a thread in #maths about it

[Scott Morrison]

Oh, okay, I woke up confused. Yes, I agree the stuff about semifunctoriality is not what Johan had in mind, and is not in the definition.

[Kevin Buzzard]

I don't know whether to continue here on in #maths. I agree that my stuff on the branch is problematic, I had not realised this issue about how we might have to do a whole bunch of stuff again but now I fear you're right.

[Johan Commelin]

@Scott Morrison I'm open to changing things that don't work well. In particular, I'm very much in favour of changing the name.

[Johan Commelin]

I think that it's important that d i i is not the identity.

[Johan Commelin]

And it would be great if we can model both chain and cochain complexes together, somehow.

[Scott Morrison]

Yes, sorry, me saying d i i should be the identity was me being very confused.

[Johan Commelin]

Do you have a suggestion for a new name?

[Scott Morrison]

I was tempted by something like pre_dgo. It's not yet a dgo = "differential graded object", because the differential and the grading don't see each other.

[Kevin Buzzard]

Another thing I don't know is how to define the boundary map in a non concrete setting. You have four short exact sequences An-> Bn -> Cn (horizontal) in a complex (vertical, 0<= n<= 3) and you have something in the Ker/im subquotient of C2. Now lift to B2 by instantiating an exists, push to B3 and lift to A3 instantiating another one. For R-mod the epis are surjections and you can just do it with choice. I'm assuming there's a way to do it from the category axioms but I don't see it yet

[Johan Commelin]

pre_dgo

sounds like just the right level of obfuscation for these obscure objects (-;

[Johan Commelin]

@Kevin Buzzard s/situations/surjections/ auto-complete-fail?

[Kevin Buzzard]

Graded object -- in all sensible cases the d map respects the grading if you allow a twist of your index set

[Kevin Buzzard]

If we go for this d^2=0 model with one d then we're ruling out double complexes anyway. There we need two d 's and the axiom that they commute...wait, that isn't even true :-( a sensible d1d2 from A i j to B i+1 j+1 isn'ta silly d2d1

[Bhavik Mehta]

This sounds like exactly the sort of thing Markus gave us pseudoelements to do

[Kevin Buzzard]

I thought that pseudoelements were just homs from a random object? The problem is that Z/4 -> Z/2 is a surjection in the category of abelian groups but this unfortunately doesn't mean that Hom(X,Z/4) -> Hom(X,Z/2) is a surjection, e.g. if X=Z/2 then this map is the zero map and doesn't hit the identity. I'm just asking how to state the snake lemma in an arbitrary abelian category basically. I don't see how to define the boundary map from ker(f3) to coker(f1) in a non-concrete setting.

[Adam Topaz]

I think using monos and epis

[Adam Topaz]

And for the boundary map, yeah, map into the diagram from some random object and use the mono/epi property of the morphisms involved

[Adam Topaz]

@Bhavik Mehta maybe we should formalize the Freyd embedding theorem?

[Kevin Buzzard]

but epi doesn't imply surjection on hom sets -- if A -> B is epi then Hom(X,A) -> hom(X,B) might not be a surjection. I don't see how to start with this boundary map right now.

[Adam Topaz]

I'm just thinking of the usual snake lemma, no Hom(X,Y) involved there.

[Kevin Buzzard]

I need to define a map from ker(f3) to coker(f1). How do I even start? This is what I'm missing

[Adam Topaz]

Take ker (f3) to be the "test object" (the object you're mapping from)

[Bhavik Mehta]

Kevin I think you're thinking of generalised elements rather than pseudoelements

[Adam Topaz]

Then chase around what happens to the identity morphism on ker f3.

[Bhavik Mehta]

docs#category_theory.abelian.pseudoelements

[Bhavik Mehta]

Also if @Markus Himmel is about, I think he could give much more helpful answers

[Kevin Buzzard]

Adam Topaz said:

Then chase around what happens to the identity morphism on ker f3.

I don't understand what this means. I don't know the "initial move" right now.

[Kevin Buzzard]

/-- An epimorphism is surjective on pseudoelements. -/
theorem pseudo_surjective_of_epi {P Q : C} (f : P ⟶ Q) [epi f] : function.surjective f :=

What is this black magic?

[Adam Topaz]

That's the definition of epi :)

[Bhavik Mehta]

There's a coe from morphisms to functions on pseudoelements, and that function is surj iff the morphism is epi

[Peter Scholze]

I don't know what pseudoelements are, but one way to think about this is that you take $\mathrm{Hom}$'s from some test object $X$, but you allow yourself to replace $X$ by anything mapping surjectively onto it, at will

[Kevin Buzzard]

Yes, this seems to be the pseudoelement trick

[Peter Scholze]

(Formally, there are enough projective objects in the pro-category, but this is surely overkill)

[Kevin Buzzard]

so I just replace ker(f3) by ker(f2) for example, which maps to B2.

[Kevin Buzzard]

A classic application of pseudoelements are diagram lemmas like the four lemma or the snake lemma.

@Bhavik Mehta do you know if Markus did the snake lemma? I think I need it for some class of categories e.g. abelian categories, I mean, I need it for R-modules, but I think Johan already hacked out a proof of that a long time ago -- I would rather prove it in an abelian category (once I've figured out how to define the boundary map!)

[Markus Himmel]

I did the snake lemma, but it didn't make it into mathlib

[Kevin Buzzard]

Boundary map: I end up with some object A which surjects onto ker(f3) and also maps to coker(f1). I guess now I need to prove some results which says that something factors through something but I see how to do it now.

[Kevin Buzzard]

Where is it? I might be able to mathlib it up.

[Kevin Buzzard]

I've just this minute understood how to state it :-)

[Adam Topaz]

Kevin, if X is the top-right element in the diagram for the snake lemma, and f3is the map down from it, you probably want the map ker(f3) -> X as your "test object"

[Adam Topaz]

Does zulip do tikz?

[Kevin Buzzard]

yes I see how to do it all now

[Markus Himmel]

It's here but it's far from pretty

[Adam Topaz]

\begin{tikzcd} A \ar[r] & B \end{tikzcd}

[Kevin Buzzard]

It's A1 -> B1 -> C1 above A2 -> B2 -> C2 with maps f1, f2, f3 :-)

[Bhavik Mehta]

Adam Topaz said:

Bhavik Mehta maybe we should formalize the Freyd embedding theorem?

About this, I remember @Markus Himmel saying this was too hard at the time, but now that there's renewed interest and need in this, do you think it's feasible if a bunch of us work on it? If so, do you have an idea of what approaches would be cleanest?

[Peter Scholze]

Actually, would this even help in the case of the snake lemma? You wouldn't want the construction of the map to depend on an embedding into a category of modules

[Peter Scholze]

And I think the construction of the map should be the most tedious part of this

[Kevin Buzzard]

The pseudoelement construction of the map goes like this: if 0 -> A1 -> B1 -> C1 -> 0 and same for 2 and we have maps down fA, fB, fC, then the crucial definition is X := B1 x_{B2} A2, which maps to C1 and to coker(fA), and one checks that X -> C1 is surjective and its kernel is mapped to zero in coker(fA), so X induces a map C1 -> coker(fA).

[Peter Scholze]

I think you should also take a fibre product over C_1 with the kernel of fC?

[Kevin Buzzard]

sorry you're right, I switched notation between pen and typing :-/ X maps to ker(C1) is surjective, but to get the map you should pull back again.

[Johan Commelin]

New style complexes and homotopies are in mathlib!!!

[Johan Commelin]

@Scott Morrison I think that maybe the comm' field in hom is stated in the wrong direction compared to nat_trans.naturality. Because now we need

def mul_one_iso : (mul 1).obj BD ≅ BD :=
homological_complex.iso_of_components (λ i, FreeMat.one_mul_iso.app _) $
λ i j, (FreeMat.one_mul_iso.hom.naturality (BD.d i j)).symm
-- notice the `.symm` at the end of the previous line

[Johan Commelin]

Another bug:

src/category_theory/limits/shapes/zero.lean
180:localized "attribute [instance] has_zero_object.has_zero" in zero_object
181:localized "attribute [instance] has_zero_object.unique_to" in zero_object
182:localized "attribute [instance] has_zero_object.unique_from" in zero_object

these should use fully qualified names

[Johan Commelin]

Ooh, and this is a more serious bug:

-- #check @homotopy
homotopy :
  Π {ι : Type u_3} {V : Type u_2} [_inst_1 : category V] [_inst_2 : has_zero_object V]
  [_inst_3 : category_theory.preadditive V] {c : complex_shape ι} {C D : homological_complex V c},
    (C ⟶ D) → (C ⟶ D) → Type (max u_3 u_1)

The definition of homotopy requires has_zero_object whereas it should only ask for zero morphisms. The category FreeMat doesn't have a zero object.

[Johan Commelin]

I've pushed what I've done so far (not so much) to homological-refactor

[Johan Commelin]

#7619 fixes the locale issue

[Adam Topaz]

Johan Commelin said:

Ooh, and this is a more serious bug:

-- #check @homotopy
homotopy :
  Π {ι : Type u_3} {V : Type u_2} [_inst_1 : category V] [_inst_2 : has_zero_object V]
  [_inst_3 : category_theory.preadditive V] {c : complex_shape ι} {C D : homological_complex V c},
    (C ⟶ D) → (C ⟶ D) → Type (max u_3 u_1)

The definition of homotopy requires has_zero_object whereas it should only ask for zero morphisms. The category FreeMat doesn't have a zero object.

I think you need preadditive for homotopy. But you're right, it shouldn't require zero objects

[Johan Commelin]

The way it is currently set-up it fundamentally uses zero objects in some aux definitions.

[Adam Topaz]

oof

[Johan Commelin]

It's not just weakening the type class and we're good to go. We'll really need to tweak some code.

[Adam Topaz]

Oh I see... you need zero objects for X_next and its friends

[Adam Topaz]

So we can only talk about the next and previous objects when we have zero objects. That's an issue all in itself isn't it?

[Johan Commelin]

Yes, I think so.

[Adam Topaz]

Well, I guess we have C.next which gives option ...

[Johan Commelin]

For nat-indexed complexes with objects in a category without zero object we are basically stuck

[Johan Commelin]

Aha, so we need to take option more serious

[Adam Topaz]

Yeah, we can change the definition of homotopy.comm to match on some option type, but that will get tedious really quickly

[Johan Commelin]

I think there are two options: state 4 (?) conditions, that deal with all the edge cases,
or turn $h_i \circ d_i$ into a new definition, and make this 0 whenever $h_i$ is not defined

[Adam Topaz]

Oh that's a good idea!

[Adam Topaz]

The one with $h_i \circ d_i$ I mean

[Adam Topaz]

Quick sketch--

def d_next (f : Π i j, C.X i ⟶ D.X j) (i : ι) : C.X i ⟶ D.X i :=
match c.next i with
| none := 0
| some ⟨i',w⟩ := C.d _ _ ≫ f i' i
end

def prev_d (f : Π i j, C.X i ⟶ D.X j) (j : ι) : C.X j ⟶ D.X j :=
match c.prev j with
| none := 0
| some ⟨j',w⟩ := f j j' ≫ D.d _ _
end

/--
A homotopy `h` between chain maps `f` and `g` consists of components `h i j : C.X i ⟶ D.X j`
which are zero unless `c.rel j i`, satisfying the homotopy condition.
-/
@[ext, nolint has_inhabited_instance]
structure homotopy (f g : C ⟶ D) :=
(hom : Π i j, C.X i ⟶ D.X j)
(zero' : ∀ i j, ¬ c.rel j i → hom i j = 0 . obviously)
(comm' : ∀ i, f.f i = d_next hom _ + prev_d hom _ . obviously')

[Adam Topaz]

I have to go for now, but I'll try to play with this defn later

[Johan Commelin]

:rofl: why a line break in comm'? The condition is now really short... :rofl:

[Johan Commelin]

I think I like this idea. It's quite close to the informal justifications that we give when someone asks about the edge conditions.

[Adam Topaz]

Sorry, the above is wrong -- we need this:

@[ext, nolint has_inhabited_instance]
structure homotopy (f g : C ⟶ D) :=
(hom : Π i j, C.X i ⟶ D.X j)
(zero' : ∀ i j, ¬ c.rel j i → hom i j = 0 . obviously)
(comm' : ∀ i, f.f i - g.f i = d_next hom _ + prev_d hom _ . obviously')

[Adam Topaz]

( I deleted too much :) )

[Adam Topaz]

Modulo a couple of sorry's and some linting that needs to be done, here's a branch with the fix to homotopy: branch#homotopy_fix

[Adam Topaz]

I don't know how this affects all the other PRs though...

[Adam Topaz]

@Scott Morrison @Johan Commelin please feel free to adopt and/or do whatever you want with this branch!

[Johan Commelin]

I think @Scott Morrison is the only one with a clear overview of how this will affect the other PRs

[Scott Morrison]

Okay, I've fixed a few sorries. You changed the term order in comm', so I'm updating some things in the inductive constructions to match that, but may end up flipping the term order back later.

[Scott Morrison]

I'll try the last sorry now, then try it out in branch#homotopy_category. If it works okay there (it should) everything else will probably be fine.

[Scott Morrison]

This is a nice fix, @Adam Topaz!

[Scott Morrison]

It seems there's more work required to restore the proof of homology_map_eq_of_homotopy in this branch.

[Scott Morrison]

We need to be able to see easily that d_next factors through d_from (which is the case whether these are zero or not).

[Scott Morrison]

Okay, I've dealt with this.

[Scott Morrison]

branch#homotopy_category works with no changes, so I've just merged this branch into that.

[Scott Morrison]

@Adam Topaz, do you want to make branch#homotopy_fix a separate PR, and I'll add the dependency?

[Adam Topaz]

Sure, that works! I won't be able to open the PR tonight, but I can probably do it at some point tomorrow, or you could open the PR now if you have time.

[Scott Morrison]

#7621

[Scott Morrison]

@Johan Commelin, a way above in this thread you said FreeMat doesn't have a zero object. Surely Free k (Mat R) (not that we actually have that yet, sorry) has a zero object. (Err... the zero-ary direct sum? not sure what to call it besides the zero object!) Am I being confused?

[Johan Commelin]

Another minor bug: homotopy is not in the category_theory namespace. I guess that _root_.homotopy deserves to be reserved for homotopies in topology.

[Johan Commelin]

Another small bug:

-- move to mathlib
attribute [simps] homotopy.refl homotopy.symm homotopy.trans homotopy.comp_left homotopy.comp_right

[Scott Morrison]

I don't think we should put anything about homological algebra in the category_theory namespace. If we need to disambiguate two versions of homotopy lets use homological_algebra.homotopy or homology.homotopy or topology.homotopy or continuous_map.homotopy.

[Johan Commelin]

homological_complex.homotopy?

[Johan Commelin]

So, we merged the homotopy fix that uses d_next and prev_d. But now I'm wondering if the following hack would be too evil to pass up:

def complex_shape.next' (i) :=
match c.next i with
| none := i
| some \<j,w\> := j

etc...
Then we can still write "the usual homotopy condition", using hom i (c.prev' i) and hom (c.next' i) i. But for the edge cases these will become "vertical" homotopy maps composed with "stationary" differentials. Those compositions will be 0 for two reasons :smiley:

[Johan Commelin]

The branch homological-refactor compiles again, but I've sorried 4 proofs:

1       src/normed_spectral.lean
1       src/thm95/homotopy.lean
1       src/thm95/default.lean
10      src/thm95/constants.lean
1       src/locally_constant/SemiNormedGroup.lean
1       src/prop_92/prop_92.lean
2       src/prop_92/concrete.lean
1       src/breen_deligne/eg.lean
1       src/pseudo_normed_group/system_of_complexes.lean
Total:  19

[Johan Commelin]

Once those are fixed, I'll merge into master

[Johan Commelin]

I'm now porting the last file in the homological refactor, which had to wait for another mathlib PR.

[Johan Commelin]

After that LTE old style chain complexes can be forcefully kicked out of the project. So long, and thanks for all the fish!

[Johan Commelin]

It also means that the blueprint will compile again. Right now it is upset that there are two notions of chain complex in the project.

[Johan Commelin]

ooh, that went really smooth. 800 lines less in the project

[Peter Scholze]

What's the current de Bruijn factor of LTE?

[Kevin Buzzard]

What happens when you say "by a well known result this monoid is finitely generated" and we write 1000 lines justifying this? I've never really understood that bit of the de Bruijn story

[Peter Scholze]

Good question. Is Gordan's lemma part of mathlib? I think it should be. Everything that ends in mathlib shouldn't count towards the de Bruijn factor

[Johan Commelin]

$ git ls-files | rg "[.]tex" | rg -v web | rg -v macros | xargs wc
  294  1333 10790 src/CLC.tex
   84   329  2628 src/Mbar.tex
   61    76  1559 src/blueprint.tex
  375  1629 12449 src/breen_deligne.tex
   22    65   549 src/content.tex
  117   777  5853 src/homotopies.tex
   96   487  3779 src/normed_groups.tex
  578  3280 24037 src/normed_homological.tex
  234  1033  8196 src/polyhedral_lattice.tex
  331  1877 14912 src/proof.tex
 2192 10886 84752 total

[Johan Commelin]

The numbers are lines, words, characters

[Johan Commelin]

For the Lean repo we get (excluding for_mathlib)

 15462  94994 603189 total

[Kevin Buzzard]

Freek likes to compress the files (TeX and Lean) and compare lengths afterwards. And maybe ignoring for_mathlib is OK.

[Johan Commelin]

I agree that a proper comparison should first compress everything

[Kevin Buzzard]

Maybe comparing the blueprint with the repo is a more reasonable thing than comparing the relevant parts of the paper

[Johan Commelin]

@Peter Scholze But we aren't done yet...

[Peter Scholze]

Yes, but I'd be surprised if this changes by another factor of 2 :wink:

[Johan Commelin]

True

[Patrick Massot]

About this factor, I should point out that, in Lemma 9.2, the most Lean-consuming line is clearly "We first note that any locally constant function $\varphi ∈ V(M_{\leq r'c}^a)$ can be extended to a locally constant function $\bar \varphi ∈ V(M_{\leq c}^a)$ with the same norm". This took much more work than juggling with sums and norm estimates.

[Adam Topaz]

#7651 and #7656 (both merged) can be used to get rid of for_mathlib/simplicial/right_op.lean. I can do it later today, but just thought I would mention it in case anyone is already doing some cleaning up

[Johan Commelin]

I did half of it

[Adam Topaz]

Which half is left?

[Johan Commelin]

I only removed the first bit.

[Johan Commelin]

Because Lean told me it already existed, when I bumped mathlib

[Adam Topaz]

Oh :smile:

[Adam Topaz]

Okay, for_mathlib/simplicial/right_op.lean is no more.

[Johan Commelin]

I think we should have some (co)chain_complex.mk_hom_of that says you only need to check commutativity of squares. That would play nice with (co)chain_complex.of

[Johan Commelin]

But it shouldn't assume that the complexes are constructed using .of

[Adam Topaz]

We have it... docs#cochain_complex.of_hom

[Adam Topaz]

Some of the code in for_mathlib/simplicial/complex can be simplified using this

[Adam Topaz]

Ah sorry, that assumes they're constructed using of

[Adam Topaz]

docs#cochain_complex.augment can also be useful

[Johan Commelin]

Adam Topaz said:

We have it... docs#cochain_complex.of_hom

But this one does assume that the complexes are constructed using .of

[Johan Commelin]

Ooh, you already said that :face_palm:

[Adam Topaz]

Do we have any complexes not constructed using .of in LTE?

[Johan Commelin]

Yeah, complexes constructed using .of but then pushed through 5 functors

[Adam Topaz]

Right

[Adam Topaz]

We probably also need a construction saying that any complex is isomorphic to .of of something

[Johan Commelin]

#7666 is fixes the problem of hom_of by adding c.rel i j as condition to hom.comm'.
Instead of restate_axiom hom.comm' I then state hom.comm without c.rel i j.
Upshot: when using hom.comm you don't need the assumption, but when you need to verify the axiom you get the extra assumption.

[Johan Commelin]

#7673 does the same for d_comp_d'