English
The universal lift is defined using the compatible data on R and S to give a ring homomorphism from the Ore localization.
Русский
Универсальное поднятие задаётся с помощью совместимых данных на R и S, чтобы получить кольцевой гомоморфизм из локализации Ора.
LaTeX
$$universalHom : R[S^{-1}] →+* T$$
Lean4
/-- The universal lift from a ring homomorphism `f : R →+* T`, which maps elements in `S` to
units of `T`, to a ring homomorphism `R[S⁻¹] →+* T`. This extends the construction on
monoids. -/
def universalHom : R[S⁻¹] →+* T :=
{
universalMulHom f.toMonoidHom fS
hf with
map_zero' := by
simp only [RingHom.toMonoidHom_eq_coe, OneHom.toFun_eq_coe, MonoidHom.toOneHom_coe]
rw [OreLocalization.zero_def, universalMulHom_apply]
simp
map_add' := fun x y =>
by
simp only [RingHom.toMonoidHom_eq_coe, OneHom.toFun_eq_coe, MonoidHom.toOneHom_coe]
induction x with
| _ r₁ s₁
induction y with
| _ r₂ s₂
rcases oreDivAddChar' r₁ r₂ s₁ s₂ with ⟨r₃, s₃, h₃, h₃'⟩
rw [h₃']
clear h₃'
simp only [smul_eq_mul, universalMulHom_apply, MonoidHom.coe_coe, Submonoid.smul_def]
simp only [mul_inv_rev, MonoidHom.map_mul, RingHom.map_add, RingHom.map_mul, Units.val_mul]
rw [mul_add, mul_assoc, ← mul_assoc _ (f s₃), hf, ← Units.val_mul]
simp only [one_mul, inv_mul_cancel, Units.val_one]
congr 1
rw [← mul_assoc]
congr 1
norm_cast at h₃
have h₃' := Subtype.coe_eq_of_eq_mk h₃
rw [← Units.val_mul, ← mul_inv_rev, ← fS.map_mul, h₃']
rw [Units.inv_mul_eq_iff_eq_mul, Units.eq_mul_inv_iff_mul_eq, ← hf, ← hf]
simp only [map_mul] }
