hom_ext — Mathlib

English

Morphisms of cosimplicial objects are determined by their components at each level; i.e., two morphisms f,g: X→Y are equal if and only if f.app n = g.app n for all n.

Русский

Гомоморфизмы косимпликсальных объектов определяются их компонентами на каждом уровне; то есть f = g тогда и только тогда, когда f.app n = g.app n для всех n.

LaTeX

$$$\forall X,Y: \mathrm{CosimplicialObject}(C),\ \forall f,g: X\to Y,\ (\forall n: \mathrm{SimplexCategory},\ f_{n}=g_{n})\Rightarrow f=g$$$

Lean4

@[ext]
theorem hom_ext {X Y : CosimplicialObject C} (f g : X ⟶ Y) (h : ∀ (n : SimplexCategory), f.app n = g.app n) : f = g :=
  NatTrans.ext (by ext; apply h)

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