mapId — Mathlib

English

If P ≤ Q are submonoids, there is an embedding map from the localization at P to the localization at Q, induced by the identity on A.

Русский

Если P ≤ Q — подпомножества, существует вложение локализации по P в локализацию по Q, индуцированное тождественным отображением на A.

LaTeX

$$$$ \mathrm{mapId}: \mathrm{HomogeneousLocalization}(\mathcal{A}, P) \to \mathrm{HomogeneousLocalization}(\mathcal{A}, Q) $$$$

Lean4

/-- Let `A` be a graded algebra and `P ≤ Q` be two submonoids, then the homogeneous localization of `A`
at `P` embeds into the homogeneous localization of `A` at `Q`.
-/
abbrev mapId {P Q : Submonoid A} (h : P ≤ Q) : HomogeneousLocalization 𝒜 P →+* HomogeneousLocalization 𝒜 Q :=
  map 𝒜 𝒜 (RingHom.id _) h (fun _ _ ↦ id)

Похожие утверждения