English
The equalizer of two non-unital R-algebra homomorphisms ϕ, ψ is the set of elements a ∈ A such that ϕ(a) = ψ(a); it is closed under addition, multiplication and scalar action.
Русский
Равнозначиватель двух гомоморфизмов без единицы — это множество элементов a ∈ A таких, что ϕ(a) = ψ(a); оно замкнуто по сложению, умножению и умножению на скаляры.
LaTeX
$$NonUnitalAlgHom.equalizer(ϕ,ψ) is the subalgebra { a ∈ A | ϕ(a) = ψ(a) }$$
Lean4
/-- The equalizer of two non-unital `R`-algebra homomorphisms -/
def equalizer (ϕ ψ : F) : NonUnitalSubalgebra R A
where
carrier := {a | (ϕ a : B) = ψ a}
zero_mem' := by rw [Set.mem_setOf_eq, map_zero, map_zero]
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]
smul_mem' r x (hx : ϕ x = ψ x) := by rw [Set.mem_setOf_eq, map_smul, map_smul, hx]
