English
There is an equivalence between magma homomorphisms on α and magma homomorphisms from the quotient Magma.AssocQuotient α, given by lifting.
Русский
Существует эквиваленция между морфизмами магмы на α и морфизмами магмы из фактор-множества Magma.AssocQuotient α, задаваемая подъемом.
LaTeX
$$$\mathrm{lift} : (\alpha \to_{\mathsf{n}*} \beta) \simeq (\mathrm{AssocQuotient}(\alpha) \to_{\mathsf{n}*} \beta)$$$
Lean4
/-- Lifts a magma homomorphism `α → β` to a semigroup homomorphism `Magma.AssocQuotient α → β`
given a semigroup `β`. -/
@[to_additive (attr := simps symm_apply) /-- Lifts an additive magma homomorphism `α → β` to an
additive semigroup homomorphism `AddMagma.AssocQuotient α → β` given an additive semigroup `β`. -/
]
def lift : (α →ₙ* β) ≃ (AssocQuotient α →ₙ* β)
where
toFun
f :=
{ toFun := fun x ↦ Quot.liftOn x f <| by rintro a b (⟨c, d, e⟩ | ⟨c, d, e, f⟩) <;> simp only [map_mul, mul_assoc]
map_mul' := fun x y ↦ Quot.induction_on₂ x y (map_mul f) }
invFun f := f.comp of
