lift_comp — Mathlib

English

Let M, N, P be commutative monoids, S a submonoid of M, x ∈ M, and F a localization map away from x to N. Let g: M →* P be a monoid homomorphism with g(x) a unit in P. Then the lifted homomorphism along F, composed with F, equals g; i.e., (F.lift x hg) ∘ F = g.

Русский

Пусть M, N, P — коммутативные моноиды, S — подмоноид M, x ∈ M, и F — локализационная карта Away от x в N. Пусть g: M →* P — гомоморфизм моноидов, такой что g(x) является единицей в P. Тогда полученный по F лифт-гомоморфизм и композиция с F удовлетворяют (F.lift x hg) ∘ F = g; т.е. композиция равна g.

LaTeX

$$$ (F.lift\ x\ hg)\circ F = g $$$

Lean4

@[simp]
theorem lift_comp (hg : IsUnit (g x)) : (F.lift x hg).comp F = g :=
  Submonoid.LocalizationMap.lift_comp _ _

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