English
For rings A,B and two ring homomorphisms f,g: A → B, the inclusion from the equalizer of f and g into A is a local hom.
Русский
Пусть A,B — кольца и f,g: A → B — кольцевые гомоморфизмы. Инклюзия из равняющегося множества равенств f(a)=g(a) в A — локальный гомоморфизм.
LaTeX
$$$\\text{IsLocalHom}((\\text{equalizerFork } f\\, g).\\iota.hom)$$$
Lean4
instance : IsLocalHom (equalizerFork f g).ι.hom := by
constructor
rintro ⟨a, h₁ : _ = _⟩ (⟨⟨x, y, h₃, h₄⟩, rfl : x = _⟩ : IsUnit a)
have : y ∈ RingHom.eqLocus f.hom g.hom :=
by
apply (f.hom.isUnit_map ⟨⟨x, y, h₃, h₄⟩, rfl⟩ : IsUnit (f x)).mul_left_inj.mp
conv_rhs => rw [h₁]
rw [← f.hom.map_mul, ← g.hom.map_mul, h₄, f.hom.map_one, g.hom.map_one]
rw [isUnit_iff_exists_inv]
exact ⟨⟨y, this⟩, Subtype.eq h₃⟩
