English
The computable version δ' agrees with the abstract δ on x: for x ∈ K3, and y, z with f2(y) = ι3(x) and g1(z) = i2(y), the value of δ' at x equals the value of δ at x, and equals π1(z).
Русский
Выражение δ' совмещается с абстрактной δ на элементе x: для x ∈ K3 и y, z с f2(y) = ι3(x) и g1(z) = i2(y), значение δ' при x совпадает со значением δ при x и равно π1(z).
LaTeX
$$$\forall x\in K_3\,\forall y\in M_2\,\forall z\in N_1\; (f_2(y)=\iota_3(x)\land g_1(z)=i_2(y))\Rightarrow \delta'(x)=\pi_1(z).$$$
Lean4
/-- Suppose we have an exact commutative diagram
```
K₃
|
ι₃
↓
M₁ -f₁→ M₂ -f₂→ M₃
| | |
i₁ i₂ i₃
↓ ↓ ↓
N₁ -g₁→ N₂ -g₂→ N₃
|
π₁
↓
C₁
```
such that `f₂` is surjective and `g₁` is injective,
then this is the linear map `K₃ → C₁` given by the snake lemma.
Also see `SnakeLemma.δ` for a computable version.
-/
noncomputable def δ' (hf₂ : Surjective f₂) (hg₁ : Injective g₁) : K₃ →ₗ[R] C₁ :=
δ i₁ i₂ i₃ f₁ f₂ hf g₁ g₂ hg h₁ h₂ _ (funext (surjInv_eq hf₂)) _ (invFun_comp hg₁) ι₃ hι₃ π₁ hπ₁
