English
AddCommGrpCat is AB4Star.
Русский
AddCommGrpCat обладает свойством AB4Star.
LaTeX
$$$\operatorname{AB4Star}(AddCommGrpCat)$$$
Lean4
instance : HasExactLimitsOfShape (Discrete J) (AddCommGrpCat.{u}) :=
by
apply (config := { allowSynthFailures := true }) hasExactLimitsOfShape_of_preservesEpi
exact
{
preserves {X Y} f
hf :=
by
let iX : limit X ≅ AddCommGrpCat.of ((i : J) → X.obj ⟨i⟩) :=
(Pi.isoLimit X).symm ≪≫
(limit.isLimit _).conePointUniqueUpToIso (AddCommGrpCat.HasLimit.productLimitCone _).isLimit
let iY : limit Y ≅ AddCommGrpCat.of ((i : J) → Y.obj ⟨i⟩) :=
(Pi.isoLimit Y).symm ≪≫
(limit.isLimit _).conePointUniqueUpToIso (AddCommGrpCat.HasLimit.productLimitCone _).isLimit
have : Pi.map (fun i ↦ f.app ⟨i⟩) = iX.inv ≫ lim.map f ≫ iY.hom :=
by
simp only [Discrete.functor_obj_eq_as, Discrete.mk_as, Pi.isoLimit, IsLimit.conePointUniqueUpToIso,
limit.cone, AddCommGrpCat.HasLimit.productLimitCone, Iso.trans_inv, Functor.mapIso_inv,
IsLimit.uniqueUpToIso_inv, Cones.forget_map, IsLimit.liftConeMorphism_hom, limit.isLimit_lift, Iso.symm_inv,
Functor.mapIso_hom, IsLimit.uniqueUpToIso_hom, lim_obj, lim_map, Iso.trans_hom, Iso.symm_hom,
AddCommGrpCat.HasLimit.lift, Functor.const_obj_obj, Category.assoc, limit.lift_map_assoc, Pi.cone_pt, iX,
iY]
ext g j
change _ = (_ ≫ limit.π (Discrete.functor fun j ↦ Y.obj { as := j }) ⟨j⟩) _
simp only [Discrete.functor_obj_eq_as, productIsProduct', limit.lift_π, Fan.mk_pt, Fan.mk_π_app, Pi.map_apply]
change _ = (_ ≫ _ ≫ limit.π Y ⟨j⟩) _
simp
suffices Epi (iX.hom ≫ (iX.inv ≫ lim.map f ≫ iY.hom) ≫ iY.inv) by simpa using this
suffices Epi (iX.inv ≫ lim.map f ≫ iY.hom) from inferInstance
rw [AddCommGrpCat.epi_iff_surjective, ← this]
simp_rw [CategoryTheory.NatTrans.epi_iff_epi_app, AddCommGrpCat.epi_iff_surjective] at hf
refine fun b ↦ ⟨fun i ↦ (hf ⟨i⟩ (b i)).choose, ?_⟩
funext i
exact (hf ⟨i⟩ (b i)).choose_spec }
