English
Two lifts of quotient maps are equal if they agree on all representatives; equivalently, lifts are determined by their actions on the representatives from M.
Русский
Два лифта отображений на квотировку совпадают, если они совпадают на всех представителях; лифты задаются по их действию на представителях из M.
LaTeX
$$$\forall f,g:\; c.Quotient \to P,\; (\forall a:\, M, f(a)=g(a)) \Rightarrow f=g$$$
Lean4
/-- Homomorphisms on the quotient of a monoid by a congruence relation are equal if they
are equal on elements that are coercions from the monoid. -/
@[to_additive /-- Homomorphisms on the quotient of an `AddMonoid` by an additive congruence relation
are equal if they are equal on elements that are coercions from the `AddMonoid`. -/
]
theorem lift_funext (f g : c.Quotient →* P) (h : ∀ a : M, f a = g a) : f = g :=
hom_ext <| DFunLike.ext _ _ h
