mono_L₀_f

Mathlib.Algebra.Homology.ShortComplex.SnakeLemma

URI: https://scilib.ai/kg/mathlib#CategoryTheory.ShortComplex.SnakeInput.mono_L₀_f

← MathLib Explorer

English

If S.L1.f is mono, then S.L0.f is mono under the snake input structure.

Русский

Если S.L1.f моно, то S.L0.f также моно в структуре входа змейки.

LaTeX

$$$Mono(S.L_0.f)$$$

Lean4

instance mono_L₀_f [Mono S.L₁.f] : Mono S.L₀.f :=
  by
  have : Mono (S.L₀.f ≫ S.v₀₁.τ₂) := by
    rw [← S.v₀₁.comm₁₂]
    apply mono_comp
  exact mono_of_mono _ S.v₀₁.τ₂

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

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

Разделы

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

Аффилиация

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