mapObj_ext — Mathlib

English

The mapObj extension principle: two maps f,g from X.mapObj p j to A are equal iff they agree after precomposing with each injection ιMapObj p i j hi for all i with p i = j.

Русский

Принцип продолжения карты mapObj: два отображения f,g: X.mapObj p j ⟶ A равны тогда и только тогда, когда они совпадают после предсоединения с каждой инъекцией ιMapObj p i j hi для всех i с p i = j.

LaTeX

$$$ f = g \;\Leftrightarrow\; \forall i, hij, X.ιMapObj p i j hij ≫ f = X.ιMapObj p i j hij ≫ g $$$

Lean4

@[ext]
theorem mapObj_ext {A : C} {j : J} (f g : X.mapObj p j ⟶ A)
    (hfg : ∀ (i : I) (hij : p i = j), X.ιMapObj p i j hij ≫ f = X.ιMapObj p i j hij ≫ g) : f = g :=
  Cofan.IsColimit.hom_ext (X.isColimitCofanMapObj p j) _ _ (fun ⟨i, hij⟩ => hfg i hij)

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