smulShortComplex

Mathlib.RingTheory.Regular.Category

URI: https://scilib.ai/kg/mathlib#ModuleCat.smulShortComplex

Lean4

/-- The short (exact) complex `M → M → M⧸xM` obtain from the scalar multiple of `x : R` on `M`. -/
@[simps]
def smulShortComplex (r : R) : ShortComplex (ModuleCat R)
    where
  X₁ := M
  X₂ := M
  X₃ := ModuleCat.of R (QuotSMulTop r M)
  f := ModuleCat.ofHom (r • LinearMap.id)
  g := ModuleCat.ofHom (r • (⊤ : Submodule R M)).mkQ
  zero := by
    ext x
    exact (LinearMap.exact_smul_id_smul_top_mkQ M r).apply_apply_eq_zero x

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru