Documentation

Mathlib.Algebra.Homology.Embedding.Basic

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:

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₂)
Instances For
    theorem ComplexShape.Embedding.injective_f {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} (self : c.Embedding c') :
    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₂)
    @[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
    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 := }
    Instances For
      class ComplexShape.Embedding.IsRelIff {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} (e : c.Embedding c') :

      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₂
      Instances
        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₂
        @[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
        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
        Instances For
          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 :

          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'
          Instances
            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 :

            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'
            Instances
              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' : ι') :

              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
              Instances For
                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'

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

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

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

                  Equations
                  Instances For

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

                    Equations
                    Instances For