Homology of complexes in concrete categories #
The homology of short complexes in concrete categories was studied in
Mathlib.Algebra.Homology.ShortComplex.ConcreteCategory. In this file,
we introduce specific definitions and lemmas for the homology
of homological complexes in concrete categories. In particular,
we give a computation of the connecting homomorphism of
the homology sequence in terms of (co)cycles.
noncomputable def
HomologicalComplex.cyclesMk
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ConcreteCategory C]
[CategoryTheory.HasForget₂ C Ab]
[CategoryTheory.Abelian C]
[CategoryTheory.Functor.Additive (CategoryTheory.forget₂ C Ab)]
[CategoryTheory.Functor.PreservesHomology (CategoryTheory.forget₂ C Ab)]
{ι : Type u_1}
{c : ComplexShape ι}
(K : HomologicalComplex C c)
{i : ι}
(x : ↑((CategoryTheory.forget₂ C Ab).toPrefunctor.obj (K.X i)))
(j : ι)
(hj : ComplexShape.next c i = j)
(hx : ((CategoryTheory.forget₂ C Ab).toPrefunctor.map (K.d i j)) x = 0)
:
↑((CategoryTheory.forget₂ C Ab).toPrefunctor.obj (HomologicalComplex.cycles K i))
Constructor for cycles of a homological complex in a concrete category.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
HomologicalComplex.i_cyclesMk
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ConcreteCategory C]
[CategoryTheory.HasForget₂ C Ab]
[CategoryTheory.Abelian C]
[CategoryTheory.Functor.Additive (CategoryTheory.forget₂ C Ab)]
[CategoryTheory.Functor.PreservesHomology (CategoryTheory.forget₂ C Ab)]
{ι : Type u_1}
{c : ComplexShape ι}
(K : HomologicalComplex C c)
{i : ι}
(x : ↑((CategoryTheory.forget₂ C Ab).toPrefunctor.obj (K.X i)))
(j : ι)
(hj : ComplexShape.next c i = j)
(hx : ((CategoryTheory.forget₂ C Ab).toPrefunctor.map (K.d i j)) x = 0)
:
((CategoryTheory.forget₂ C Ab).toPrefunctor.map (HomologicalComplex.iCycles K i))
(HomologicalComplex.cyclesMk K x j hj hx) = x
theorem
CategoryTheory.ShortComplex.ShortExact.δ_apply'
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ConcreteCategory C]
[CategoryTheory.HasForget₂ C Ab]
[CategoryTheory.Abelian C]
[CategoryTheory.Functor.Additive (CategoryTheory.forget₂ C Ab)]
[CategoryTheory.Functor.PreservesHomology (CategoryTheory.forget₂ C Ab)]
{ι : Type u_1}
{c : ComplexShape ι}
{S : CategoryTheory.ShortComplex (HomologicalComplex C c)}
(hS : CategoryTheory.ShortComplex.ShortExact S)
(i : ι)
(j : ι)
(hij : c.Rel i j)
(x₃ : ↑((CategoryTheory.forget₂ C Ab).toPrefunctor.obj (HomologicalComplex.homology S.X₃ i)))
(x₂ : ↑((CategoryTheory.forget₂ C Ab).toPrefunctor.obj (HomologicalComplex.opcycles S.X₂ i)))
(x₁ : ↑((CategoryTheory.forget₂ C Ab).toPrefunctor.obj (HomologicalComplex.cycles S.X₁ j)))
(h₂ : ((CategoryTheory.forget₂ C Ab).toPrefunctor.map (HomologicalComplex.opcyclesMap S.g i)) x₂ = ((CategoryTheory.forget₂ C Ab).toPrefunctor.map (HomologicalComplex.homologyι S.X₃ i)) x₃)
(h₁ : ((CategoryTheory.forget₂ C Ab).toPrefunctor.map (HomologicalComplex.cyclesMap S.f j)) x₁ = ((CategoryTheory.forget₂ C Ab).toPrefunctor.map (HomologicalComplex.opcyclesToCycles S.X₂ i j)) x₂)
:
((CategoryTheory.forget₂ C Ab).toPrefunctor.map (CategoryTheory.ShortComplex.ShortExact.δ hS i j hij)) x₃ = ((CategoryTheory.forget₂ C Ab).toPrefunctor.map (HomologicalComplex.homologyπ S.X₁ j)) x₁
theorem
CategoryTheory.ShortComplex.ShortExact.δ_apply
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ConcreteCategory C]
[CategoryTheory.HasForget₂ C Ab]
[CategoryTheory.Abelian C]
[CategoryTheory.Functor.Additive (CategoryTheory.forget₂ C Ab)]
[CategoryTheory.Functor.PreservesHomology (CategoryTheory.forget₂ C Ab)]
{ι : Type u_1}
{c : ComplexShape ι}
{S : CategoryTheory.ShortComplex (HomologicalComplex C c)}
(hS : CategoryTheory.ShortComplex.ShortExact S)
(i : ι)
(j : ι)
(hij : c.Rel i j)
(x₃ : ↑((CategoryTheory.forget₂ C Ab).toPrefunctor.obj (S.X₃.X i)))
(hx₃ : ((CategoryTheory.forget₂ C Ab).toPrefunctor.map (S.X₃.d i j)) x₃ = 0)
(x₂ : ↑((CategoryTheory.forget₂ C Ab).toPrefunctor.obj (S.X₂.X i)))
(hx₂ : ((CategoryTheory.forget₂ C Ab).toPrefunctor.map (S.g.f i)) x₂ = x₃)
(x₁ : ↑((CategoryTheory.forget₂ C Ab).toPrefunctor.obj (S.X₁.X j)))
(hx₁ : ((CategoryTheory.forget₂ C Ab).toPrefunctor.map (S.f.f j)) x₁ = ((CategoryTheory.forget₂ C Ab).toPrefunctor.map (S.X₂.d i j)) x₂)
(k : ι)
(hk : ComplexShape.next c j = k)
:
((CategoryTheory.forget₂ C Ab).toPrefunctor.map (CategoryTheory.ShortComplex.ShortExact.δ hS i j hij))
(((CategoryTheory.forget₂ C Ab).toPrefunctor.map (HomologicalComplex.homologyπ S.X₃ i))
(HomologicalComplex.cyclesMk S.X₃ x₃ j (_ : ComplexShape.next c i = j) hx₃)) = ((CategoryTheory.forget₂ C Ab).toPrefunctor.map (HomologicalComplex.homologyπ S.X₁ j))
(HomologicalComplex.cyclesMk S.X₁ x₁ k hk
(_ : ((CategoryTheory.forget₂ C Ab).toPrefunctor.map (S.X₁.d j k)) x₁ = 0))