mk_surjective — Mathlib

English

Analogous surjectivity for CostructuredArrowDownwards: f is mk w g X1 a b comm for some X1, a, b, comm.

Русский

Аналогичная сюръективность для CostructuredArrowDownwards: f = mk w g X1 a b comm для некоторых X1, a, b, comm.

LaTeX

$$$\exists X_1, a, b, comm\; (f = \mathrm{mk}\ w\ g\ X_1\ a\ b\ comm)$$$

Lean4

theorem mk_surjective (f : w.CostructuredArrowDownwards g) :
    ∃ (X₁ : C₁) (a : X₂ ⟶ T.obj X₁) (b : L.obj X₁ ⟶ X₃) (comm : R.map a ≫ w.app X₁ ≫ B.map b = g),
      f = mk w g X₁ a b comm :=
  by
  obtain ⟨g, φ, rfl⟩ := CostructuredArrow.mk_surjective f
  obtain ⟨X₁, a, rfl⟩ := g.mk_surjective
  obtain ⟨b, hb, rfl⟩ := StructuredArrow.homMk_surjective φ
  exact ⟨X₁, a, b, by simpa using hb, rfl⟩

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