English
Let M be a monoid and c a congruence on M. Given a function f that assigns to any triple (x, y, hxy, hyx) a value in α, and a suitable compatibility condition Hf, the lift of f evaluated at the unit determined by x and y coincides with the value f takes on the representatives x and y (via the congruence data). In other words, the lift behaves as expected on units coming from pairs (x, y) of M.
Русский
Пусть M — моноид и c — конгруэнция на M. Пусть f задает для любых x, y и доказательств hxy, hyx элемент α, а при этом выполнено совместное условие совместимости Hf. Тогда liftOnUnits на единице, соответствующей паре (x, y), даёт значение, равное f на representing x и y (с учётом эквивалентности по c). Говоря иначе, лифт корректно определяет значение на единицах, появляющихся из пар (x, y).
LaTeX
$$$\operatorname{liftOnUnits}\langle x, y, hxy, hyx \rangle f Hf = f x y (c.eq.1\ hxy) (c.eq.1\ hyx)$$$
Lean4
@[to_additive (attr := simp)]
theorem liftOnUnits_mk (f : ∀ x y : M, c (x * y) 1 → c (y * x) 1 → α)
(Hf : ∀ x y hxy hyx x' y' hxy' hyx', c x x' → c y y' → f x y hxy hyx = f x' y' hxy' hyx') (x y : M) (hxy hyx) :
liftOnUnits ⟨(x : c.Quotient), y, hxy, hyx⟩ f Hf = f x y (c.eq.1 hxy) (c.eq.1 hyx) :=
rfl
