English
Under the Snake Lemma hypotheses, the map δ: K3 → C1 is given by δ(x) = π1(ρ(i2(σ(ι3(x))))) and is linear.
Русский
При предположениях Змеинной леммы отображение δ: K3 → C1 задаётся δ(x) = π1(ρ(i2(σ(ι3(x))))) и является линейным.
LaTeX
$$$\\delta = \\pi_1 \\circ \\rho \\circ i_2 \\circ \\sigma \\circ \\iota_3 \;\\in\\; \\mathrm{Hom}(K_3, C_1)$$$
Lean4
theorem eq_of_eq (x : K₃) (y₁) (hy₁ : f₂ y₁ = ι₃ x) (z₁) (hz₁ : g₁ z₁ = i₂ y₁) (y₂) (hy₂ : f₂ y₂ = ι₃ x) (z₂)
(hz₂ : g₁ z₂ = i₂ y₂) : π₁ z₁ = π₁ z₂ :=
by
have := sub_eq_zero.mpr (hy₁.trans hy₂.symm)
rw [← map_sub, hf] at this
obtain ⟨d, hd⟩ := this
rw [← eq_sub_iff_add_eq.mp hd, map_add, ← hz₂, ← sub_eq_iff_eq_add, ← map_sub, ← i₂.comp_apply, ← h₁,
LinearMap.comp_apply, (HasLeftInverse.injective ⟨ρ, congr_fun hρ⟩).eq_iff] at hz₁
rw [← sub_eq_zero, ← map_sub, hz₁, hπ₁]
exact ⟨_, rfl⟩
