Complexes of modules #
We provide some additional API to work with homological complexes in
ModuleCat R.
theorem
ModuleCat.homology_ext
{R : Type v}
[Ring R]
{L : ModuleCat R}
{M : ModuleCat R}
{N : ModuleCat R}
{K : ModuleCat R}
{f : L ⟶ M}
{g : M ⟶ N}
(w : CategoryTheory.CategoryStruct.comp f g = 0)
{h : homology f g w ⟶ K}
{k : homology f g w ⟶ K}
(w : ∀ (x : { x // x ∈ LinearMap.ker g }),
↑h (↑(CategoryTheory.Limits.cokernel.π (imageToKernel f g w)) (↑ModuleCat.toKernelSubobject x)) = ↑k (↑(CategoryTheory.Limits.cokernel.π (imageToKernel f g w)) (↑ModuleCat.toKernelSubobject x)))
:
h = k
To prove that two maps out of a homology group are equal, it suffices to check they are equal on the images of cycles.
@[inline, reducible]
abbrev
ModuleCat.toCycles
{R : Type v}
[Ring R]
{ι : Type u_1}
{c : ComplexShape ι}
{C : HomologicalComplex (ModuleCat R) c}
{i : ι}
(x : { x // x ∈ LinearMap.ker (HomologicalComplex.dFrom C i) })
:
↑(CategoryTheory.Subobject.underlying.obj (HomologicalComplex.cycles C i))
Bundle an element C.X i such that C.dFrom i x = 0 as a term of C.cycles i.
Instances For
theorem
ModuleCat.cycles_ext
{R : Type v}
[Ring R]
{ι : Type u_1}
{c : ComplexShape ι}
{C : HomologicalComplex (ModuleCat R) c}
{i : ι}
{x : ↑(CategoryTheory.Subobject.underlying.obj (HomologicalComplex.cycles C i))}
{y : ↑(CategoryTheory.Subobject.underlying.obj (HomologicalComplex.cycles C i))}
(w : ↑(CategoryTheory.Subobject.arrow (HomologicalComplex.cycles C i)) x = ↑(CategoryTheory.Subobject.arrow (HomologicalComplex.cycles C i)) y)
:
x = y
@[simp]
theorem
ModuleCat.cyclesMap_toCycles
{R : Type v}
[Ring R]
{ι : Type u_1}
{c : ComplexShape ι}
{C : HomologicalComplex (ModuleCat R) c}
{D : HomologicalComplex (ModuleCat R) c}
(f : C ⟶ D)
{i : ι}
(x : { x // x ∈ LinearMap.ker (HomologicalComplex.dFrom C i) })
:
↑(cyclesMap f i) (ModuleCat.toCycles x) = ModuleCat.toCycles
{ val := ↑(HomologicalComplex.Hom.f f i) ↑x,
property := (_ : ↑(HomologicalComplex.Hom.f f i) ↑x ∈ LinearMap.ker (HomologicalComplex.dFrom D i)) }
@[inline, reducible]
abbrev
ModuleCat.toHomology
{R : Type v}
[Ring R]
{ι : Type u_1}
{c : ComplexShape ι}
{C : HomologicalComplex (ModuleCat R) c}
{i : ι}
(x : { x // x ∈ LinearMap.ker (HomologicalComplex.dFrom C i) })
:
↑(HomologicalComplex.homology C i)
Build a term of C.homology i from an element C.X i such that C.d_from i x = 0.
Instances For
theorem
ModuleCat.homology_ext'
{R : Type v}
[Ring R]
{ι : Type u_1}
{c : ComplexShape ι}
{C : HomologicalComplex (ModuleCat R) c}
{M : ModuleCat R}
(i : ι)
{h : HomologicalComplex.homology C i ⟶ M}
{k : HomologicalComplex.homology C i ⟶ M}
(w : ∀ (x : { x // x ∈ LinearMap.ker (HomologicalComplex.dFrom C i) }),
↑h (ModuleCat.toHomology x) = ↑k (ModuleCat.toHomology x))
:
h = k