English
The functor taking a discrete ℕ-indexed diagram of LightCondMod R preserves epimorphisms: Limits.Pi.map f is epi whenever each f(n) is epi.
Русский
Функтор, задающий диаграмму с дискретной натуральной числовой индексацией в LightCondMod R, сохраняет эпиморфизмы: Limits.Pi.map f является эпиморфизмом, если каждый f(n) является эпиморфизмом.
LaTeX
$$$\text{Limits.Pi.map}(f)$ is epi whenever $\forall n, \text{Epi}(f(n))$.$$
Lean4
instance : (lim (J := Discrete ℕ) (C := LightCondMod R)).PreservesEpimorphisms where
preserves f
_ :=
by
have : lim.map f = (Pi.isoLimit _).inv ≫ Limits.Pi.map (f.app ⟨·⟩) ≫ (Pi.isoLimit _).hom :=
by
apply limit.hom_ext
intro ⟨n⟩
simp only [lim_obj, lim_map, limMap, IsLimit.map, limit.isLimit_lift, limit.lift_π, Cones.postcompose_obj_pt,
limit.cone_x, Cones.postcompose_obj_π, NatTrans.comp_app, Functor.const_obj_obj, limit.cone_π, Pi.isoLimit,
Limits.Pi.map, Category.assoc, limit.conePointUniqueUpToIso_hom_comp, Pi.cone_pt, Pi.cone_π,
Discrete.natTrans_app, Discrete.functor_obj_eq_as]
erw [IsLimit.conePointUniqueUpToIso_inv_comp_assoc]
rfl
rw [this]
infer_instance
