English
The fork on 𝟙 ⊗ f and 𝟙 ⊗ g is given by S ⊗R eq(f,g); i.e., the fork map is (tensorProd R S).map of the equalizer (in Under).
Русский
Форк на 𝟙 ⊗ f и 𝟙 ⊗ g задаётся S ⊗R eq(f,g); то есть отображение форка равно (tensorProd R S).map от равенства.
LaTeX
$$$ \\text{Fork}((\\text{tensorProd } R S).map f, (\\text{tensorProd } R S).map g) = \\text{Fork.of}_{\\iota}((\\text{tensorProd } R S).map((\\mathrm{AlgHom.equalizer} (toAlgHom f) (toAlgHom g)).val.toUnder))$$$
Lean4
/-- The fork on `𝟙 ⊗[R] f` and `𝟙 ⊗[R] g` given by `S ⊗[R] eq(f, g)`. -/
def tensorProdEqualizer {A B : Under R} (f g : A ⟶ B) : Fork ((tensorProd R S).map f) ((tensorProd R S).map g) :=
Fork.ofι ((tensorProd R S).map ((AlgHom.equalizer (toAlgHom f) (toAlgHom g)).val.toUnder)) <| by
rw [← Functor.map_comp, equalizer_comp, Functor.map_comp]
