## Stream: condensed mathematics

### Topic: complexes, d, dtt

#### Johan Commelin (Mar 05 2021 at 06:48):

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 (Mar 05 2021 at 06:49):

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

#### Johan Commelin (Mar 05 2021 at 06:49):

d_comp_d is true without any proof obligations

#### Johan Commelin (Mar 05 2021 at 06:49):

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

#### Johan Commelin (Mar 05 2021 at 06:52):

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 (Mar 05 2021 at 06:53):

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 (Mar 05 2021 at 08:32):

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 (Mar 05 2021 at 08:33):

soft_truncation.lean is a nice test case

#### Kevin Buzzard (Mar 05 2021 at 08:33):

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

#### Kevin Buzzard (Mar 05 2021 at 08:34):

(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 (Mar 05 2021 at 08:34):

It's in src/

#### Johan Commelin (Mar 05 2021 at 08:34):

and full of sorrys

#### Johan Commelin (Mar 05 2021 at 08:35):

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

#### Johan Commelin (Mar 05 2021 at 08:35):

And those proofs are all boring and distracting

#### Johan Commelin (Mar 05 2021 at 08:35):

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

#### Johan Commelin (Mar 05 2021 at 08:35):

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

#### Kevin Buzzard (Mar 05 2021 at 08:36):

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 (Mar 05 2021 at 08:39):

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 (Mar 05 2021 at 08:39):

No! I'm not using mathlibs version

#### Johan Commelin (Mar 05 2021 at 08:39):

Sorry for the confusion

#### Johan Commelin (Mar 05 2021 at 08:40):

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

#### Kevin Buzzard (Mar 05 2021 at 08:40):

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

Yes

#### Johan Commelin (Mar 05 2021 at 08:40):

but it doesn't use my top post yet

#### Johan Commelin (Mar 05 2021 at 08:41):

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

#### Kevin Buzzard (Mar 05 2021 at 08:45):

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 (Mar 05 2021 at 08:46):

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 (Mar 05 2021 at 08:50):

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 (Mar 05 2021 at 08:50):

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 (Mar 05 2021 at 08:50):

@Kevin Buzzard yes, that challenge sounds about right

#### Johan Commelin (Mar 05 2021 at 08:50):

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

#### Johan Commelin (Mar 05 2021 at 08:51):

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

#### Johan Commelin (Mar 05 2021 at 08:51):

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

#### Johan Commelin (Mar 05 2021 at 08:52):

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

#### Johan Commelin (Mar 05 2021 at 08:53):

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 (Mar 05 2021 at 08:53):

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 (Mar 05 2021 at 08:53):

But designing a good test suite is hard

#### Kevin Buzzard (Mar 05 2021 at 08:53):

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

#### Johan Commelin (Mar 05 2021 at 08:53):

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 (Mar 05 2021 at 08:54):

And it worked? So what is the problem?

#### Johan Commelin (Mar 05 2021 at 08:54):

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

#### Kevin Buzzard (Mar 05 2021 at 08:54):

I don't understand what you mean.

#### Kevin Buzzard (Mar 05 2021 at 08:54):

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

#### Johan Commelin (Mar 05 2021 at 08:55):

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

I don't know.

#### Kevin Buzzard (Mar 05 2021 at 08:55):

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.

I understand

#### Johan Commelin (Mar 05 2021 at 08:56):

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

#### Kevin Buzzard (Mar 05 2021 at 08:56):

OK then maybe I am asking for too much.

#### Johan Commelin (Mar 05 2021 at 08:56):

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

#### Johan Commelin (Mar 05 2021 at 08:57):

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

#### Kevin Buzzard (Mar 05 2021 at 08:57):

OK so let's go back to that file.

#### Johan Commelin (Mar 05 2021 at 08:57):

So I want something better.

#### Johan Commelin (Mar 05 2021 at 08:57):

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 (Mar 05 2021 at 08:57):

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

#### Kevin Buzzard (Mar 05 2021 at 08:58):

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

#### Kevin Buzzard (Mar 05 2021 at 08:59):

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

#### Kevin Buzzard (Mar 05 2021 at 09:00):

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

#### Johan Commelin (Mar 05 2021 at 09:00):

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 (Mar 05 2021 at 09:01):

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

#### Kevin Buzzard (Mar 05 2021 at 09:01):

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 (Mar 05 2021 at 09:01):

I agree that the succ idea is brilliant.

#### Johan Commelin (Mar 05 2021 at 09:03):

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

#### Kevin Buzzard (Mar 05 2021 at 09:03):

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

#### Kevin Buzzard (Mar 05 2021 at 09:07):

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 (Mar 05 2021 at 09:09):

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 (Mar 05 2021 at 09:10):

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

#### Johan Commelin (Mar 05 2021 at 09:11):

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

#### Johan Commelin (Mar 05 2021 at 09:12):

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

#### Johan Commelin (Mar 05 2021 at 09:12):

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

#### Johan Commelin (Mar 05 2021 at 09:12):

API theorems? Or the big goal?

#### Mario Carneiro (Mar 05 2021 at 09:13):

Something that has DTT hell issues

#### Mario Carneiro (Mar 05 2021 at 09:13):

probably not the big goal

#### Johan Commelin (Mar 05 2021 at 09:14):

Ok, soft_truncation has those

#### Johan Commelin (Mar 05 2021 at 09:15):

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

#### Johan Commelin (Mar 05 2021 at 09:16):

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

#### Johan Commelin (Mar 05 2021 at 09:17):

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

#### Mario Carneiro (Mar 05 2021 at 09:17):

Complete proofs are fine, especially if the result is unsatisfactory

#### Johan Commelin (Mar 05 2021 at 09:21):

First sorry is on line 37 :rofl:

#### Johan Commelin (Mar 05 2021 at 09:21):

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

#### Johan Commelin (Mar 05 2021 at 09:55):

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),
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 (Mar 05 2021 at 09:55): 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 (Mar 05 2021 at 09:56):

