lift_localizationMap_mk' — Mathlib

English

If j: N →* P satisfies j(f x) = g x for all x, then f.lift hg = j.

Русский

Если j: N →* P удовлетворяет j(f x) = g x для всех x, тогда f.lift hg = j.

LaTeX

$$$ f.lift hg = j $ given $\forall x, j(f(x)) = g(x)$$$

Lean4

/-- Given a Localization map `f : M →* N` for a Submonoid `S ⊆ M` and a localization map
`g : M →* P` for the same submonoid, the homomorphism induced from
`N` to `P` maps `f x * (f y)⁻¹` to `g x * (g y)⁻¹` for all `x : M, y ∈ S`. -/
@[to_additive (attr := simp) /--
    Given a Localization map `f : M →+ N` for an AddSubmonoid `S ⊆ M` and a localization map
    `g : M →+ P` for the same submonoid, the homomorphism
    induced from `N` to `P` maps `f x - f y` to `g x - g y` for all `x : M, y ∈ S`. -/
    ]
theorem lift_localizationMap_mk' (g : S.LocalizationMap P) (x y) : f.lift g.map_units (f.mk' x y) = g.mk' x y :=
  f.lift_mk' _ _ _

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