English
The map liftEquiv defines an equivalence between the product of homomorphisms (M →* P) × (N →* P) and the homomorphisms M ∗ N →* P; its toFun sends (f,g) to lift f g and its inverse sends f to (f ∘ inl, f ∘ inr).
Русский
Отображение liftEquiv задаёт эквивалентность между произведением гомоморфизмов (M →* P) × (N →* P) и гомоморфизмами M ∗ N →* P; к функции toFun для пары (f,g) присваивает lift f g, а обратная функция от f даёт (f ∘ inl, f ∘ inr).
LaTeX
$$$\\\\text{liftEquiv} : (M \\\\to^* P) \xtimes (N \\\\to^* P) \\\\simeq (M \\\\ast N \\\\to^* P).$$$
Lean4
/-- `Coprod.lift` as an equivalence. -/
@[to_additive /-- `AddMonoid.Coprod.lift` as an equivalence. -/
]
def liftEquiv : (M →* P) × (N →* P) ≃ (M ∗ N →* P)
where
toFun fg := lift fg.1 fg.2
invFun f := (f.comp inl, f.comp inr)
right_inv _ := Eq.symm <| lift_unique rfl rfl
