English
If f is a localization map for S ⊆ M and k is an isomorphism N ≃* P, then the composition k ∘ f is a localization map for M at S.
Русский
Если f — локализационная проекция для S ⊆ M, и k — изоморфизм N ≃* P, то композиция k ∘ f является локализацией на M по S.
LaTeX
$$$\\text{ofMulEquivOfLocalizations}(k) : S.LocMap P$ whenever $f : S.LocMap N$ and $k : N \\simeq^* P$.$$
Lean4
/-- If `f : M →* N` is a Localization map for a Submonoid `S` and `k : N ≃* P` is an isomorphism
of `CommMonoid`s, `k ∘ f` is a Localization map for `M` at `S`. -/
@[to_additive /-- If `f : M →+ N` is a Localization map for a Submonoid `S` and `k : N ≃+ P` is an isomorphism
of `AddCommMonoid`s, `k ∘ f` is a Localization map for `M` at `S`. -/
]
def ofMulEquivOfLocalizations (k : N ≃* P) : LocalizationMap S P :=
(k.toMonoidHom.comp f.toMonoidHom).toLocalizationMap (fun y ↦ isUnit_comp f k.toMonoidHom y)
(fun v ↦
let ⟨z, hz⟩ := k.surjective v
let ⟨x, hx⟩ := f.surj z
⟨x, show v * k (f _) = k (f _) by rw [← hx, map_mul, ← hz]⟩)
fun x y ↦ (k.apply_eq_iff_eq.trans f.eq_iff_exists).1
