instMonoFNatι

Mathlib.CategoryTheory.Preadditive.Injective.Resolution

URI: https://scilib.ai/kg/mathlib#CategoryTheory.InjectiveResolution.instMonoFNatι

English

In an injective resolution I of Z, every component map I.ι.f n is a monomorphism.

Русский

В разрешении I объекта Z каждый компонент I.ι.f n является моно morphism.

LaTeX

$$$\forall n:\mathbb{N},\; Mono(I.ι.f\,n)$$$

Lean4

instance (n : ℕ) : Mono (I.ι.f n) := by
  cases n
  · exact mono_of_isLimit_fork I.isLimitKernelFork
  · rw [ι_f_succ]; infer_instance

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

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

Разделы

Аффилиация

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