English
There is an equivalence between magma homomorphisms from G to A and non-unital algebra homomorphisms from MonoidAlgebra k G to A; this is the adjoint correspondence to the forgetful functor.
Русский
Существует эквиваленция между гомоморфизмами магмы G →* A и неговантовыми алгебра-гомоморфизмами MonoidAlgebra k G →ₙₐ[k] A; это связка сопряженности к забывающей функтору.
LaTeX
$$$\\text{lift} : (G \\to* A) \\simeq (MonoidAlgebra k G \\toₐ[k] A)$$$
Lean4
/-- The functor `G ↦ MonoidAlgebra k G`, from the category of magmas to the category of non-unital,
non-associative algebras over `k` is adjoint to the forgetful functor in the other direction. -/
@[simps apply_apply symm_apply]
def liftMagma [Module k A] [IsScalarTower k A A] [SMulCommClass k A A] : (G →ₙ* A) ≃ (MonoidAlgebra k G →ₙₐ[k] A)
where
toFun
f :=
{
liftAddHom fun x =>
(smulAddHom k A).flip (f x) with
toFun := fun a => a.sum fun m t => t • f m
map_smul' := fun t' a => by
rw [Finsupp.smul_sum, sum_smul_index']
· simp_rw [smul_assoc, MonoidHom.id_apply]
· intro m
exact zero_smul k (f m)
map_mul' := fun a₁ a₂ => by
let g : G → k → A := fun m t => t • f m
have h₁ : ∀ m, g m 0 = 0 := by
intro m
exact zero_smul k (f m)
have h₂ : ∀ (m) (t₁ t₂ : k), g m (t₁ + t₂) = g m t₁ + g m t₂ :=
by
intros
rw [← add_smul]
-- Porting note: `reducible` cannot be `local` so proof gets long.
simp_rw [Finsupp.mul_sum, Finsupp.sum_mul, smul_mul_smul_comm, ← f.map_mul, mul_def, sum_comm a₂ a₁]
rw [sum_sum_index h₁ h₂]; congr; ext
rw [sum_sum_index h₁ h₂]; congr; ext
rw [sum_single_index (h₁ _)] }
invFun F := F.toMulHom.comp (ofMagma k G)
left_inv
f := by
ext m
simp only [NonUnitalAlgHom.coe_mk, ofMagma_apply, NonUnitalAlgHom.toMulHom_eq_coe, sum_single_index,
Function.comp_apply, one_smul, zero_smul, MulHom.coe_comp, NonUnitalAlgHom.coe_to_mulHom]
right_inv
F := by
ext m
simp only [NonUnitalAlgHom.coe_mk, ofMagma_apply, NonUnitalAlgHom.toMulHom_eq_coe, sum_single_index,
Function.comp_apply, one_smul, zero_smul, MulHom.coe_comp, NonUnitalAlgHom.coe_to_mulHom]
