instPreservesMonomorphismsObjFunctorTypeSigmaConst

English

Let C be a category with coproducts and MonoCoprod; for any A in C, the functor sigmaConst.obj A preserves monomorphisms.

Русский

Пусть C — категория с копроодитами и структурой MonoCoprod; для любого объекта A в C функтор σConst.Obj(A) сохраняет мономорфизмы.

LaTeX

$$$$ \\operatorname{PreservesMonomorphisms}\\left( \\sigma_{\\mathrm{const}}(A) \\right) $$$$

Lean4

instance (A : C) [HasCoproducts.{u} C] [MonoCoprod C] : (sigmaConst.{u}.obj A).PreservesMonomorphisms where
  preserves {J I} ι
    hι := by
    rw [mono_iff_injective] at hι
    exact MonoCoprod.mono_map'_of_injective (fun (i : I) ↦ A) ι hι

Похожие утверждения