Lean4
/-- Implementation, see `leftExactFunctorForgetEquivalence`.
This is the complicated bit, where we show that forgetting the group structure in the image of
`F` and then reconstructing it recovers the group structure we started with. -/
noncomputable def unitIsoAux (F : C ⥤ AddCommGrpCat.{v}) [PreservesFiniteLimits F] (X : C) :
letI : (F ⋙ forget AddCommGrpCat).Braided := .ofChosenFiniteProducts _
commGrpTypeEquivalenceCommGrp.inverse.obj (AddCommGrpCat.toCommGrp.obj (F.obj X)) ≅
(F ⋙ forget AddCommGrpCat).mapCommGrp.obj (Preadditive.commGrpEquivalence.functor.obj X) :=
by
letI : (F ⋙ forget AddCommGrpCat).Braided := .ofChosenFiniteProducts _
letI : F.Monoidal := .ofChosenFiniteProducts _
refine
CommGrp_.mkIso Multiplicative.toAdd.toIso
(by
erw [Functor.mapCommGrp_obj_grp_one]
cat_disch)
?_
dsimp [-Functor.comp_map, -ConcreteCategory.forget_map_eq_coe, -forget_map]
have : F.Additive := Functor.additive_of_preserves_binary_products _
simp only [Category.id_comp]
erw [Functor.mapCommGrp_obj_grp_mul]
erw [Functor.comp_map, F.map_add, Functor.Monoidal.μ_comp F (forget AddCommGrpCat) X X, Category.assoc, ←
Functor.map_comp, Preadditive.comp_add, Functor.Monoidal.μ_fst, Functor.Monoidal.μ_snd]
cat_disch
