English
There is a universal lift from a ring morphism f: R →* T, together with a morphism fS from S to Units T, giving a morphism R[S⁻¹] →* T with a compatibility condition hf.
Русский
Существует универсальный подъем от морфизма колец f: R →* T вместе с морфизмом fS: S →* Units T, задающим морфизм R[S⁻¹] →* T с условием совместимости hf.
LaTeX
$$$\\text{universalMulHom}(f,fS,hf): R[S^{-1}] \\to* T$ с требованием совместимости на numeratorHom.$$
Lean4
/-- The universal lift from a morphism `R →* T`, which maps elements of `S` to units of `T`,
to a morphism `R[S⁻¹] →* T`. -/
@[to_additive /-- The universal lift from a morphism `R →+ T`, which maps elements of `S` to
additive-units of `T`, to a morphism `AddOreLocalization R S →+ T`. -/
]
def universalMulHom (hf : ∀ s : S, f s = fS s) : R[S⁻¹] →* T
where
toFun
x :=
x.liftExpand (fun r s => ((fS s)⁻¹ : Units T) * f r) fun r t s ht =>
by
simp only [smul_eq_mul]
have : (fS ⟨t * s, ht⟩ : T) = f t * fS s := by simp only [← hf, MonoidHom.map_mul]
conv_rhs =>
rw [MonoidHom.map_mul, ← one_mul (f r), ← Units.val_one, ← mul_inv_cancel (fS s)]
rw [Units.val_mul, mul_assoc, ← mul_assoc _ (fS s : T), ← this, ← mul_assoc]
simp only [one_mul, Units.inv_mul]
map_one' := by beta_reduce; rw [OreLocalization.one_def, liftExpand_of]; simp
map_mul' x
y :=
by
cases x with
| _ r₁ s₁
cases y with
| _ r₂ s₂
rcases oreDivMulChar' r₁ r₂ s₁ s₂ with ⟨ra, sa, ha, ha'⟩; rw [ha']; clear ha'
rw [liftExpand_of, liftExpand_of, liftExpand_of, Units.inv_mul_eq_iff_eq_mul, map_mul, map_mul, Units.val_mul,
mul_assoc, ← mul_assoc (fS s₁ : T), ← mul_assoc (fS s₁ : T), Units.mul_inv, one_mul, ← hf, ← mul_assoc, ←
map_mul _ _ r₁, ha, map_mul, hf s₂, mul_assoc, ← mul_assoc (fS s₂ : T), (fS s₂).mul_inv, one_mul]
