Lean4
/-- The "snake input" which gives the exact sequence
`0 ⟶ ker f ⟶ ker (f ≫ g) ⟶ ker g ⟶ coker f ⟶ coker (f ≫ g) ⟶ coker g ⟶ 0`,
see `kernelCokernelCompSequence_exact`. -/
@[simps]
noncomputable def snakeInput : ShortComplex.SnakeInput C
where
L₀ :=
{ f := kernel.map f (f ≫ g) (𝟙 _) g (by simp)
g := kernel.map (f ≫ g) g f (𝟙 _) (by simp)
zero := by aesop }
L₁ := ShortComplex.mk (biprod.inl : X ⟶ _) (biprod.snd : _ ⟶ Y) (by simp)
L₂ := ShortComplex.mk (biprod.inl : Y ⟶ _) (biprod.snd : _ ⟶ Z) (by simp)
L₃ :=
{ f := cokernel.map f (f ≫ g) (𝟙 _) g (by simp)
g := cokernel.map (f ≫ g) g f (𝟙 _) (by simp)
zero := by aesop }
v₀₁ :=
{ τ₁ := kernel.ι f
τ₂ := ι f g
τ₃ := kernel.ι g }
v₁₂ :=
{ τ₁ := f
τ₂ := φ f g
τ₃ := g }
v₂₃ :=
{ τ₁ := cokernel.π f
τ₂ := π f g
τ₃ := cokernel.π g }
h₀ := by
apply ShortComplex.isLimitOfIsLimitπ <;> apply (KernelFork.isLimitMapConeEquiv _ _).2
· exact kernelIsKernel _
· exact isLimit f g
· exact kernelIsKernel _
h₃ := by
apply ShortComplex.isColimitOfIsColimitπ <;> apply (CokernelCofork.isColimitMapCoconeEquiv _ _).2
· exact cokernelIsCokernel _
· exact isColimit f g
· exact cokernelIsCokernel _
epi_L₁_g := by dsimp; infer_instance
mono_L₂_f := by dsimp; infer_instance
L₁_exact := (ShortComplex.Splitting.ofHasBinaryBiproduct X Y).exact
L₂_exact := (ShortComplex.Splitting.ofHasBinaryBiproduct Y Z).exact
