exact_and_mono_f_iff_f_is_kernel — Mathlib

English

In an abelian setting, S has exactness with f mono if and only if the kernel condition holds, i.e., IsLimit(KernelFork.ofι S.f ⋯) exists.

Русский

В абелевой среде существует эквивалентность между точностью S с моно f и существованием предела ядра для короткого комплекса.

LaTeX

$$$S.Exact \land Mono(S.f) \iff \exists\, IsLimit(KernelFork.ofι\; S.f\; \cdots)$$$

Lean4

theorem exact_and_mono_f_iff_f_is_kernel [S.HasHomology] :
    S.Exact ∧ Mono S.f ↔ Nonempty (IsLimit (KernelFork.ofι S.f S.zero)) :=
  by
  constructor
  · intro ⟨hS, _⟩
    exact ⟨hS.fIsKernel⟩
  · intro ⟨hS⟩
    exact ⟨S.exact_of_f_is_kernel hS, mono_of_isLimit_fork hS⟩

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