Bounded Cochain Complexes

A computable version of CochainComplex backed by an explicit Finset ℤ of cohomological degrees in the support, analogous to CMat_ vs Mat_.

structure BoundedCochainComplex (V : Type u_1) [CategoryTheory.Category.{u_2, u_1} V] [CategoryTheory.Limits.HasZeroObject V] [CategoryTheory.Preadditive V] extends HomologicalComplex V (ComplexShape.up ℤ) : Type (max u_1 u_2)

• X : ℤ → V
• d (i j : ℤ) : self.X i ⟶ self.X j
• shape (i j : ℤ) : ¬(ComplexShape.up ℤ).Rel i j → self.d i j = 0
• d_comp_d' (i j k : ℤ) : (ComplexShape.up ℤ).Rel i j → (ComplexShape.up ℤ).Rel j k → CategoryTheory.CategoryStruct.comp (self.d i j) (self.d j k) = 0
• support : Finset ℤ
• not_isZero_iff_mem_support (i : ℤ) : ¬CategoryTheory.Limits.IsZero (self.X i) ↔ i ∈ self.support

def BoundedCochainComplex.length {V : Type u_1} [CategoryTheory.Category.{u_2, u_1} V] [CategoryTheory.Limits.HasZeroObject V] [CategoryTheory.Preadditive V] (c : BoundedCochainComplex V) : ℤ

Equations

• c.length = if h : c.support.Nonempty then c.support.max' h - c.support.min' h else 0

structure BoundedCochainComplex.Hom {V : Type u_1} [CategoryTheory.Category.{u_2, u_1} V] [CategoryTheory.Limits.HasZeroObject V] [CategoryTheory.Preadditive V] (c₁ c₂ : BoundedCochainComplex V) : Type u_2

The morphisms in BoundedCochainComplex V are the morphisms in CochainComplex V ℤ between the underlying complexes, packaged in a one-field structure (mirroring CategoryTheory.InducedCategory.Hom).

• hom : c₁.toHomologicalComplex ⟶ c₂.toHomologicalComplex

theorem BoundedCochainComplex.Hom.ext {V : Type u_1} {inst✝ : CategoryTheory.Category.{u_2, u_1} V} {inst✝¹ : CategoryTheory.Limits.HasZeroObject V} {inst✝² : CategoryTheory.Preadditive V} {c₁ c₂ : BoundedCochainComplex V} {x y : c₁.Hom c₂} (hom : x.hom = y.hom) : x = y

theorem BoundedCochainComplex.Hom.ext_iff {V : Type u_1} {inst✝ : CategoryTheory.Category.{u_2, u_1} V} {inst✝¹ : CategoryTheory.Limits.HasZeroObject V} {inst✝² : CategoryTheory.Preadditive V} {c₁ c₂ : BoundedCochainComplex V} {x y : c₁.Hom c₂} : x = y ↔ x.hom = y.hom

@[reducible, inline]

abbrev BoundedCochainComplex.Hom.f {V : Type u_1} [CategoryTheory.Category.{u_2, u_1} V] [CategoryTheory.Limits.HasZeroObject V] [CategoryTheory.Preadditive V] {c₁ c₂ : BoundedCochainComplex V} (h : c₁.Hom c₂) (i : ℤ) : c₁.X i ⟶ c₂.X i

Equations

• h.f i = h.hom.f i

@[implicit_reducible]

instance BoundedCochainComplex.instCategory {V : Type u_1} [CategoryTheory.Category.{u_2, u_1} V] [CategoryTheory.Limits.HasZeroObject V] [CategoryTheory.Preadditive V] : CategoryTheory.Category.{u_2, max u_2 u_1} (BoundedCochainComplex V)

Equations

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

@[simp]

theorem BoundedCochainComplex.id_hom {V : Type u_1} [CategoryTheory.Category.{u_2, u_1} V] [CategoryTheory.Limits.HasZeroObject V] [CategoryTheory.Preadditive V] (c : BoundedCochainComplex V) : (CategoryTheory.CategoryStruct.id c).hom = CategoryTheory.CategoryStruct.id c.toHomologicalComplex

