learning Lean, running into problems

Stream: new members

[Drew Johnson]

I've worked through some tutorials and read some documentation and I'm excited about Lean. Whenever I try to do something non-trivial by myself, I run into problems. Here's an example. I'm trying to define a dg-category (this is mostly an education exercise for me. but I didn't see this in mathlib, yet either, so maybe I can contribute eventually):

import algebra.category.Module.basic
import algebra.homology.chain_complex

open category_theory

universes v u

variables (C : Type u)

class dgcat :=
  (hom : Π P Q : C, (cochain_complex (Module(ℚ))))
  (comp: Π {P Q R: C} {i j : ℤ}, (hom Q R).X i -> (hom P Q).X j -> (hom P R).X (i+j))
  (id : Π P : C, (hom P P).X 0)
  (leibnitz: Π (P Q R: C) (i j : ℤ)  (g: (hom Q R).X i) (f : (hom P Q).X j),
    (hom P R).d (i+j) (comp g f) = comp ((hom Q R).d i g) f + (-1)^i * comp g ((hom P Q).d j f)

The last property of the class does not check out. If I comment it out and put

variables (D:Type u) [dgcat D]
variables P Q R: D
variables i j : ℤ
variable (g: (dgcat.hom Q R).X i)
variable (f : (dgcat.hom P Q).X j)

#check (dgcat.hom P R).d (i+j) (dgcat.comp g f)

#check dgcat.comp ((dgcat.hom Q R).d i g) f

#check dgcat.comp g ((dgcat.hom P Q).d j f)

then you can see why. Lean doesn't recognize these as the same type, even though they should be living in (hom P R) (i+j+1). The types are given by

⇑((dgcat.hom P R).d (i + j)) (dgcat.comp g f) :
  ↥((shift (graded_object_with_shift 1 (Module ℚ)) ^ 1).functor.obj (dgcat.hom P R).X (i + j))

dgcat.comp (⇑((dgcat.hom Q R).d i) g) f :
  ↥((dgcat.hom P R).X
       (⇑({to_fun := λ (b : ℤ), b - 1, inv_fun := λ (b : ℤ), b + 1, left_inv := _, right_inv := _}.symm) i + j))

dgcat.comp g (⇑((dgcat.hom P Q).d j) f) :
  ↥((dgcat.hom P R).X
       (i + ⇑({to_fun := λ (b : ℤ), b - 1, inv_fun := λ (b : ℤ), b + 1, left_inv := _, right_inv := _}.symm) j))

What do the various up pointing arrows mean? Is there a way I can make this work? Thank you for any hints!

[Bryan Gin-ge Chen]

The arrows are different types of coercions; you can read more about them in Section 10.6 of TPiL.

[Drew Johnson]

Thanks! I'll read up on that.

[Alex J. Best]

You should check out this old thread on cdgas https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/CDGAs/near/167848869 . It's quite possible you are running into this classic problem with this sort of maths in leans type theory, where you can prove the indices are equal, but they are not equal by definition so lean will not treat them as terms of the same type

[Alex J. Best]

And also see https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/tensor.20algebras.20and.20a.20construction/near/214985046

[Drew Johnson]

Thank you! I think that was exactly the issue I was running into.