Embeddings of complex shapes

Given two complex shapes c : ComplexShape ι and c' : ComplexShape ι', an embedding from c to c' (e : c.Embedding c') consists of the data of an injective map f : ι → ι' such that for all i₁ i₂ : ι, c.Rel i₁ i₂ implies c'.Rel (e.f i₁) (e.f i₂). We define a type class e.IsRelIff to express that this implication is an equivalence. Other type classes e.IsTruncLE and e.IsTruncGE are introduced in order to formalize truncation functors.

This notion first appeared in the Liquid Tensor Experiment, and was developed there mostly by Johan Commelin, Adam Topaz and Joël Riou. It shall be used in order to relate the categories CochainComplex C ℕ and ChainComplex C ℕ to CochainComplex C ℤ. It shall also be used in the construction of the canonical t-structure on the derived category of an abelian category (TODO).

Description of the API

• The extension functor e.extendFunctor C : HomologicalComplex C c ⥤ HomologicalComplex C c' (extending by the zero object outside of the image of e.f) is defined in the file Embedding.Extend;
• assuming e.IsRelIff, the restriction functor e.restrictionFunctor C : HomologicalComplex C c' ⥤ HomologicalComplex C c is defined in the file Embedding.Restriction;
• the stupid truncation functor e.stupidTruncFunctor C : HomologicalComplex C c' ⥤ HomologicalComplex C c' which is the composition of the two previous functors is defined in the file Embedding.StupidTrunc.
• assuming e.IsTruncGE, we have truncation functors e.truncGE'Functor C : HomologicalComplex C c' ⥤ HomologicalComplex C c and e.truncGEFunctor C : HomologicalComplex C c' ⥤ HomologicalComplex C c' (see the file Embedding.TruncGE), and a natural transformation e.πTruncGENatTrans : 𝟭 _ ⟶ e.truncGEFunctor C which is a quasi-isomorphism in degrees in the image of e.f (TODO);
• assuming e.IsTruncLE, we have truncation functors e.truncLE'Functor C : HomologicalComplex C c' ⥤ HomologicalComplex C c and e.truncLEFunctor C : HomologicalComplex C c' ⥤ HomologicalComplex C c', and a natural transformation e.ιTruncLENatTrans : e.truncGEFunctor C ⟶ 𝟭 _ which is a quasi-isomorphism in degrees in the image of e.f (TODO);

