morphisms between objects that are "equal"

Stream: general

[Johan Commelin]

I'm looking at complexes again... and I'm hitting the old problem with defeq issues on int.

def graded_object (M : simplicial_module R) : graded_object_with_shift (-1:ℤ) (Module R)
| -[1+n] := Module.of R punit -- this should just be 0
| (n:ℕ)  := (skeletal.obj M).obj (op n)

def graded_object_d (M : simplicial_module R) :
  M.graded_object ⟶ M.graded_object⟦1⟧
| -[1+n]  := 0
| (0:ℕ)   := 0
| (n+1:ℕ) :=
begin
  refine M.boundary n ≫ _,
  show M.graded_object n ⟶ M.graded_object (n+1-1),
  -- aahrg :scream:
end

[Johan Commelin]

Because of the way nat.sub is defined, n+1-1 is not defeq to n. And hence we are in trouble.

[Johan Commelin]

What is the correct way forward?

[Johan Commelin]

If you want to play with this, I suggest leanproject get -b mathlib:sset and then look at topology/simplicial/simplicial_complex

[Johan Commelin]

Of course I can congr my way through, but that generated ugly inductions on equality, and I thought those were really evil in category theory.

[Johan Commelin]

@Scott Morrison What do you think?

[Johan Commelin]

Maybe graded_object should be defined as functors from discrete \b to C?

[Johan Commelin]

That way, I could do graded_object.map and reduce this to a morphism in the discrete category.

[Johan Commelin]

Over there, eq.rec is less of a problem, I guess.

[Scott Morrison]

How is graded_object defined now?

[Johan Commelin]

Functions

[Scott Morrison]

what's wrong with just composing with an eq_to_hom?

[Johan Commelin]

Let me try

[Scott Morrison]

I think eq_to_hom is as much of a solution as we have for this.

[Johan Commelin]

Ok, so it doesn't matter that I'm proving an equality of types afterwards?

[Johan Commelin]

