monoCoprod_of_preservesCoprod_of_reflectsMono

English

For each i, the canonical Sigma.inj map into the Sigma type is mono.

Русский

Для каждого i каноническое отображение Sigma.inj моно.

LaTeX

$$[Mono (Sigma.ι X i)]$$

Lean4

theorem monoCoprod_of_preservesCoprod_of_reflectsMono [MonoCoprod D] [PreservesColimitsOfShape (Discrete WalkingPair) F]
    [ReflectsMonomorphisms F] : MonoCoprod C where
  binaryCofan_inl {A B} c
    h := by
    let c' := BinaryCofan.mk (F.map c.inl) (F.map c.inr)
    apply mono_of_mono_map F
    change Mono c'.inl
    apply MonoCoprod.binaryCofan_inl
    apply mapIsColimitOfPreservesOfIsColimit F
    apply IsColimit.ofIsoColimit h
    refine Cocones.ext (φ := eqToIso rfl) ?_
    rintro ⟨(j₁ | j₂)⟩ <;>
      simp only [const_obj_obj, eqToIso_refl, Iso.refl_hom, Category.comp_id, BinaryCofan.mk_inl, BinaryCofan.mk_inr]

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