Zulip Chat Archive

Stream: new members

Topic: learning Lean, running into problems


view this post on Zulip Drew Johnson (Dec 15 2020 at 22:59):

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!

view this post on Zulip Bryan Gin-ge Chen (Dec 15 2020 at 23:00):

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

view this post on Zulip Drew Johnson (Dec 15 2020 at 23:01):

Thanks! I'll read up on that.

view this post on Zulip Alex J. Best (Dec 15 2020 at 23:12):

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

view this post on Zulip Alex J. Best (Dec 15 2020 at 23:14):

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

view this post on Zulip Drew Johnson (Dec 16 2020 at 17:44):

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


Last updated: May 08 2021 at 11:09 UTC