English
The equalizer of two R-algebra homomorphisms φ, ψ: F → F is the subalgebra of A consisting of all a with φ(a) = ψ(a).
Русский
Эквалайзером двух R-алгебрных гомоморфизмов φ, ψ: F → F служит подалгебра A, состоящая из всех a с φ(a) = ψ(a).
LaTeX
$$$\operatorname{equalizer}(\varphi, \psi) = \{ a \in A \mid \varphi(a) = \psi(a) \}$$$
Lean4
/-- The equalizer of two R-algebra homomorphisms -/
@[simps coe toSubsemiring]
def equalizer (ϕ ψ : F) [FunLike F A B] [AlgHomClass F R A B] : Subalgebra R A
where
carrier := {a | ϕ a = ψ a}
zero_mem' := by simp only [Set.mem_setOf_eq, map_zero]
one_mem' := by simp only [Set.mem_setOf_eq, map_one]
add_mem' {x y} (hx : ϕ x = ψ x) (hy : ϕ y = ψ y) := by rw [Set.mem_setOf_eq, map_add, map_add, hx, hy]
mul_mem' {x y} (hx : ϕ x = ψ x) (hy : ϕ y = ψ y) := by rw [Set.mem_setOf_eq, map_mul, map_mul, hx, hy]
algebraMap_mem' x := by simp only [Set.mem_setOf_eq, AlgHomClass.commutes]
