Documentation

Mathlib.Algebra.Homology.Embedding.Boundary

Boundary of an embedding of complex shapes #

In the file Mathlib.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 Mathlib.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.

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

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

Instances For

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

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] :

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

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

Instances For

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

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.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] :

theorem ComplexShape.boundaryGE_embeddingUpIntGE_iff (p : ℤ) (n : ℕ) :

(ComplexShape.embeddingUpIntGE p).BoundaryGE n ↔ n = 0

theorem ComplexShape.boundaryLE_embeddingUpIntLE_iff (p : ℤ) (n : ℕ) :

(ComplexShape.embeddingUpIntGE p).BoundaryGE n ↔ n = 0