English
Construction producing a short complex in the module category from two linear maps f,g with g∘f = 0.
Русский
Конструкция порождает короткий комплекс в категории модулей из двух линейных отображений f,g с условием g ∘ f = 0.
LaTeX
$$$\\text{ShortComplex}(\\mathrm{ModuleCat}\\, R)$ exists with$ f:X_1\\to X_2$, $g:X_2\\to X_3$ and $g\\circ f=0$$$
Lean4
/-- Constructor for short complexes in `ModuleCat.{v} R` taking as inputs
linear maps `f` and `g` and the vanishing of their composition. -/
@[simps]
def moduleCatMk {X₁ X₂ X₃ : Type v} [AddCommGroup X₁] [AddCommGroup X₂] [AddCommGroup X₃] [Module R X₁] [Module R X₂]
[Module R X₃] (f : X₁ →ₗ[R] X₂) (g : X₂ →ₗ[R] X₃) (hfg : g.comp f = 0) : ShortComplex (ModuleCat.{v} R) :=
ShortComplex.mk (ModuleCat.ofHom f) (ModuleCat.ofHom g) (ModuleCat.hom_ext hfg)
