lift_surjective_iff — Mathlib

English

The lift is surjective if and only if every element v ∈ P can be expressed as g(x) times the inverse of g(y) for some x ∈ R, y ∈ M; i.e., there exists (x,y) with v = g(x)/g(y).

Русский

Лифт сюръективен тогда и только тогда, когда каждый элемент v ∈ P можно записать как g(x)/g(y) для некоторых x ∈ R, y ∈ M.

LaTeX

$$$ \\text{Surjective }(\\mathrm{lift}\\;hg) \\iff \\forall v \\in P, \\exists x \\in R, y \\in M,\\; v = g(x) \\cdot (g(y))^{-1}. $$$

Lean4

theorem lift_surjective_iff : Surjective (lift hg : S → P) ↔ ∀ v : P, ∃ x : R × M, v * g x.2 = g x.1 :=
  (toLocalizationMap M S).lift_surjective_iff hg

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