English
IsIso φ.hom₂ and hT, hT' imply something about φ.hom₃
Русский
Изоморфизм φ.hom₂ и условия hT, hT' дают свойство φ.hom₃
LaTeX
$$$\\forall T,T' \\in \\mathrm{distTriang} \\, C, (\\phi : T \\to T') \\;\\Rightarrow \\mathrm{IsIso}(\\phi.hom_2) \\Rightarrow \\mathrm{IsIso}(\\phi.hom_3)$$$
Lean4
theorem isIso₂_of_isIso₁₃ {T T' : Triangle C} (φ : T ⟶ T') (hT : T ∈ distTriang C) (hT' : T' ∈ distTriang C)
(h₁ : IsIso φ.hom₁) (h₃ : IsIso φ.hom₃) : IsIso φ.hom₂ :=
by
have : Mono φ.hom₂ := by
rw [mono_iff_cancel_zero]
intro A f hf
obtain ⟨g, rfl⟩ :=
Triangle.coyoneda_exact₂ _ hT f
(by rw [← cancel_mono φ.hom₃, assoc, φ.comm₂, reassoc_of% hf, zero_comp, zero_comp])
rw [assoc] at hf
obtain ⟨h, hh⟩ :=
Triangle.coyoneda_exact₂ T'.invRotate (inv_rot_of_distTriang _ hT') (g ≫ φ.hom₁)
(by dsimp; rw [assoc, ← φ.comm₁, hf])
obtain ⟨k, rfl⟩ : ∃ (k : A ⟶ T.invRotate.obj₁), k ≫ T.invRotate.mor₁ = g :=
by
refine ⟨h ≫ inv (φ.hom₃⟦(-1 : ℤ)⟧'), ?_⟩
have eq := ((invRotate C).map φ).comm₁
dsimp only [invRotate] at eq
rw [← cancel_mono φ.hom₁, assoc, assoc, eq, IsIso.inv_hom_id_assoc, hh]
erw [assoc, comp_distTriang_mor_zero₁₂ _ (inv_rot_of_distTriang _ hT), comp_zero]
refine isIso_of_yoneda_map_bijective _ (fun A => ⟨?_, ?_⟩)
· intro f₁ f₂ h
simpa only [← cancel_mono φ.hom₂] using h
· intro y₂
obtain ⟨x₃, hx₃⟩ : ∃ (x₃ : A ⟶ T.obj₃), x₃ ≫ φ.hom₃ = y₂ ≫ T'.mor₂ := ⟨y₂ ≫ T'.mor₂ ≫ inv φ.hom₃, by simp⟩
obtain ⟨x₂, hx₂⟩ :=
Triangle.coyoneda_exact₃ _ hT x₃
(by
rw [← cancel_mono (φ.hom₁⟦(1 : ℤ)⟧'), assoc, zero_comp, φ.comm₃, reassoc_of% hx₃,
comp_distTriang_mor_zero₂₃ _ hT', comp_zero])
obtain ⟨y₁, hy₁⟩ :=
Triangle.coyoneda_exact₂ _ hT' (y₂ - x₂ ≫ φ.hom₂)
(by rw [sub_comp, assoc, ← φ.comm₂, ← reassoc_of% hx₂, hx₃, sub_self])
obtain ⟨x₁, hx₁⟩ : ∃ (x₁ : A ⟶ T.obj₁), x₁ ≫ φ.hom₁ = y₁ := ⟨y₁ ≫ inv φ.hom₁, by simp⟩
refine ⟨x₂ + x₁ ≫ T.mor₁, ?_⟩
dsimp
rw [add_comp, assoc, φ.comm₁, reassoc_of% hx₁, ← hy₁, add_sub_cancel]
