mem_homologicalKernel_trW_iff — Mathlib

English

Exactness of a δ-construction in a sequence of shifted triangles.

Русский

Точность конструирования δ в последовательности сдвинутых треугольников.

LaTeX

$$$\text{Exact}_{δ_0}$$$

Lean4

theorem mem_homologicalKernel_trW_iff {X Y : C} (f : X ⟶ Y) :
    F.homologicalKernel.trW f ↔ ∀ (n : ℤ), IsIso ((F.shift n).map f) :=
  by
  obtain ⟨Z, g, h, hT⟩ := distinguished_cocone_triangle f
  apply (F.homologicalKernel.trW_iff_of_distinguished _ hT).trans
  have h₁ := fun n => (F.homologySequence_exact₃ _ hT n _ rfl).isZero_X₂_iff
  have h₂ := fun n => F.homologySequence_mono_shift_map_mor₁_iff _ hT n _ rfl
  have h₃ := fun n => F.homologySequence_epi_shift_map_mor₁_iff _ hT n
  dsimp at h₁ h₂ h₃ ⊢
  simp only [mem_homologicalKernel_iff, h₁, ← h₂, ← h₃]
  constructor
  · intro h n
    obtain ⟨m, rfl⟩ : ∃ (m : ℤ), n = m + 1 := ⟨n - 1, by simp⟩
    have := (h (m + 1)).1
    have := (h m).2
    apply isIso_of_mono_of_epi
  · intros
    constructor <;> infer_instance

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