English
For A, B commutative rings with R-algebra structures, and f, g: A → B, the ι component of the equalizer fork in Under is equal to the ι in AlgHom equalizer, i.e. the map components coincide with the underlying equalizer morphism.
Русский
Для A, B колец с структурами R-алгебр и гомоморфизмов f, g: A → B, компонент ι равноправного вилочного предела в Under равен компоненте ι в гомоморфе-гомоморфе равенства.
LaTeX
$$$ (\\text{Under.equalizerFork'} f g)\\;\\!\\!\\!_{\\ }\\;\\iota = (\\text{AlgHom.equalizer } f g).\\text{val}.toUnder $$$
Lean4
/-- Variant of `Under.equalizerFork'` for algebra maps. This is definitionally equal to
`Under.equalizerFork` but this is costly in applications. -/
def equalizerFork' {A B : Type u} [CommRing A] [CommRing B] [Algebra R A] [Algebra R B] (f g : A →ₐ[R] B) :
Fork f.toUnder g.toUnder :=
Fork.ofι ((AlgHom.equalizer f g).val.toUnder) <| by ext a; exact a.property
