isAmalgamation_iff_ofArrows — Mathlib

English

For a family of elements x in a presieve of arrows, x is an amalgamation for t ∈ P(B) iff it agrees with the images of t along each arrow π_i, i.e., P.map(π_i)^op(t) = x_i for all i.

Русский

Для семейства элементов x в предшайве стрелок x является амальгаммацией для t ∈ P(B) тогда, когда тождество выполняется: P.map(π_i)^op(t) = x_i для всех i.

LaTeX

$$$ x.IsAmalgamation(t) \iff \forall i, P.map(\pi_i).op(t) = x_i $$$

Lean4

theorem isAmalgamation_iff_ofArrows (x : FamilyOfElements P (ofArrows X π)) (t : P.obj (op B)) :
    x.IsAmalgamation t ↔ ∀ (i : I), P.map (π i).op t = x _ (ofArrows.mk i) :=
  ⟨fun h i ↦ h _ (ofArrows.mk i), fun h _ f ⟨i⟩ ↦ h i⟩

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