English
A completeDistinguishedTriangleMorphism provides a morphism of distinguished triangles with specified commutativity data.
Русский
completeDistinguishedTriangleMorphism задаёт морфизм между распознаваемыми треугольниками с заданными данными коммутативности.
LaTeX
$$$\\text{Definition: completeDistinguishedTriangleMorphism}$$$
Lean4
/-- A product of distinguished triangles is distinguished -/
theorem productTriangle_distinguished {J : Type*} (T : J → Triangle C) (hT : ∀ j, T j ∈ distTriang C)
[HasProduct (fun j => (T j).obj₁)] [HasProduct (fun j => (T j).obj₂)] [HasProduct (fun j => (T j).obj₃)]
[HasProduct (fun j => (T j).obj₁⟦(1 : ℤ)⟧)] : productTriangle T ∈ distTriang C := by
/- The proof proceeds by constructing a morphism of triangles
`φ' : T' ⟶ productTriangle T` with `T'` distinguished, and such that
`φ'.hom₁` and `φ'.hom₂` are identities. Then, it suffices to show that
`φ'.hom₃` is an isomorphism, which is achieved by using Yoneda's lemma
and diagram chases. -/
let f₁ := Limits.Pi.map (fun j => (T j).mor₁)
obtain ⟨Z, f₂, f₃, hT'⟩ := distinguished_cocone_triangle f₁
let T' := Triangle.mk f₁ f₂ f₃
change T' ∈ distTriang C at hT'
let φ : ∀ j, T' ⟶ T j := fun j =>
completeDistinguishedTriangleMorphism _ _ hT' (hT j) (Pi.π _ j) (Pi.π _ j) (by simp [f₁, T'])
let φ' := productTriangle.lift _ φ
have h₁ : φ'.hom₁ = 𝟙 _ := by cat_disch
have h₂ : φ'.hom₂ = 𝟙 _ := by cat_disch
have : IsIso φ'.hom₁ := by rw [h₁]; infer_instance
have : IsIso φ'.hom₂ := by rw [h₂]; infer_instance
suffices IsIso φ'.hom₃
by
have : IsIso φ' := by
apply Triangle.isIso_of_isIsos
all_goals infer_instance
exact isomorphic_distinguished _ hT' _ (asIso φ').symm
refine
isIso_of_yoneda_map_bijective _
(fun A => ⟨?_, ?_⟩)
/- the proofs by diagram chase start here -/
· suffices Mono φ'.hom₃ by
intro a₁ a₂ ha
simpa only [← cancel_mono φ'.hom₃] using ha
rw [mono_iff_cancel_zero]
intro A f hf
have hf' : f ≫ T'.mor₃ = 0 := by
rw [← cancel_mono (φ'.hom₁⟦1⟧'), zero_comp, assoc, φ'.comm₃, reassoc_of% hf, zero_comp]
obtain ⟨g, hg⟩ := T'.coyoneda_exact₃ hT' f hf'
have hg' : ∀ j, (g ≫ Pi.π _ j) ≫ (T j).mor₂ = 0 := fun j =>
by
have : g ≫ T'.mor₂ ≫ φ'.hom₃ ≫ Pi.π _ j = 0 := by rw [← reassoc_of% hg, reassoc_of% hf, zero_comp]
rw [φ'.comm₂_assoc, h₂, id_comp] at this
simpa using this
have hg'' := fun j => (T j).coyoneda_exact₂ (hT j) _ (hg' j)
let α := fun j => (hg'' j).choose
have hα : ∀ j, _ = α j ≫ _ := fun j => (hg'' j).choose_spec
have hg''' : g = Pi.lift α ≫ T'.mor₁ := by dsimp [f₁, T']; ext j; rw [hα]; simp
rw [hg, hg''', assoc, comp_distTriang_mor_zero₁₂ _ hT', comp_zero]
· intro a
obtain ⟨a', ha'⟩ : ∃ (a' : A ⟶ Z), a' ≫ T'.mor₃ = a ≫ (productTriangle T).mor₃ :=
by
have zero : ((productTriangle T).mor₃) ≫ (shiftFunctor C 1).map T'.mor₁ = 0 :=
by
rw [← cancel_mono (φ'.hom₂⟦1⟧'), zero_comp, assoc, ← Functor.map_comp, φ'.comm₁, h₁, id_comp,
productTriangle.zero₃₁]
intro j
exact comp_distTriang_mor_zero₃₁ _ (hT j)
have ⟨g, hg⟩ := T'.coyoneda_exact₁ hT' (a ≫ (productTriangle T).mor₃) (by rw [assoc, zero, comp_zero])
exact ⟨g, hg.symm⟩
have ha'' := fun (j : J) =>
(T j).coyoneda_exact₃ (hT j) ((a - a' ≫ φ'.hom₃) ≫ Pi.π _ j)
(by
simp only [sub_comp, assoc]
erw [← (productTriangle.π T j).comm₃]
rw [← φ'.comm₃_assoc]
rw [reassoc_of% ha', sub_eq_zero, h₁, Functor.map_id, id_comp])
let b := fun j => (ha'' j).choose
have hb : ∀ j, _ = b j ≫ _ := fun j => (ha'' j).choose_spec
have hb' : a - a' ≫ φ'.hom₃ = Pi.lift b ≫ (productTriangle T).mor₂ :=
Limits.Pi.hom_ext _ _ (fun j => by rw [hb]; simp)
have : (a' + (by exact Pi.lift b) ≫ T'.mor₂) ≫ φ'.hom₃ = a := by
rw [add_comp, assoc, φ'.comm₂, h₂, id_comp, ← hb', add_sub_cancel]
exact ⟨_, this⟩
