sound — Mathlib

English

If two morphisms f1, f2: a → b in C are r-related, then their images under the quotient functor are equal in the quotient category.

Русский

Если два морфизма f1, f2: a → b в C связаны отношением r, то их изображения под квоти-функтором равны в квотной категории.

LaTeX

$$$\forall {a,b}\, {f_1,f_2:\, a\to b},\; r\ f_1\ f_2 \rightarrow (\mathrm{functor}\ r).map f_1 = (\mathrm{functor}\ r).map f_2.$$$

Lean4

protected theorem sound {a b : C} {f₁ f₂ : a ⟶ b} (h : r f₁ f₂) : (functor r).map f₁ = (functor r).map f₂ := by
  simpa using Quot.sound (CompClosure.intro (𝟙 a) f₁ f₂ (𝟙 b) h)

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