feat(Algebra/Homology): left shifting cochains (#9054)

In this PR, we study the behaviour of cochains (of the complex of homomorphisms) with respect to shifts on the source. In particular, we obtain an additive equivalence `leftShiftAddEquiv K L n a n' h : Cochain K L n ≃+ Cochain K⟦a⟧ L n'` when `h : n + a = n'`. Co-authored-by: Joël Riou <[email protected]>
leanprover-community · Jan 5, 2024 · 710ecf0 · 710ecf0
1 parent e3d1c7a
commit 710ecf0
Show file tree

Hide file tree

Showing 2 changed files with 314 additions and 5 deletions.
diff --git a/Mathlib/Algebra/GroupPower/NegOnePow.lean b/Mathlib/Algebra/GroupPower/NegOnePow.lean
@@ -86,4 +86,13 @@ lemma negOnePow_eq_iff (n₁ n₂ : ℤ) :
       Int.even_iff_not_odd, Int.even_iff_not_odd]
     tauto
 
+@[simp]
+lemma negOnePow_mul_self (n : ℤ) : (n * n).negOnePow = n.negOnePow := by
+  suffices Even (n * (n - 1)) by
+    simpa [mul_sub, mul_one, negOnePow_eq_iff] using this
+  rw [even_mul]
+  by_cases h : Even (n - 1)
+  · exact Or.inr h
+  · exact Or.inl (by simpa using Int.even_add_one.2 h)
+
 end Int