isoModSerre_isInvertedBy_iff — Mathlib

English

Under finite limits/colimits preservation, isoModSerre.IsInvertedBy F is equivalent to P ≤ F.kernel.

Русский

При сохранении пределов и сопряжений из диапазона, isoModSerre.IsInvertedBy F эквивалентно P ≤ kernel(F).

LaTeX

$$$P.isoModSerre.IsInvertedBy(F) \iff P \le F.kernel$$

Lean4

theorem isoModSerre_isInvertedBy_iff (F : C ⥤ D) [PreservesFiniteLimits F] [PreservesFiniteColimits F] :
    P.isoModSerre.IsInvertedBy F ↔ P ≤ F.kernel :=
  by
  refine ⟨P.le_kernel_of_isoModSerre_isInvertedBy F, fun hF X Y f ⟨h₁, h₂⟩ ↦ ?_⟩
  have : Mono (F.map f) :=
    (((ShortComplex.mk _ _ (kernel.condition f)).exact_of_f_is_kernel (kernelIsKernel f)).map F).mono_g
      (((hF _ h₁).eq_of_src _ _))
  have : Epi (F.map f) :=
    (((ShortComplex.mk _ _ (cokernel.condition f)).exact_of_g_is_cokernel (cokernelIsCokernel f)).map F).epi_f
      (((hF _ h₂).eq_of_tgt _ _))
  exact isIso_of_mono_of_epi (F.map f)

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