In particular the entire of_shift lemma is no longer needed

#### Johan Commelin (Mar 05 2021 at 09:56):

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

#### Johan Commelin (Mar 05 2021 at 10:02):

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

#### Riccardo Brasca (Mar 05 2021 at 10:38):

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 (Mar 05 2021 at 10:45):

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

#### Johan Commelin (Mar 05 2021 at 10:45):

Namely going from weak exactness to strong exactness

#### Riccardo Brasca (Mar 05 2021 at 11:21):

yes, in that lemma there are some i-1

#### Kevin Buzzard (Mar 05 2021 at 12:33):

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 (Mar 05 2021 at 12:39):

No, I agree with Sebastien

#### Johan Commelin (Mar 05 2021 at 12:40):

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

#### Johan Commelin (Mar 05 2021 at 12:40):

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

#### Kevin Buzzard (Mar 05 2021 at 12:42):

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 (Mar 05 2021 at 12:43):

We need with_neg_one_nat ;-)

#### Sebastien Gouezel (Mar 05 2021 at 12:44):

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 (Mar 05 2021 at 13:14):

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 (Mar 05 2021 at 13:14):

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

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 (Mar 05 2021 at 13:20):

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

#### Johan Commelin (Mar 05 2021 at 13:26):

hah! that looks quite nice!

#### Kevin Buzzard (Mar 05 2021 at 13:28):

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

#### Kevin Buzzard (Mar 05 2021 at 13:31):

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 (Mar 05 2021 at 13:32):

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 (Mar 05 2021 at 13:35):

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 (Mar 05 2021 at 15:42):

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 (Mar 05 2021 at 20:59):

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 (Mar 05 2021 at 21:32):

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).

#### Kevin Buzzard (Mar 05 2021 at 21:58):

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 (Mar 05 2021 at 21:59):

@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 (Mar 05 2021 at 22:00):

Oh, I jsut pushed that proof too :)

oh great!

#### Adam Topaz (Mar 05 2021 at 22:00):

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

#### Adam Topaz (Mar 05 2021 at 22:00):

Note the comment...

#### Adam Topaz (Mar 05 2021 at 22:01):

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

#### Kevin Buzzard (Mar 05 2021 at 22:03):

Oh nice! So it works!

#### Adam Topaz (Mar 05 2021 at 22:03):

Yeah, it works :)

#### Adam Topaz (Mar 05 2021 at 22:03):

