Weak exactness in finite matrix additive hulls #
Exactness against every singleton source (respectively singleton target)
extends rowwise (respectively columnwise) to a weak kernel (respectively
weak cokernel) in Mat_ C. These lemmas isolate the finite-matrix transport
used by the abstract word-mesh category.
theorem
QuotientSubmoduleEquidistribution.Iyama.mat_isWeakKernel_of_exact_embedding
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
(S : CategoryTheory.ShortComplex (CategoryTheory.Mat_ C))
(hS :
∀ (X : C),
Function.Exact
(fun (l : (CategoryTheory.Mat_.embedding C).obj X ⟶ S.X₁) => CategoryTheory.CategoryStruct.comp l S.f)
fun (k : (CategoryTheory.Mat_.embedding C).obj X ⟶ S.X₂) => CategoryTheory.CategoryStruct.comp k S.g)
:
Exactness of a matrix short complex against every singleton source is enough to make its first map a weak kernel of its second map.
theorem
QuotientSubmoduleEquidistribution.Iyama.mat_isWeakCokernel_of_exact_embedding
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
(S : CategoryTheory.ShortComplex (CategoryTheory.Mat_ C))
(hS :
∀ (X : C),
Function.Exact
(fun (l : S.X₃ ⟶ (CategoryTheory.Mat_.embedding C).obj X) => CategoryTheory.CategoryStruct.comp S.g l)
fun (k : S.X₂ ⟶ (CategoryTheory.Mat_.embedding C).obj X) => CategoryTheory.CategoryStruct.comp S.f k)
:
Exactness of a matrix short complex against every singleton target is enough to make its second map a weak cokernel of its first map.