isColimitEquivIsColimitCokernelCofork

English

For a CauSeq with an absolute value on a field with a linear order, if the sequence is positive, then it cannot converge to zero in the limit sense.

Русский

Для Cau-последовательности с абсолютной величиной над полем с линейным порядком, если последовательность положительная, то она не сходится к нулю в пределе.

LaTeX

$$$ \forall \ f: CauSeq\; \alpha\; abs,\; Pos\, f \Rightarrow \lnot LimZero\, f. $$$

Lean4

/-- A commutative square in a preadditive category is a pushout square iff
the corresponding diagram `X₁ ⟶ X₂ ⊞ X₃ ⟶ X₄ ⟶ 0` makes `X₄` a cokernel. -/
noncomputable def isColimitEquivIsColimitCokernelCofork (sq : CommSq f g inl inr) :
    IsColimit (PushoutCocone.mk _ _ sq.w) ≃ IsColimit sq.cokernelCofork
    where
  toFun
    h :=
    Cofork.IsColimit.mk _
      (fun s ↦
        PushoutCocone.IsColimit.desc h (biprod.inl ≫ s.π) (biprod.inr ≫ s.π)
          (by
            rw [← sub_eq_zero, ← assoc, ← assoc, ← Preadditive.sub_comp]
            convert s.condition <;> cat_disch))
      (fun s ↦ by
        dsimp
        ext
        · simp only [biprod.inl_desc_assoc]
          apply PushoutCocone.IsColimit.inl_desc h
        · simp only [biprod.inr_desc_assoc]
          apply PushoutCocone.IsColimit.inr_desc h)
      (fun s m hm ↦ by
        apply PushoutCocone.IsColimit.hom_ext h
        · replace hm := biprod.inl ≫= hm
          dsimp at hm ⊢
          simp only [biprod.inl_desc_assoc] at hm
          rw [hm]
          symm
          apply PushoutCocone.IsColimit.inl_desc h
        · replace hm := biprod.inr ≫= hm
          dsimp at hm ⊢
          simp only [biprod.inr_desc_assoc] at hm
          rw [hm]
          symm
          apply PushoutCocone.IsColimit.inr_desc h)
  invFun
    h :=
    PushoutCocone.IsColimit.mk _ (fun s ↦ h.desc (CokernelCofork.ofπ (biprod.desc s.inl s.inr) (by simp [s.condition])))
      (fun s ↦ by
        simpa using biprod.inl ≫= h.fac (CokernelCofork.ofπ (biprod.desc s.inl s.inr) (by simp [s.condition])) .one)
      (fun s ↦ by
        simpa using biprod.inr ≫= h.fac (CokernelCofork.ofπ (biprod.desc s.inl s.inr) (by simp [s.condition])) .one)
      (fun s m hm₁ hm₂ ↦ by
        apply Cofork.IsColimit.hom_ext h
        convert (h.fac (CokernelCofork.ofπ (biprod.desc s.inl s.inr) (by simp [s.condition])) .one).symm
        cat_disch)
  left_inv _ := Subsingleton.elim _ _
  right_inv _ := Subsingleton.elim _ _

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