mk_surjective — Mathlib

English

Every morphism f in w.StructuredArrowRightwards g arises from data X1, a, b with a commutativity relation, i.e., f = mk w g X1 a b comm for some X1, a, b, comm.

Русский

Каждый морфизм f в w.StructuredArrowRightwards g получается из данных X1, a, b, comm с выполнением соотношения comm, то есть f = mk w g X1 a b comm.

LaTeX

$$$\exists X_1, a, b, comm\; (f = \mathrm{mk}\ w\ g\ X_1\ a\ b\ comm)\;\land\; R\!\text{map} \ a \; \circ \ w\!\mathrm{app} \ X_1 \circ B\!\mathrm{map} \ b = g$$$

Lean4

theorem mk_surjective (f : w.StructuredArrowRightwards 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⟩ := StructuredArrow.mk_surjective f
  obtain ⟨X₁, b, rfl⟩ := g.mk_surjective
  obtain ⟨a, ha, rfl⟩ := CostructuredArrow.homMk_surjective φ
  exact ⟨X₁, a, b, by simpa using ha, rfl⟩

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