chore(algebra/homology): further dualization (#7657)

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

src/algebra/homology/augment.lean

@@ -8,7 +8,7 @@ import algebra.homology.exact
 import tactic.linarith
 
 /-!
-# Augmentation and truncation of `ℕ`-indexed chain complexes.
+# Augmentation and truncation of `ℕ`-indexed (co)chain complexes.
 -/
 
 open category_theory
@@ -115,7 +115,7 @@ def truncate_augment (C : chain_complex V ℕ) {X : V} (f : C.X 0 ⟶ X) (w : C.
   (truncate_augment C f w).inv.f i = 𝟙 ((truncate.obj (augment C f w)).X i) :=
 by { cases i; refl, }
 
-@[simp] lemma cochain_complex_d_succ_succ_zero (C : chain_complex V ℕ) (i : ℕ) :
+@[simp] lemma chain_complex_d_succ_succ_zero (C : chain_complex V ℕ) (i : ℕ) :
   C.d (i+2) 0 = 0 :=
 by { rw C.shape, simp, omega, }
 
@@ -159,3 +159,142 @@ def to_single₀_as_complex
 let ⟨f, w⟩ := to_single₀_equiv C X f in augment C f w
 
 end chain_complex
+
+namespace cochain_complex
+
+/--
+The truncation of a `ℕ`-indexed cochain complex,
+deleting the object at `0` and shifting everything else down.
+-/
+@[simps]
+def truncate [has_zero_morphisms V] : cochain_complex V ℕ ⥤ cochain_complex V ℕ :=
+{ obj := λ C,
+  { X := λ i, C.X (i+1),
+    d := λ i j, C.d (i+1) (j+1),
+    shape' := λ i j w, by { apply C.shape, dsimp at w ⊢, omega, }, },
+  map := λ C D f,
+  { f := λ i, f.f (i+1), }, }
+
+/--
+There is a canonical chain map from the truncation of a cochain complex `C` to
+the "single object" cochain complex consisting of the truncated object `C.X 0` in degree 0.
+The components of this chain map are `C.d 0 1` in degree 0, and zero otherwise.
+-/
+def to_truncate [has_zero_object V] [has_zero_morphisms V] (C : cochain_complex V ℕ) :
+  (single₀ V).obj (C.X 0) ⟶ truncate.obj C :=
+(from_single₀_equiv (truncate.obj C) (C.X 0)).symm ⟨C.d 0 1, by tidy⟩
+
+variables [has_zero_morphisms V]
+
+/--
+We can "augment" a cochain complex by inserting an arbitrary object in degree zero
+(shifting everything else up), along with a suitable differential.
+-/
+def augment (C : cochain_complex V ℕ) {X : V} (f : X ⟶ C.X 0) (w : f ≫ C.d 0 1 = 0) :
+  cochain_complex V ℕ :=
+{ X := λ i, match i with
+  | 0 := X
+  | (i+1) := C.X i
+  end,
+  d := λ i j, match i, j with
+  | 0, 1 := f
+  | (i+1), (j+1) := C.d i j
+  | _, _ := 0
+  end,
+  shape' := λ i j s, begin
+    simp at s,
+    rcases j with _|_|j; cases i; unfold_aux; try { simp },
+    { simpa using s, },
+    { rw [C.shape], simp, omega, },
+  end,
+  d_comp_d' := λ i j k, begin
+    rcases k with _|_|k; rcases j with _|_|j; cases i; unfold_aux; try { simp },
+    cases k,
+    { exact w, },
+    { rw [C.shape, comp_zero],
+      simp, omega, },
+  end, }
+
+@[simp] lemma augment_X_zero
+  (C : cochain_complex V ℕ) {X : V} (f : X ⟶ C.X 0) (w : f ≫ C.d 0 1 = 0) :
+  (augment C f w).X 0 = X := rfl
+
+@[simp] lemma augment_X_succ
+  (C : cochain_complex V ℕ) {X : V} (f : X ⟶ C.X 0) (w : f ≫ C.d 0 1 = 0) (i : ℕ) :
+  (augment C f w).X (i+1) = C.X i := rfl
+
+@[simp] lemma augment_d_zero_one
+  (C : cochain_complex V ℕ) {X : V} (f : X ⟶ C.X 0) (w : f ≫ C.d 0 1 = 0) :
+  (augment C f w).d 0 1 = f := rfl
+
+@[simp] lemma augment_d_succ_succ
+  (C : cochain_complex V ℕ) {X : V} (f : X ⟶ C.X 0) (w : f ≫ C.d 0 1 = 0) (i j : ℕ) :
+  (augment C f w).d (i+1) (j+1) = C.d i j :=
+by { dsimp [augment], rcases i with _|i, refl, refl, }
+
+/--
+Truncating an augmented cochain complex is isomorphic (with components the identity)
+to the original complex.
+-/
+def truncate_augment (C : cochain_complex V ℕ) {X : V} (f : X ⟶ C.X 0) (w : f ≫ C.d 0 1 = 0) :
+  truncate.obj (augment C f w) ≅ C :=
+{ hom :=
+  { f := λ i, 𝟙 _, },
+  inv :=
+  { f := λ i, by { cases i; exact 𝟙 _, },
+    comm' := λ i j, by { cases i; cases j; { dsimp, simp, }, }, },
+  hom_inv_id' := by { ext i, cases i; { dsimp, simp, }, },
+  inv_hom_id' := by { ext i, cases i; { dsimp, simp, }, }, }.
+
+@[simp] lemma truncate_augment_hom_f
+  (C : cochain_complex V ℕ) {X : V} (f : X ⟶ C.X 0) (w : f ≫ C.d 0 1 = 0) (i : ℕ) :
+  (truncate_augment C f w).hom.f i = 𝟙 (C.X i) := rfl
+@[simp] lemma truncate_augment_inv_f
+  (C : cochain_complex V ℕ) {X : V} (f : X ⟶ C.X 0) (w : f ≫ C.d 0 1 = 0) (i : ℕ) :
+  (truncate_augment C f w).inv.f i = 𝟙 ((truncate.obj (augment C f w)).X i) :=
+by { cases i; refl, }
+
+@[simp] lemma cochain_complex_d_succ_succ_zero (C : cochain_complex V ℕ) (i : ℕ) :
+  C.d 0 (i+2) = 0 :=
+by { rw C.shape, simp, omega, }
+
+/--
+Augmenting a truncated complex with the original object and morphism is isomorphic
+(with components the identity) to the original complex.
+-/
+def augment_truncate (C : cochain_complex V ℕ) :
+  augment (truncate.obj C) (C.d 0 1) (C.d_comp_d _ _ _) ≅ C :=
+{ hom :=
+  { f := λ i, by { cases i; exact 𝟙 _, },
+    comm' := λ i j, by { rcases j with _|_|j; cases i; { dsimp, simp, }, }, },
+  inv :=
+  { f := λ i, by { cases i; exact 𝟙 _, },
+    comm' := λ i j, by { rcases j with _|_|j; cases i; { dsimp, simp, }, }, },
+  hom_inv_id' := by { ext i, cases i; { dsimp, simp, }, },
+  inv_hom_id' := by { ext i, cases i; { dsimp, simp, }, }, }.
+
+@[simp] lemma augment_truncate_hom_f_zero (C : cochain_complex V ℕ) :
+  (augment_truncate C).hom.f 0 = 𝟙 (C.X 0) :=
+rfl
+@[simp] lemma augment_truncate_hom_f_succ (C : cochain_complex V ℕ) (i : ℕ) :
+  (augment_truncate C).hom.f (i+1) = 𝟙 (C.X (i+1)) :=
+rfl
+@[simp] lemma augment_truncate_inv_f_zero (C : cochain_complex V ℕ) :
+  (augment_truncate C).inv.f 0 = 𝟙 (C.X 0) :=
+rfl
+@[simp] lemma augment_truncate_inv_f_succ (C : cochain_complex V ℕ) (i : ℕ) :
+  (augment_truncate C).inv.f (i+1) = 𝟙 (C.X (i+1)) :=
+rfl
+
+/--
+A chain map from a single object cochain complex in degree zero to a cochain complex
+can be reinterpreted as a cochain complex.
+
+Ths is the inverse construction of `to_truncate`.
+-/
+def from_single₀_as_complex
+  [has_zero_object V] (C : cochain_complex V ℕ) (X : V) (f : (single₀ V).obj X ⟶ C) :
+  cochain_complex V ℕ :=
+let ⟨f, w⟩ := from_single₀_equiv C X f in augment C f w
+
+end cochain_complex

src/algebra/homology/homological_complex.lean

@@ -544,8 +544,6 @@ end of_hom
 
 section mk
 
-/- TODO: dualize to `cochain_complex` -/
-
 /--
 Auxiliary structure for setting up the recursion in `mk`.
 This is purely an implementation detail: for some reason just using the dependent 6-tuple directly
@@ -739,4 +737,140 @@ from a dependently typed collection of morphisms.
 
 end of_hom
 
+section mk
+
+/--
+Auxiliary structure for setting up the recursion in `mk`.
+This is purely an implementation detail: for some reason just using the dependent 6-tuple directly
+results in `mk_aux` taking much longer (well over the `-T100000` limit) to elaborate.
+-/
+@[nolint has_inhabited_instance]
+structure mk_struct :=
+(X₀ X₁ X₂ : V)
+(d₀ : X₀ ⟶ X₁)
+(d₁ : X₁ ⟶ X₂)
+(s : d₀ ≫ d₁ = 0)
+
+variables {V}
+
+/-- Flatten to a tuple. -/
+def mk_struct.flat (t : mk_struct V) :
+  Σ' (X₀ X₁ X₂ : V) (d₀ : X₀ ⟶ X₁) (d₁ : X₁ ⟶ X₂), d₀ ≫ d₁ = 0 :=
+⟨t.X₀, t.X₁, t.X₂, t.d₀, t.d₁, t.s⟩
+
+variables (X₀ X₁ X₂ : V) (d₀ : X₀ ⟶ X₁) (d₁ : X₁ ⟶ X₂) (s : d₀ ≫ d₁ = 0)
+  (succ : Π (t : Σ' (X₀ X₁ X₂ : V) (d₀ : X₀ ⟶ X₁) (d₁ : X₁ ⟶ X₂), d₀ ≫ d₁ = 0),
+    Σ' (X₃ : V) (d₂ : t.2.2.1 ⟶ X₃), t.2.2.2.2.1 ≫ d₂ = 0)
+
+/-- Auxiliary definition for `mk`. -/
+def mk_aux :
+  Π n : ℕ, mk_struct V
+| 0 := ⟨X₀, X₁, X₂, d₀, d₁, s⟩
+| (n+1) :=
+  let p := mk_aux n in
+  ⟨p.X₁, p.X₂, (succ p.flat).1, p.d₁, (succ p.flat).2.1, (succ p.flat).2.2⟩
+
+/--
+A inductive constructor for `ℕ`-indexed cochain complexes.
+
+You provide explicitly the first two differentials,
+then a function which takes two differentials and the fact they compose to zero,
+and returns the next object, its differential, and the fact it composes appropiately to zero.
+
+See also `mk'`, which only sees the previous differential in the inductive step.
+-/
+def mk : cochain_complex V ℕ :=
+of (λ n, (mk_aux X₀ X₁ X₂ d₀ d₁ s succ n).X₀) (λ n, (mk_aux X₀ X₁ X₂ d₀ d₁ s succ n).d₀)
+  (λ n, (mk_aux X₀ X₁ X₂ d₀ d₁ s succ n).s)
+
+@[simp] lemma mk_X_0 : (mk X₀ X₁ X₂ d₀ d₁ s succ).X 0 = X₀ := rfl
+@[simp] lemma mk_X_1 : (mk X₀ X₁ X₂ d₀ d₁ s succ).X 1 = X₁ := rfl
+@[simp] lemma mk_X_2 : (mk X₀ X₁ X₂ d₀ d₁ s succ).X 2 = X₂ := rfl
+@[simp] lemma mk_d_1_0 : (mk X₀ X₁ X₂ d₀ d₁ s succ).d 0 1 = d₀ :=
+by { change ite (1 = 0 + 1) (d₀ ≫ 𝟙 X₁) 0 = d₀, rw [if_pos rfl, category.comp_id] }
+@[simp] lemma mk_d_2_0 : (mk X₀ X₁ X₂ d₀ d₁ s succ).d 1 2 = d₁ :=
+by { change ite (2 = 1 + 1) (d₁ ≫ 𝟙 X₂) 0 = d₁, rw [if_pos rfl, category.comp_id] }
+-- TODO simp lemmas for the inductive steps? It's not entirely clear that they are needed.
+
+/--
+A simpler inductive constructor for `ℕ`-indexed cochain complexes.
+
+You provide explicitly the first differential,
+then a function which takes a differential,
+and returns the next object, its differential, and the fact it composes appropriately to zero.
+-/
+def mk' (X₀ X₁ : V) (d : X₀ ⟶ X₁)
+  (succ' : Π (t : Σ (X₀ X₁ : V), X₀ ⟶ X₁), Σ' (X₂ : V) (d : t.2.1 ⟶ X₂), t.2.2 ≫ d = 0) :
+  cochain_complex V ℕ :=
+mk X₀ X₁ (succ' ⟨X₀, X₁, d⟩).1 d (succ' ⟨X₀, X₁, d⟩).2.1 (succ' ⟨X₀, X₁, d⟩).2.2
+  (λ t, succ' ⟨t.2.1, t.2.2.1, t.2.2.2.2.1⟩)
+
+variables (succ' : Π (t : Σ (X₀ X₁ : V), X₀ ⟶ X₁), Σ' (X₂ : V) (d : t.2.1 ⟶ X₂), t.2.2 ≫ d = 0)
+
+@[simp] lemma mk'_X_0 : (mk' X₀ X₁ d₀ succ').X 0 = X₀ := rfl
+@[simp] lemma mk'_X_1 : (mk' X₀ X₁ d₀ succ').X 1 = X₁ := rfl
+@[simp] lemma mk'_d_1_0 : (mk' X₀ X₁ d₀ succ').d 0 1 = d₀ :=
+by { change ite (1 = 0 + 1) (d₀ ≫ 𝟙 X₁) 0 = d₀, rw [if_pos rfl, category.comp_id] }
+-- TODO simp lemmas for the inductive steps? It's not entirely clear that they are needed.
+
+end mk
+
+section mk_hom
+
+variables {V} (P Q : cochain_complex V ℕ)
+  (zero : P.X 0 ⟶ Q.X 0)
+  (one : P.X 1 ⟶ Q.X 1)
+  (one_zero_comm : zero ≫ Q.d 0 1 = P.d 0 1 ≫ one)
+  (succ : ∀ (n : ℕ)
+    (p : Σ' (f : P.X n ⟶ Q.X n) (f' : P.X (n+1) ⟶ Q.X (n+1)), f ≫ Q.d n (n+1) = P.d n (n+1) ≫ f'),
+    Σ' f'' : P.X (n+2) ⟶ Q.X (n+2), p.2.1 ≫ Q.d (n+1) (n+2) = P.d (n+1) (n+2) ≫ f'')
+
+/--
+An auxiliary construction for `mk_hom`.
+
+Here we build by induction a family of commutative squares,
+but don't require at the type level that these successive commutative squares actually agree.
+They do in fact agree, and we then capture that at the type level (i.e. by constructing a chain map)
+in `mk_hom`.
+-/
+def mk_hom_aux :
+  Π n, Σ' (f : P.X n ⟶ Q.X n) (f' : P.X (n+1) ⟶ Q.X (n+1)), f ≫ Q.d n (n+1) = P.d n (n+1) ≫ f'
+| 0 := ⟨zero, one, one_zero_comm⟩
+| (n+1) := ⟨(mk_hom_aux n).2.1,
+    (succ n (mk_hom_aux n)).1, (succ n (mk_hom_aux n)).2⟩
+
+/--
+A constructor for chain maps between `ℕ`-indexed cochain complexes,
+working by induction on commutative squares.
+
+You need to provide the components of the chain map in degrees 0 and 1,
+show that these form a commutative square,
+and then give a construction of each component,
+and the fact that it forms a commutative square with the previous component,
+using as an inductive hypothesis the data (and commutativity) of the previous two components.
+-/
+def mk_hom : P ⟶ Q :=
+{ f := λ n, (mk_hom_aux P Q zero one one_zero_comm succ n).1,
+  comm' := λ n m,
+  begin
+    by_cases h : n + 1 = m,
+    { subst h,
+      exact (mk_hom_aux P Q zero one one_zero_comm succ n).2.2 },
+    { rw [P.shape n m h, Q.shape n m h], simp }
+  end }
+
+@[simp] lemma mk_hom_f_0 : (mk_hom P Q zero one one_zero_comm succ).f 0 = zero := rfl
+@[simp] lemma mk_hom_f_1 : (mk_hom P Q zero one one_zero_comm succ).f 1 = one := rfl
+@[simp] lemma mk_hom_f_succ_succ (n : ℕ) :
+  (mk_hom P Q zero one one_zero_comm succ).f (n+2) =
+    (succ n ⟨(mk_hom P Q zero one one_zero_comm succ).f n,
+      (mk_hom P Q zero one one_zero_comm succ).f (n+1),
+        (mk_hom P Q zero one one_zero_comm succ).comm n (n+1)⟩).1 :=
+begin
+  dsimp [mk_hom, mk_hom_aux],
+  induction n; congr,
+end
+
+end mk_hom
+
 end cochain_complex