I'll try this, let's hope for the best (-;

[Scott Morrison]

In some branch (...?) I also introduced some congr_eq_to_hom (I forget the name exactly), which addressed this..

[Scott Morrison]

If f : J \to C, j j' : J, h : j = j' then I defined congr_eq_to_hom f h : f j \hom f j'.

[Scott Morrison]

But somehow the point was that if you didn't unfold it, you never had an equation in Type (or C), but only in the index category, and once you reached the end of things they would all resolve away.

[Scott Morrison]

Let me see what I can find. I can't even place the context right now.

[Scott Morrison]

Sorry, not finding it right away.

[Johan Commelin]

This is a really crappy problem, and it's not really going away I fear.

[Johan Commelin]

M.graded_object_d (↑n + 1 + 1) ≫ M.graded_object_d (↑n + 1 + 1 + -1) = 0

[Johan Commelin]

That's my next goal

[Johan Commelin]

And of course the definition doesn't reduce nicely, because ↑n + 1 + 1 + -1 doesn't simplify

[Johan Commelin]

@Mario Carneiro I'm inclined to redefine nat.sub... but that's just going to shift the problem, right?

[Johan Commelin]

What is the "official" solution?

[Johan Commelin]

example (n : ℕ) : 0 - n = 0 := rfl -- fails :sad:

[Mario Carneiro]

you need an eq_to_hom definition for M.graded_object_d

[Johan Commelin]

def graded_object (M : simplicial_module R) : graded_object_with_shift (-1:ℤ) (Module R)
| -[1+n] := Module.of R punit -- this should just be 0
| (n:ℕ)  := (skeletal.obj M).obj (op n)

def graded_object_d (M : simplicial_module R) :
  M.graded_object ⟶ M.graded_object⟦1⟧
| -[1+n]  := 0
| 0       := 0
| (n+1:ℕ) := M.boundary n ≫
               eq_to_hom (show M.graded_object n = M.graded_object (↑n + 1 + -1), by simp)

example (n : ℕ) : (n:ℤ)+1 - -1 = n+2 := rfl
example (n : ℕ) : 0 - n = 0 := rfl

lemma graded_object_d_squared (M : simplicial_module R) :
  ∀ i, (M.graded_object_d⟦-1⟧' ≫ M.graded_object_d⟦1⟧'⟦-1⟧') i = 0
| -[1+(n+1)] := rfl
| -1         := rfl
| 0          := rfl
| (n+1:ℕ)    :=
begin
  dsimp [shift, has_shift.shift],
  -- have aux : ∀ i j, i = j → M.graded_object_d i == M.graded_object_d j,
  -- { rintro i j rfl, exact heq.refl _ },
  -- dsimp [graded_object_d],
  -- specialize aux (n + 1) (n + 1 + 1 + -1) (by simp),
  -- show (_ ≫ _) ≫ _ = 0,
end

[Johan Commelin]

I did that

[Johan Commelin]

Now try to prove d_squared

[Kenny Lau]

did you use the Mariolization?

[Kenny Lau]

i.e. use Sigma

[Mario Carneiro]

No no, you need M.graded_object.eq_to_hom : a = b -> M.graded_object a -> M.graded_object b

[Mario Carneiro]

kenny's suggestion to use my earlier suggestion is also feasible

[Johan Commelin]

Which earlier suggestion?

[Mario Carneiro]

mix everything into one untyped pot

[Kenny Lau]

use Sigma n, M n (or direct sum I guess)

[Kenny Lau]

and state every identity there

[Mario Carneiro]

that eliminates the dependent types so you won't have to deal with equalities in type dependencies anymore

[Johan Commelin]

I guess that doesn't work for arbitrary categories

[Mario Carneiro]

It works on anything

[Kenny Lau]

what is graded_object_with_shift?

[Mario Carneiro]

it has it's own downsides, but it is a good technique to use when DTT hell starts

[Mario Carneiro]

do you have an MWE that I can play with?

[Johan Commelin]

Sigma might work, but the direct sum doesn't

[Johan Commelin]

I don't have an MWE... but you can leanproject get mathlib:sset...

[Johan Commelin]

I'm not sure the graded_object_eq_to_hom trick is sufficient here...

[Mario Carneiro]

then what?

[Mario Carneiro]

MWE please

[Johan Commelin]

I've now proven

lemma graded_object_d_congr (i j : ℤ) (h : i = j) :
  M.graded_object_d i = M.graded_object_eq_to_hom i j h ≫ M.graded_object_d j ≫
    M.graded_object_eq_to_hom (j-1) (i-1) (by rw h) :=
begin
  subst h, simp only [graded_object_eq_to_hom, category.id_comp, eq_to_hom_refl],
  erw category.comp_id,
end

[Johan Commelin]

This is a very ugly hack

[Johan Commelin]

Whoah, I managed to prove it:

lemma graded_object_d_squared (M : simplicial_module R) :
  ∀ i, (M.graded_object_d ≫ M.graded_object_d⟦1⟧') i = 0
| -[1+n]  := rfl
| 0       := rfl
| 1       := rfl
| (n+2:ℕ) :=
begin
  dsimp,
  show M.graded_object_d (n + 1 + 1) ≫ M.graded_object_d (n + 1 + 1 + -1) = 0,
  rw M.graded_object_d_congr (n + 1 + 1 + -1) (n + 1) (by simp),
  show (_ ≫ _) ≫ _ ≫ (_ ≫ _) ≫ _ = 0,
  simp only [graded_object_eq_to_hom, eq_to_hom_trans, category.id_comp,
    eq_to_hom_refl, eq_to_hom_trans_assoc, category.assoc],
  rw ← category.assoc,
  show (M.boundary ((n + 1)) ≫ M.boundary (n)) ≫ eq_to_hom _ = 0,
  rw M.boundary_boundary n,
  simp only [limits.has_zero_morphisms.zero_comp]
end

[Johan Commelin]

But I'm not sure whether this method scales...

[Johan Commelin]

I guess we need some custom constructors for complexes.

[Scott Morrison]

I made a constructor for finite length complexes, out of an inductive type for composable morphisms

[Scott Morrison]

it's on a branch SES, which is not very pretty

[Johan Commelin]

But this one isn't finite length

[Scott Morrison]

Yes, I was just including this under "some". :-)

[Mario Carneiro]

hrm, there is still no MWE. What file are you working in? What are the imports? What does anything mean? You aren't being very nice

[Scott Morrison]

Which file is this in?

[Scott Morrison]

Also, how about you push your latest additions to that branch? :-)

[Johan Commelin]

Johan Commelin said:

If you want to play with this, I suggest leanproject get -b mathlib:sset and then look at topology/simplicial/simplicial_complex

I just pushed

[Johan Commelin]

I think that we almost have the chain complex

[Johan Commelin]

The hom_congr suggestion works sufficiently well, I think.
Thanks @Mario Carneiro

[Johan Commelin]

We have lunch and a chain complex (-;

[Johan Commelin]

This is how far we are from the homology functors on topological spaces:

R: Type u
_inst_1: comm_ring R
i: ℤ
⊢ Top ⥤ Module R
Messages (3)
singular.lean:62:27
failed to synthesize type class instance for
R : Type u,
_inst_1 : comm_ring R,
i : ℤ
⊢ limits.has_images (Module R)
singular.lean:62:27
failed to synthesize type class instance for
R : Type u,
_inst_1 : comm_ring R,
i : ℤ
⊢ limits.has_equalizers (Module R)
singular.lean:62:27
failed to synthesize type class instance for
R : Type u,
_inst_1 : comm_ring R,
i : ℤ
⊢ limits.has_cokernels (Module R)

[Markus Himmel]

All of this exists, just not in mathlib

[Markus Himmel]

Unless @Scott Morrison has done this already in one of his branches, I can make a PR with my proof of abelian (Module R), which takes care of the images. Equalizers and cokernels should be in #3463.

[Johan Commelin]

Great!

[Scott Morrison]

Yes please!

[Scott Morrison]

#3463 is hopefully close to the merge queue. :-)

[Reid Barton]

wait, how could the Sigma approach work on an arbitrary category?

[Mario Carneiro]

In an arbitrary category, you get a type arrow C containing all homs, or something like that

[Markus Himmel]

@Scott Morrison @Johan Commelin there's a sorry-free proof of abelian (Module R) at https://github.com/leanprover-community/mathlib/commit/0f08541d770094c3e88ce1b45d6928c1defebafc. Some parts can certainly be cleaned up, but I'm done for today and will return to this tomorrow.

[Scott Morrison]

Excellent, thank you! This will be a real milestone, our first abelian category. :-)

[Kevin Buzzard]

How come you didn't get a bunch of grief about no abelian categories and end up showing that the trivial category is abelian?? That happened for us with perfectoid spaces :-)

[Johan Commelin]

lemma singular_chain_complex_d_one_of_unique [subsingleton X] :
  ((singular_chain_complex R).obj X).d 1 = 0 :=

This means that if X is a topological space with at most 1 element, then the first differential d 1 of the singular chain complex of X with coefficients in a ring R is... the zero morphism.

[Johan Commelin]

Lean agrees that this is true.