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

TODO

Define the following:

• the extension functor e.extendFunctor C : HomologicalComplex C c ⥤ HomologicalComplex C c' (extending by the zero object outside of the image of e.f);
• assuming e.IsRelIff, the restriction functor e.restrictionFunctor C : HomologicalComplex C c' ⥤ HomologicalComplex C c;
• the stupid truncation functor e.stupidTruncFunctor C : HomologicalComplex C c' ⥤ HomologicalComplex C c' which is the composition of the two previous functors.
• assuming e.IsTruncGE, truncation functors e.truncGE'Functor C : HomologicalComplex C c' ⥤ HomologicalComplex C c and e.truncGEFunctor C : HomologicalComplex C c' ⥤ HomologicalComplex C c', and a natural transformation e.πTruncGENatTrans : 𝟭 _ ⟶ e.truncGEFunctor C which is a quasi-isomorphism in degrees in the image of e.f;
• assuming e.IsTruncLE, 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;

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 a 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₂ : ι}, c.Rel i₁ i₂ → c'.Rel (self.f i₁) (self.f i₂)

theorem ComplexShape.Embedding.injective_f {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} (self : c.Embedding c') : Function.Injective self.f

theorem ComplexShape.Embedding.rel {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} (self : c.Embedding c') {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'.

Equations

• e.op = { f := e.f, injective_f := ⋯, rel := ⋯ }

@[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₂ : ι), c'.Rel (e.f i₁) (e.f i₂) → c.Rel i₁ i₂

theorem ComplexShape.Embedding.IsRelIff.rel' {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {e : c.Embedding c'} [self : e.IsRelIff] (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₂

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

Equations

• ComplexShape.Embedding.mk' c c' f hf iff = { f := f, injective_f := hf, rel := ⋯ }

@[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 : ι), (ComplexShape.Embedding.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₂)) : (ComplexShape.Embedding.mk' c c' f hf iff).IsRelIff

Equations

• ⋯ = ⋯

class ComplexShape.Embedding.IsTruncGE {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} (e : c.Embedding c') extends ComplexShape.Embedding.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₂ : ι), c'.Rel (e.f i₁) (e.f i₂) → c.Rel i₁ i₂
• mem_next : ∀ {j : ι} {k' : ι'}, c'.Rel (e.f j) k' → ∃ (k : ι), e.f k = k'

theorem ComplexShape.Embedding.IsTruncGE.mem_next {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {e : c.Embedding c'} [self : e.IsTruncGE] {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 ComplexShape.Embedding.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₂ : ι), c'.Rel (e.f i₁) (e.f i₂) → c.Rel i₁ i₂
• mem_prev : ∀ {i' : ι'} {j : ι}, c'.Rel i' (e.f j) → ∃ (i : ι), e.f i = i'

theorem ComplexShape.Embedding.IsTruncLE.mem_prev {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {e : c.Embedding c'} [self : e.IsTruncLE] {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'

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.

Equations

• e.r i' = if h : ∃ (i : ι), e.f i = i' then some h.choose else 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.embeddingUpNat : (ComplexShape.up ℕ).Embedding (ComplexShape.up ℤ)

The obvious embedding from up ℕ to up ℤ.

Equations

• ComplexShape.embeddingUpNat = ComplexShape.Embedding.mk' (ComplexShape.up ℕ) (ComplexShape.up ℤ) (fun (n : ℕ) => ↑n) ComplexShape.embeddingUpNat.proof_1 ComplexShape.embeddingUpNat.proof_2

@[simp]

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

instance ComplexShape.instIsRelIffNatIntEmbeddingUpNat : ComplexShape.embeddingUpNat.IsRelIff

Equations

• ComplexShape.instIsRelIffNatIntEmbeddingUpNat = ⋯

instance ComplexShape.instIsTruncGENatIntEmbeddingUpNat : ComplexShape.embeddingUpNat.IsTruncGE

Equations

• ComplexShape.instIsTruncGENatIntEmbeddingUpNat = ⋯

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

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

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

instance ComplexShape.instIsRelIffNatIntEmbeddingDownNat : ComplexShape.embeddingDownNat.IsRelIff

Equations

• ComplexShape.instIsRelIffNatIntEmbeddingDownNat = ⋯

instance ComplexShape.instIsTruncLENatIntEmbeddingDownNat : ComplexShape.embeddingDownNat.IsTruncLE

Equations

• ComplexShape.instIsTruncLENatIntEmbeddingDownNat = ⋯

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

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

Equations

• ComplexShape.embeddingUpIntGE p = ComplexShape.Embedding.mk' (ComplexShape.up ℕ) (ComplexShape.up ℤ) (fun (n : ℕ) => p + ↑n) ⋯ ⋯

@[simp]

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

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

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

Equations

• ComplexShape.embeddingUpIntLE p = ComplexShape.Embedding.mk' (ComplexShape.down ℕ) (ComplexShape.up ℤ) (fun (n : ℕ) => p - ↑n) ⋯ ⋯

@[simp]

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

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