## Stream: condensed mathematics

#### Johan Commelin (Feb 15 2021 at 15:01):

Hmm, I can't replicate the solution that worked in the previous example.
Here are two rather minimal examples that explain the problem.

import algebra.homology.chain_complex
import algebra.category.Group
import tactic.ring

open category_theory

section

open tactic

meta def int_magic : tactic unit :=
do (assumption <|> tactic.interactive.ring1 none <|> tactic.interactive.refl) <|>
target >>= trace

end

/-- Convenience definition:
The identity morphism of an object in the system of complexes
when it is given by different indices that are not
definitionally equal. -/
def congr_hom {i j : ℤ} (h : i = j) :
C.X i ⟶ C.X j :=
eq_to_hom \$ by { subst h }

/-- C.d is the differential C i ⟶ C (i+1) for a cochain complex C. -/
def differential (i j : ℤ) (hij : i + 1 = j) :
C.X i ⟶ C.X j :=
C.d i ≫ congr_hom C hij

local notation d := differential _ _ _ (by int_magic)

lemma differential_rfl (i : ℤ) : differential C i (i+1) rfl = C.d i :=
by { ext, refl }

lemma d_comp_d {i₁ i₂ i₃ : ℤ} (h : i₁ + 1 = i₂) (h' : i₂ + 1 = i₃) :
(d : C.X i₁ ⟶ C.X i₂) ≫ (d : C.X i₂ ⟶ C.X i₃) = 0 :=
begin
subst i₂, subst i₃,
simp only [differential_rfl],
exact homological_complex.d_squared _ _
end

lemma d_d {i₁ i₂ i₃ : ℤ} (h : i₁ + 1 = i₂) (h' : i₂ + 1 = i₃) (x : C.X i₁) :
(differential C i₂ _ (by int_magic) (d x : C.X i₂) : C.X i₃) = 0 :=
show ((d : C.X i₁ ⟶ C.X i₂) ≫ (d : C.X i₂ ⟶ C.X i₃)) x = 0,
by { rw d_comp_d, refl }

example (h : ∀ i : ℤ, ∀ x : C.X (i+1), d x = 0 → ∃ y, d y = x)
(i : ℤ) (x : C.X i) (hx : d x = 0) :
∃ y : C.X (i-1), d y = x :=
begin
specialize h (i-1),
simp at h,
end

example (h : ∀ i : ℤ, ∀ x : C.X i, d x = 0 → ∃ y : C.X (i-1), d y = x)
(i : ℤ) (x : C.X (i+1)) (hx : d x = 0) :
∃ y, d y = x :=
begin
specialize h (i+1),
simp at h,
end


#### Johan Commelin (Feb 15 2021 at 15:04):

I don't care so much about how we invoke automation, as long as it works :stuck_out_tongue_wink:

1. The above approach hides an automatic tactic call behind notation d . Downside: the notation will not be used in the goal view.
2. Use auto_param. But this doesn't work with bundled morphisms.
3. Use fact (i + 1 = j). I fear that this might not scale when it comes to chaining equalities together using transitivity.

#### Johan Commelin (Feb 15 2021 at 15:05):

But the problem outlined above is orthogonal to these 3 approaches.

#### Adam Topaz (Feb 15 2021 at 15:16):

@Johan Commelin Have you thought about trying tricks similar to the following?

@[simp] def test {i : ℤ} (x : C.X (i-1+1)) : C.X i := congr_hom C (by int_magic) x

example {i : ℤ} (cond : ∃ x : C.X (i-1+1), true) : ∃ x : C.X i, true :=
begin
cases cond,
simp at cond_w,
finish,
end


#### Adam Topaz (Feb 15 2021 at 15:16):

I don't know if this would be helpful at all.

#### Johan Commelin (Feb 15 2021 at 15:18):

I would like to hide congr_hom as much as possible behind a basic API. Otherwise we'll end up with many silly proof steps, saying that the norm of congr_hom x is the same as the norm of x, etc... etc...

#### Adam Topaz (Feb 15 2021 at 15:19):

I imagine we can solve these issues with some carefully chosen simp lemmas

#### Johan Commelin (Feb 15 2021 at 15:21):

You can take a look at system_of_complexes.lean on the wip_dtt branch... it didn't look pleasant to me.

#### Johan Commelin (Feb 15 2021 at 15:47):

There was the other proposal to use a massive direct sum, and define d on that. But I don't see how that will play nicely with either categorical language, where you don't have elements (so how do you define a complex in the first place? as something isomorphic to a massive direct sum?) or with elements (how do you move from x : C i to the massive direct sum? will we have canonical inclusion maps before every other element?).
Still, if someone wants to try a test of this, and it works well, then I'll shut up :grinning: :speak_no_evil:

#### Kevin Buzzard (Feb 15 2021 at 16:52):

example (h : ∀ i : ℤ, ∀ x : C.X (i+1), d x = 0 → ∃ y, d y = x)
(i : ℤ) (x : C.X i) (hx : d x = 0) :
∃ y : C.X (i-1), d y = x :=
begin
suffices : ∀ i j (x : C.X j) (hij : i + 1 = j) (hx : d x = 0),
∃ y : C.X i, d y = x,
{ exact this _ _ _ _ hx }, clear hx x i,
rintros i j x rfl hx,
exact h _ _ hx,
end


#### Kevin Buzzard (Feb 15 2021 at 16:54):

example (h : ∀ i : ℤ, ∀ x : C.X i, d x = 0 → ∃ y : C.X (i-1), d y = x)
(i : ℤ) (x : C.X (i+1)) (hx : d x = 0) :
∃ y, d y = x :=
begin
suffices : ∀ i j (x : C.X j) (hij : i + 1 = j) (hx : d x = 0),
∃ y : C.X i, d y = x,
{ exact this _ _ _ _ hx }, clear hx x i,
rintros i j x hij hx,
have hij' : i = j - 1 := eq_sub_of_add_eq hij,
subst hij',
exact h _ _ hx,
end


#### Kevin Buzzard (Feb 15 2021 at 16:54):

Everything is easy if the hypothesis is stated in the type-theoretically correct way -- there are no fancy tricks here.

#### Kevin Buzzard (Feb 15 2021 at 16:55):

  suffices : ∀ i j (x : C.X j) (hij : i + 1 = j) (hx : d x = 0),
∃ y : C.X i, d y = x,


This is great because we're quantifying over i and j, and all our dependent types (C.X i and C.X j) can be specialised to the case in hand.

#### Johan Commelin (Feb 15 2021 at 17:21):

On the other hand, it means that we'll always be writing (hij : i + 1 = j) all over the place. It would be great if some tactic could remove that need.

#### Mario Carneiro (Feb 15 2021 at 17:24):

I like this solution, it puts the i+1=j proof into a subgoal where it can be proved by any means necessary

#### Mario Carneiro (Feb 15 2021 at 17:26):

Writing nontrivial terms in rigid positions in a dependent type seems to be a recurring source of problems

#### Adam Topaz (Feb 15 2021 at 17:26):

Crazy idea:

open category_theory
def complex := { C : ℤ ⥤ AddCommGroup // ∀ (i j : ℤ) (h : i + 2 ≤ j), C.map (hom_of_le h) = 0 }


#### Kevin Buzzard (Feb 15 2021 at 17:27):

It'll be fun explaining that to the normal people

#### Kevin Buzzard (Feb 15 2021 at 17:28):

I guess that is of no relevance -- my students don't yet know what the actual definition of is_compact is and yet they can still prove things by finding finite subcovers of open covers

#### Mario Carneiro (Feb 15 2021 at 17:28):

What's it supposed to look like? That seems like a pretty normal definition

d^2=0

#### Kevin Buzzard (Feb 15 2021 at 17:29):

I mean, like that exact string of characters. It's like a set phrase.

#### Mario Carneiro (Feb 15 2021 at 17:29):

aha, I see now, I like this crazy idea

#### Kevin Buzzard (Feb 15 2021 at 17:31):

I have no idea how to search for d^2=0 on mathoverflow but I am convinced it will be everywhere.

#### Mario Carneiro (Feb 15 2021 at 17:31):

I wonder how common it is to have this whole functor available instead of d

#### Kevin Buzzard (Feb 15 2021 at 17:32):

It's the fact that mathematicians constantly abuse this d notation to mean "all the maps" which makes me open to the idea of the direct sum approach, where one really does have one map d, from the direct sum (or disjoint union, depending on which category you're taking the coproduct in).

#### Alex J. Best (Feb 15 2021 at 17:58):

Kevin Buzzard said:

I have no idea how to search for d^2=0 on mathoverflow but I am convinced it will be everywhere.

#### Johan Commelin (Feb 15 2021 at 18:18):

Kevin Buzzard said:

It's the fact that mathematicians constantly abuse this d notation to mean "all the maps" which makes me open to the idea of the direct sum approach, where one really does have one map d, from the direct sum (or disjoint union, depending on which category you're taking the coproduct in).

But I don't see how to write this down in lean, in such a way that you can do complexes of objects in an arbitrary (abelian) category, and at the same time make is useful when trying to apply d to elements of a module in some concrete complex.

#### Johan Commelin (Feb 15 2021 at 18:18):

How do you express that the big complex-object is the direct sum of the constituent objects?

#### Mario Carneiro (Feb 15 2021 at 18:19):

Given any suitable definition of the d function, it's possible to construct a functor like Adam Topaz 's version, and as long as you don't need to reduce it you can just work from that

#### Johan Commelin (Feb 15 2021 at 18:20):

Crazy idea:

open category_theory
def complex := { C : ℤ ⥤ AddCommGroup // ∀ (i j : ℤ) (h : i + 2 ≤ j), C.map (hom_of_le h) = 0 }


Would this solve the issue that we have in the example from the first post? Of does this just mean that we should never ever talk about d, and always use hom_of_le instead? Doesn't sound like it will be very readable... :sad:

#### Mario Carneiro (Feb 15 2021 at 18:21):

I think you can wrap that behind a definition of type \all i j : int, C i -> C j

#### Kevin Buzzard (Feb 15 2021 at 18:22):

Such a map only exists for i<=j, right? The situation is C i -> C (i + 1) -> C (i + 2) -> ...

#### Adam Topaz (Feb 15 2021 at 18:22):

@Johan Commelin I'm playing with this idea now. And the answer seems to be no, still getting the same issue :-/

#### Mario Carneiro (Feb 15 2021 at 18:22):

ah yeah, it would be \all i j, i <= j -> C i -> C j

#### Mario Carneiro (Feb 15 2021 at 18:23):

and I guess the last arrow is a hom of some kind

#### Kevin Buzzard (Feb 15 2021 at 18:23):

I guess the category of finite abelian groups is a perfectly good abelian category which doesn't have infinite direct sums.

#### Mario Carneiro (Feb 15 2021 at 18:24):

Is it possible / desirable to totalize here? C j is an abelian group so you've got the zero morphism

#### Kevin Buzzard (Feb 15 2021 at 18:24):

yeah, there are zero morphisms in an arbitrary abelian category too

#### Mario Carneiro (Feb 15 2021 at 18:28):

leading to the less well known identity $d^{-1}=0$

#### Johan Commelin (Feb 15 2021 at 18:32):

But even if you totalize... does this mean we should just put type ascriptions every where? And give up on the idea that d is a degree 1 map?

#### Johan Commelin (Feb 15 2021 at 18:33):

So you have d : C i -> C j for all i and j. And

1. if j = i, then d = id
2. if j = i, then d =  "the actual $d$"
3. otherwise, d = 0

#### Johan Commelin (Feb 15 2021 at 18:35):

And so there will be a simp lemma that says that d composed with d is d (This is false, the right hand side could be id while the left hand side is d >> 0). And

lemma d_eq_zero (i j) (h : i + 2 \le j) :
(d : C i -> C j) = 0 := sorry


#### Johan Commelin (Feb 15 2021 at 18:36):

I was just hoping that lean would be able to infer the type of d x from the type of x... but I guess that's asking for lots of pain, at least in lean3.

#### Adam Topaz (Feb 15 2021 at 18:36):

import algebra.homology.chain_complex
import algebra.category.Group

def ι {i : ℤ} {F : ℤ → AddCommGroup} : F i ⟶ mk_graded F := cocone_morphism (discrete.functor F) i

structure complex :=
(d_graded : ∀ i : ℤ, ∃ f : F i ⟶ F (i+1), ι ≫ d = f ≫ ι)
(d_squared : d ≫ d = 0)


#### Adam Topaz (Feb 15 2021 at 18:37):

In case anyone wants to play with a totalized version

#### Johan Commelin (Feb 15 2021 at 18:39):

But there are two downsides, afaik (sorry for being critical, without having a better solution):

1. mk_graded might not fit into your category (e.g. complexes of findim vector spaces)
2. if I have a concrete example of a complex, then I will have some x : F i, and if I want to do a bit of homological algebra, then those $\iota$ maps will be all over the place

#### Adam Topaz (Feb 15 2021 at 18:41):

Yeah, I agree. But I still think it's worth some experimentation

#### Mario Carneiro (Feb 15 2021 at 18:42):

those $\iota$ maps will be all over the place

I don't think this is a major problem; it's kind of like working with integer expressions involving nats with \u a + \u b - 1 = \u c

#### Mario Carneiro (Feb 15 2021 at 18:43):

Regarding 1, is it possible to take a synthetic colimit here, putting you in a completion of the original category? Like a sigma

#### Adam Topaz (Feb 15 2021 at 18:44):

Yeah, that's what I'm thinking too.

#### Adam Topaz (Feb 15 2021 at 18:44):

Maybe @Bhavik Mehta 's work on ind completions would help here.

#### Bhavik Mehta (Feb 15 2021 at 18:50):

Yeah you can take the synthetic colimit if it's a filtered colimit, but there's already the free cocompletion in mathlib

#### Bhavik Mehta (Feb 15 2021 at 18:50):

But this comes with the caveat that the new category will be (potentially) a lot bigger than the original one - even in non-Lean maths if you take the cocompletion of a small category you end up with a large one

#### Adam Topaz (Feb 15 2021 at 18:51):

Plus the differential in the complex would become some morphism of presheaves, which might confuse even more people :)

#### Mario Carneiro (Feb 15 2021 at 18:52):

In this case you only need the completion wrt colimits of length int

#### Kevin Buzzard (Feb 15 2021 at 18:53):

I still kind of think that d : C_i -> C_j = 0 for i > j is kind of insane. It would then not be true that for all i,j,k, d o d = d, for example. Chains seem to have been implemented as a functor from the integers (so again there are no d's if i > j) and the "d = 0 if i+2<=j" condition does sound like a cool way of setting it up.

#### Mario Carneiro (Feb 15 2021 at 18:54):

It would then not be true that for all i,j,k, d o d = d, for example.

That was never true, because d o d = d doesn't typecheck for a lot of values of i,j,k

#### Johan Commelin (Feb 15 2021 at 18:55):

chain complexes have an "ad hoc" definition. They aren't implemented as functors. Just a collection of int-indexed objects with a d (of degree 1) between them.

#### Mario Carneiro (Feb 15 2021 at 18:55):

the only difference now is that those assumptions are moving from type correctness assumptions to regular assumptions

#### Johan Commelin (Feb 15 2021 at 18:57):

it also means that you get less type inference. so statements will become a lot clunkier

#### Mario Carneiro (Feb 15 2021 at 18:58):

I'm not sure the hypotheses that were being supplied are actually the ones you want though

#### Mario Carneiro (Feb 15 2021 at 18:59):

for example a type correctness hypothesis might be needlessly obtuse like i+1+1 <= j+1 while a regular hypothesis can be stated as i+1 <= j

#### Johan Commelin (Feb 15 2021 at 19:13):

I've adapted the example to a totalized d:

import algebra.category.Group
import tactic

open category_theory

structure cochain_complex extends ℤ ⥤ AddCommGroup :=
(is_complex : ∀ (i j : ℤ) (h : i + 2 ≤ j), map (hom_of_le (show i ≤ j, by linarith)) = 0)

variables {C : cochain_complex} {i j k : ℤ}

/-- C.d is the differential C i ⟶ C (i+1) for a cochain complex C. -/
def d : C.obj i ⟶ C.obj j :=
if h : i ≤ j then C.map (hom_of_le h) else 0

lemma d_comp_d (h : i + 2 ≤ k) :
(d : C.obj i ⟶ C.obj j) ≫ (d : C.obj j ⟶ C.obj k) = 0 :=
begin
delta d,
by_cases h12 : i ≤ j,
{ by_cases h23 : j ≤ k,
{ rw [dif_pos h12, dif_pos h23, ← functor.map_comp],
exact C.is_complex i k h },
{ rw dif_neg h23, rw limits.comp_zero } },
{ rw dif_neg h12, rw limits.zero_comp }
end

lemma d_d (h : i + 2 ≤ k) (x : C.obj i) :
(d (d x : C.obj j) : C.obj k) = 0 :=
show ((d : C.obj i ⟶ C.obj j) ≫ (d : C.obj j ⟶ C.obj k)) x = 0,
by { rw d_comp_d h, refl }

example (h : ∀ i : ℤ, ∀ x : C.obj (i+1), (d x : C.obj (i+2)) = 0 → ∃ y : C.obj i, d y = x)
(i : ℤ) (x : C.obj i) (hx : (d x : C.obj (i+1)) = 0) :
∃ y : C.obj (i-1), d y = x :=
begin
specialize h (i-1),
simp at h,
end

example (h : ∀ i : ℤ, ∀ x : C.obj i, (d x : C.obj (i+1)) = 0 → ∃ y : C.obj (i-1), d y = x)
(i : ℤ) (x : C.obj (i+1)) (hx : (d x : C.obj (i+1+1)) = 0) :
∃ y : C.obj i, d y = x :=
begin
specialize h (i+1),
simp at h,
end


#### Johan Commelin (Feb 15 2021 at 19:14):

But these statements are still problematic... Should they be written differently now? I don't see how.

#### Johan Commelin (Feb 15 2021 at 19:15):

Unless we use Kevin's approach again... but that also worked with the untotal d.

#### Kevin Buzzard (Feb 15 2021 at 19:17):

Johan Commelin said:

chain complexes have an "ad hoc" definition. They aren't implemented as functors. Just a collection of int-indexed objects with a d (of degree 1) between them.

Oh sorry, I was looking at Adam's definition! I had assumed it was official in some way :-) I think that it definitely has its merits!

#### Mario Carneiro (Feb 15 2021 at 19:19):

What's problematic? The rw add_sub_cancel lines work now

#### Johan Commelin (Feb 15 2021 at 19:19):

Sure, but we would definitely want a constructor that only needs a degree 1 map. E.g., when building a complex from a simplicial module by taking alternating sums of the degeneracy maps... you don't want to worry about arbitrary compositions at that point.

#### Mario Carneiro (Feb 15 2021 at 19:19):

and you can use i+2 instead of i+1+1

#### Johan Commelin (Feb 15 2021 at 19:20):

aah, so why is rw working and simp failing?

#### Adam Topaz (Feb 15 2021 at 19:20):

Yeah:

example (h : ∀ i : ℤ, ∀ x : C.obj (i+1), (d x : C.obj (i+2)) = 0 → ∃ y : C.obj i, d y = x)
(i : ℤ) (x : C.obj i) (hx : (d x : C.obj (i+1)) = 0) :
∃ y : C.obj (i-1), d y = x :=
begin
specialize h (i-1),
rw sub_add_cancel i 1 at h,
apply h,
assumption, -- fails :(
end


#### Adam Topaz (Feb 15 2021 at 19:20):

The d x = 0 assumption doesn't match with the d x = 0 goal.

#### Mario Carneiro (Feb 15 2021 at 19:21):

I think this would be a lot clearer (and shorter than the type ascriptions) if j was an explicit arg to d

#### Johan Commelin (Feb 15 2021 at 19:22):

We might need to do that

#### Johan Commelin (Feb 15 2021 at 19:22):

Mario Carneiro said:

and you can use i+2 instead of i+1+1

this causes the fail that Adam noticed

#### Kevin Buzzard (Feb 15 2021 at 19:23):

I think d should take a proof that i <= j. That proof which split up into cases -- nobody is going to need the j < i situation ever, right?

#### Mario Carneiro (Feb 15 2021 at 19:23):

that's what causes all the simp sadness though

#### Kevin Buzzard (Feb 15 2021 at 19:23):

Because it's a proof, we don't care if we have a proof of i <= j + 1 - 1 or whatever

#### Mario Carneiro (Feb 15 2021 at 19:24):

but if it's an arg to d then it ends up in statements which is why nothing rewrites properly

#### Johan Commelin (Feb 15 2021 at 19:25):

@Mario Carneiro why can't angry_simp just blast through those annoying badly-typed motives?

#### Johan Commelin (Feb 15 2021 at 19:25):

It will have to fix up those proof arguments... but isn't that just some trans or subst?

#### Adam Topaz (Feb 15 2021 at 19:27):

import algebra.category.Group
import tactic

open category_theory

structure cochain_complex extends ℤ ⥤ AddCommGroup :=
(is_complex : ∀ (i j : ℤ) (h : i + 2 ≤ j), map (hom_of_le (show i ≤ j, by linarith)) = 0)

variables {C : cochain_complex} {i j k : ℤ}

/-- C.d is the differential C i ⟶ C (i+1) for a cochain complex C. -/
def d : C.obj i ⟶ C.obj j :=
if h : i ≤ j then C.map (hom_of_le h) else 0

def d' (j) : C.obj i ⟶ C.obj j := d

lemma d_comp_d (h : i + 2 ≤ k) :
(d : C.obj i ⟶ C.obj j) ≫ (d : C.obj j ⟶ C.obj k) = 0 :=
begin
delta d,
by_cases h12 : i ≤ j,
{ by_cases h23 : j ≤ k,
{ rw [dif_pos h12, dif_pos h23, ← functor.map_comp],
exact C.is_complex i k h },
{ rw dif_neg h23, rw limits.comp_zero } },
{ rw dif_neg h12, rw limits.zero_comp }
end

lemma d_d (h : i + 2 ≤ k) (x : C.obj i) :
(d (d x : C.obj j) : C.obj k) = 0 :=
show ((d : C.obj i ⟶ C.obj j) ≫ (d : C.obj j ⟶ C.obj k)) x = 0,
by { rw d_comp_d h, refl }

example (h : ∀ i : ℤ, ∀ x : C.obj (i+1), (d' (i+2) x) = 0 → ∃ y : C.obj i, d y = x)
(i : ℤ) (x : C.obj i) (hx : (d' (i+1) x) = 0) :
∃ y : C.obj (i-1), d y = x :=
begin
specialize h (i-1),
rw (show i-1+1 = i, by ring) at h,
rw (show i-1+2 = i+1, by ring) at h,
exact h _ hx,
end

example (h : ∀ i : ℤ, ∀ x : C.obj i, (d x : C.obj (i+1)) = 0 → ∃ y : C.obj (i-1), d y = x)
(i : ℤ) (x : C.obj (i+1)) (hx : (d x : C.obj (i+1+1)) = 0) :
∃ y : C.obj i, d y = x :=
begin
specialize h (i+1),
rw (show i+1-1 = i, by ring) at h,
apply h _ hx,
end


#### Adam Topaz (Feb 15 2021 at 19:27):

simp's instead of rewrites still don't seem to work

#### Mario Carneiro (Feb 15 2021 at 19:28):

/-- C.d is the differential C i ⟶ C (i+1) for a cochain complex C. -/
def d (j : ℤ) : C.obj i ⟶ C.obj j :=
if h : i ≤ j then C.map (hom_of_le h) else 0

lemma d_comp_d (h : i + 2 ≤ k) :
(d j : C.obj i ⟶ _) ≫ d k = 0 :=
begin
delta d,
by_cases h12 : i ≤ j,
{ by_cases h23 : j ≤ k,
{ rw [dif_pos h12, dif_pos h23, ← functor.map_comp],
exact C.is_complex i k h },
{ rw dif_neg h23, rw limits.comp_zero } },
{ rw dif_neg h12, rw limits.zero_comp }
end

lemma d_d (h : i + 2 ≤ k) (x : C.obj i) : d k (d j x) = 0 :=
show (d j ≫ d k) x = 0, by { rw d_comp_d h, refl }

example (h : ∀ i : ℤ, ∀ x : C.obj (i+1), d (i+2) x = 0 → ∃ y : C.obj i, d _ y = x)
(i : ℤ) (x : C.obj i) (hx : d (i+1) x = 0) : ∃ y : C.obj (i-1), d _ y = x :=
begin
specialize h (i-1),
apply h,
rwa (by linarith : i - 1 + 2 = i + 1),
end


#### Mario Carneiro (Feb 15 2021 at 19:30):

The statements are indeed a lot shorter, and simp doesn't work because it involves uniformly rewriting in places where simp can't reach because of dependencies (the rwa is actually changing the type of the equality)

#### Mario Carneiro (Feb 15 2021 at 19:31):

rw is too stupid to question whether the rewrite is going to work, it just yolo's and reports motive is not type correct if it turns out not to work

#### Johan Commelin (Feb 15 2021 at 19:31):

I want yolo_simp

#### Johan Commelin (Feb 15 2021 at 19:32):

Are there theoretical obstructions to its existence? Or could a carefully crafted dtt_simp make life easier, without resigning to a bunch of ad hoc hacks?

#### Mario Carneiro (Feb 15 2021 at 19:33):

well the disadvantage of the yolo approach is that you can end up getting tripped up by occurrences of the pattern where it would be best not to touch, like inside proof arguments in the statement

#### Mario Carneiro (Feb 15 2021 at 19:34):

A usable but kind of ugly solution would be to specify exactly which occurrences you want to replace

#### Mario Carneiro (Feb 15 2021 at 19:35):

and that still might not work with situations like the rewrite you sent me

Is the issue that (is_weak_bounded_exact._proof_2 (i + 1)) is only a proof of i + 1 - 1 + 1 = i + 1 and not a proof of i + 1 = i + 1?

#### Mario Carneiro (Feb 15 2021 at 19:37):

As for dtt_simp, things get pretty hairy once you have heterogeneous equality. I think there is a way to do this but it requires pathovers, which we don't have in mathlib

#### Johan Commelin (Feb 15 2021 at 19:38):

But those kind of proofs should be fixable, right? By doing some transitivity of equality.

#### Mario Carneiro (Feb 15 2021 at 19:38):

Yes, the solution is to replace the proof is_weak_bounded_exact._proof_2 (i + 1) with congr_arg (+1) h where h : i + 1 - 1 = 1 is the lemma you are rewriting with

#### Mario Carneiro (Feb 15 2021 at 19:39):

and then replace h with rfl along with everything else

#### Mario Carneiro (Feb 15 2021 at 19:39):

but doing that in a rw line with no hairy middle steps is a challenge

#### Kevin Buzzard (Feb 15 2021 at 19:40):

Here's the "generalize" approach:

example (h : ∀ i : ℤ, ∀ x : C.obj (i+1), (d x : C.obj (i+2)) = 0 → ∃ y : C.obj i, d y = x)
(i : ℤ) (x : C.obj i) (hx : (d x : C.obj (i+1)) = 0) :
∃ y : C.obj (i-1), d y = x :=
begin
suffices : ∀ i j k : ℤ, j = i + 1 → k = i + 2 → ∀ x : C.obj j, (d x : C.obj k) = 0 → ∃ y : C.obj i, d y = x,
{ apply this _ _ _ _ _ _ hx; ring }, clear hx x i,
rintros i j k rfl rfl x hx,
exact h _ _ hx,
end


#### Mario Carneiro (Feb 15 2021 at 19:40):

The generalize_proofs tactic may come in useful here, it will hoist these lemmas into the context where you can replace them in a more targeted way

#### Mario Carneiro (Feb 15 2021 at 19:42):

The suffices line is morally equivalent to the motive that rw is cooking up - the trick is to generalize the right things in the context and it's easy but verbose for a human and hard for a tactic that doesn't know what you are trying to do

#### Mauricio Collares (Feb 15 2021 at 19:51):

Sorry for a (very likely) useless suggestion, but is https://www.cl.cam.ac.uk/~jdy22/papers/frex-indexing-modulo-equations-with-free-extensions.pdf useful for the index computations? I guess it at least provides funny terms such as "slime avoidance" and "fording"

#### Johan Commelin (Feb 15 2021 at 20:08):

It certainly looks relevant... but I don't know enough type theory lingo to see how to apply it in the context at hand

#### Scott Morrison (Feb 16 2021 at 00:53):

Looks like I missed some fun. :-) I've played with this ℤ ⥤ V with C.map (hom_of_le _) = 0 a few times previously. It's a fun definition, and if it actually helped I'm sure we could persuade people that it wasn't insane...

#### Scott Morrison (Feb 16 2021 at 00:55):

But I'm not sure that you get anything from this definition that you don't get just by being careful to insert lots of eq_to_homs.

#### Mario Carneiro (Feb 16 2021 at 01:19):

I think the statements are generally shorter, and you don't have proofs in the statements which causes most of the problem in proofs

#### Scott Morrison (Feb 16 2021 at 02:11):

I guess what I meant was that you still frequently need to move between C.X i and C.X j when you know i = j, you just have an extra way to do this: C.map (hom_of_le (le_of_eq h)), in addition to the general purpose eq_to_hom (congr_arg C.X h).

#### Scott Morrison (Feb 19 2021 at 11:28):

I experimented with yet another definition of a complex, that seems to specialise reasonably to int indexed (co)chain complexes, and to nat indexed chain complexes.

It is:

structure hc {N : Type*} [add_comm_monoid N] (a b : N) :=
(X : N → V)
(d : Π n : N, X (n + a) ⟶ X (n + b))
(d_squared' : ∀ (n m : N) (h : n + b = m + a), d n ≫ tra X h ≫ d m = 0 . d_squared_tac)


Here:

• there are _two_ parameters a b in the definition, which controls where the differential goes.
• for int indexed chain complexes you want a=0, b=-1.
• for int indexed cochain complexes you want a=0, b=1.
• for nat indexed chain complexes you want a=1, b=0.
• tra X h is just defined as eq_to_hom (congr_arg X h), i.e. it's transport through a type family, as a morphism in the category
• d_squared_tac is [{ intros n m h, simp at h, try { subst h }, obviously }].

You can see in https://github.com/leanprover-community/mathlib/blob/hexp/src/algebra/homology/chain_complex_2.lean that at least building the equivalence of categories to cochain complexes, or the equivalence to nat-indexed chain complexes as proposed in #6260, is _relatively_ painless -- d_squared_tac works when you want it to, and tidy manages all the proofs.

Of course, just proving equivalences between definitions is far from enough evidence that this is usable.

#### Scott Morrison (Feb 19 2021 at 11:30):

I was pretty happy in in #6308 that the nat indexed chain complexes of #6260 worked smoothly for defining the Moore complex. So that is some evidence that that definition is usable. I may try redoing the Moore complex using this definition, to see how it goes.

#### Scott Morrison (Feb 19 2021 at 11:32):

The other obvious tests are:

• adapt the existing algebra/homology/homology.lean
• write some other equivalences (e.g. coming from an additive automorphism of the indexing monoid N)
• show that given an inclusion of monoids, the chain complexes on the small monoid are equivalent to chain complexes indexed by the big monoid, supported on the small monoid

#### Scott Morrison (Feb 19 2021 at 11:32):

These aren't the most exciting tests to carry out... So I'm happy to hear feedback or take directions. :-)

#### Scott Morrison (Feb 19 2021 at 11:33):

I'd also like to test out the ℕ ⥤ V approach, of course.

#### Johan Commelin (Feb 19 2021 at 11:36):

Another test is to switch (a branch of) lean-liquid over to your mathlib branch, and rewrite the homological algebra that we've done so far, in terms of this new definition.

#### Kevin Buzzard (Feb 19 2021 at 11:41):

@Floris van Doorn did some homological algebra in Lean 2 using a succ_structure for a base.

#### Floris van Doorn (Feb 20 2021 at 18:02):

Yeah, in Lean 2 I defined chain complexes indexed by a "successor structure" which is just any type equipped with an endofunction, called the successor. It worked nicely, especially when dealing with chain complexes that have some vague periodicity. For example, the long exact sequence of homotopy groups was indexed by nat x fin 3, since every three indices you go up one dimension.

Scott's add_comm_monoid also works for this, and has the advantage that it works well with cochain complexes defined over nat (in my definition this didn't work great, since it would contain one extra map: ... <- X 2 <- X 1 <- X 0 <- X (pred 0))

I also defined graded objects. The linked comment describes two design decisions that are worth considering, though I'm not sure if they would be right for mathlib ((1) looks strange, and (2) might not be a problem if tidy can deal with all the transports.

#### Johan Commelin (Feb 20 2021 at 18:14):

So far, we've been running headfirst into the wall that (2) describes :head_bandage:

#### Johan Commelin (Feb 20 2021 at 18:15):

So I'm inclined to define d as something like

def d {i} (j) : X i -> X j :=
if h : i + 1 = j then (actual def) else 0


#### Johan Commelin (Feb 20 2021 at 18:16):

Note that d >> d = 0 will then hold without proof obligations. For other lemmas/facts we might want to have an auto param that automatically discharges the i + 1 = j-type goals

#### Johan Commelin (Feb 20 2021 at 18:16):

probably a combi of ring and maybe linarith`

Last updated: May 09 2021 at 23:10 UTC