English
There is an equivalence between monoid homomorphisms α → R and ring homomorphisms FreeAbelianGroup α → R, given by the lifting construction.
Русский
Существует обратимость между моноид-гомоморфизмами α → R и кольцовыми гомоморфизмами FreeAbelianGroup α → R через конструкцию lift.
LaTeX
$$$\text{liftMonoid}: (α \to_* R) \simeq (FreeAbelianGroup α \to_*^+ R)$$$
Lean4
/-- If `f` preserves multiplication, then so does `lift f`. -/
def liftMonoid : (α →* R) ≃ (FreeAbelianGroup α →+* R)
where
toFun
f :=
{ lift f with
toFun := lift f
map_one' := (lift_apply_of f _).trans f.map_one
map_mul' := fun x y ↦
by
refine FreeAbelianGroup.induction_on y (by simp only [mul_zero, map_zero]) (fun L2 ↦ ?_) (fun L2 ih ↦ ?_) ?_
· refine FreeAbelianGroup.induction_on x (by simp only [zero_mul, map_zero]) (fun L1 ↦ ?_) (fun L1 ih ↦ ?_) ?_
· simp_rw [of_mul_of, lift_apply_of]
exact f.map_mul _ _
· simp_rw [neg_mul, map_neg, neg_mul]
exact congr_arg Neg.neg ih
· intro x1 x2 ih1 ih2
simp only [add_mul, map_add, ih1, ih2]
· rw [mul_neg, map_neg, map_neg, mul_neg, ih]
· intro y1 y2 ih1 ih2
rw [mul_add, map_add, map_add, mul_add, ih1, ih2] }
invFun F := MonoidHom.comp (↑F) ofMulHom
left_inv
f :=
MonoidHom.ext <| by
simp only [RingHom.coe_monoidHom_mk, MonoidHom.coe_comp, MonoidHom.coe_mk, OneHom.coe_mk, ofMulHom_coe,
Function.comp_apply, lift_apply_of, forall_const]
right_inv
F :=
RingHom.coe_addMonoidHom_injective <| by
simp only
rw [← lift.apply_symm_apply (↑F : FreeAbelianGroup α →+ R)]
rfl