Err, sorry I lied.

#### Adam Topaz (Mar 05 2021 at 22:04):

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

#### Adam Topaz (Mar 05 2021 at 22:04):

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

#### Adam Topaz (Mar 05 2021 at 22:06):

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 (Mar 05 2021 at 22:08):

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

#### Kevin Buzzard (Mar 05 2021 at 22:08):

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

Oh sure.

#### Kevin Buzzard (Mar 05 2021 at 22:10):

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 (Mar 05 2021 at 22:22):

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 (Mar 05 2021 at 22:22):

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

#### Kevin Buzzard (Mar 05 2021 at 23:10):

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 (Mar 05 2021 at 23:34):

@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 (Mar 05 2021 at 23:36):

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

#### Adam Topaz (Mar 05 2021 at 23:36):

Does tidy solve soft_truncation'_d_neg?

#### Adam Topaz (Mar 05 2021 at 23:36):

Or even rfl?

#### Kevin Buzzard (Mar 05 2021 at 23:48):

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 (Mar 05 2021 at 23:56):

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 (Mar 06 2021 at 00:00):

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

#### Adam Topaz (Mar 06 2021 at 00:02):

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

#### Kevin Buzzard (Mar 06 2021 at 00:12):

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

#### Kevin Buzzard (Mar 06 2021 at 00:13):

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

#### Adam Topaz (Mar 06 2021 at 00:19):

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 (Mar 06 2021 at 06:01):

Thanks a lot for your help.

#### Johan Commelin (Mar 06 2021 at 06:01):

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

#### Johan Commelin (Mar 06 2021 at 06:02):

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

#### Johan Commelin (Mar 06 2021 at 09:07):

Everything compiles again!

#### Johan Commelin (Mar 06 2021 at 09:07):

I pushed to jmc-complex

#### Kevin Buzzard (Mar 06 2021 at 09:18):

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

#### Kevin Buzzard (Mar 06 2021 at 09:19):

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 (Mar 08 2021 at 08:15):

@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 (Mar 08 2021 at 16:35):

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 (Mar 08 2021 at 16:37):

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 (Mar 08 2021 at 16:38):

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

#### Kevin Buzzard (Mar 08 2021 at 16:39):

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 (Mar 08 2021 at 16:40):

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

#### Adam Topaz (Mar 08 2021 at 16:48):

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

#### Adam Topaz (Mar 08 2021 at 16:48):

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

#### Johan Commelin (Mar 08 2021 at 17:21):

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 (Mar 08 2021 at 17:21):

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 (Mar 08 2021 at 17:22):

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 (Mar 08 2021 at 21:30):

@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 (Mar 08 2021 at 21:46):

@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 (Mar 09 2021 at 01:17):

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 (Mar 09 2021 at 05:35):

@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 (Mar 09 2021 at 05:36):

I'm thinking about the following renames:

differential_object  -> predifferential_object
differential_object' -> differential_object


#### Johan Commelin (Mar 09 2021 at 06:52):

How do people feel about merging this branch into master?

#### Johan Commelin (Mar 09 2021 at 06:53):

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

#### Johan Commelin (Mar 09 2021 at 06:53):

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 (Mar 09 2021 at 06:59):

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 (Mar 09 2021 at 07:04):

Ok, I merged the branch

#### Johan Commelin (Mar 09 2021 at 07:05):

So jmc-complex is now officially EOL

#### Johan Commelin (Mar 09 2021 at 09:36):

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

#### Johan Commelin (Mar 09 2021 at 09:39):

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 (Mar 09 2021 at 09:40):

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 (Mar 09 2021 at 09:40):

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

#### Johan Commelin (Mar 09 2021 at 09:40):

No mention of succ or pred or whatever

#### Johan Commelin (Mar 09 2021 at 09:41):

Ooh, wait, I retract the comment about double complexes

#### Johan Commelin (Mar 09 2021 at 09:41):

Because d_comp_d is false there

#### Johan Commelin (Mar 09 2021 at 09:41):

So maybe I will remove that axiom!

#### Johan Commelin (Mar 09 2021 at 09:41):

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

