feat(Algebra/Homology): boundaries of embeddings of complex shapes (#14650)

In this PR, we define the lower/upper boundaries of embeddings of complex shapes. These notions shall be important when constructing canonical truncations of homological complexes.

Author: joelriou

Mathlib.lean

@@ -324,6 +324,7 @@ import Mathlib.Algebra.Homology.DerivedCategory.ShortExact
 import Mathlib.Algebra.Homology.DerivedCategory.SingleTriangle
 import Mathlib.Algebra.Homology.DifferentialObject
 import Mathlib.Algebra.Homology.Embedding.Basic
+import Mathlib.Algebra.Homology.Embedding.Boundary
 import Mathlib.Algebra.Homology.Embedding.Extend
 import Mathlib.Algebra.Homology.Embedding.IsSupported
 import Mathlib.Algebra.Homology.Embedding.Restriction

Mathlib/Algebra/Homology/ComplexShape.lean

@@ -164,6 +164,22 @@ theorem prev_eq' (c : ComplexShape ι) {i j : ι} (h : c.Rel i j) : c.prev j = i
   exact Exists.choose_spec (⟨i, h⟩ : ∃ k, c.Rel k j)
 #align complex_shape.prev_eq' ComplexShape.prev_eq'
 
+lemma next_eq_self' (c : ComplexShape ι) (j : ι) (hj : ∀ k, ¬ c.Rel j k) :
+    c.next j = j :=
+  dif_neg (by simpa using hj)
+
+lemma prev_eq_self' (c : ComplexShape ι) (j : ι) (hj : ∀ i, ¬ c.Rel i j) :
+    c.prev j = j :=
+  dif_neg (by simpa using hj)
+
+lemma next_eq_self (c : ComplexShape ι) (j : ι) (hj : ¬ c.Rel j (c.next j)) :
+    c.next j = j :=
+  c.next_eq_self' j (fun k hk' => hj (by simpa only [c.next_eq' hk'] using hk'))
+
+lemma prev_eq_self (c : ComplexShape ι) (j : ι) (hj : ¬ c.Rel (c.prev j) j) :
+    c.prev j = j :=
+  c.prev_eq_self' j (fun k hk' => hj (by simpa only [c.prev_eq' hk'] using hk'))
+
 /-- The `ComplexShape` allowing differentials from `X i` to `X (i+a)`.
 (For example when `a = 1`, a cohomology theory indexed by `ℕ` or `ℤ`)
 -/

Mathlib/Algebra/Homology/Embedding/Basic.lean

@@ -106,12 +106,18 @@ class IsTruncGE extends e.IsRelIff : Prop where
   mem_next {j : ι} {k' : ι'} (h : c'.Rel (e.f j) k') :
     ∃ k, e.f k = k'
 
+lemma mem_next [e.IsTruncGE] {j : ι} {k' : ι'} (h : c'.Rel (e.f j) k') : ∃ k, e.f k = k' :=
+  IsTruncGE.mem_next h
+
 /-- The condition that the image of the map `e.f` of an embedding of
 complex shapes `e : Embedding c c'` is stable by `c'.prev`. -/
 class IsTruncLE extends e.IsRelIff : Prop where
   mem_prev {i' : ι'} {j : ι} (h : c'.Rel i' (e.f j)) :
     ∃ i, e.f i = i'
 
+lemma mem_prev [e.IsTruncLE] {i' : ι'} {j : ι} (h : c'.Rel i' (e.f j)) : ∃ i, e.f i = i' :=
+  IsTruncLE.mem_prev h
+
 open Classical in
 /-- The map `ι' → Option ι` which sends `e.f i` to `some i` and the other elements to `none`. -/
 noncomputable def r (i' : ι') : Option ι :=

Mathlib/Algebra/Homology/Embedding/Boundary.lean

@@ -0,0 +1,181 @@
+/-
+Copyright (c) 2024 Joël Riou. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joël Riou
+-/
+import Mathlib.Algebra.Homology.Embedding.Basic
+import Mathlib.Algebra.Homology.HomologicalComplex
+
+/-!
+# Boundary of an embedding of complex shapes
+
+In the file `Algebra.Homology.Embedding.Basic`, given `p : ℤ`, we have defined
+an embedding `embeddingUpIntGE p` of `ComplexShape.up ℕ` in `ComplexShape.up ℤ`
+which sends `n : ℕ` to `p + n`. The (canonical) truncation (`≥ p`) of
+`K : CochainComplex C ℤ` shall be defined as the extension to `ℤ`
+(see `Algebra.Homology.Embedding.Extend`) of
+a certain cochain complex indexed by `ℕ`:
+
+`Q ⟶ K.X (p + 1) ⟶ K.X (p + 2) ⟶ K.X (p + 3) ⟶ ...`
+
+where in degree `0`, the object `Q` identifies to the cokernel
+of `K.X (p - 1) ⟶ K.X p` (this is `K.opcycles p`). In this case,
+we see that the degree `0 : ℕ` needs a particular attention when
+constructing the truncation.
+
+In this file, more generally, for `e : Embedding c c'`, we define
+a predicate `ι → Prop` named `e.BoundaryGE` which shall be relevant
+when constructing the truncation `K.truncGE e` when `e.IsTruncGE`.
+In the case of `embeddingUpIntGE p`, we show that `0 : ℕ` is the
+only element in this lower boundary. Similarly, we define
+`Embedding.BoundaryLE`.
+
+-/
+
+namespace ComplexShape
+
+namespace Embedding
+
+variable {ι ι' : Type*} (c : ComplexShape ι) (c' : ComplexShape ι') (e : Embedding c c')
+
+/-- The lower boundary of an embedding `e : Embedding c c'`, as a predicate on `ι`.
+It is satisfied by `j : ι` when there exists `i' : ι'` not in the image of `e.f`
+such that `c'.Rel i' (e.f j)`. -/
+def BoundaryGE (j : ι) : Prop :=
+  c'.Rel (c'.prev (e.f j)) (e.f j) ∧ ∀ i, ¬c'.Rel (e.f i) (e.f j)
+
+lemma boundaryGE {i' : ι'} {j : ι} (hj : c'.Rel i' (e.f j)) (hi' : ∀ i, e.f i ≠ i') :
+    e.BoundaryGE j := by
+  constructor
+  · simpa only [c'.prev_eq' hj] using hj
+  · intro i hi
+    apply hi' i
+    rw [← c'.prev_eq' hj, c'.prev_eq' hi]
+
+lemma not_boundaryGE_next [e.IsRelIff] {j k : ι} (hk : c.Rel j k) :
+    ¬ e.BoundaryGE k := by
+  dsimp [BoundaryGE]
+  simp only [not_and, not_forall, not_not]
+  intro
+  exact ⟨j, by simpa only [e.rel_iff] using hk⟩
+
+lemma not_boundaryGE_next' [e.IsRelIff] {j k : ι} (hj : ¬ e.BoundaryGE j) (hk : c.next j = k) :
+    ¬ e.BoundaryGE k := by
+  by_cases hjk : c.Rel j k
+  · exact e.not_boundaryGE_next hjk
+  · subst hk
+    simpa only [c.next_eq_self j hjk] using hj
+
+variable {e} in
+lemma BoundaryGE.not_mem {j : ι} (hj : e.BoundaryGE j) {i' : ι'} (hi' : c'.Rel i' (e.f j))
+    (a : ι) : e.f a ≠ i' := fun ha =>
+  hj.2 a (by simpa only [ha] using hi')
+
+lemma prev_f_of_not_boundaryGE [e.IsRelIff] {i j : ι} (hij : c.prev j = i)
+    (hj : ¬ e.BoundaryGE j) :
+    c'.prev (e.f j) = e.f i := by
+  by_cases hij' : c.Rel i j
+  · exact c'.prev_eq' (by simpa only [e.rel_iff] using hij')
+  · obtain rfl : j = i := by
+      simpa only [c.prev_eq_self j (by simpa only [hij] using hij')] using hij
+    apply c'.prev_eq_self
+    intro hj'
+    simp only [BoundaryGE, not_and, not_forall, not_not] at hj
+    obtain ⟨i, hi⟩ := hj hj'
+    rw [e.rel_iff] at hi
+    rw [c.prev_eq' hi] at hij
+    exact hij' (by simpa only [hij] using hi)
+
+variable {e} in
+lemma BoundaryGE.false {j : ι} (hj : e.BoundaryGE j) [e.IsTruncLE] : False := by
+  obtain ⟨i, hi⟩ := e.mem_prev hj.1
+  exact hj.2 i (by simpa only [hi] using hj.1)
+
+/-- The upper boundary of an embedding `e : Embedding c c'`, as a predicate on `ι`.
+It is satisfied by `j : ι` when there exists `k' : ι'` not in the image of `e.f`
+such that `c'.Rel (e.f j) k'`. -/
+def BoundaryLE (j : ι) : Prop :=
+  c'.Rel (e.f j) (c'.next (e.f j)) ∧ ∀ k, ¬c'.Rel (e.f j) (e.f k)
+
+lemma boundaryLE {k' : ι'} {j : ι} (hj : c'.Rel (e.f j) k') (hk' : ∀ i, e.f i ≠ k') :
+    e.BoundaryLE j := by
+  constructor
+  · simpa only [c'.next_eq' hj] using hj
+  · intro k hk
+    apply hk' k
+    rw [← c'.next_eq' hj, c'.next_eq' hk]
+
+lemma not_boundaryLE_prev [e.IsRelIff] {i j : ι} (hi : c.Rel i j) :
+    ¬ e.BoundaryLE i := by
+  dsimp [BoundaryLE]
+  simp only [not_and, not_forall, not_not]
+  intro
+  exact ⟨j, by simpa only [e.rel_iff] using hi⟩
+
+lemma not_boundaryLE_prev' [e.IsRelIff] {i j : ι} (hj : ¬ e.BoundaryLE j) (hk : c.prev j = i) :
+    ¬ e.BoundaryLE i := by
+  by_cases hij : c.Rel i j
+  · exact e.not_boundaryLE_prev hij
+  · subst hk
+    simpa only [c.prev_eq_self j hij] using hj
+
+variable {e} in
+lemma BoundaryLE.not_mem {j : ι} (hj : e.BoundaryLE j) {k' : ι'} (hk' : c'.Rel (e.f j) k')
+    (a : ι) : e.f a ≠ k' := fun ha =>
+  hj.2 a (by simpa only [ha] using hk')
+
+lemma next_f_of_not_boundaryLE [e.IsRelIff] {j k : ι} (hjk : c.next j = k)
+    (hj : ¬ e.BoundaryLE j) :
+    c'.next (e.f j) = e.f k := by
+  by_cases hjk' : c.Rel j k
+  · exact c'.next_eq' (by simpa only [e.rel_iff] using hjk')
+  · obtain rfl : j = k := by
+      simpa only [c.next_eq_self j (by simpa only [hjk] using hjk')] using hjk
+    apply c'.next_eq_self
+    intro hj'
+    simp only [BoundaryLE, not_and, not_forall, not_not] at hj
+    obtain ⟨k, hk⟩ := hj hj'
+    rw [e.rel_iff] at hk
+    rw [c.next_eq' hk] at hjk
+    exact hjk' (by simpa only [hjk] using hk)
+
+variable {e} in
+lemma BoundaryLE.false {j : ι} (hj : e.BoundaryLE j) [e.IsTruncGE] : False := by
+  obtain ⟨k, hk⟩ := e.mem_next hj.1
+  exact hj.2 k (by simpa only [hk] using hj.1)
+
+end Embedding
+
+lemma boundaryGE_embeddingUpIntGE_iff (p : ℤ) (n : ℕ) :
+    (embeddingUpIntGE p).BoundaryGE n ↔ n = 0 := by
+  constructor
+  · intro h
+    obtain _|n := n
+    · rfl
+    · have := h.2 n
+      dsimp at this
+      omega
+  · rintro rfl
+    constructor
+    · simp
+    · intro i hi
+      dsimp at hi
+      omega
+
+lemma boundaryLE_embeddingUpIntLE_iff (p : ℤ) (n : ℕ) :
+    (embeddingUpIntGE p).BoundaryGE n ↔ n = 0 := by
+  constructor
+  · intro h
+    obtain _|n := n
+    · rfl
+    · have := h.2 n
+      dsimp at this
+      omega
+  · rintro rfl
+    constructor
+    · simp
+    · intro i hi
+      dsimp at hi
+      omega
+
+end ComplexShape