Lean4
/-- Given a short exact short complex `S : HomologicalComplex C c`, and degrees `i` and `j`
such that `c.Rel i j`, this is the snake diagram whose four lines are respectively
obtained by applying the functors `homologyFunctor C c i`, `opcyclesFunctor C c i`,
`cyclesFunctor C c j`, `homologyFunctor C c j` to `S`. Applying the snake lemma to this
gives the homology sequence of `S`. -/
@[simps]
noncomputable def snakeInput (hS : S.ShortExact) (i j : ι) (hij : c.Rel i j) : ShortComplex.SnakeInput C
where
L₀ := (homologyFunctor C c i).mapShortComplex.obj S
L₁ := (opcyclesFunctor C c i).mapShortComplex.obj S
L₂ := (cyclesFunctor C c j).mapShortComplex.obj S
L₃ := (homologyFunctor C c j).mapShortComplex.obj S
v₀₁ := S.mapNatTrans (natTransHomologyι C c i)
v₁₂ := S.mapNatTrans (natTransOpCyclesToCycles C c i j)
v₂₃ := S.mapNatTrans (natTransHomologyπ C c j)
h₀ := by
apply ShortComplex.isLimitOfIsLimitπ
all_goals exact (KernelFork.isLimitMapConeEquiv _ _).symm ((composableArrows₃_exact _ i j hij).exact 0).fIsKernel
h₃ := by
apply ShortComplex.isColimitOfIsColimitπ
all_goals
exact (CokernelCofork.isColimitMapCoconeEquiv _ _).symm ((composableArrows₃_exact _ i j hij).exact 1).gIsCokernel
L₁_exact := by
have := hS.epi_g
exact opcycles_right_exact S hS.exact i
L₂_exact := by
have := hS.mono_f
exact cycles_left_exact S hS.exact j
epi_L₁_g := by
have := hS.epi_g
dsimp
infer_instance
mono_L₂_f := by
have := hS.mono_f
dsimp
infer_instance
