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 : ↥(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 : ↥(LinearMap.ker (HomologicalComplex.dFrom C i)))
:
↑(CategoryTheory.Subobject.underlying.toPrefunctor.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.
Equations
- ModuleCat.toCycles' x = ModuleCat.toKernelSubobject x
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.toPrefunctor.obj (HomologicalComplex.cycles' C i))}
{y : ↑(CategoryTheory.Subobject.underlying.toPrefunctor.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.cycles'Map_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 : ↥(LinearMap.ker (HomologicalComplex.dFrom C i)))
:
(cycles'Map f i) (ModuleCat.toCycles' x) = ModuleCat.toCycles' { val := (f.f i) ↑x, property := (_ : (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 : ↥(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.
Equations
- One or more equations did not get rendered due to their size.
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 : ↥(LinearMap.ker (HomologicalComplex.dFrom C i))), h (ModuleCat.toHomology' x) = k (ModuleCat.toHomology' x))
:
h = k