English
Let M, P be commutative monoids and S ⊆ M, T ⊆ P submonoids. If f is a localization map for S and k is an isomorphism P ≃* M such that k(T) = S, then f ∘ k is a localization map for T.
Русский
Пусть M и P — коммутативные моноиды, S ⊆ M и T ⊆ P — подмножества моноидов. Если f является локализационной картой для S и k — изоморфизм P ≃* M такой, что k(T) = S, то состав f ∘ k является локализационной картой для T.
LaTeX
$$$\text{Let } M, P \text{ be commutative monoids } S \le M, T \le P. \\text{If } f: S \to N \text{ is a localization map and } k: P \simeq M \\text{with } T.map\ k^{\mathrm{toMonoidHom}} = S, \\text{then } f \circ k \text{ is a localization map for } T.$$$
Lean4
/-- Given `CommMonoid`s `M, P` and Submonoids `S ⊆ M, T ⊆ P`, if `f : M →* N` is a Localization
map for `S` and `k : P ≃* M` is an isomorphism of `CommMonoid`s such that `k(T) = S`, `f ∘ k`
is a Localization map for `T`. -/
@[to_additive /-- Given `AddCommMonoid`s `M, P` and `AddSubmonoid`s `S ⊆ M, T ⊆ P`, if `f : M →* N` is a
Localization map for `S` and `k : P ≃+ M` is an isomorphism of `AddCommMonoid`s such that
`k(T) = S`, `f ∘ k` is a Localization map for `T`. -/
]
def ofMulEquivOfDom {k : P ≃* M} (H : T.map k.toMonoidHom = S) : LocalizationMap T N :=
have H' : S.comap k.toMonoidHom = T := H ▸ (SetLike.coe_injective <| T.1.1.preimage_image_eq k.toEquiv.injective)
(f.toMonoidHom.comp k.toMonoidHom).toLocalizationMap
(fun y ↦
let ⟨z, hz⟩ := f.map_units ⟨k y, H ▸ Set.mem_image_of_mem k y.2⟩
⟨z, hz⟩)
(fun z ↦
let ⟨x, hx⟩ := f.surj z
let ⟨v, hv⟩ := k.surjective x.1
let ⟨w, hw⟩ := k.surjective x.2
⟨(v, ⟨w, H' ▸ show k w ∈ S from hw.symm ▸ x.2.2⟩),
by
simp_rw [MonoidHom.comp_apply, MulEquiv.toMonoidHom_eq_coe, MonoidHom.coe_coe, hv, hw]
dsimp
rw [hx]⟩)
fun x y ↦
by
rw [MonoidHom.comp_apply, MonoidHom.comp_apply, MulEquiv.toMonoidHom_eq_coe, MonoidHom.coe_coe, toMonoidHom_apply,
toMonoidHom_apply, f.eq_iff_exists]
rintro ⟨c, hc⟩
let ⟨d, hd⟩ := k.surjective c
refine ⟨⟨d, H' ▸ show k d ∈ S from hd.symm ▸ c.2⟩, ?_⟩
rw [← hd, ← map_mul k, ← map_mul k] at hc; exact k.injective hc
