English
The universal lift commutes with the numerator map: universalMulHom f fS hf (numeratorHom r) = f r for all r.
Русский
Универсальный подъем commute с отображением числителя: universalMulHom f fS hf (numeratorHom r) = f r для всех r.
LaTeX
$$$\\text{universalMulHom}(f,fS,hf)(\\text{numeratorHom}(r)) = f(r).$$$
Lean4
/-- Scalar multiplication in a monoid localization. -/
@[to_additive (attr := irreducible) /-- Vector addition in an additive monoid localization. -/
]
protected def hsmul (c : R) : X[S⁻¹] → X[S⁻¹] :=
liftExpand (fun m s ↦ oreNum (c • 1) s • m /ₒ oreDenom (c • 1) s)
(fun r t s ht ↦ by
dsimp only
rw [← mul_one (oreDenom (c • 1) s), ← oreDiv_smul_oreDiv, ← mul_one (oreDenom (c • 1) _), ← oreDiv_smul_oreDiv, ←
OreLocalization.expand])
/- Warning: This gives an diamond on `SMul R[S⁻¹] M[S⁻¹][S⁻¹]`, but we will almost never localize
at the same monoid twice. -/
/- Although the definition does not require `IsScalarTower R M X`,
it does not make sense without it. -/
