English
To define a function on units of the quotient, it suffices to define it on representatives with compatibility conditions.
Русский
Чтобы определить функцию на единицах фактор-алгебры, достаточно задать её на представителях и обеспечить совместимость.
LaTeX
$$$\\text{liftOnUnits }(u) = \\text{hrecOn₂ with representatives and compatibility}$$$
Lean4
/-- In order to define a function `(Con.Quotient c)ˣ → α` on the units of `Con.Quotient c`,
where `c : Con M` is a multiplicative congruence on a monoid, it suffices to define a function `f`
that takes elements `x y : M` with proofs of `c (x * y) 1` and `c (y * x) 1`, and returns an element
of `α` provided that `f x y _ _ = f x' y' _ _` whenever `c x x'` and `c y y'`. -/
@[to_additive]
def liftOnUnits (u : Units c.Quotient) (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') : α :=
by
refine
Con.hrecOn₂ (cN := c) (φ := fun x y => x * y = 1 → y * x = 1 → α) (u : c.Quotient) (↑u⁻¹ : c.Quotient)
(fun (x y : M) (hxy : (x * y : c.Quotient) = 1) (hyx : (y * x : c.Quotient) = 1) =>
f x y (c.eq.1 hxy) (c.eq.1 hyx))
(fun x y x' y' hx hy => ?_) u.3 u.4
refine Function.hfunext ?_ ?_
· rw [c.eq.2 hx, c.eq.2 hy]
· rintro Hxy Hxy' -
refine Function.hfunext ?_ ?_
· rw [c.eq.2 hx, c.eq.2 hy]
· rintro Hyx Hyx' -
exact heq_of_eq (Hf _ _ _ _ _ _ _ _ hx hy)
