exact₂_iff — Mathlib

English

If S is a ComposableArrows C 2, w: Eq (comp (S.map' 0 1) (S.map' 1 2)) 0, and h: (ShortComplex.mk _ _ w).Exact, then S.Exact.

Русский

Если S — композиционные стрелки C2, w: равенство, и h: ShortComplex.mk с w точен, то S точен.

LaTeX

$$$(S:\mathrm{ComposableArrows}(C,2)) \Rightarrow (w: \mathrm{Eq}(\mathrm{comp}(S.map' 0 1, S.map' 1 2)) 0) \rightarrow (h: (\mathrm{ShortComplex.mk} \; \_ \; \_ \; w).\mathrm{Exact}) \Rightarrow S.\mathrm{Exact}$$$

Lean4

theorem exact₂_iff (S : ComposableArrows C 2) (hS : S.IsComplex) : S.Exact ↔ (S.sc' hS 0 1 2).Exact :=
  by
  constructor
  · intro h
    exact h.exact 0 (by cutsat)
  · intro h
    refine Exact.mk hS (fun i hi => ?_)
    obtain rfl : i = 0 := by cutsat
    exact h

Похожие утверждения