@[simp]

theorem BoundedCochainComplex.comp_hom {V : Type u_1} [CategoryTheory.Category.{u_2, u_1} V] [CategoryTheory.Limits.HasZeroObject V] [CategoryTheory.Preadditive V] {c₁ c₂ c₃ : BoundedCochainComplex V} (f : c₁ ⟶ c₂) (g : c₂ ⟶ c₃) : (CategoryTheory.CategoryStruct.comp f g).hom = CategoryTheory.CategoryStruct.comp f.hom g.hom

def BoundedCochainComplex.homMk {V : Type u_1} [CategoryTheory.Category.{u_2, u_1} V] [CategoryTheory.Limits.HasZeroObject V] [CategoryTheory.Preadditive V] {c₁ c₂ : BoundedCochainComplex V} (f : c₁.toHomologicalComplex ⟶ c₂.toHomologicalComplex) : c₁ ⟶ c₂

Construct a morphism in BoundedCochainComplex V from a morphism in CochainComplex V ℤ between the underlying complexes.

Equations

• BoundedCochainComplex.homMk f = { hom := f }

@[simp]

theorem BoundedCochainComplex.homMk_hom {V : Type u_1} [CategoryTheory.Category.{u_2, u_1} V] [CategoryTheory.Limits.HasZeroObject V] [CategoryTheory.Preadditive V] {c₁ c₂ : BoundedCochainComplex V} (f : c₁.toHomologicalComplex ⟶ c₂.toHomologicalComplex) : (homMk f).hom = f

def BoundedCochainComplex.homEquiv {V : Type u_1} [CategoryTheory.Category.{u_2, u_1} V] [CategoryTheory.Limits.HasZeroObject V] [CategoryTheory.Preadditive V] {c₁ c₂ : BoundedCochainComplex V} : (c₁ ⟶ c₂) ≃ (c₁.toHomologicalComplex ⟶ c₂.toHomologicalComplex)

Morphisms in BoundedCochainComplex V identify with morphisms in CochainComplex V ℤ between the underlying complexes.

Equations

