Working with cochain complexes

Stream: new members

[Liran Shaul]

Hello!

I am trying to understand how to do some very basic things (for now) with cochain complexes over a ring.
For instance, the simple property that if M is a complex, it holds that d^1_M d^0_M (x) = 0 for all x in M^0.

I ran into a problem, with the following code:
variable (A : Type u) [CommRing A] [IsNoetherianRing A]

variable (M : CochainComplex (ModuleCat A) ℤ)

example : ∀ x: M.X 0, (M.d 1 2) ((M.d 0 1) x) = 0 := by

intro x

sorry

The state I have is

A : Type u
inst✝¹ : CommRing A
inst✝ : IsNoetherianRing A
M : CochainComplex (ModuleCat A) ℤ
⊢ ∀ (x : ↑(M.X 0)), (CategoryTheory.ConcreteCategory.hom (M.d 1 2)) ((CategoryTheory.ConcreteCategory.hom (M.d 0 1)) x) = 0

Now, Homological complex has the property d_comp_d', which should give the result. My problem is that it gives me an assumption l : CategoryTheory.CategoryStruct.comp (M.d 0 1) (M.d 1 2) = 0
⊢ (CategoryTheory.ConcreteCategory.hom (M.d 1 2)) and lean doesn't know how to connect CategoryTheory.CategoryStruct.comp with CategoryTheory.ConcreteCategory.hom. Any idea how to proceed? this surely should have a very simple solution. Thank you!

[Vlad Tsyrklevich]

Pleaser read #backticks and #mwe for some guidelines for how to post to make it easier for people answering your question.

[Vlad Tsyrklevich]

I was able to use the rw? tactic to find the necessary lemma. rw? and apply? can often be used to find the lemma you require in such a moment--though for more complicated situations it is useful to know how to use loogle to search for lemmas.

import Mathlib

variable (A : Type u) [CommRing A] [IsNoetherianRing A]

variable (M : CochainComplex (ModuleCat A) ℤ)

example : ∀ x: M.X 0, (M.d 1 2) ((M.d 0 1) x) = 0 := by
  intro x
  rw [← ModuleCat.comp_apply] -- rw?
  rw [M.d_comp_d' 0 1 2 rfl rfl] -- rw?
  rfl

[Liran Shaul]

Excellent, thank you very much!
And I will keep in mind the posting guidelines as well.

Vlad Tsyrklevich said:

I was able to use the rw? tactic to find the necessary lemma. rw? and apply? can often be used to find the lemma you require in such a moment--though for more complicated situations it is useful to know how to use loogle to search for lemmas.

import Mathlib

variable (A : Type u) [CommRing A] [IsNoetherianRing A]

variable (M : CochainComplex (ModuleCat A) ℤ)

example : ∀ x: M.X 0, (M.d 1 2) ((M.d 0 1) x) = 0 := by
  intro x
  rw [← ModuleCat.comp_apply] -- rw?
  rw [M.d_comp_d' 0 1 2 rfl rfl] -- rw?
  rfl