English
The equalizer of two nonunital star R-algebra homomorphisms ϕ, ψ: A →⋆ₙₐ[R] B is the largest subalgebra of A on which ϕ and ψ agree; concretely, it is the NonUnitalStarSubalgebra consisting of all x ∈ A with ϕ(x) = ψ(x).
Русский
Равняющее подалгебра двух ненулевых звёздных R-алгебровых однородных отображений ϕ, ψ: A →⋆ₙₐ[R] B — это наибольшая подпалгебра в A, на которой ϕ и ψ совпадают; конкретно это NonUnitalStarSubalgebra всех x ∈ A с ϕ(x) = ψ(x).
LaTeX
$$$\mathrm{equalizer}(\varphi, \psi) = \{ a \in A \mid \varphi(a) = \psi(a) \}$ as a NonUnitalStarSubalgebra of A.$$
Lean4
/-- The equalizer of two non-unital star `R`-algebra homomorphisms -/
def equalizer (ϕ ψ : F) : NonUnitalStarSubalgebra R A
where
toNonUnitalSubalgebra := NonUnitalAlgHom.equalizer ϕ ψ
star_mem' := @fun x (hx : ϕ x = ψ x) => by simp [map_star, hx]