• BoundedCochainComplex.homEquiv = { toFun := BoundedCochainComplex.Hom.hom, invFun := BoundedCochainComplex.homMk, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem BoundedCochainComplex.homEquiv_symm_apply {V : Type u_1} [CategoryTheory.Category.{u_2, u_1} V] [CategoryTheory.Limits.HasZeroObject V] [CategoryTheory.Preadditive V] {c₁ c₂ : BoundedCochainComplex V} (f : c₁.toHomologicalComplex ⟶ c₂.toHomologicalComplex) : homEquiv.symm f = homMk f

@[simp]

theorem BoundedCochainComplex.homEquiv_apply {V : Type u_1} [CategoryTheory.Category.{u_2, u_1} V] [CategoryTheory.Limits.HasZeroObject V] [CategoryTheory.Preadditive V] {c₁ c₂ : BoundedCochainComplex V} (self : c₁.Hom c₂) : homEquiv self = self.hom

def BoundedCochainComplex.embed {V : Type u_1} [CategoryTheory.Category.{u_2, u_1} V] [CategoryTheory.Limits.HasZeroObject V] [CategoryTheory.Preadditive V] : CategoryTheory.Functor (BoundedCochainComplex V) (CochainComplex V ℤ)

The forgetful functor from bounded cochain complexes to ordinary cochain complexes.

Equations

• BoundedCochainComplex.embed = { obj := fun (c : BoundedCochainComplex V) => c.toHomologicalComplex, map := fun {X Y : BoundedCochainComplex V} (f : X ⟶ Y) => f.hom, map_id := ⋯, map_comp := ⋯ }

@[simp]

theorem BoundedCochainComplex.embed_map {V : Type u_1} [CategoryTheory.Category.{u_2, u_1} V] [CategoryTheory.Limits.HasZeroObject V] [CategoryTheory.Preadditive V] {X✝ Y✝ : BoundedCochainComplex V} (f : X✝ ⟶ Y✝) : embed.map f = f.hom

@[simp]

theorem BoundedCochainComplex.embed_obj {V : Type u_1} [CategoryTheory.Category.{u_2, u_1} V] [CategoryTheory.Limits.HasZeroObject V] [CategoryTheory.Preadditive V] (c : BoundedCochainComplex V) : embed.obj c = c.toHomologicalComplex

def BoundedCochainComplex.fullyFaithfulEmbed {V : Type u_1} [CategoryTheory.Category.{u_2, u_1} V] [CategoryTheory.Limits.HasZeroObject V] [CategoryTheory.Preadditive V] : embed.FullyFaithful

embed is fully faithful — its action on hom-sets is the identification homEquiv.

Equations

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

instance BoundedCochainComplex.instFaithfulCochainComplexIntEmbed {V : Type u_1} [CategoryTheory.Category.{u_2, u_1} V] [CategoryTheory.Limits.HasZeroObject V] [CategoryTheory.Preadditive V] : embed.Faithful

instance BoundedCochainComplex.instFullCochainComplexIntEmbed {V : Type u_1} [CategoryTheory.Category.{u_2, u_1} V] [CategoryTheory.Limits.HasZeroObject V] [CategoryTheory.Preadditive V] : embed.Full

@[implicit_reducible]

instance BoundedCochainComplex.instPreadditive {V : Type u_1} [CategoryTheory.Category.{u_2, u_1} V] [CategoryTheory.Limits.HasZeroObject V] [CategoryTheory.Preadditive V] : CategoryTheory.Preadditive (BoundedCochainComplex V)

Equations

• BoundedCochainComplex.instPreadditive = CategoryTheory.Preadditive.ofFullyFaithful BoundedCochainComplex.fullyFaithfulEmbed

@[implicit_reducible]

instance BoundedCochainComplex.instLinear {V : Type u_1} [CategoryTheory.Category.{u_3, u_1} V] [CategoryTheory.Limits.HasZeroObject V] [CategoryTheory.Preadditive V] {R : Type u_2} [Semiring R] [CategoryTheory.Linear R V] : CategoryTheory.Linear R (BoundedCochainComplex V)

Equations

• BoundedCochainComplex.instLinear = { homModule := fun (c₁ c₂ : BoundedCochainComplex V) => Equiv.module R BoundedCochainComplex.homEquiv, smul_comp := ⋯, comp_smul := ⋯ }

def BoundedCochainComplex.of {V : Type u_1} [CategoryTheory.Category.{u_2, u_1} V] [CategoryTheory.Limits.HasZeroObject V] [CategoryTheory.Preadditive V] [DecidablePred CategoryTheory.Limits.IsZero] (X : ℤ → V) (support : Finset ℤ) (h : ∀ (i : ℤ), ¬CategoryTheory.Limits.IsZero (X i) ↔ i ∈ support) (d : (i : ℤ) → X i ⟶ X (i + 1)) (hd : ∀ (i : ℤ), CategoryTheory.CategoryStruct.comp (d i) (d (i + 1)) = 0) : BoundedCochainComplex V

Equations

• BoundedCochainComplex.of X support h d hd = { toHomologicalComplex := CochainComplex.of X d hd, support := support, not_isZero_iff_mem_support := h }

def BoundedCochainComplex.ofHom {V : Type u_1} [CategoryTheory.Category.{u_2, u_1} V] [CategoryTheory.Limits.HasZeroObject V] [CategoryTheory.Preadditive V] [DecidablePred CategoryTheory.Limits.IsZero] (X : ℤ → V) (support_X : Finset ℤ) (d_X : (i : ℤ) → X i ⟶ X (i + 1)) (h_X : ∀ (i : ℤ), ¬CategoryTheory.Limits.IsZero (X i) ↔ i ∈ support_X) (sq_X : ∀ (i : ℤ), CategoryTheory.CategoryStruct.comp (d_X i) (d_X (i + 1)) = 0) (Y : ℤ → V) (support_Y : Finset ℤ) (d_Y : (i : ℤ) → Y i ⟶ Y (i + 1)) (h_Y : ∀ (i : ℤ), ¬CategoryTheory.Limits.IsZero (Y i) ↔ i ∈ support_Y) (sq_Y : ∀ (i : ℤ), CategoryTheory.CategoryStruct.comp (d_Y i) (d_Y (i + 1)) = 0) (f : (i : ℤ) → X i ⟶ Y i) (comm : ∀ (i : ℤ), CategoryTheory.CategoryStruct.comp (f i) (d_Y i) = CategoryTheory.CategoryStruct.comp (d_X i) (f (i + 1))) : of X support_X h_X d_X sq_X ⟶ of Y support_Y h_Y d_Y sq_Y

Equations

• BoundedCochainComplex.ofHom X support_X d_X h_X sq_X Y support_Y d_Y h_Y sq_Y f comm = { hom := CochainComplex.ofHom X d_X sq_X Y d_Y sq_Y f comm }

theorem BoundedCochainComplex.ofHom_f {V : Type u_1} [CategoryTheory.Category.{u_2, u_1} V] [CategoryTheory.Limits.HasZeroObject V] [CategoryTheory.Preadditive V] [DecidablePred CategoryTheory.Limits.IsZero] (X : ℤ → V) (support_X : Finset ℤ) (d_X : (i : ℤ) → X i ⟶ X (i + 1)) (h_X : ∀ (i : ℤ), ¬CategoryTheory.Limits.IsZero (X i) ↔ i ∈ support_X) (sq_X : ∀ (i : ℤ), CategoryTheory.CategoryStruct.comp (d_X i) (d_X (i + 1)) = 0) (Y : ℤ → V) (support_Y : Finset ℤ) (d_Y : (i : ℤ) → Y i ⟶ Y (i + 1)) (h_Y : ∀ (i : ℤ), ¬CategoryTheory.Limits.IsZero (Y i) ↔ i ∈ support_Y) (sq_Y : ∀ (i : ℤ), CategoryTheory.CategoryStruct.comp (d_Y i) (d_Y (i + 1)) = 0) (f : (i : ℤ) → X i ⟶ Y i) (comm : ∀ (i : ℤ), CategoryTheory.CategoryStruct.comp (f i) (d_Y i) = CategoryTheory.CategoryStruct.comp (d_X i) (f (i + 1))) (i : ℤ) : Hom.f (ofHom X support_X d_X h_X sq_X Y support_Y d_Y h_Y sq_Y f comm) i = f i

def BoundedCochainComplex.mkOfBounded {V : Type u_1} [CategoryTheory.Category.{u_2, u_1} V] [CategoryTheory.Limits.HasZeroObject V] [CategoryTheory.Preadditive V] [DecidablePred CategoryTheory.Limits.IsZero] (c : CochainComplex V ℤ) {supersetOfSupport : Finset ℤ} (h : ∀ (i : ℤ), ¬CategoryTheory.Limits.IsZero (c.X i) → i ∈ supersetOfSupport) : BoundedCochainComplex V

Build a BoundedCochainComplex from a CochainComplex together with a finite superset of its true support.

Equations

• BoundedCochainComplex.mkOfBounded c h = { toHomologicalComplex := c, support := {i ∈ supersetOfSupport | ¬CategoryTheory.Limits.IsZero (c.X i)}, not_isZero_iff_mem_support := ⋯ }

@[simp]

theorem BoundedCochainComplex.mkOfBounded_toHomologicalComplex {V : Type u_1} [CategoryTheory.Category.{u_2, u_1} V] [CategoryTheory.Limits.HasZeroObject V] [CategoryTheory.Preadditive V] [DecidablePred CategoryTheory.Limits.IsZero] (c : CochainComplex V ℤ) {s : Finset ℤ} (h : ∀ (i : ℤ), ¬CategoryTheory.Limits.IsZero (c.X i) → i ∈ s) : (mkOfBounded c h).toHomologicalComplex = c

theorem BoundedCochainComplex.mkOfBounded_eq {V : Type u_1} [CategoryTheory.Category.{u_2, u_1} V] [CategoryTheory.Limits.HasZeroObject V] [CategoryTheory.Preadditive V] [DecidablePred CategoryTheory.Limits.IsZero] (c : CochainComplex V ℤ) {s₁ s₂ : Finset ℤ} (h₁ : ∀ (i : ℤ), ¬CategoryTheory.Limits.IsZero (c.X i) → i ∈ s₁) (h₂ : ∀ (i : ℤ), ¬CategoryTheory.Limits.IsZero (c.X i) → i ∈ s₂) : mkOfBounded c h₁ = mkOfBounded c h₂

def BoundedCochainComplex.liftEndofunctor {V : Type u_1} [CategoryTheory.Category.{u_2, u_1} V] [CategoryTheory.Limits.HasZeroObject V] [CategoryTheory.Preadditive V] [DecidablePred CategoryTheory.Limits.IsZero] (H : CategoryTheory.Functor (CochainComplex V ℤ) (CochainComplex V ℤ)) (b : BoundedCochainComplex V → Finset ℤ) (hb : ∀ (X : BoundedCochainComplex V) (i : ℤ), ¬CategoryTheory.Limits.IsZero ((H.obj (embed.obj X)).X i) → i ∈ b X) : CategoryTheory.Functor (BoundedCochainComplex V) (BoundedCochainComplex V)

Lift an endofunctor H : CochainComplex V ℤ ⥤ CochainComplex V ℤ to a functor BoundedCochainComplex V ⥤ BoundedCochainComplex V, given a Finset-valued bound b : BoundedCochainComplex V → Finset ℤ such that for every X, the support of H.obj (embed.obj X) is contained in b X.

Equations

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

@[simp]

theorem BoundedCochainComplex.liftEndofunctor_obj {V : Type u_1} [CategoryTheory.Category.{u_2, u_1} V] [CategoryTheory.Limits.HasZeroObject V] [CategoryTheory.Preadditive V] [DecidablePred CategoryTheory.Limits.IsZero] (H : CategoryTheory.Functor (CochainComplex V ℤ) (CochainComplex V ℤ)) (b : BoundedCochainComplex V → Finset ℤ) (hb : ∀ (X : BoundedCochainComplex V) (i : ℤ), ¬CategoryTheory.Limits.IsZero ((H.obj (embed.obj X)).X i) → i ∈ b X) (X : BoundedCochainComplex V) : (liftEndofunctor H b hb).obj X = mkOfBounded (H.obj (embed.obj X)) ⋯

@[simp]

theorem BoundedCochainComplex.liftEndofunctor_map {V : Type u_1} [CategoryTheory.Category.{u_2, u_1} V] [CategoryTheory.Limits.HasZeroObject V] [CategoryTheory.Preadditive V] [DecidablePred CategoryTheory.Limits.IsZero] (H : CategoryTheory.Functor (CochainComplex V ℤ) (CochainComplex V ℤ)) (b : BoundedCochainComplex V → Finset ℤ) (hb : ∀ (X : BoundedCochainComplex V) (i : ℤ), ¬CategoryTheory.Limits.IsZero ((H.obj (embed.obj X)).X i) → i ∈ b X) {x✝ x✝¹ : BoundedCochainComplex V} (f : x✝ ⟶ x✝¹) : (liftEndofunctor H b hb).map f = homMk (H.map f.hom)

def BoundedCochainComplex.liftEndofunctorCompEmbed {V : Type u_1} [CategoryTheory.Category.{u_2, u_1} V] [CategoryTheory.Limits.HasZeroObject V] [CategoryTheory.Preadditive V] [DecidablePred CategoryTheory.Limits.IsZero] (H : CategoryTheory.Functor (CochainComplex V ℤ) (CochainComplex V ℤ)) (b : BoundedCochainComplex V → Finset ℤ) (hb : ∀ (X : BoundedCochainComplex V) (i : ℤ), ¬CategoryTheory.Limits.IsZero ((H.obj (embed.obj X)).X i) → i ∈ b X) : (liftEndofunctor H b hb).comp embed ≅ embed.comp H

The lifted functor commutes with the embedding to CochainComplex V ℤ.

Equations

• BoundedCochainComplex.liftEndofunctorCompEmbed H b hb = CategoryTheory.Iso.refl ((BoundedCochainComplex.liftEndofunctor H b hb).comp BoundedCochainComplex.embed)

@[simp]

theorem BoundedCochainComplex.liftEndofunctorCompEmbed_hom_app_f {V : Type u_1} [CategoryTheory.Category.{u_2, u_1} V] [CategoryTheory.Limits.HasZeroObject V] [CategoryTheory.Preadditive V] [DecidablePred CategoryTheory.Limits.IsZero] (H : CategoryTheory.Functor (CochainComplex V ℤ) (CochainComplex V ℤ)) (b : BoundedCochainComplex V → Finset ℤ) (hb : ∀ (X : BoundedCochainComplex V) (i : ℤ), ¬CategoryTheory.Limits.IsZero ((H.obj (embed.obj X)).X i) → i ∈ b X) (X : BoundedCochainComplex V) (x✝ : ℤ) : ((liftEndofunctorCompEmbed H b hb).hom.app X).f x✝ = CategoryTheory.CategoryStruct.id ((H.obj X.toHomologicalComplex).X x✝)

@[simp]

theorem BoundedCochainComplex.liftEndofunctorCompEmbed_inv_app_f {V : Type u_1} [CategoryTheory.Category.{u_2, u_1} V] [CategoryTheory.Limits.HasZeroObject V] [CategoryTheory.Preadditive V] [DecidablePred CategoryTheory.Limits.IsZero] (H : CategoryTheory.Functor (CochainComplex V ℤ) (CochainComplex V ℤ)) (b : BoundedCochainComplex V → Finset ℤ) (hb : ∀ (X : BoundedCochainComplex V) (i : ℤ), ¬CategoryTheory.Limits.IsZero ((H.obj (embed.obj X)).X i) → i ∈ b X) (X : BoundedCochainComplex V) (x✝ : ℤ) : ((liftEndofunctorCompEmbed H b hb).inv.app X).f x✝ = CategoryTheory.CategoryStruct.id ((H.obj X.toHomologicalComplex).X x✝)

def BoundedCochainComplex.shiftFunctor {V : Type u_1} [CategoryTheory.Category.{u_2, u_1} V] [CategoryTheory.Limits.HasZeroObject V] [CategoryTheory.Preadditive V] [DecidablePred CategoryTheory.Limits.IsZero] (n : ℤ) : CategoryTheory.Functor (BoundedCochainComplex V) (BoundedCochainComplex V)

Equations

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

def BoundedCochainComplex.toTexRow {C : Type u_2} [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [Texify C] [(X Y : C) → Texify (X ⟶ Y)] (A : BoundedCochainComplex C) (leftmost rightmost : ℤ) (placeDifferentialsBelow : Bool := false) : String

Equations

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

def BoundedCochainComplex.Hom.toTexRow {C : Type u_2} [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [Texify C] [(X Y : C) → Texify (X ⟶ Y)] {A B : BoundedCochainComplex C} (h : A ⟶ B) (leftmost rightmost : ℤ) : String

Equations

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

@[implicit_reducible]

instance BoundedCochainComplex.instTexifyOfHom (C : Type u_2) [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [Texify C] [(X Y : C) → Texify (X ⟶ Y)] : Texify (BoundedCochainComplex C)

Equations

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

@[implicit_reducible]

instance BoundedCochainComplex.instTexifyHom (C : Type u_2) [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [Texify C] [(X Y : C) → Texify (X ⟶ Y)] (A B : BoundedCochainComplex C) : Texify (A ⟶ B)

Equations

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