Homological complexes. #
A HomologicalComplex V c with a "shape" controlled by c : ComplexShape ι
has chain groups X i (objects in V) indexed by i : ι,
and a differential d i j whenever c.Rel i j.
We in fact ask for differentials d i j for all i j : ι,
but have a field shape requiring that these are zero when not allowed by c.
This avoids a lot of dependent type theory hell!
The composite of any two differentials d i j ≫ d j k must be zero.
We provide ChainComplex V α for
α-indexed chain complexes in which d i j ≠ 0 only if j + 1 = i,
and similarly CochainComplex V α, with i = j + 1.
There is a category structure, where morphisms are chain maps.
For C : HomologicalComplex V c, we define C.xNext i, which is either C.X j for some
arbitrarily chosen j such that c.r i j, or C.X i if there is no such j.
Similarly we have C.xPrev j.
Defined in terms of these we have C.dFrom i : C.X i ⟶ C.xNext i and
C.dTo j : C.xPrev j ⟶ C.X j, which are either defined as C.d i j, or zero, as needed.
structure
HomologicalComplex
{ι : Type u_1}
(V : Type u)
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
(c : ComplexShape ι)
:
Type (max (max u u_1) v)
- X : ι → V
- d : (i j : ι) → HomologicalComplex.X s i ⟶ HomologicalComplex.X s j
- shape : ∀ (i j : ι), ¬ComplexShape.Rel c i j → HomologicalComplex.d s i j = 0
- d_comp_d' : ∀ (i j k : ι), ComplexShape.Rel c i j → ComplexShape.Rel c j k → CategoryTheory.CategoryStruct.comp (HomologicalComplex.d s i j) (HomologicalComplex.d s j k) = 0
A HomologicalComplex V c with a "shape" controlled by c : ComplexShape ι
has chain groups X i (objects in V) indexed by i : ι,
and a differential d i j whenever c.Rel i j.
We in fact ask for differentials d i j for all i j : ι,
but have a field shape requiring that these are zero when not allowed by c.
This avoids a lot of dependent type theory hell!
The composite of any two differentials d i j ≫ d j k must be zero.
Instances For
@[simp]
theorem
HomologicalComplex.d_comp_d_assoc
{ι : Type u_1}
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
{c : ComplexShape ι}
(C : HomologicalComplex V c)
(i : ι)
(j : ι)
(k : ι)
{Z : V}
(h : HomologicalComplex.X C k ⟶ Z)
:
@[simp]
theorem
HomologicalComplex.d_comp_d
{ι : Type u_1}
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
{c : ComplexShape ι}
(C : HomologicalComplex V c)
(i : ι)
(j : ι)
(k : ι)
:
CategoryTheory.CategoryStruct.comp (HomologicalComplex.d C i j) (HomologicalComplex.d C j k) = 0
theorem
HomologicalComplex.ext
{ι : Type u_1}
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
{c : ComplexShape ι}
{C₁ : HomologicalComplex V c}
{C₂ : HomologicalComplex V c}
(h_X : C₁.X = C₂.X)
(h_d : ∀ (i j : ι),
ComplexShape.Rel c i j →
CategoryTheory.CategoryStruct.comp (HomologicalComplex.d C₁ i j)
(CategoryTheory.eqToHom (_ : HomologicalComplex.X C₁ j = HomologicalComplex.X C₂ j)) = CategoryTheory.CategoryStruct.comp
(CategoryTheory.eqToHom (_ : HomologicalComplex.X C₁ i = HomologicalComplex.X C₂ i))
(HomologicalComplex.d C₂ i j))
:
C₁ = C₂
def
HomologicalComplex.XIsoOfEq
{ι : Type u_1}
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
{c : ComplexShape ι}
(K : HomologicalComplex V c)
{p : ι}
{q : ι}
(h : p = q)
:
The obvious isomorphism K.X p ≅ K.X q when p = q.
Instances For
@[simp]
theorem
HomologicalComplex.XIsoOfEq_rfl
{ι : Type u_1}
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
{c : ComplexShape ι}
(K : HomologicalComplex V c)
(p : ι)
:
HomologicalComplex.XIsoOfEq K (_ : p = p) = CategoryTheory.Iso.refl (HomologicalComplex.X K p)
@[simp]
theorem
HomologicalComplex.XIsoOfEq_hom_comp_XIsoOfEq_hom_assoc
{ι : Type u_1}
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
{c : ComplexShape ι}
(K : HomologicalComplex V c)
{p₁ : ι}
{p₂ : ι}
{p₃ : ι}
(h₁₂ : p₁ = p₂)
(h₂₃ : p₂ = p₃)
{Z : V}
(h : HomologicalComplex.X K p₃ ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (HomologicalComplex.XIsoOfEq K h₁₂).hom
(CategoryTheory.CategoryStruct.comp (HomologicalComplex.XIsoOfEq K h₂₃).hom h) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.XIsoOfEq K (_ : p₁ = p₃)).hom h
@[simp]
theorem
HomologicalComplex.XIsoOfEq_hom_comp_XIsoOfEq_hom
{ι : Type u_1}
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
{c : ComplexShape ι}
(K : HomologicalComplex V c)
{p₁ : ι}
{p₂ : ι}
{p₃ : ι}
(h₁₂ : p₁ = p₂)
(h₂₃ : p₂ = p₃)
:
CategoryTheory.CategoryStruct.comp (HomologicalComplex.XIsoOfEq K h₁₂).hom (HomologicalComplex.XIsoOfEq K h₂₃).hom = (HomologicalComplex.XIsoOfEq K (_ : p₁ = p₃)).hom
@[simp]
theorem
HomologicalComplex.XIsoOfEq_hom_comp_XIsoOfEq_inv_assoc
{ι : Type u_1}
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
{c : ComplexShape ι}
(K : HomologicalComplex V c)
{p₁ : ι}
{p₂ : ι}
{p₃ : ι}
(h₁₂ : p₁ = p₂)
(h₃₂ : p₃ = p₂)
{Z : V}
(h : HomologicalComplex.X K p₃ ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (HomologicalComplex.XIsoOfEq K h₁₂).hom
(CategoryTheory.CategoryStruct.comp (HomologicalComplex.XIsoOfEq K h₃₂).inv h) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.XIsoOfEq K (_ : p₁ = p₃)).hom h
@[simp]
theorem
HomologicalComplex.XIsoOfEq_hom_comp_XIsoOfEq_inv
{ι : Type u_1}
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
{c : ComplexShape ι}
(K : HomologicalComplex V c)
{p₁ : ι}
{p₂ : ι}
{p₃ : ι}
(h₁₂ : p₁ = p₂)
(h₃₂ : p₃ = p₂)
:
CategoryTheory.CategoryStruct.comp (HomologicalComplex.XIsoOfEq K h₁₂).hom (HomologicalComplex.XIsoOfEq K h₃₂).inv = (HomologicalComplex.XIsoOfEq K (_ : p₁ = p₃)).hom
@[simp]
theorem
HomologicalComplex.XIsoOfEq_inv_comp_XIsoOfEq_hom_assoc
{ι : Type u_1}
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
{c : ComplexShape ι}
(K : HomologicalComplex V c)
{p₁ : ι}
{p₂ : ι}
{p₃ : ι}
(h₂₁ : p₂ = p₁)
(h₂₃ : p₂ = p₃)
{Z : V}
(h : HomologicalComplex.X K p₃ ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (HomologicalComplex.XIsoOfEq K h₂₁).inv
(CategoryTheory.CategoryStruct.comp (HomologicalComplex.XIsoOfEq K h₂₃).hom h) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.XIsoOfEq K (_ : p₁ = p₃)).hom h
@[simp]
theorem
HomologicalComplex.XIsoOfEq_inv_comp_XIsoOfEq_hom
{ι : Type u_1}
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
{c : ComplexShape ι}
(K : HomologicalComplex V c)
{p₁ : ι}
{p₂ : ι}
{p₃ : ι}
(h₂₁ : p₂ = p₁)
(h₂₃ : p₂ = p₃)
:
CategoryTheory.CategoryStruct.comp (HomologicalComplex.XIsoOfEq K h₂₁).inv (HomologicalComplex.XIsoOfEq K h₂₃).hom = (HomologicalComplex.XIsoOfEq K (_ : p₁ = p₃)).hom
@[simp]
theorem
HomologicalComplex.XIsoOfEq_inv_comp_XIsoOfEq_inv_assoc
{ι : Type u_1}
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
{c : ComplexShape ι}
(K : HomologicalComplex V c)
{p₁ : ι}
{p₂ : ι}
{p₃ : ι}
(h₂₁ : p₂ = p₁)
(h₃₂ : p₃ = p₂)
{Z : V}
(h : HomologicalComplex.X K p₃ ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (HomologicalComplex.XIsoOfEq K h₂₁).inv
(CategoryTheory.CategoryStruct.comp (HomologicalComplex.XIsoOfEq K h₃₂).inv h) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.XIsoOfEq K (_ : p₁ = p₃)).hom h
@[simp]
theorem
HomologicalComplex.XIsoOfEq_inv_comp_XIsoOfEq_inv
{ι : Type u_1}
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
{c : ComplexShape ι}
(K : HomologicalComplex V c)
{p₁ : ι}
{p₂ : ι}
{p₃ : ι}
(h₂₁ : p₂ = p₁)
(h₃₂ : p₃ = p₂)
:
CategoryTheory.CategoryStruct.comp (HomologicalComplex.XIsoOfEq K h₂₁).inv (HomologicalComplex.XIsoOfEq K h₃₂).inv = (HomologicalComplex.XIsoOfEq K (_ : p₁ = p₃)).hom
@[simp]
theorem
HomologicalComplex.XIsoOfEq_hom_comp_d_assoc
{ι : Type u_1}
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
{c : ComplexShape ι}
(K : HomologicalComplex V c)
{p₁ : ι}
{p₂ : ι}
(h : p₁ = p₂)
(p₃ : ι)
{Z : V}
(h : HomologicalComplex.X K p₃ ⟶ Z)
:
@[simp]
theorem
HomologicalComplex.XIsoOfEq_hom_comp_d
{ι : Type u_1}
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
{c : ComplexShape ι}
(K : HomologicalComplex V c)
{p₁ : ι}
{p₂ : ι}
(h : p₁ = p₂)
(p₃ : ι)
:
CategoryTheory.CategoryStruct.comp (HomologicalComplex.XIsoOfEq K h).hom (HomologicalComplex.d K p₂ p₃) = HomologicalComplex.d K p₁ p₃
@[simp]
theorem
HomologicalComplex.XIsoOfEq_inv_comp_d_assoc
{ι : Type u_1}
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
{c : ComplexShape ι}
(K : HomologicalComplex V c)
{p₂ : ι}
{p₁ : ι}
(h : p₂ = p₁)
(p₃ : ι)
{Z : V}
(h : HomologicalComplex.X K p₃ ⟶ Z)
:
@[simp]
theorem
HomologicalComplex.XIsoOfEq_inv_comp_d
{ι : Type u_1}
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
{c : ComplexShape ι}
(K : HomologicalComplex V c)
{p₂ : ι}
{p₁ : ι}
(h : p₂ = p₁)
(p₃ : ι)
:
CategoryTheory.CategoryStruct.comp (HomologicalComplex.XIsoOfEq K h).inv (HomologicalComplex.d K p₂ p₃) = HomologicalComplex.d K p₁ p₃
@[simp]
theorem
HomologicalComplex.d_comp_XIsoOfEq_hom_assoc
{ι : Type u_1}
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
{c : ComplexShape ι}
(K : HomologicalComplex V c)
{p₂ : ι}
{p₃ : ι}
(h : p₂ = p₃)
(p₁ : ι)
{Z : V}
(h : HomologicalComplex.X K p₃ ⟶ Z)
:
@[simp]
theorem
HomologicalComplex.d_comp_XIsoOfEq_hom
{ι : Type u_1}
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
{c : ComplexShape ι}
(K : HomologicalComplex V c)
{p₂ : ι}
{p₃ : ι}
(h : p₂ = p₃)
(p₁ : ι)
:
CategoryTheory.CategoryStruct.comp (HomologicalComplex.d K p₁ p₂) (HomologicalComplex.XIsoOfEq K h).hom = HomologicalComplex.d K p₁ p₃
@[simp]
theorem
HomologicalComplex.d_comp_XIsoOfEq_inv_assoc
{ι : Type u_1}
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
{c : ComplexShape ι}
(K : HomologicalComplex V c)
{p₂ : ι}
{p₃ : ι}
(h : p₃ = p₂)
(p₁ : ι)
{Z : V}
(h : HomologicalComplex.X K p₃ ⟶ Z)
:
@[simp]
theorem
HomologicalComplex.d_comp_XIsoOfEq_inv
{ι : Type u_1}
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
{c : ComplexShape ι}
(K : HomologicalComplex V c)
{p₂ : ι}
{p₃ : ι}
(h : p₃ = p₂)
(p₁ : ι)
:
CategoryTheory.CategoryStruct.comp (HomologicalComplex.d K p₁ p₂) (HomologicalComplex.XIsoOfEq K h).inv = HomologicalComplex.d K p₁ p₃
@[inline, reducible]
abbrev
ChainComplex
(V : Type u)
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
(α : Type u_2)
[AddRightCancelSemigroup α]
[One α]
:
Type (max (max u v) u_2)
An α-indexed chain complex is a HomologicalComplex
in which d i j ≠ 0 only if j + 1 = i.
Instances For
@[inline, reducible]
abbrev
CochainComplex
(V : Type u)
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
(α : Type u_2)
[AddRightCancelSemigroup α]
[One α]
:
Type (max (max u v) u_2)
An α-indexed cochain complex is a HomologicalComplex
in which d i j ≠ 0 only if i + 1 = j.
Instances For
@[simp]
theorem
ChainComplex.prev
(α : Type u_2)
[AddRightCancelSemigroup α]
[One α]
(i : α)
:
ComplexShape.prev (ComplexShape.down α) i = i + 1
@[simp]
theorem
ChainComplex.next
(α : Type u_2)
[AddGroup α]
[One α]
(i : α)
:
ComplexShape.next (ComplexShape.down α) i = i - 1
@[simp]
@[simp]
theorem
CochainComplex.prev
(α : Type u_2)
[AddGroup α]
[One α]
(i : α)
:
ComplexShape.prev (ComplexShape.up α) i = i - 1
@[simp]
theorem
CochainComplex.next
(α : Type u_2)
[AddRightCancelSemigroup α]
[One α]
(i : α)
:
ComplexShape.next (ComplexShape.up α) i = i + 1
@[simp]
theorem
HomologicalComplex.Hom.ext
{ι : Type u_1}
{V : Type u}
:
∀ {inst : CategoryTheory.Category.{v, u} V} {inst_1 : CategoryTheory.Limits.HasZeroMorphisms V} {c : ComplexShape ι}
{A B : HomologicalComplex V c} (x y : HomologicalComplex.Hom A B), x.f = y.f → x = y
theorem
HomologicalComplex.Hom.ext_iff
{ι : Type u_1}
{V : Type u}
:
∀ {inst : CategoryTheory.Category.{v, u} V} {inst_1 : CategoryTheory.Limits.HasZeroMorphisms V} {c : ComplexShape ι}
{A B : HomologicalComplex V c} (x y : HomologicalComplex.Hom A B), x = y ↔ x.f = y.f
structure
HomologicalComplex.Hom
{ι : Type u_1}
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
{c : ComplexShape ι}
(A : HomologicalComplex V c)
(B : HomologicalComplex V c)
:
Type (max u_1 v)
- f : (i : ι) → HomologicalComplex.X A i ⟶ HomologicalComplex.X B i
- comm' : ∀ (i j : ι), ComplexShape.Rel c i j → CategoryTheory.CategoryStruct.comp (HomologicalComplex.Hom.f s i) (HomologicalComplex.d B i j) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.d A i j) (HomologicalComplex.Hom.f s j)
A morphism of homological complexes consists of maps between the chain groups, commuting with the differentials.
Instances For
@[simp]
theorem
HomologicalComplex.Hom.comm_assoc
{ι : Type u_1}
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
{c : ComplexShape ι}
{A : HomologicalComplex V c}
{B : HomologicalComplex V c}
(f : HomologicalComplex.Hom A B)
(i : ι)
(j : ι)
{Z : V}
(h : HomologicalComplex.X B j ⟶ Z)
:
@[simp]
theorem
HomologicalComplex.Hom.comm
{ι : Type u_1}
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
{c : ComplexShape ι}
{A : HomologicalComplex V c}
{B : HomologicalComplex V c}
(f : HomologicalComplex.Hom A B)
(i : ι)
(j : ι)
:
instance
HomologicalComplex.instInhabitedHom
{ι : Type u_1}
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
{c : ComplexShape ι}
(A : HomologicalComplex V c)
(B : HomologicalComplex V c)
:
def
HomologicalComplex.id
{ι : Type u_1}
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
{c : ComplexShape ι}
(A : HomologicalComplex V c)
:
Identity chain map.
Instances For
def
HomologicalComplex.comp
{ι : Type u_1}
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
{c : ComplexShape ι}
(A : HomologicalComplex V c)
(B : HomologicalComplex V c)
(C : HomologicalComplex V c)
(φ : HomologicalComplex.Hom A B)
(ψ : HomologicalComplex.Hom B C)
:
Composition of chain maps.
Instances For
instance
HomologicalComplex.instCategoryHomologicalComplex
{ι : Type u_1}
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
{c : ComplexShape ι}
:
theorem
HomologicalComplex.hom_ext
{ι : Type u_1}
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
{c : ComplexShape ι}
{C : HomologicalComplex V c}
{D : HomologicalComplex V c}
(f : C ⟶ D)
(g : C ⟶ D)
(h : ∀ (i : ι), HomologicalComplex.Hom.f f i = HomologicalComplex.Hom.f g i)
:
f = g
@[simp]
theorem
HomologicalComplex.id_f
{ι : Type u_1}
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
{c : ComplexShape ι}
(C : HomologicalComplex V c)
(i : ι)
:
@[simp]
theorem
HomologicalComplex.comp_f
{ι : Type u_1}
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
{c : ComplexShape ι}
{C₁ : HomologicalComplex V c}
{C₂ : HomologicalComplex V c}
{C₃ : HomologicalComplex V c}
(f : C₁ ⟶ C₂)
(g : C₂ ⟶ C₃)
(i : ι)
:
@[simp]
theorem
HomologicalComplex.eqToHom_f
{ι : Type u_1}
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
{c : ComplexShape ι}
{C₁ : HomologicalComplex V c}
{C₂ : HomologicalComplex V c}
(h : C₁ = C₂)
(n : ι)
:
HomologicalComplex.Hom.f (CategoryTheory.eqToHom h) n = CategoryTheory.eqToHom (_ : HomologicalComplex.X C₁ n = HomologicalComplex.X C₂ n)
theorem
HomologicalComplex.hom_f_injective
{ι : Type u_1}
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
{c : ComplexShape ι}
{C₁ : HomologicalComplex V c}
{C₂ : HomologicalComplex V c}
:
Function.Injective fun f => f.f
instance
HomologicalComplex.instZeroHomHomologicalComplexToQuiverToCategoryStructInstCategoryHomologicalComplex
{ι : Type u_1}
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
{c : ComplexShape ι}
(X : HomologicalComplex V c)
(Y : HomologicalComplex V c)
:
@[simp]
theorem
HomologicalComplex.zero_f
{ι : Type u_1}
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
{c : ComplexShape ι}
(C : HomologicalComplex V c)
(D : HomologicalComplex V c)
(i : ι)
:
HomologicalComplex.Hom.f 0 i = 0
noncomputable def
HomologicalComplex.zero
{ι : Type u_1}
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
{c : ComplexShape ι}
[CategoryTheory.Limits.HasZeroObject V]
:
The zero complex
Instances For
theorem
HomologicalComplex.isZero_zero
{ι : Type u_1}
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
{c : ComplexShape ι}
[CategoryTheory.Limits.HasZeroObject V]
:
CategoryTheory.Limits.IsZero HomologicalComplex.zero
instance
HomologicalComplex.instHasZeroObjectHomologicalComplexInstCategoryHomologicalComplex
{ι : Type u_1}
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
{c : ComplexShape ι}
[CategoryTheory.Limits.HasZeroObject V]
:
noncomputable instance
HomologicalComplex.instInhabitedHomologicalComplex
{ι : Type u_1}
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
{c : ComplexShape ι}
[CategoryTheory.Limits.HasZeroObject V]
:
Inhabited (HomologicalComplex V c)
theorem
HomologicalComplex.congr_hom
{ι : Type u_1}
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
{c : ComplexShape ι}
{C : HomologicalComplex V c}
{D : HomologicalComplex V c}
{f : C ⟶ D}
{g : C ⟶ D}
(w : f = g)
(i : ι)
:
@[simp]
theorem
HomologicalComplex.eval_map
{ι : Type u_1}
(V : Type u)
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
(c : ComplexShape ι)
(i : ι)
:
∀ {X Y : HomologicalComplex V c} (f : X ⟶ Y), (HomologicalComplex.eval V c i).map f = HomologicalComplex.Hom.f f i
@[simp]
theorem
HomologicalComplex.eval_obj
{ι : Type u_1}
(V : Type u)
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
(c : ComplexShape ι)
(i : ι)
(C : HomologicalComplex V c)
:
(HomologicalComplex.eval V c i).obj C = HomologicalComplex.X C i
def
HomologicalComplex.eval
{ι : Type u_1}
(V : Type u)
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
(c : ComplexShape ι)
(i : ι)
:
The functor picking out the i-th object of a complex.
Instances For
@[simp]
theorem
HomologicalComplex.forget_map
{ι : Type u_1}
(V : Type u)
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
(c : ComplexShape ι)
:
∀ {X Y : HomologicalComplex V c} (f : X ⟶ Y) (i : ι),
(HomologicalComplex V c).map CategoryTheory.CategoryStruct.toQuiver (CategoryTheory.GradedObject ι V)
CategoryTheory.CategoryStruct.toQuiver (HomologicalComplex.forget V c).toPrefunctor X Y f i = HomologicalComplex.Hom.f f i
@[simp]
theorem
HomologicalComplex.forget_obj
{ι : Type u_1}
(V : Type u)
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
(c : ComplexShape ι)
(C : HomologicalComplex V c)
:
∀ (a : ι),
(HomologicalComplex V c).obj CategoryTheory.CategoryStruct.toQuiver (CategoryTheory.GradedObject ι V)
CategoryTheory.CategoryStruct.toQuiver (HomologicalComplex.forget V c).toPrefunctor C a = HomologicalComplex.X C a
def
HomologicalComplex.forget
{ι : Type u_1}
(V : Type u)
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
(c : ComplexShape ι)
:
The functor forgetting the differential in a complex, obtaining a graded object.
Instances For
@[simp]
theorem
HomologicalComplex.forgetEval_hom_app
{ι : Type u_1}
(V : Type u)
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
(c : ComplexShape ι)
(i : ι)
(X : HomologicalComplex V c)
:
(HomologicalComplex.forgetEval V c i).hom.app X = CategoryTheory.CategoryStruct.id (HomologicalComplex.X X i)
@[simp]
theorem
HomologicalComplex.forgetEval_inv_app
{ι : Type u_1}
(V : Type u)
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
(c : ComplexShape ι)
(i : ι)
(X : HomologicalComplex V c)
:
(HomologicalComplex.forgetEval V c i).inv.app X = CategoryTheory.CategoryStruct.id (HomologicalComplex.X X i)
def
HomologicalComplex.forgetEval
{ι : Type u_1}
(V : Type u)
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
(c : ComplexShape ι)
(i : ι)
:
Forgetting the differentials than picking out the i-th object is the same as
just picking out the i-th object.
Instances For
theorem
HomologicalComplex.XIsoOfEq_hom_naturality_assoc
{ι : Type u_1}
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
{c : ComplexShape ι}
{K : HomologicalComplex V c}
{L : HomologicalComplex V c}
(φ : K ⟶ L)
{n : ι}
{n' : ι}
(h : n = n')
{Z : V}
(h : HomologicalComplex.X L n' ⟶ Z)
:
theorem
HomologicalComplex.XIsoOfEq_hom_naturality
{ι : Type u_1}
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
{c : ComplexShape ι}
{K : HomologicalComplex V c}
{L : HomologicalComplex V c}
(φ : K ⟶ L)
{n : ι}
{n' : ι}
(h : n = n')
:
theorem
HomologicalComplex.XIsoOfEq_inv_naturality_assoc
{ι : Type u_1}
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
{c : ComplexShape ι}
{K : HomologicalComplex V c}
{L : HomologicalComplex V c}
(φ : K ⟶ L)
{n : ι}
{n' : ι}
(h : n = n')
{Z : V}
(h : HomologicalComplex.X L n ⟶ Z)
:
theorem
HomologicalComplex.XIsoOfEq_inv_naturality
{ι : Type u_1}
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
{c : ComplexShape ι}
{K : HomologicalComplex V c}
{L : HomologicalComplex V c}
(φ : K ⟶ L)
{n : ι}
{n' : ι}
(h : n = n')
:
theorem
HomologicalComplex.d_comp_eqToHom
{ι : Type u_1}
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
{c : ComplexShape ι}
(C : HomologicalComplex V c)
{i : ι}
{j : ι}
{j' : ι}
(rij : ComplexShape.Rel c i j)
(rij' : ComplexShape.Rel c i j')
:
CategoryTheory.CategoryStruct.comp (HomologicalComplex.d C i j')
(CategoryTheory.eqToHom (_ : HomologicalComplex.X C j' = HomologicalComplex.X C j)) = HomologicalComplex.d C i j
If C.d i j and C.d i j' are both allowed, then we must have j = j',
and so the differentials only differ by an eqToHom.
theorem
HomologicalComplex.eqToHom_comp_d
{ι : Type u_1}
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
{c : ComplexShape ι}
(C : HomologicalComplex V c)
{i : ι}
{i' : ι}
{j : ι}
(rij : ComplexShape.Rel c i j)
(rij' : ComplexShape.Rel c i' j)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom (_ : HomologicalComplex.X C i = HomologicalComplex.X C i'))
(HomologicalComplex.d C i' j) = HomologicalComplex.d C i j
If C.d i j and C.d i' j are both allowed, then we must have i = i',
and so the differentials only differ by an eqToHom.
theorem
HomologicalComplex.kernel_eq_kernel
{ι : Type u_1}
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
{c : ComplexShape ι}
(C : HomologicalComplex V c)
[CategoryTheory.Limits.HasKernels V]
{i : ι}
{j : ι}
{j' : ι}
(r : ComplexShape.Rel c i j)
(r' : ComplexShape.Rel c i j')
:
theorem
HomologicalComplex.image_eq_image
{ι : Type u_1}
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
{c : ComplexShape ι}
(C : HomologicalComplex V c)
[CategoryTheory.Limits.HasImages V]
[CategoryTheory.Limits.HasEqualizers V]
{i : ι}
{i' : ι}
{j : ι}
(r : ComplexShape.Rel c i j)
(r' : ComplexShape.Rel c i' j)
:
@[inline, reducible]
abbrev
HomologicalComplex.xPrev
{ι : Type u_1}
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
{c : ComplexShape ι}
(C : HomologicalComplex V c)
(j : ι)
:
V
Either C.X i, if there is some i with c.Rel i j, or C.X j.
Instances For
def
HomologicalComplex.xPrevIso
{ι : Type u_1}
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
{c : ComplexShape ι}
(C : HomologicalComplex V c)
{i : ι}
{j : ι}
(r : ComplexShape.Rel c i j)
:
If c.Rel i j, then C.xPrev j is isomorphic to C.X i.
Instances For
def
HomologicalComplex.xPrevIsoSelf
{ι : Type u_1}
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
{c : ComplexShape ι}
(C : HomologicalComplex V c)
{j : ι}
(h : ¬ComplexShape.Rel c (ComplexShape.prev c j) j)
:
If there is no i so c.Rel i j, then C.xPrev j is isomorphic to C.X j.
Instances For
@[inline, reducible]
abbrev
HomologicalComplex.xNext
{ι : Type u_1}
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
{c : ComplexShape ι}
(C : HomologicalComplex V c)
(i : ι)
:
V
Either C.X j, if there is some j with c.rel i j, or C.X i.
Instances For
def
HomologicalComplex.xNextIso
{ι : Type u_1}
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
{c : ComplexShape ι}
(C : HomologicalComplex V c)
{i : ι}
{j : ι}
(r : ComplexShape.Rel c i j)
:
If c.Rel i j, then C.xNext i is isomorphic to C.X j.
Instances For
def
HomologicalComplex.xNextIsoSelf
{ι : Type u_1}
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
{c : ComplexShape ι}
(C : HomologicalComplex V c)
{i : ι}
(h : ¬ComplexShape.Rel c i (ComplexShape.next c i))
:
If there is no j so c.Rel i j, then C.xNext i is isomorphic to C.X i.
Instances For
@[inline, reducible]
abbrev
HomologicalComplex.dTo
{ι : Type u_1}
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
{c : ComplexShape ι}
(C : HomologicalComplex V c)
(j : ι)
:
The differential mapping into C.X j, or zero if there isn't one.
Instances For
@[inline, reducible]
abbrev
HomologicalComplex.dFrom
{ι : Type u_1}
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
{c : ComplexShape ι}
(C : HomologicalComplex V c)
(i : ι)
:
The differential mapping out of C.X i, or zero if there isn't one.
Instances For
theorem
HomologicalComplex.dTo_eq
{ι : Type u_1}
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
{c : ComplexShape ι}
(C : HomologicalComplex V c)
{i : ι}
{j : ι}
(r : ComplexShape.Rel c i j)
:
HomologicalComplex.dTo C j = CategoryTheory.CategoryStruct.comp (HomologicalComplex.xPrevIso C r).hom (HomologicalComplex.d C i j)
@[simp]
theorem
HomologicalComplex.dTo_eq_zero
{ι : Type u_1}
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
{c : ComplexShape ι}
(C : HomologicalComplex V c)
{j : ι}
(h : ¬ComplexShape.Rel c (ComplexShape.prev c j) j)
:
HomologicalComplex.dTo C j = 0
theorem
HomologicalComplex.dFrom_eq
{ι : Type u_1}
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
{c : ComplexShape ι}
(C : HomologicalComplex V c)
{i : ι}
{j : ι}
(r : ComplexShape.Rel c i j)
:
@[simp]
theorem
HomologicalComplex.dFrom_eq_zero
{ι : Type u_1}
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
{c : ComplexShape ι}
(C : HomologicalComplex V c)
{i : ι}
(h : ¬ComplexShape.Rel c i (ComplexShape.next c i))
:
HomologicalComplex.dFrom C i = 0
@[simp]
theorem
HomologicalComplex.xPrevIso_comp_dTo_assoc
{ι : Type u_1}
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
{c : ComplexShape ι}
(C : HomologicalComplex V c)
{i : ι}
{j : ι}
(r : ComplexShape.Rel c i j)
{Z : V}
(h : HomologicalComplex.X C j ⟶ Z)
:
@[simp]
theorem
HomologicalComplex.xPrevIso_comp_dTo
{ι : Type u_1}
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
{c : ComplexShape ι}
(C : HomologicalComplex V c)
{i : ι}
{j : ι}
(r : ComplexShape.Rel c i j)
:
CategoryTheory.CategoryStruct.comp (HomologicalComplex.xPrevIso C r).inv (HomologicalComplex.dTo C j) = HomologicalComplex.d C i j
@[simp]
theorem
HomologicalComplex.xPrevIsoSelf_comp_dTo_assoc
{ι : Type u_1}
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
{c : ComplexShape ι}
(C : HomologicalComplex V c)
{j : ι}
(h : ¬ComplexShape.Rel c (ComplexShape.prev c j) j)
{Z : V}
(h : HomologicalComplex.X C j ⟶ Z)
:
@[simp]
theorem
HomologicalComplex.xPrevIsoSelf_comp_dTo
{ι : Type u_1}
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
{c : ComplexShape ι}
(C : HomologicalComplex V c)
{j : ι}
(h : ¬ComplexShape.Rel c (ComplexShape.prev c j) j)
:
@[simp]
theorem
HomologicalComplex.dFrom_comp_xNextIso_assoc
{ι : Type u_1}
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
{c : ComplexShape ι}
(C : HomologicalComplex V c)
{i : ι}
{j : ι}
(r : ComplexShape.Rel c i j)
{Z : V}
(h : HomologicalComplex.X C j ⟶ Z)
:
@[simp]
theorem
HomologicalComplex.dFrom_comp_xNextIso
{ι : Type u_1}
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
{c : ComplexShape ι}
(C : HomologicalComplex V c)
{i : ι}
{j : ι}
(r : ComplexShape.Rel c i j)
:
@[simp]
theorem
HomologicalComplex.dFrom_comp_xNextIsoSelf_assoc
{ι : Type u_1}
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
{c : ComplexShape ι}
(C : HomologicalComplex V c)
{i : ι}
(h : ¬ComplexShape.Rel c i (ComplexShape.next c i))
{Z : V}
(h : HomologicalComplex.X C i ⟶ Z)
:
@[simp]
theorem
HomologicalComplex.dFrom_comp_xNextIsoSelf
{ι : Type u_1}
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
{c : ComplexShape ι}
(C : HomologicalComplex V c)
{i : ι}
(h : ¬ComplexShape.Rel c i (ComplexShape.next c i))
:
@[simp]
theorem
HomologicalComplex.dTo_comp_dFrom
{ι : Type u_1}
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
{c : ComplexShape ι}
(C : HomologicalComplex V c)
(j : ι)
:
theorem
HomologicalComplex.kernel_from_eq_kernel
{ι : Type u_1}
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
{c : ComplexShape ι}
(C : HomologicalComplex V c)
[CategoryTheory.Limits.HasKernels V]
{i : ι}
{j : ι}
(r : ComplexShape.Rel c i j)
:
theorem
HomologicalComplex.image_to_eq_image
{ι : Type u_1}
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
{c : ComplexShape ι}
(C : HomologicalComplex V c)
[CategoryTheory.Limits.HasImages V]
[CategoryTheory.Limits.HasEqualizers V]
{i : ι}
{j : ι}
(r : ComplexShape.Rel c i j)
:
@[simp]
theorem
HomologicalComplex.Hom.isoApp_inv
{ι : Type u_1}
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
{c : ComplexShape ι}
{C₁ : HomologicalComplex V c}
{C₂ : HomologicalComplex V c}
(f : C₁ ≅ C₂)
(i : ι)
:
(HomologicalComplex.Hom.isoApp f i).inv = HomologicalComplex.Hom.f f.inv i
@[simp]
theorem
HomologicalComplex.Hom.isoApp_hom
{ι : Type u_1}
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
{c : ComplexShape ι}
{C₁ : HomologicalComplex V c}
{C₂ : HomologicalComplex V c}
(f : C₁ ≅ C₂)
(i : ι)
:
(HomologicalComplex.Hom.isoApp f i).hom = HomologicalComplex.Hom.f f.hom i
def
HomologicalComplex.Hom.isoApp
{ι : Type u_1}
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
{c : ComplexShape ι}
{C₁ : HomologicalComplex V c}
{C₂ : HomologicalComplex V c}
(f : C₁ ≅ C₂)
(i : ι)
:
HomologicalComplex.X C₁ i ≅ HomologicalComplex.X C₂ i
The i-th component of an isomorphism of chain complexes.
Instances For
@[simp]
theorem
HomologicalComplex.Hom.isoOfComponents_hom_f
{ι : Type u_1}
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
{c : ComplexShape ι}
{C₁ : HomologicalComplex V c}
{C₂ : HomologicalComplex V c}
(f : (i : ι) → HomologicalComplex.X C₁ i ≅ HomologicalComplex.X C₂ i)
(hf : autoParam
(∀ (i j : ι),
ComplexShape.Rel c i j →
CategoryTheory.CategoryStruct.comp (f i).hom (HomologicalComplex.d C₂ i j) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.d C₁ i j) (f j).hom)
_auto✝)
(i : ι)
:
HomologicalComplex.Hom.f (HomologicalComplex.Hom.isoOfComponents f).hom i = (f i).hom
@[simp]
theorem
HomologicalComplex.Hom.isoOfComponents_inv_f
{ι : Type u_1}
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
{c : ComplexShape ι}
{C₁ : HomologicalComplex V c}
{C₂ : HomologicalComplex V c}
(f : (i : ι) → HomologicalComplex.X C₁ i ≅ HomologicalComplex.X C₂ i)
(hf : autoParam
(∀ (i j : ι),
ComplexShape.Rel c i j →
CategoryTheory.CategoryStruct.comp (f i).hom (HomologicalComplex.d C₂ i j) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.d C₁ i j) (f j).hom)
_auto✝)
(i : ι)
:
HomologicalComplex.Hom.f (HomologicalComplex.Hom.isoOfComponents f).inv i = (f i).inv
def
HomologicalComplex.Hom.isoOfComponents
{ι : Type u_1}
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
{c : ComplexShape ι}
{C₁ : HomologicalComplex V c}
{C₂ : HomologicalComplex V c}
(f : (i : ι) → HomologicalComplex.X C₁ i ≅ HomologicalComplex.X C₂ i)
(hf : autoParam
(∀ (i j : ι),
ComplexShape.Rel c i j →
CategoryTheory.CategoryStruct.comp (f i).hom (HomologicalComplex.d C₂ i j) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.d C₁ i j) (f j).hom)
_auto✝)
:
C₁ ≅ C₂
Construct an isomorphism of chain complexes from isomorphism of the objects which commute with the differentials.
Instances For
@[simp]
theorem
HomologicalComplex.Hom.isoOfComponents_app
{ι : Type u_1}
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
{c : ComplexShape ι}
{C₁ : HomologicalComplex V c}
{C₂ : HomologicalComplex V c}
(f : (i : ι) → HomologicalComplex.X C₁ i ≅ HomologicalComplex.X C₂ i)
(hf : ∀ (i j : ι),
ComplexShape.Rel c i j →
CategoryTheory.CategoryStruct.comp (f i).hom (HomologicalComplex.d C₂ i j) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.d C₁ i j) (f j).hom)
(i : ι)
:
theorem
HomologicalComplex.Hom.isIso_of_components
{ι : Type u_1}
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
{c : ComplexShape ι}
{C₁ : HomologicalComplex V c}
{C₂ : HomologicalComplex V c}
(f : C₁ ⟶ C₂)
[∀ (n : ι), CategoryTheory.IsIso (HomologicalComplex.Hom.f f n)]
:
@[inline, reducible]
abbrev
HomologicalComplex.Hom.prev
{ι : Type u_1}
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
{c : ComplexShape ι}
{C₁ : HomologicalComplex V c}
{C₂ : HomologicalComplex V c}
(f : HomologicalComplex.Hom C₁ C₂)
(j : ι)
:
f.prev j is f.f i if there is some r i j, and f.f j otherwise.
Instances For
theorem
HomologicalComplex.Hom.prev_eq
{ι : Type u_1}
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
{c : ComplexShape ι}
{C₁ : HomologicalComplex V c}
{C₂ : HomologicalComplex V c}
(f : HomologicalComplex.Hom C₁ C₂)
{i : ι}
{j : ι}
(w : ComplexShape.Rel c i j)
:
@[inline, reducible]
abbrev
HomologicalComplex.Hom.next
{ι : Type u_1}
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
{c : ComplexShape ι}
{C₁ : HomologicalComplex V c}
{C₂ : HomologicalComplex V c}
(f : HomologicalComplex.Hom C₁ C₂)
(i : ι)
:
f.next i is f.f j if there is some r i j, and f.f j otherwise.
Instances For
theorem
HomologicalComplex.Hom.next_eq
{ι : Type u_1}
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
{c : ComplexShape ι}
{C₁ : HomologicalComplex V c}
{C₂ : HomologicalComplex V c}
(f : HomologicalComplex.Hom C₁ C₂)
{i : ι}
{j : ι}
(w : ComplexShape.Rel c i j)
:
@[simp]
theorem
HomologicalComplex.Hom.comm_from_assoc
{ι : Type u_1}
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
{c : ComplexShape ι}
{C₁ : HomologicalComplex V c}
{C₂ : HomologicalComplex V c}
(f : HomologicalComplex.Hom C₁ C₂)
(i : ι)
{Z : V}
(h : HomologicalComplex.xNext C₂ i ⟶ Z)
:
@[simp]
theorem
HomologicalComplex.Hom.comm_from_apply
{ι : Type u_1}
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
{c : ComplexShape ι}
{C₁ : HomologicalComplex V c}
{C₂ : HomologicalComplex V c}
(f : HomologicalComplex.Hom C₁ C₂)
(i : ι)
[inst : CategoryTheory.ConcreteCategory V]
(x : (CategoryTheory.forget V).obj (HomologicalComplex.X C₁ i))
:
↑(HomologicalComplex.d C₂ i (ComplexShape.next c i)) (↑(HomologicalComplex.Hom.f f i) x) = ↑(HomologicalComplex.Hom.f f (ComplexShape.next c i)) (↑(HomologicalComplex.d C₁ i (ComplexShape.next c i)) x)
theorem
HomologicalComplex.Hom.comm_from
{ι : Type u_1}
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
{c : ComplexShape ι}
{C₁ : HomologicalComplex V c}
{C₂ : HomologicalComplex V c}
(f : HomologicalComplex.Hom C₁ C₂)
(i : ι)
:
@[simp]
theorem
HomologicalComplex.Hom.comm_to_assoc
{ι : Type u_1}
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
{c : ComplexShape ι}
{C₁ : HomologicalComplex V c}
{C₂ : HomologicalComplex V c}
(f : HomologicalComplex.Hom C₁ C₂)
(j : ι)
{Z : V}
(h : HomologicalComplex.X C₂ j ⟶ Z)
:
@[simp]
theorem
HomologicalComplex.Hom.comm_to_apply
{ι : Type u_1}
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
{c : ComplexShape ι}
{C₁ : HomologicalComplex V c}
{C₂ : HomologicalComplex V c}
(f : HomologicalComplex.Hom C₁ C₂)
(j : ι)
[inst : CategoryTheory.ConcreteCategory V]
(x : (CategoryTheory.forget V).obj (HomologicalComplex.X C₁ (ComplexShape.prev c j)))
:
↑(HomologicalComplex.d C₂ (ComplexShape.prev c j) j) (↑(HomologicalComplex.Hom.f f (ComplexShape.prev c j)) x) = ↑(HomologicalComplex.Hom.f f j) (↑(HomologicalComplex.d C₁ (ComplexShape.prev c j) j) x)
theorem
HomologicalComplex.Hom.comm_to
{ι : Type u_1}
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
{c : ComplexShape ι}
{C₁ : HomologicalComplex V c}
{C₂ : HomologicalComplex V c}
(f : HomologicalComplex.Hom C₁ C₂)
(j : ι)
:
def
HomologicalComplex.Hom.sqFrom
{ι : Type u_1}
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
{c : ComplexShape ι}
{C₁ : HomologicalComplex V c}
{C₂ : HomologicalComplex V c}
(f : HomologicalComplex.Hom C₁ C₂)
(i : ι)
:
A morphism of chain complexes induces a morphism of arrows of the differentials out of each object.
Instances For
@[simp]
theorem
HomologicalComplex.Hom.sqFrom_left
{ι : Type u_1}
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
{c : ComplexShape ι}
{C₁ : HomologicalComplex V c}
{C₂ : HomologicalComplex V c}
(f : HomologicalComplex.Hom C₁ C₂)
(i : ι)
:
(HomologicalComplex.Hom.sqFrom f i).left = HomologicalComplex.Hom.f f i
@[simp]
theorem
HomologicalComplex.Hom.sqFrom_right
{ι : Type u_1}
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
{c : ComplexShape ι}
{C₁ : HomologicalComplex V c}
{C₂ : HomologicalComplex V c}
(f : HomologicalComplex.Hom C₁ C₂)
(i : ι)
:
(HomologicalComplex.Hom.sqFrom f i).right = HomologicalComplex.Hom.next f i
@[simp]
theorem
HomologicalComplex.Hom.sqFrom_id
{ι : Type u_1}
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
{c : ComplexShape ι}
(C₁ : HomologicalComplex V c)
(i : ι)
:
@[simp]
theorem
HomologicalComplex.Hom.sqFrom_comp
{ι : Type u_1}
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
{c : ComplexShape ι}
{C₁ : HomologicalComplex V c}
{C₂ : HomologicalComplex V c}
{C₃ : HomologicalComplex V c}
(f : C₁ ⟶ C₂)
(g : C₂ ⟶ C₃)
(i : ι)
:
def
HomologicalComplex.Hom.sqTo
{ι : Type u_1}
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
{c : ComplexShape ι}
{C₁ : HomologicalComplex V c}
{C₂ : HomologicalComplex V c}
(f : HomologicalComplex.Hom C₁ C₂)
(j : ι)
:
A morphism of chain complexes induces a morphism of arrows of the differentials into each object.
Instances For
@[simp]
theorem
HomologicalComplex.Hom.sqTo_left
{ι : Type u_1}
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
{c : ComplexShape ι}
{C₁ : HomologicalComplex V c}
{C₂ : HomologicalComplex V c}
(f : HomologicalComplex.Hom C₁ C₂)
(j : ι)
:
(HomologicalComplex.Hom.sqTo f j).left = HomologicalComplex.Hom.prev f j
@[simp]
theorem
HomologicalComplex.Hom.sqTo_right
{ι : Type u_1}
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
{c : ComplexShape ι}
{C₁ : HomologicalComplex V c}
{C₂ : HomologicalComplex V c}
(f : HomologicalComplex.Hom C₁ C₂)
(j : ι)
:
(HomologicalComplex.Hom.sqTo f j).right = HomologicalComplex.Hom.f f j
def
ChainComplex.of
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
{α : Type u_2}
[AddRightCancelSemigroup α]
[One α]
[DecidableEq α]
(X : α → V)
(d : (n : α) → X (n + 1) ⟶ X n)
(sq : ∀ (n : α), CategoryTheory.CategoryStruct.comp (d (n + 1)) (d n) = 0)
:
ChainComplex V α
Construct an α-indexed chain complex from a dependently-typed differential.
Instances For
@[simp]
theorem
ChainComplex.of_x
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
{α : Type u_2}
[AddRightCancelSemigroup α]
[One α]
[DecidableEq α]
(X : α → V)
(d : (n : α) → X (n + 1) ⟶ X n)
(sq : ∀ (n : α), CategoryTheory.CategoryStruct.comp (d (n + 1)) (d n) = 0)
(n : α)
:
HomologicalComplex.X (ChainComplex.of X d sq) n = X n
@[simp]
theorem
ChainComplex.of_d
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
{α : Type u_2}
[AddRightCancelSemigroup α]
[One α]
[DecidableEq α]
(X : α → V)
(d : (n : α) → X (n + 1) ⟶ X n)
(sq : ∀ (n : α), CategoryTheory.CategoryStruct.comp (d (n + 1)) (d n) = 0)
(j : α)
:
HomologicalComplex.d (ChainComplex.of X d sq) (j + 1) j = d j
theorem
ChainComplex.of_d_ne
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
{α : Type u_2}
[AddRightCancelSemigroup α]
[One α]
[DecidableEq α]
(X : α → V)
(d : (n : α) → X (n + 1) ⟶ X n)
(sq : ∀ (n : α), CategoryTheory.CategoryStruct.comp (d (n + 1)) (d n) = 0)
{i : α}
{j : α}
(h : i ≠ j + 1)
:
HomologicalComplex.d (ChainComplex.of X d sq) i j = 0
@[simp]
theorem
ChainComplex.ofHom_f
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
{α : Type u_2}
[AddRightCancelSemigroup α]
[One α]
[DecidableEq α]
(X : α → V)
(d_X : (n : α) → X (n + 1) ⟶ X n)
(sq_X : ∀ (n : α), CategoryTheory.CategoryStruct.comp (d_X (n + 1)) (d_X n) = 0)
(Y : α → V)
(d_Y : (n : α) → Y (n + 1) ⟶ Y n)
(sq_Y : ∀ (n : α), CategoryTheory.CategoryStruct.comp (d_Y (n + 1)) (d_Y n) = 0)
(f : (i : α) → X i ⟶ Y i)
(comm : ∀ (i : α), CategoryTheory.CategoryStruct.comp (f (i + 1)) (d_Y i) = CategoryTheory.CategoryStruct.comp (d_X i) (f i))
(i : α)
:
HomologicalComplex.Hom.f (ChainComplex.ofHom X d_X sq_X Y d_Y sq_Y f comm) i = f i
def
ChainComplex.ofHom
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
{α : Type u_2}
[AddRightCancelSemigroup α]
[One α]
[DecidableEq α]
(X : α → V)
(d_X : (n : α) → X (n + 1) ⟶ X n)
(sq_X : ∀ (n : α), CategoryTheory.CategoryStruct.comp (d_X (n + 1)) (d_X n) = 0)
(Y : α → V)
(d_Y : (n : α) → Y (n + 1) ⟶ Y n)
(sq_Y : ∀ (n : α), CategoryTheory.CategoryStruct.comp (d_Y (n + 1)) (d_Y n) = 0)
(f : (i : α) → X i ⟶ Y i)
(comm : ∀ (i : α), CategoryTheory.CategoryStruct.comp (f (i + 1)) (d_Y i) = CategoryTheory.CategoryStruct.comp (d_X i) (f i))
:
ChainComplex.of X d_X sq_X ⟶ ChainComplex.of Y d_Y sq_Y
A constructor for chain maps between α-indexed chain complexes built using ChainComplex.of,
from a dependently typed collection of morphisms.
Instances For
structure
ChainComplex.MkStruct
(V : Type u)
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
:
Type (max u v)
- X₀ : V
- X₁ : V
- X₂ : V
- d₀ : s.X₁ ⟶ s.X₀
- d₁ : s.X₂ ⟶ s.X₁
- s : CategoryTheory.CategoryStruct.comp s.d₁ s.d₀ = 0
Auxiliary structure for setting up the recursion in mk.
This is purely an implementation detail: for some reason just using the dependent 6-tuple directly
results in mk_aux taking much longer (well over the -T100000 limit) to elaborate.
Instances For
def
ChainComplex.MkStruct.flat
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
(t : ChainComplex.MkStruct V)
:
(X₀ : V) ×' (X₁ : V) ×' (X₂ : V) ×' (d₀ : X₁ ⟶ X₀) ×' (d₁ : X₂ ⟶ X₁) ×' CategoryTheory.CategoryStruct.comp d₁ d₀ = 0
Flatten to a tuple.
Instances For
def
ChainComplex.mkAux
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
(X₀ : V)
(X₁ : V)
(X₂ : V)
(d₀ : X₁ ⟶ X₀)
(d₁ : X₂ ⟶ X₁)
(s : CategoryTheory.CategoryStruct.comp d₁ d₀ = 0)
(succ : (t :
(X₀ : V) ×'
(X₁ : V) ×' (X₂ : V) ×' (d₀ : X₁ ⟶ X₀) ×' (d₁ : X₂ ⟶ X₁) ×' CategoryTheory.CategoryStruct.comp d₁ d₀ = 0) →
(X₃ : V) ×' (d₂ : X₃ ⟶ t.snd.snd.fst) ×' CategoryTheory.CategoryStruct.comp d₂ t.snd.snd.snd.snd.fst = 0)
:
Auxiliary definition for mk.
Equations
- One or more equations did not get rendered due to their size.
- ChainComplex.mkAux X₀ X₁ X₂ d₀ d₁ s succ 0 = { X₀ := X₀, X₁ := X₁, X₂ := X₂, d₀ := d₀, d₁ := d₁, s := s }
Instances For
def
ChainComplex.mk
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
(X₀ : V)
(X₁ : V)
(X₂ : V)
(d₀ : X₁ ⟶ X₀)
(d₁ : X₂ ⟶ X₁)
(s : CategoryTheory.CategoryStruct.comp d₁ d₀ = 0)
(succ : (t :
(X₀ : V) ×'
(X₁ : V) ×' (X₂ : V) ×' (d₀ : X₁ ⟶ X₀) ×' (d₁ : X₂ ⟶ X₁) ×' CategoryTheory.CategoryStruct.comp d₁ d₀ = 0) →
(X₃ : V) ×' (d₂ : X₃ ⟶ t.snd.snd.fst) ×' CategoryTheory.CategoryStruct.comp d₂ t.snd.snd.snd.snd.fst = 0)
:
An inductive constructor for ℕ-indexed chain complexes.
You provide explicitly the first two differentials, then a function which takes two differentials and the fact they compose to zero, and returns the next object, its differential, and the fact it composes appropriately to zero.
See also mk', which only sees the previous differential in the inductive step.
Instances For
@[simp]
theorem
ChainComplex.mk_X_0
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
(X₀ : V)
(X₁ : V)
(X₂ : V)
(d₀ : X₁ ⟶ X₀)
(d₁ : X₂ ⟶ X₁)
(s : CategoryTheory.CategoryStruct.comp d₁ d₀ = 0)
(succ : (t :
(X₀ : V) ×'
(X₁ : V) ×' (X₂ : V) ×' (d₀ : X₁ ⟶ X₀) ×' (d₁ : X₂ ⟶ X₁) ×' CategoryTheory.CategoryStruct.comp d₁ d₀ = 0) →
(X₃ : V) ×' (d₂ : X₃ ⟶ t.snd.snd.fst) ×' CategoryTheory.CategoryStruct.comp d₂ t.snd.snd.snd.snd.fst = 0)
:
HomologicalComplex.X (ChainComplex.mk X₀ X₁ X₂ d₀ d₁ s succ) 0 = X₀
@[simp]
theorem
ChainComplex.mk_X_1
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
(X₀ : V)
(X₁ : V)
(X₂ : V)
(d₀ : X₁ ⟶ X₀)
(d₁ : X₂ ⟶ X₁)
(s : CategoryTheory.CategoryStruct.comp d₁ d₀ = 0)
(succ : (t :
(X₀ : V) ×'
(X₁ : V) ×' (X₂ : V) ×' (d₀ : X₁ ⟶ X₀) ×' (d₁ : X₂ ⟶ X₁) ×' CategoryTheory.CategoryStruct.comp d₁ d₀ = 0) →
(X₃ : V) ×' (d₂ : X₃ ⟶ t.snd.snd.fst) ×' CategoryTheory.CategoryStruct.comp d₂ t.snd.snd.snd.snd.fst = 0)
:
HomologicalComplex.X (ChainComplex.mk X₀ X₁ X₂ d₀ d₁ s succ) 1 = X₁
@[simp]
theorem
ChainComplex.mk_X_2
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
(X₀ : V)
(X₁ : V)
(X₂ : V)
(d₀ : X₁ ⟶ X₀)
(d₁ : X₂ ⟶ X₁)
(s : CategoryTheory.CategoryStruct.comp d₁ d₀ = 0)
(succ : (t :
(X₀ : V) ×'
(X₁ : V) ×' (X₂ : V) ×' (d₀ : X₁ ⟶ X₀) ×' (d₁ : X₂ ⟶ X₁) ×' CategoryTheory.CategoryStruct.comp d₁ d₀ = 0) →
(X₃ : V) ×' (d₂ : X₃ ⟶ t.snd.snd.fst) ×' CategoryTheory.CategoryStruct.comp d₂ t.snd.snd.snd.snd.fst = 0)
:
HomologicalComplex.X (ChainComplex.mk X₀ X₁ X₂ d₀ d₁ s succ) 2 = X₂
@[simp]
theorem
ChainComplex.mk_d_1_0
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
(X₀ : V)
(X₁ : V)
(X₂ : V)
(d₀ : X₁ ⟶ X₀)
(d₁ : X₂ ⟶ X₁)
(s : CategoryTheory.CategoryStruct.comp d₁ d₀ = 0)
(succ : (t :
(X₀ : V) ×'
(X₁ : V) ×' (X₂ : V) ×' (d₀ : X₁ ⟶ X₀) ×' (d₁ : X₂ ⟶ X₁) ×' CategoryTheory.CategoryStruct.comp d₁ d₀ = 0) →
(X₃ : V) ×' (d₂ : X₃ ⟶ t.snd.snd.fst) ×' CategoryTheory.CategoryStruct.comp d₂ t.snd.snd.snd.snd.fst = 0)
:
HomologicalComplex.d (ChainComplex.mk X₀ X₁ X₂ d₀ d₁ s succ) 1 0 = d₀
@[simp]
theorem
ChainComplex.mk_d_2_0
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
(X₀ : V)
(X₁ : V)
(X₂ : V)
(d₀ : X₁ ⟶ X₀)
(d₁ : X₂ ⟶ X₁)
(s : CategoryTheory.CategoryStruct.comp d₁ d₀ = 0)
(succ : (t :
(X₀ : V) ×'
(X₁ : V) ×' (X₂ : V) ×' (d₀ : X₁ ⟶ X₀) ×' (d₁ : X₂ ⟶ X₁) ×' CategoryTheory.CategoryStruct.comp d₁ d₀ = 0) →
(X₃ : V) ×' (d₂ : X₃ ⟶ t.snd.snd.fst) ×' CategoryTheory.CategoryStruct.comp d₂ t.snd.snd.snd.snd.fst = 0)
:
HomologicalComplex.d (ChainComplex.mk X₀ X₁ X₂ d₀ d₁ s succ) 2 1 = d₁
def
ChainComplex.mk'
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
(X₀ : V)
(X₁ : V)
(d : X₁ ⟶ X₀)
(succ' : (t : (X₀ : V) × (X₁ : V) × (X₁ ⟶ X₀)) →
(X₂ : V) ×' (d : X₂ ⟶ t.snd.fst) ×' CategoryTheory.CategoryStruct.comp d t.snd.snd = 0)
:
A simpler inductive constructor for ℕ-indexed chain complexes.
You provide explicitly the first differential, then a function which takes a differential, and returns the next object, its differential, and the fact it composes appropriately to zero.
Instances For
@[simp]
theorem
ChainComplex.mk'_X_0
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
(X₀ : V)
(X₁ : V)
(d₀ : X₁ ⟶ X₀)
(succ' : (t : (X₀ : V) × (X₁ : V) × (X₁ ⟶ X₀)) →
(X₂ : V) ×' (d : X₂ ⟶ t.snd.fst) ×' CategoryTheory.CategoryStruct.comp d t.snd.snd = 0)
:
HomologicalComplex.X (ChainComplex.mk' X₀ X₁ d₀ succ') 0 = X₀
@[simp]
theorem
ChainComplex.mk'_X_1
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
(X₀ : V)
(X₁ : V)
(d₀ : X₁ ⟶ X₀)
(succ' : (t : (X₀ : V) × (X₁ : V) × (X₁ ⟶ X₀)) →
(X₂ : V) ×' (d : X₂ ⟶ t.snd.fst) ×' CategoryTheory.CategoryStruct.comp d t.snd.snd = 0)
:
HomologicalComplex.X (ChainComplex.mk' X₀ X₁ d₀ succ') 1 = X₁
@[simp]
theorem
ChainComplex.mk'_d_1_0
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
(X₀ : V)
(X₁ : V)
(d₀ : X₁ ⟶ X₀)
(succ' : (t : (X₀ : V) × (X₁ : V) × (X₁ ⟶ X₀)) →
(X₂ : V) ×' (d : X₂ ⟶ t.snd.fst) ×' CategoryTheory.CategoryStruct.comp d t.snd.snd = 0)
:
HomologicalComplex.d (ChainComplex.mk' X₀ X₁ d₀ succ') 1 0 = d₀
def
ChainComplex.mkHomAux
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
(P : ChainComplex V ℕ)
(Q : ChainComplex V ℕ)
(zero : HomologicalComplex.X P 0 ⟶ HomologicalComplex.X Q 0)
(one : HomologicalComplex.X P 1 ⟶ HomologicalComplex.X Q 1)
(one_zero_comm : CategoryTheory.CategoryStruct.comp one (HomologicalComplex.d Q 1 0) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.d P 1 0) zero)
(succ : (n : ℕ) →
(p :
(f : HomologicalComplex.X P n ⟶ HomologicalComplex.X Q n) ×'
(f' : HomologicalComplex.X P (n + 1) ⟶ HomologicalComplex.X Q (n + 1)) ×'
CategoryTheory.CategoryStruct.comp f' (HomologicalComplex.d Q (n + 1) n) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.d P (n + 1) n) f) →
(f'' : HomologicalComplex.X P (n + 2) ⟶ HomologicalComplex.X Q (n + 2)) ×'
CategoryTheory.CategoryStruct.comp f'' (HomologicalComplex.d Q (n + 2) (n + 1)) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.d P (n + 2) (n + 1)) p.snd.fst)
(n : ℕ)
:
(f : HomologicalComplex.X P n ⟶ HomologicalComplex.X Q n) ×'
(f' : HomologicalComplex.X P (n + 1) ⟶ HomologicalComplex.X Q (n + 1)) ×'
CategoryTheory.CategoryStruct.comp f' (HomologicalComplex.d Q (n + 1) n) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.d P (n + 1) n) f
An auxiliary construction for mkHom.
Here we build by induction a family of commutative squares,
but don't require at the type level that these successive commutative squares actually agree.
They do in fact agree, and we then capture that at the type level (i.e. by constructing a chain map)
in mkHom.
Equations
- One or more equations did not get rendered due to their size.
- ChainComplex.mkHomAux P Q zero one one_zero_comm succ 0 = { fst := zero, snd := { fst := one, snd := one_zero_comm } }
Instances For
def
ChainComplex.mkHom
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
(P : ChainComplex V ℕ)
(Q : ChainComplex V ℕ)
(zero : HomologicalComplex.X P 0 ⟶ HomologicalComplex.X Q 0)
(one : HomologicalComplex.X P 1 ⟶ HomologicalComplex.X Q 1)
(one_zero_comm : CategoryTheory.CategoryStruct.comp one (HomologicalComplex.d Q 1 0) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.d P 1 0) zero)
(succ : (n : ℕ) →
(p :
(f : HomologicalComplex.X P n ⟶ HomologicalComplex.X Q n) ×'
(f' : HomologicalComplex.X P (n + 1) ⟶ HomologicalComplex.X Q (n + 1)) ×'
CategoryTheory.CategoryStruct.comp f' (HomologicalComplex.d Q (n + 1) n) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.d P (n + 1) n) f) →
(f'' : HomologicalComplex.X P (n + 2) ⟶ HomologicalComplex.X Q (n + 2)) ×'
CategoryTheory.CategoryStruct.comp f'' (HomologicalComplex.d Q (n + 2) (n + 1)) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.d P (n + 2) (n + 1)) p.snd.fst)
:
P ⟶ Q
A constructor for chain maps between ℕ-indexed chain complexes,
working by induction on commutative squares.
You need to provide the components of the chain map in degrees 0 and 1, show that these form a commutative square, and then give a construction of each component, and the fact that it forms a commutative square with the previous component, using as an inductive hypothesis the data (and commutativity) of the previous two components.
Instances For
@[simp]
theorem
ChainComplex.mkHom_f_0
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
(P : ChainComplex V ℕ)
(Q : ChainComplex V ℕ)
(zero : HomologicalComplex.X P 0 ⟶ HomologicalComplex.X Q 0)
(one : HomologicalComplex.X P 1 ⟶ HomologicalComplex.X Q 1)
(one_zero_comm : CategoryTheory.CategoryStruct.comp one (HomologicalComplex.d Q 1 0) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.d P 1 0) zero)
(succ : (n : ℕ) →
(p :
(f : HomologicalComplex.X P n ⟶ HomologicalComplex.X Q n) ×'
(f' : HomologicalComplex.X P (n + 1) ⟶ HomologicalComplex.X Q (n + 1)) ×'
CategoryTheory.CategoryStruct.comp f' (HomologicalComplex.d Q (n + 1) n) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.d P (n + 1) n) f) →
(f'' : HomologicalComplex.X P (n + 2) ⟶ HomologicalComplex.X Q (n + 2)) ×'
CategoryTheory.CategoryStruct.comp f'' (HomologicalComplex.d Q (n + 2) (n + 1)) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.d P (n + 2) (n + 1)) p.snd.fst)
:
HomologicalComplex.Hom.f (ChainComplex.mkHom P Q zero one one_zero_comm succ) 0 = zero
@[simp]
theorem
ChainComplex.mkHom_f_1
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
(P : ChainComplex V ℕ)
(Q : ChainComplex V ℕ)
(zero : HomologicalComplex.X P 0 ⟶ HomologicalComplex.X Q 0)
(one : HomologicalComplex.X P 1 ⟶ HomologicalComplex.X Q 1)
(one_zero_comm : CategoryTheory.CategoryStruct.comp one (HomologicalComplex.d Q 1 0) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.d P 1 0) zero)
(succ : (n : ℕ) →
(p :
(f : HomologicalComplex.X P n ⟶ HomologicalComplex.X Q n) ×'
(f' : HomologicalComplex.X P (n + 1) ⟶ HomologicalComplex.X Q (n + 1)) ×'
CategoryTheory.CategoryStruct.comp f' (HomologicalComplex.d Q (n + 1) n) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.d P (n + 1) n) f) →
(f'' : HomologicalComplex.X P (n + 2) ⟶ HomologicalComplex.X Q (n + 2)) ×'
CategoryTheory.CategoryStruct.comp f'' (HomologicalComplex.d Q (n + 2) (n + 1)) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.d P (n + 2) (n + 1)) p.snd.fst)
:
HomologicalComplex.Hom.f (ChainComplex.mkHom P Q zero one one_zero_comm succ) 1 = one
@[simp]
theorem
ChainComplex.mkHom_f_succ_succ
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
(P : ChainComplex V ℕ)
(Q : ChainComplex V ℕ)
(zero : HomologicalComplex.X P 0 ⟶ HomologicalComplex.X Q 0)
(one : HomologicalComplex.X P 1 ⟶ HomologicalComplex.X Q 1)
(one_zero_comm : CategoryTheory.CategoryStruct.comp one (HomologicalComplex.d Q 1 0) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.d P 1 0) zero)
(succ : (n : ℕ) →
(p :
(f : HomologicalComplex.X P n ⟶ HomologicalComplex.X Q n) ×'
(f' : HomologicalComplex.X P (n + 1) ⟶ HomologicalComplex.X Q (n + 1)) ×'
CategoryTheory.CategoryStruct.comp f' (HomologicalComplex.d Q (n + 1) n) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.d P (n + 1) n) f) →
(f'' : HomologicalComplex.X P (n + 2) ⟶ HomologicalComplex.X Q (n + 2)) ×'
CategoryTheory.CategoryStruct.comp f'' (HomologicalComplex.d Q (n + 2) (n + 1)) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.d P (n + 2) (n + 1)) p.snd.fst)
(n : ℕ)
:
HomologicalComplex.Hom.f (ChainComplex.mkHom P Q zero one one_zero_comm succ) (n + 2) = (succ n
{ fst := HomologicalComplex.Hom.f (ChainComplex.mkHom P Q zero one one_zero_comm succ) n,
snd :=
{ fst := HomologicalComplex.Hom.f (ChainComplex.mkHom P Q zero one one_zero_comm succ) (n + 1),
snd :=
(_ :
CategoryTheory.CategoryStruct.comp
(HomologicalComplex.Hom.f (ChainComplex.mkHom P Q zero one one_zero_comm succ) (n + 1))
(HomologicalComplex.d Q (n + 1) n) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.d P (n + 1) n)
(HomologicalComplex.Hom.f (ChainComplex.mkHom P Q zero one one_zero_comm succ) n)) } }).fst
def
CochainComplex.of
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
{α : Type u_2}
[AddRightCancelSemigroup α]
[One α]
[DecidableEq α]
(X : α → V)
(d : (n : α) → X n ⟶ X (n + 1))
(sq : ∀ (n : α), CategoryTheory.CategoryStruct.comp (d n) (d (n + 1)) = 0)
:
CochainComplex V α
Construct an α-indexed cochain complex from a dependently-typed differential.
Instances For
@[simp]
theorem
CochainComplex.of_x
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
{α : Type u_2}
[AddRightCancelSemigroup α]
[One α]
[DecidableEq α]
(X : α → V)
(d : (n : α) → X n ⟶ X (n + 1))
(sq : ∀ (n : α), CategoryTheory.CategoryStruct.comp (d n) (d (n + 1)) = 0)
(n : α)
:
HomologicalComplex.X (CochainComplex.of X d sq) n = X n
@[simp]
theorem
CochainComplex.of_d
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
{α : Type u_2}
[AddRightCancelSemigroup α]
[One α]
[DecidableEq α]
(X : α → V)
(d : (n : α) → X n ⟶ X (n + 1))
(sq : ∀ (n : α), CategoryTheory.CategoryStruct.comp (d n) (d (n + 1)) = 0)
(j : α)
:
HomologicalComplex.d (CochainComplex.of X d sq) j (j + 1) = d j
theorem
CochainComplex.of_d_ne
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
{α : Type u_2}
[AddRightCancelSemigroup α]
[One α]
[DecidableEq α]
(X : α → V)
(d : (n : α) → X n ⟶ X (n + 1))
(sq : ∀ (n : α), CategoryTheory.CategoryStruct.comp (d n) (d (n + 1)) = 0)
{i : α}
{j : α}
(h : i + 1 ≠ j)
:
HomologicalComplex.d (CochainComplex.of X d sq) i j = 0
@[simp]
theorem
CochainComplex.ofHom_f
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
{α : Type u_2}
[AddRightCancelSemigroup α]
[One α]
[DecidableEq α]
(X : α → V)
(d_X : (n : α) → X n ⟶ X (n + 1))
(sq_X : ∀ (n : α), CategoryTheory.CategoryStruct.comp (d_X n) (d_X (n + 1)) = 0)
(Y : α → V)
(d_Y : (n : α) → Y n ⟶ Y (n + 1))
(sq_Y : ∀ (n : α), CategoryTheory.CategoryStruct.comp (d_Y n) (d_Y (n + 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 : α)
:
HomologicalComplex.Hom.f (CochainComplex.ofHom X d_X sq_X Y d_Y sq_Y f comm) i = f i
def
CochainComplex.ofHom
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
{α : Type u_2}
[AddRightCancelSemigroup α]
[One α]
[DecidableEq α]
(X : α → V)
(d_X : (n : α) → X n ⟶ X (n + 1))
(sq_X : ∀ (n : α), CategoryTheory.CategoryStruct.comp (d_X n) (d_X (n + 1)) = 0)
(Y : α → V)
(d_Y : (n : α) → Y n ⟶ Y (n + 1))
(sq_Y : ∀ (n : α), CategoryTheory.CategoryStruct.comp (d_Y n) (d_Y (n + 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)))
:
CochainComplex.of X d_X sq_X ⟶ CochainComplex.of Y d_Y sq_Y
A constructor for chain maps between α-indexed cochain complexes built using CochainComplex.of,
from a dependently typed collection of morphisms.
Instances For
structure
CochainComplex.MkStruct
(V : Type u)
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
:
Type (max u v)
- X₀ : V
- X₁ : V
- X₂ : V
- d₀ : s.X₀ ⟶ s.X₁
- d₁ : s.X₁ ⟶ s.X₂
- s : CategoryTheory.CategoryStruct.comp s.d₀ s.d₁ = 0
Auxiliary structure for setting up the recursion in mk.
This is purely an implementation detail: for some reason just using the dependent 6-tuple directly
results in mkAux taking much longer (well over the -T100000 limit) to elaborate.
Instances For
def
CochainComplex.MkStruct.flat
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
(t : CochainComplex.MkStruct V)
:
(X₀ : V) ×' (X₁ : V) ×' (X₂ : V) ×' (d₀ : X₀ ⟶ X₁) ×' (d₁ : X₁ ⟶ X₂) ×' CategoryTheory.CategoryStruct.comp d₀ d₁ = 0
Flatten to a tuple.
Instances For
def
CochainComplex.mkAux
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
(X₀ : V)
(X₁ : V)
(X₂ : V)
(d₀ : X₀ ⟶ X₁)
(d₁ : X₁ ⟶ X₂)
(s : CategoryTheory.CategoryStruct.comp d₀ d₁ = 0)
(succ : (t :
(X₀ : V) ×'
(X₁ : V) ×' (X₂ : V) ×' (d₀ : X₀ ⟶ X₁) ×' (d₁ : X₁ ⟶ X₂) ×' CategoryTheory.CategoryStruct.comp d₀ d₁ = 0) →
(X₃ : V) ×' (d₂ : t.snd.snd.fst ⟶ X₃) ×' CategoryTheory.CategoryStruct.comp t.snd.snd.snd.snd.fst d₂ = 0)
:
Auxiliary definition for mk.
Equations
- One or more equations did not get rendered due to their size.
- CochainComplex.mkAux X₀ X₁ X₂ d₀ d₁ s succ 0 = { X₀ := X₀, X₁ := X₁, X₂ := X₂, d₀ := d₀, d₁ := d₁, s := s }
Instances For
def
CochainComplex.mk
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
(X₀ : V)
(X₁ : V)
(X₂ : V)
(d₀ : X₀ ⟶ X₁)
(d₁ : X₁ ⟶ X₂)
(s : CategoryTheory.CategoryStruct.comp d₀ d₁ = 0)
(succ : (t :
(X₀ : V) ×'
(X₁ : V) ×' (X₂ : V) ×' (d₀ : X₀ ⟶ X₁) ×' (d₁ : X₁ ⟶ X₂) ×' CategoryTheory.CategoryStruct.comp d₀ d₁ = 0) →
(X₃ : V) ×' (d₂ : t.snd.snd.fst ⟶ X₃) ×' CategoryTheory.CategoryStruct.comp t.snd.snd.snd.snd.fst d₂ = 0)
:
An inductive constructor for ℕ-indexed cochain complexes.
You provide explicitly the first two differentials, then a function which takes two differentials and the fact they compose to zero, and returns the next object, its differential, and the fact it composes appropriately to zero.
See also mk', which only sees the previous differential in the inductive step.
Instances For
@[simp]
theorem
CochainComplex.mk_X_0
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
(X₀ : V)
(X₁ : V)
(X₂ : V)
(d₀ : X₀ ⟶ X₁)
(d₁ : X₁ ⟶ X₂)
(s : CategoryTheory.CategoryStruct.comp d₀ d₁ = 0)
(succ : (t :
(X₀ : V) ×'
(X₁ : V) ×' (X₂ : V) ×' (d₀ : X₀ ⟶ X₁) ×' (d₁ : X₁ ⟶ X₂) ×' CategoryTheory.CategoryStruct.comp d₀ d₁ = 0) →
(X₃ : V) ×' (d₂ : t.snd.snd.fst ⟶ X₃) ×' CategoryTheory.CategoryStruct.comp t.snd.snd.snd.snd.fst d₂ = 0)
:
HomologicalComplex.X (CochainComplex.mk X₀ X₁ X₂ d₀ d₁ s succ) 0 = X₀
@[simp]
theorem
CochainComplex.mk_X_1
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
(X₀ : V)
(X₁ : V)
(X₂ : V)
(d₀ : X₀ ⟶ X₁)
(d₁ : X₁ ⟶ X₂)
(s : CategoryTheory.CategoryStruct.comp d₀ d₁ = 0)
(succ : (t :
(X₀ : V) ×'
(X₁ : V) ×' (X₂ : V) ×' (d₀ : X₀ ⟶ X₁) ×' (d₁ : X₁ ⟶ X₂) ×' CategoryTheory.CategoryStruct.comp d₀ d₁ = 0) →
(X₃ : V) ×' (d₂ : t.snd.snd.fst ⟶ X₃) ×' CategoryTheory.CategoryStruct.comp t.snd.snd.snd.snd.fst d₂ = 0)
:
HomologicalComplex.X (CochainComplex.mk X₀ X₁ X₂ d₀ d₁ s succ) 1 = X₁
@[simp]
theorem
CochainComplex.mk_X_2
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
(X₀ : V)
(X₁ : V)
(X₂ : V)
(d₀ : X₀ ⟶ X₁)
(d₁ : X₁ ⟶ X₂)
(s : CategoryTheory.CategoryStruct.comp d₀ d₁ = 0)
(succ : (t :
(X₀ : V) ×'
(X₁ : V) ×' (X₂ : V) ×' (d₀ : X₀ ⟶ X₁) ×' (d₁ : X₁ ⟶ X₂) ×' CategoryTheory.CategoryStruct.comp d₀ d₁ = 0) →
(X₃ : V) ×' (d₂ : t.snd.snd.fst ⟶ X₃) ×' CategoryTheory.CategoryStruct.comp t.snd.snd.snd.snd.fst d₂ = 0)
:
HomologicalComplex.X (CochainComplex.mk X₀ X₁ X₂ d₀ d₁ s succ) 2 = X₂
@[simp]
theorem
CochainComplex.mk_d_1_0
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
(X₀ : V)
(X₁ : V)
(X₂ : V)
(d₀ : X₀ ⟶ X₁)
(d₁ : X₁ ⟶ X₂)
(s : CategoryTheory.CategoryStruct.comp d₀ d₁ = 0)
(succ : (t :
(X₀ : V) ×'
(X₁ : V) ×' (X₂ : V) ×' (d₀ : X₀ ⟶ X₁) ×' (d₁ : X₁ ⟶ X₂) ×' CategoryTheory.CategoryStruct.comp d₀ d₁ = 0) →
(X₃ : V) ×' (d₂ : t.snd.snd.fst ⟶ X₃) ×' CategoryTheory.CategoryStruct.comp t.snd.snd.snd.snd.fst d₂ = 0)
:
HomologicalComplex.d (CochainComplex.mk X₀ X₁ X₂ d₀ d₁ s succ) 0 1 = d₀
@[simp]
theorem
CochainComplex.mk_d_2_0
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
(X₀ : V)
(X₁ : V)
(X₂ : V)
(d₀ : X₀ ⟶ X₁)
(d₁ : X₁ ⟶ X₂)
(s : CategoryTheory.CategoryStruct.comp d₀ d₁ = 0)
(succ : (t :
(X₀ : V) ×'
(X₁ : V) ×' (X₂ : V) ×' (d₀ : X₀ ⟶ X₁) ×' (d₁ : X₁ ⟶ X₂) ×' CategoryTheory.CategoryStruct.comp d₀ d₁ = 0) →
(X₃ : V) ×' (d₂ : t.snd.snd.fst ⟶ X₃) ×' CategoryTheory.CategoryStruct.comp t.snd.snd.snd.snd.fst d₂ = 0)
:
HomologicalComplex.d (CochainComplex.mk X₀ X₁ X₂ d₀ d₁ s succ) 1 2 = d₁
def
CochainComplex.mk'
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
(X₀ : V)
(X₁ : V)
(d : X₀ ⟶ X₁)
(succ' : (t : (X₀ : V) × (X₁ : V) × (X₀ ⟶ X₁)) →
(X₂ : V) ×' (d : t.snd.fst ⟶ X₂) ×' CategoryTheory.CategoryStruct.comp t.snd.snd d = 0)
:
A simpler inductive constructor for ℕ-indexed cochain complexes.
You provide explicitly the first differential, then a function which takes a differential, and returns the next object, its differential, and the fact it composes appropriately to zero.
Instances For
@[simp]
theorem
CochainComplex.mk'_X_0
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
(X₀ : V)
(X₁ : V)
(d₀ : X₀ ⟶ X₁)
(succ' : (t : (X₀ : V) × (X₁ : V) × (X₀ ⟶ X₁)) →
(X₂ : V) ×' (d : t.snd.fst ⟶ X₂) ×' CategoryTheory.CategoryStruct.comp t.snd.snd d = 0)
:
HomologicalComplex.X (CochainComplex.mk' X₀ X₁ d₀ succ') 0 = X₀
@[simp]
theorem
CochainComplex.mk'_X_1
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
(X₀ : V)
(X₁ : V)
(d₀ : X₀ ⟶ X₁)
(succ' : (t : (X₀ : V) × (X₁ : V) × (X₀ ⟶ X₁)) →
(X₂ : V) ×' (d : t.snd.fst ⟶ X₂) ×' CategoryTheory.CategoryStruct.comp t.snd.snd d = 0)
:
HomologicalComplex.X (CochainComplex.mk' X₀ X₁ d₀ succ') 1 = X₁
@[simp]
theorem
CochainComplex.mk'_d_1_0
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
(X₀ : V)
(X₁ : V)
(d₀ : X₀ ⟶ X₁)
(succ' : (t : (X₀ : V) × (X₁ : V) × (X₀ ⟶ X₁)) →
(X₂ : V) ×' (d : t.snd.fst ⟶ X₂) ×' CategoryTheory.CategoryStruct.comp t.snd.snd d = 0)
:
HomologicalComplex.d (CochainComplex.mk' X₀ X₁ d₀ succ') 0 1 = d₀
def
CochainComplex.mkHomAux
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
(P : CochainComplex V ℕ)
(Q : CochainComplex V ℕ)
(zero : HomologicalComplex.X P 0 ⟶ HomologicalComplex.X Q 0)
(one : HomologicalComplex.X P 1 ⟶ HomologicalComplex.X Q 1)
(one_zero_comm : CategoryTheory.CategoryStruct.comp zero (HomologicalComplex.d Q 0 1) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.d P 0 1) one)
(succ : (n : ℕ) →
(p :
(f : HomologicalComplex.X P n ⟶ HomologicalComplex.X Q n) ×'
(f' : HomologicalComplex.X P (n + 1) ⟶ HomologicalComplex.X Q (n + 1)) ×'
CategoryTheory.CategoryStruct.comp f (HomologicalComplex.d Q n (n + 1)) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.d P n (n + 1)) f') →
(f'' : HomologicalComplex.X P (n + 2) ⟶ HomologicalComplex.X Q (n + 2)) ×'
CategoryTheory.CategoryStruct.comp p.snd.fst (HomologicalComplex.d Q (n + 1) (n + 2)) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.d P (n + 1) (n + 2)) f'')
(n : ℕ)
:
(f : HomologicalComplex.X P n ⟶ HomologicalComplex.X Q n) ×'
(f' : HomologicalComplex.X P (n + 1) ⟶ HomologicalComplex.X Q (n + 1)) ×'
CategoryTheory.CategoryStruct.comp f (HomologicalComplex.d Q n (n + 1)) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.d P n (n + 1)) f'
An auxiliary construction for mkHom.
Here we build by induction a family of commutative squares,
but don't require at the type level that these successive commutative squares actually agree.
They do in fact agree, and we then capture that at the type level (i.e. by constructing a chain map)
in mkHom.
Equations
- One or more equations did not get rendered due to their size.
- CochainComplex.mkHomAux P Q zero one one_zero_comm succ 0 = { fst := zero, snd := { fst := one, snd := one_zero_comm } }
Instances For
def
CochainComplex.mkHom
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
(P : CochainComplex V ℕ)
(Q : CochainComplex V ℕ)
(zero : HomologicalComplex.X P 0 ⟶ HomologicalComplex.X Q 0)
(one : HomologicalComplex.X P 1 ⟶ HomologicalComplex.X Q 1)
(one_zero_comm : CategoryTheory.CategoryStruct.comp zero (HomologicalComplex.d Q 0 1) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.d P 0 1) one)
(succ : (n : ℕ) →
(p :
(f : HomologicalComplex.X P n ⟶ HomologicalComplex.X Q n) ×'
(f' : HomologicalComplex.X P (n + 1) ⟶ HomologicalComplex.X Q (n + 1)) ×'
CategoryTheory.CategoryStruct.comp f (HomologicalComplex.d Q n (n + 1)) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.d P n (n + 1)) f') →
(f'' : HomologicalComplex.X P (n + 2) ⟶ HomologicalComplex.X Q (n + 2)) ×'
CategoryTheory.CategoryStruct.comp p.snd.fst (HomologicalComplex.d Q (n + 1) (n + 2)) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.d P (n + 1) (n + 2)) f'')
:
P ⟶ Q
A constructor for chain maps between ℕ-indexed cochain complexes,
working by induction on commutative squares.
You need to provide the components of the chain map in degrees 0 and 1, show that these form a commutative square, and then give a construction of each component, and the fact that it forms a commutative square with the previous component, using as an inductive hypothesis the data (and commutativity) of the previous two components.
Instances For
@[simp]
theorem
CochainComplex.mkHom_f_0
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
(P : CochainComplex V ℕ)
(Q : CochainComplex V ℕ)
(zero : HomologicalComplex.X P 0 ⟶ HomologicalComplex.X Q 0)
(one : HomologicalComplex.X P 1 ⟶ HomologicalComplex.X Q 1)
(one_zero_comm : CategoryTheory.CategoryStruct.comp zero (HomologicalComplex.d Q 0 1) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.d P 0 1) one)
(succ : (n : ℕ) →
(p :
(f : HomologicalComplex.X P n ⟶ HomologicalComplex.X Q n) ×'
(f' : HomologicalComplex.X P (n + 1) ⟶ HomologicalComplex.X Q (n + 1)) ×'
CategoryTheory.CategoryStruct.comp f (HomologicalComplex.d Q n (n + 1)) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.d P n (n + 1)) f') →
(f'' : HomologicalComplex.X P (n + 2) ⟶ HomologicalComplex.X Q (n + 2)) ×'
CategoryTheory.CategoryStruct.comp p.snd.fst (HomologicalComplex.d Q (n + 1) (n + 2)) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.d P (n + 1) (n + 2)) f'')
:
HomologicalComplex.Hom.f (CochainComplex.mkHom P Q zero one one_zero_comm succ) 0 = zero
@[simp]
theorem
CochainComplex.mkHom_f_1
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
(P : CochainComplex V ℕ)
(Q : CochainComplex V ℕ)
(zero : HomologicalComplex.X P 0 ⟶ HomologicalComplex.X Q 0)
(one : HomologicalComplex.X P 1 ⟶ HomologicalComplex.X Q 1)
(one_zero_comm : CategoryTheory.CategoryStruct.comp zero (HomologicalComplex.d Q 0 1) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.d P 0 1) one)
(succ : (n : ℕ) →
(p :
(f : HomologicalComplex.X P n ⟶ HomologicalComplex.X Q n) ×'
(f' : HomologicalComplex.X P (n + 1) ⟶ HomologicalComplex.X Q (n + 1)) ×'
CategoryTheory.CategoryStruct.comp f (HomologicalComplex.d Q n (n + 1)) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.d P n (n + 1)) f') →
(f'' : HomologicalComplex.X P (n + 2) ⟶ HomologicalComplex.X Q (n + 2)) ×'
CategoryTheory.CategoryStruct.comp p.snd.fst (HomologicalComplex.d Q (n + 1) (n + 2)) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.d P (n + 1) (n + 2)) f'')
:
HomologicalComplex.Hom.f (CochainComplex.mkHom P Q zero one one_zero_comm succ) 1 = one
@[simp]
theorem
CochainComplex.mkHom_f_succ_succ
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
(P : CochainComplex V ℕ)
(Q : CochainComplex V ℕ)
(zero : HomologicalComplex.X P 0 ⟶ HomologicalComplex.X Q 0)
(one : HomologicalComplex.X P 1 ⟶ HomologicalComplex.X Q 1)
(one_zero_comm : CategoryTheory.CategoryStruct.comp zero (HomologicalComplex.d Q 0 1) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.d P 0 1) one)
(succ : (n : ℕ) →
(p :
(f : HomologicalComplex.X P n ⟶ HomologicalComplex.X Q n) ×'
(f' : HomologicalComplex.X P (n + 1) ⟶ HomologicalComplex.X Q (n + 1)) ×'
CategoryTheory.CategoryStruct.comp f (HomologicalComplex.d Q n (n + 1)) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.d P n (n + 1)) f') →
(f'' : HomologicalComplex.X P (n + 2) ⟶ HomologicalComplex.X Q (n + 2)) ×'
CategoryTheory.CategoryStruct.comp p.snd.fst (HomologicalComplex.d Q (n + 1) (n + 2)) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.d P (n + 1) (n + 2)) f'')
(n : ℕ)
:
HomologicalComplex.Hom.f (CochainComplex.mkHom P Q zero one one_zero_comm succ) (n + 2) = (succ n
{ fst := HomologicalComplex.Hom.f (CochainComplex.mkHom P Q zero one one_zero_comm succ) n,
snd :=
{ fst := HomologicalComplex.Hom.f (CochainComplex.mkHom P Q zero one one_zero_comm succ) (n + 1),
snd :=
(_ :
CategoryTheory.CategoryStruct.comp
(HomologicalComplex.Hom.f (CochainComplex.mkHom P Q zero one one_zero_comm succ) n)
(HomologicalComplex.d Q n (n + 1)) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.d P n (n + 1))
(HomologicalComplex.Hom.f (CochainComplex.mkHom P Q zero one one_zero_comm succ) (n + 1))) } }).fst