structure ComplexShape.Embedding {ι : Type u_1} {ι' : Type u_2} (c : ComplexShape ι) (c' : ComplexShape ι') : Type (max u_1 u_2)

An embedding of a complex shape c : ComplexShape ι into a complex shape c' : ComplexShape ι' consists of an injective map f : ι → ι' which satisfies a compatibility with respect to the relations c.Rel and c'.Rel.

• f : ι → ι'

  the map between the underlying types of indices

• injective_f : Function.Injective self.f
• rel {i₁ i₂ : ι} (h : c.Rel i₁ i₂) : c'.Rel (self.f i₁) (self.f i₂)

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

The opposite embedding in Embedding c.symm c'.symm of e : Embedding c c'.

@[simp]

theorem ComplexShape.Embedding.op_f {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} (e : c.Embedding c') (a✝ : ι) : e.op.f a✝ = e.f a✝

class ComplexShape.Embedding.IsRelIff {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} (e : c.Embedding c') : Prop

An embedding of complex shapes e satisfies e.IsRelIff if the implication e.rel is an equivalence.

• rel' (i₁ i₂ : ι) (h : c'.Rel (e.f i₁) (e.f i₂)) : c.Rel i₁ i₂

theorem ComplexShape.Embedding.rel_iff {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} (e : c.Embedding c') [e.IsRelIff] (i₁ i₂ : ι) : c'.Rel (e.f i₁) (e.f i₂) ↔ c.Rel i₁ i₂

instance ComplexShape.Embedding.instIsRelIffOp {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} (e : c.Embedding c') [e.IsRelIff] : e.op.IsRelIff

def ComplexShape.Embedding.mk' {ι : Type u_1} {ι' : Type u_2} (c : ComplexShape ι) (c' : ComplexShape ι') (f : ι → ι') (hf : Function.Injective f) (iff : ∀ (i₁ i₂ : ι), c.Rel i₁ i₂ ↔ c'.Rel (f i₁) (f i₂)) : c.Embedding c'

Constructor for embeddings between complex shapes when we have an equivalence ∀ (i₁ i₂ : ι), c.Rel i₁ i₂ ↔ c'.Rel (f i₁) (f i₂).

@[simp]

theorem ComplexShape.Embedding.mk'_f {ι : Type u_1} {ι' : Type u_2} (c : ComplexShape ι) (c' : ComplexShape ι') (f : ι → ι') (hf : Function.Injective f) (iff : ∀ (i₁ i₂ : ι), c.Rel i₁ i₂ ↔ c'.Rel (f i₁) (f i₂)) (a✝ : ι) : (mk' c c' f hf iff).f a✝ = f a✝

instance ComplexShape.Embedding.instIsRelIffMk' {ι : Type u_1} {ι' : Type u_2} (c : ComplexShape ι) (c' : ComplexShape ι') (f : ι → ι') (hf : Function.Injective f) (iff : ∀ (i₁ i₂ : ι), c.Rel i₁ i₂ ↔ c'.Rel (f i₁) (f i₂)) : (mk' c c' f hf iff).IsRelIff

class ComplexShape.Embedding.IsTruncGE {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} (e : c.Embedding c') extends e.IsRelIff : Prop

The condition that the image of the map e.f of an embedding of complex shapes e : Embedding c c' is stable by c'.next.

• rel' (i₁ i₂ : ι) (h : c'.Rel (e.f i₁) (e.f i₂)) : c.Rel i₁ i₂
• mem_next {j : ι} {k' : ι'} (h : c'.Rel (e.f j) k') : ∃ (k : ι), e.f k = k'

theorem ComplexShape.Embedding.mem_next {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} (e : c.Embedding c') [e.IsTruncGE] {j : ι} {k' : ι'} (h : c'.Rel (e.f j) k') : ∃ (k : ι), e.f k = k'

class ComplexShape.Embedding.IsTruncLE {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} (e : c.Embedding c') extends e.IsRelIff : Prop

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.

• rel' (i₁ i₂ : ι) (h : c'.Rel (e.f i₁) (e.f i₂)) : c.Rel i₁ i₂
• mem_prev {i' : ι'} {j : ι} (h : c'.Rel i' (e.f j)) : ∃ (i : ι), e.f i = i'

theorem ComplexShape.Embedding.mem_prev {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} (e : c.Embedding c') [e.IsTruncLE] {i' : ι'} {j : ι} (h : c'.Rel i' (e.f j)) : ∃ (i : ι), e.f i = i'

instance ComplexShape.Embedding.instIsTruncLEOpOfIsTruncGE {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} (e : c.Embedding c') [e.IsTruncGE] : e.op.IsTruncLE

instance ComplexShape.Embedding.instIsTruncGEOpOfIsTruncLE {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} (e : c.Embedding c') [e.IsTruncLE] : e.op.IsTruncGE

noncomputable def ComplexShape.Embedding.r {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} (e : c.Embedding c') (i' : ι') : Option ι

The map ι' → Option ι which sends e.f i to some i and the other elements to none.

theorem ComplexShape.Embedding.r_eq_some {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} (e : c.Embedding c') {i : ι} {i' : ι'} (hi : e.f i = i') : e.r i' = some i

theorem ComplexShape.Embedding.r_eq_none {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} (e : c.Embedding c') (i' : ι') (hi : ∀ (i : ι), e.f i ≠ i') : e.r i' = none

@[simp]

theorem ComplexShape.Embedding.r_f {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} (e : c.Embedding c') (i : ι) : e.r (e.f i) = some i

theorem ComplexShape.Embedding.f_eq_of_r_eq_some {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} (e : c.Embedding c') {i : ι} {i' : ι'} (hi : e.r i' = some i) : e.f i = i'

def ComplexShape.embeddingUp'Add {A : Type u_3} [AddCommSemigroup A] [IsRightCancelAdd A] (a b : A) : (up' a).Embedding (up' a)

The embedding from up' a to itself via (· + b).

@[simp]

theorem ComplexShape.embeddingUp'Add_f {A : Type u_3} [AddCommSemigroup A] [IsRightCancelAdd A] (a b x✝ : A) : (embeddingUp'Add a b).f x✝ = x✝ + b

instance ComplexShape.instIsRelIffEmbeddingUp'Add {A : Type u_3} [AddCommSemigroup A] [IsRightCancelAdd A] (a b : A) : (embeddingUp'Add a b).IsRelIff

instance ComplexShape.instIsTruncGEEmbeddingUp'Add {A : Type u_3} [AddCommSemigroup A] [IsRightCancelAdd A] (a b : A) : (embeddingUp'Add a b).IsTruncGE

def ComplexShape.embeddingDown'Add {A : Type u_3} [AddCommSemigroup A] [IsRightCancelAdd A] (a b : A) : (down' a).Embedding (down' a)

The embedding from down' a to itself via (· + b).

@[simp]

theorem ComplexShape.embeddingDown'Add_f {A : Type u_3} [AddCommSemigroup A] [IsRightCancelAdd A] (a b x✝ : A) : (embeddingDown'Add a b).f x✝ = x✝ + b

instance ComplexShape.instIsRelIffEmbeddingDown'Add {A : Type u_3} [AddCommSemigroup A] [IsRightCancelAdd A] (a b : A) : (embeddingDown'Add a b).IsRelIff

instance ComplexShape.instIsTruncLEEmbeddingDown'Add {A : Type u_3} [AddCommSemigroup A] [IsRightCancelAdd A] (a b : A) : (embeddingDown'Add a b).IsTruncLE

def ComplexShape.embeddingUpNat : (up ℕ).Embedding (up ℤ)

The obvious embedding from up ℕ to up ℤ.

@[simp]

theorem ComplexShape.embeddingUpNat_f (n : ℕ) : embeddingUpNat.f n = ↑n

instance ComplexShape.instIsRelIffNatIntEmbeddingUpNat : embeddingUpNat.IsRelIff

instance ComplexShape.instIsTruncGENatIntEmbeddingUpNat : embeddingUpNat.IsTruncGE

def ComplexShape.embeddingDownNat : (down ℕ).Embedding (up ℤ)

The embedding from down ℕ to up ℤ with sends n to -n.

@[simp]

theorem ComplexShape.embeddingDownNat_f (n : ℕ) : embeddingDownNat.f n = -↑n

instance ComplexShape.instIsRelIffNatIntEmbeddingDownNat : embeddingDownNat.IsRelIff

instance ComplexShape.instIsTruncLENatIntEmbeddingDownNat : embeddingDownNat.IsTruncLE

def ComplexShape.embeddingUpIntGE (p : ℤ) : (up ℕ).Embedding (up ℤ)

The embedding from up ℕ to up ℤ which sends n : ℕ to p + n.

@[simp]

theorem ComplexShape.embeddingUpIntGE_f (p : ℤ) (n : ℕ) : (embeddingUpIntGE p).f n = p + ↑n

instance ComplexShape.instIsRelIffNatIntEmbeddingUpIntGE (p : ℤ) : (embeddingUpIntGE p).IsRelIff

instance ComplexShape.instIsTruncGENatIntEmbeddingUpIntGE (p : ℤ) : (embeddingUpIntGE p).IsTruncGE

def ComplexShape.embeddingUpIntLE (p : ℤ) : (down ℕ).Embedding (up ℤ)

The embedding from down ℕ to up ℤ which sends n : ℕ to p - n.

@[simp]

theorem ComplexShape.embeddingUpIntLE_f (p : ℤ) (n : ℕ) : (embeddingUpIntLE p).f n = p - ↑n

instance ComplexShape.instIsRelIffNatIntEmbeddingUpIntLE (p : ℤ) : (embeddingUpIntLE p).IsRelIff

instance ComplexShape.instIsTruncLENatIntEmbeddingUpIntLE (p : ℤ) : (embeddingUpIntLE p).IsTruncLE

theorem ComplexShape.notMem_range_embeddingUpIntLE_iff (p n : ℤ) : (∀ (i : ℕ), (embeddingUpIntLE p).f i ≠ n) ↔ p < n

theorem ComplexShape.notMem_range_embeddingUpIntGE_iff (p n : ℤ) : (∀ (i : ℕ), (embeddingUpIntGE p).f i ≠ n) ↔ n < p