From 7f46c81169668848c435e8579dca700a880ba3ca Mon Sep 17 00:00:00 2001 From: Scott Morrison Date: Tue, 23 Feb 2021 14:09:44 +0000 Subject: [PATCH] feat(chain_complex): lemmas about eq_to_hom (#6250) Adds two lemmas relating `eq_to_hom` to differentials and chain maps. Useful in the ubiquitous circumstance of having to apply identities in the index of a chain complex. Also add some `@[reassoc]` tags for convenience. Co-authored-by: Scott Morrison --- src/algebra/homology/chain_complex.lean | 23 ++++++++++++++++++++--- 1 file changed, 20 insertions(+), 3 deletions(-) diff --git a/src/algebra/homology/chain_complex.lean b/src/algebra/homology/chain_complex.lean index 41dcb35b29bdd..c5cdffa80c36c 100644 --- a/src/algebra/homology/chain_complex.lean +++ b/src/algebra/homology/chain_complex.lean @@ -65,7 +65,7 @@ namespace homological_complex variables {V} variables {β : Type} [add_comm_group β] {b : β} -@[simp] +@[simp, reassoc] lemma d_squared (C : homological_complex V b) (i : β) : C.d i ≫ C.d (i+b) = 0 := congr_fun (C.d_squared) i @@ -75,15 +75,32 @@ A convenience lemma for morphisms of cochain complexes, picking out one component of the commutation relation. -/ -- I haven't been able to get this to work with projection notation: `f.comm_at i` -@[simp] +@[simp, reassoc] lemma comm_at {C D : homological_complex V b} (f : C ⟶ D) (i : β) : C.d i ≫ f.f (i+b) = f.f i ≫ D.d i := congr_fun f.comm i -@[simp] +@[simp, reassoc] lemma comm {C D : homological_complex V b} (f : C ⟶ D) : C.d ≫ f.f⟦1⟧' = f.f ≫ D.d := differential_object.hom.comm _ +@[reassoc] +lemma eq_to_hom_d (C : homological_complex V b) {i j : β} (h : i = j) : + eq_to_hom (congr_arg C.X h) ≫ C.d j = + C.d i ≫ eq_to_hom (congr_arg C.X (congr_arg (λ a, a + b) h) : _) := +begin + induction h, + simp, +end + +@[reassoc] +lemma eq_to_hom_f {C D : homological_complex V b} (f : C ⟶ D) {n m : β} (h : n = m) : + eq_to_hom (congr_arg C.X h) ≫ f.f m = f.f n ≫ eq_to_hom (congr_arg D.X h) := +begin + induction h, + simp +end + variables (V) /-- The forgetful functor from cochain complexes to graded objects, forgetting the differential. -/