hom_ext — Mathlib

English

Morphisms α, β between F and G are equal if they are pointwise equal on objects.

Русский

Гомоморфизмы между F и G равны, если их действиe на каждое X совпадают.

LaTeX

$$$\\forall \\alpha, \\beta: F \\to G, \\bigl(\\forall X: C, \\alpha_{X}.out = \\beta_{X}.out\\bigr) \\Rightarrow \\alpha = \\beta$$$

Lean4

@[ext]
theorem hom_ext {F G : EnrichedFunctor V C D} {α β : F ⟶ G} (h : ∀ X : C, α.out.app X = β.out.app X) : α = β :=
  by
  rcases α with ⟨α⟩
  rcases β with ⟨β⟩
  congr
  ext
  apply h

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