instFaithfulSumFromSum — Mathlib

English

The fromSum functor is faithful: it reflects equality of morphisms via the left and right inclusions.

Русский

fromSum верен: он восстанавливает равенство морфизмов через левые и правые включения.

LaTeX

$$$\mathrm{fromSum} C D\text{ is faithful}$$$

Lean4

instance : (fromSum C D).Faithful where
  map_injective {x y} h h'
    heq := by
    cases h <;> cases h'
    all_goals
      simp only [fromSum_obj, Sum.inl__obj, fromSum_map_inl, Sum.inr__obj, fromSum_map_inr] at heq
      simp [Functor.map_injective _ heq]

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