#### Sebastien Gouezel (Mar 09 2021 at 09:58):

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 (Mar 09 2021 at 10:01):

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

#### Sebastien Gouezel (Mar 09 2021 at 11:07):

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

#### Kevin Buzzard (Mar 09 2021 at 13:47):

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 (Mar 09 2021 at 13:53):

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

#### Kevin Buzzard (Mar 09 2021 at 14:23):

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

#### Johan Commelin (Mar 09 2021 at 20:10):

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

#### Johan Commelin (Mar 09 2021 at 20:11):

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

#### Johan Commelin (Mar 15 2021 at 08:28):

@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 (Mar 18 2021 at 22:21):

@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 (Mar 18 2021 at 22:59):

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 (Mar 18 2021 at 23:00):

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 (Mar 18 2021 at 23:07):

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 (Mar 18 2021 at 23:18):

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 (Mar 19 2021 at 06:53):

@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 (Mar 19 2021 at 06:54):

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

#### Johan Commelin (Mar 19 2021 at 06:54):

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

#### Scott Morrison (Mar 19 2021 at 06:55):

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

#### Johan Commelin (Mar 19 2021 at 06:57):

Do you have a suggestion for a new name?

#### Scott Morrison (Mar 19 2021 at 07:02):

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 (Mar 19 2021 at 07:03):

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 (Mar 19 2021 at 07:04):

pre_dgo

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

#### Johan Commelin (Mar 19 2021 at 07:05):

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

#### Kevin Buzzard (Mar 19 2021 at 07:05):

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

#### Kevin Buzzard (Mar 19 2021 at 07:09):

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 (Mar 19 2021 at 07:09):

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

#### Kevin Buzzard (Mar 19 2021 at 13:43):

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 (Mar 19 2021 at 13:44):

I think using monos and epis

#### Adam Topaz (Mar 19 2021 at 13:45):

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 (Mar 19 2021 at 13:46):

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

#### Kevin Buzzard (Mar 19 2021 at 13:46):

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 (Mar 19 2021 at 13:48):

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

#### Kevin Buzzard (Mar 19 2021 at 13:48):

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 (Mar 19 2021 at 13:48):

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

#### Bhavik Mehta (Mar 19 2021 at 13:49):

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

#### Adam Topaz (Mar 19 2021 at 13:49):

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

#### Bhavik Mehta (Mar 19 2021 at 13:49):

docs#category_theory.abelian.pseudoelements

#### Kevin Buzzard (Mar 19 2021 at 13:50):

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 (Mar 19 2021 at 13:50):

/-- 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 (Mar 19 2021 at 13:51):

That's the definition of epi :)

#### Bhavik Mehta (Mar 19 2021 at 13:52):

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

#### Peter Scholze (Mar 19 2021 at 13:53):

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 (Mar 19 2021 at 13:53):

Yes, this seems to be the pseudoelement trick

#### Peter Scholze (Mar 19 2021 at 13:54):

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

#### Kevin Buzzard (Mar 19 2021 at 13:54):

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

#### Kevin Buzzard (Mar 19 2021 at 13:58):

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 (Mar 19 2021 at 14:00):

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

#### Kevin Buzzard (Mar 19 2021 at 14:00):

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 (Mar 19 2021 at 14:00):

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

#### Kevin Buzzard (Mar 19 2021 at 14:00):

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

#### Adam Topaz (Mar 19 2021 at 14:01):

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 (Mar 19 2021 at 14:01):

Does zulip do tikz?

#### Kevin Buzzard (Mar 19 2021 at 14:01):

yes I see how to do it all now

#### Markus Himmel (Mar 19 2021 at 14:01):

It's here but it's far from pretty

#### Adam Topaz (Mar 19 2021 at 14:01):

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

#### Kevin Buzzard (Mar 19 2021 at 14:02):

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

#### Bhavik Mehta (Mar 19 2021 at 14:22):

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 (Mar 19 2021 at 14:23):

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 (Mar 19 2021 at 14:24):

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

#### Kevin Buzzard (Mar 19 2021 at 15:47):

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 (Mar 19 2021 at 15:53):

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

#### Kevin Buzzard (Mar 19 2021 at 15:56):

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.

Last updated: May 09 2021 at 22:13 UTC