Boundary of an embedding of complex shapes

In the file Mathlib/Algebra/Homology/Embedding/Basic.lean, 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 Mathlib/Algebra/Homology/Embedding/Extend.lean) 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.

def ComplexShape.Embedding.BoundaryGE {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} (e : c.Embedding c') (j : ι) : Prop

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).

Equations

• e.BoundaryGE j = (c'.Rel (c'.prev (e.f j)) (e.f j) ∧ ∀ (i : ι), ¬c'.Rel (e.f i) (e.f j))

theorem ComplexShape.Embedding.boundaryGE {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} (e : c.Embedding c') {i' : ι'} {j : ι} (hj : c'.Rel i' (e.f j)) (hi' : ∀ (i : ι), e.f i ≠ i') : e.BoundaryGE j

theorem ComplexShape.Embedding.not_boundaryGE_next {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} (e : c.Embedding c') [e.IsRelIff] {j k : ι} (hk : c.Rel j k) : ¬e.BoundaryGE k

theorem ComplexShape.Embedding.not_boundaryGE_next' {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} (e : c.Embedding c') [e.IsRelIff] {j k : ι} (hj : ¬e.BoundaryGE j) (hk : c.next j = k) : ¬e.BoundaryGE k

theorem ComplexShape.Embedding.BoundaryGE.notMem {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {e : c.Embedding c'} {j : ι} (hj : e.BoundaryGE j) {i' : ι'} (hi' : c'.Rel i' (e.f j)) (a : ι) : e.f a ≠ i'

@[deprecated ComplexShape.Embedding.BoundaryGE.notMem (since := "2025-05-23")]

theorem ComplexShape.Embedding.BoundaryGE.not_mem {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {e : c.Embedding c'} {j : ι} (hj : e.BoundaryGE j) {i' : ι'} (hi' : c'.Rel i' (e.f j)) (a : ι) : e.f a ≠ i'

Alias of ComplexShape.Embedding.BoundaryGE.notMem.

theorem ComplexShape.Embedding.prev_f_of_not_boundaryGE {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} (e : c.Embedding c') [e.IsRelIff] {i j : ι} (hij : c.prev j = i) (hj : ¬e.BoundaryGE j) : c'.prev (e.f j) = e.f i

theorem ComplexShape.Embedding.BoundaryGE.false_of_isTruncLE {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {e : c.Embedding c'} {j : ι} (hj : e.BoundaryGE j) [e.IsTruncLE] : False

def ComplexShape.Embedding.BoundaryLE {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} (e : c.Embedding c') (j : ι) : Prop

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'.

Equations

• e.BoundaryLE j = (c'.Rel (e.f j) (c'.next (e.f j)) ∧ ∀ (k : ι), ¬c'.Rel (e.f j) (e.f k))

theorem ComplexShape.Embedding.boundaryLE {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} (e : c.Embedding c') {k' : ι'} {j : ι} (hj : c'.Rel (e.f j) k') (hk' : ∀ (i : ι), e.f i ≠ k') : e.BoundaryLE j

theorem ComplexShape.Embedding.not_boundaryLE_prev {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} (e : c.Embedding c') [e.IsRelIff] {i j : ι} (hi : c.Rel i j) : ¬e.BoundaryLE i

theorem ComplexShape.Embedding.not_boundaryLE_prev' {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} (e : c.Embedding c') [e.IsRelIff] {i j : ι} (hj : ¬e.BoundaryLE j) (hk : c.prev j = i) : ¬e.BoundaryLE i

theorem ComplexShape.Embedding.BoundaryLE.notMem {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {e : c.Embedding c'} {j : ι} (hj : e.BoundaryLE j) {k' : ι'} (hk' : c'.Rel (e.f j) k') (a : ι) : e.f a ≠ k'

@[deprecated ComplexShape.Embedding.BoundaryLE.notMem (since := "2025-05-23")]

theorem ComplexShape.Embedding.BoundaryLE.not_mem {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {e : c.Embedding c'} {j : ι} (hj : e.BoundaryLE j) {k' : ι'} (hk' : c'.Rel (e.f j) k') (a : ι) : e.f a ≠ k'

Alias of ComplexShape.Embedding.BoundaryLE.notMem.

theorem ComplexShape.Embedding.next_f_of_not_boundaryLE {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} (e : c.Embedding c') [e.IsRelIff] {j k : ι} (hjk : c.next j = k) (hj : ¬e.BoundaryLE j) : c'.next (e.f j) = e.f k

theorem ComplexShape.Embedding.next_f {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} (e : c.Embedding c') [e.IsTruncGE] {j k : ι} (hjk : c.next j = k) : c'.next (e.f j) = e.f k

theorem ComplexShape.Embedding.prev_f {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} (e : c.Embedding c') [e.IsTruncLE] {i j : ι} (hij : c.prev j = i) : c'.prev (e.f j) = e.f i

theorem ComplexShape.Embedding.BoundaryLE.false_of_isTruncGE {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {e : c.Embedding c'} {j : ι} (hj : e.BoundaryLE j) [e.IsTruncGE] : False

@[simp]

theorem ComplexShape.Embedding.op_boundaryLE_iff {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} (e : c.Embedding c') {j : ι} : e.op.BoundaryLE j ↔ e.BoundaryGE j

@[simp]

theorem ComplexShape.Embedding.op_boundaryGE_iff {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} (e : c.Embedding c') {j : ι} : e.op.BoundaryGE j ↔ e.BoundaryLE j

theorem ComplexShape.boundaryGE_embeddingUpIntGE_iff (p : ℤ) (n : ℕ) : (embeddingUpIntGE p).BoundaryGE n ↔ n = 0

theorem ComplexShape.boundaryLE_embeddingUpIntLE_iff (p : ℤ) (n : ℕ) : (embeddingUpIntLE p).BoundaryLE n ↔ n = 0