English
Given the Snake Lemma data with exactness and the specified maps, one has π1 z1 = π1 z2 under the stated equalities among the components of the diagram.
Русский
При данных Змеинной леммы с точностью и заданными отображениями выполняется равенство π1 z1 = π1 z2 при указанных равенствах компонентов диаграммы.
LaTeX
$$$\\pi_1 z_1 = \\pi_1 z_2$$$
Lean4
/-- **Snake Lemma**
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 with a (set-theoretic) section `σ`, `g₁` is injective with a
(set-theoretic) retraction `ρ`,
then the map `π₁ ∘ ρ ∘ i₂ ∘ σ ∘ ι₃` is a linear map from `K₃` to `C₁`.
Also see `SnakeLemma.δ'` for a noncomputable version
that does not require an explicit section and retraction.
-/
def δ : K₃ →ₗ[R] C₁ :=
haveI H₁ : ∀ x, f₂ (σ x) = x := congr_fun hσ
haveI H₂ := δ_aux i₂ i₃ f₂ g₁ g₂ hg h₂ σ hσ ρ hρ ι₃ hι₃
{ toFun := fun x ↦ π₁ (ρ (i₂ (σ (ι₃ x))))
map_add' := fun x y ↦ by
rw [← map_add]
exact
eq_of_eq i₁ i₂ f₁ f₂ hf g₁ h₁ ρ hρ ι₃ π₁ hπ₁ (x + y) _ (H₁ _) _ (H₂ _) (σ (ι₃ x) + σ (ι₃ y))
(by simp only [map_add, H₁]) _ (by simp only [map_add, H₂])
map_smul' := fun r x ↦ by
simp only [← map_smul, RingHom.id_apply]
apply
eq_of_eq i₁ i₂ f₁ f₂ hf g₁ h₁ ρ hρ ι₃ π₁ hπ₁ (r • x) _ (H₁ _) _ (H₂ _) (r • σ (ι₃ x))
(by simp only [map_smul, H₁]) _ (by simp only [map_smul, H₂]) }
