instIsMultiplicativeInjective — Mathlib

English

For Concrete categories, the morphism property injective is multiplicative: the identity is injective and the composition of injective morphisms is injective.

Русский

Для конкретной категории свойство инъективности сохраняется при композиции: тождественный морфизм инъективен, а композиция инъективных морфизмов инъективна.

LaTeX

$$$ (\\text{MorphismProperty.injective } C).IsMultiplicative ,\\; id\\_mem$ and $\\text{comp\_mem}$: композиция сохраняет injective.$$

Lean4

instance : (MorphismProperty.injective C).IsMultiplicative
    where
  id_mem
    X := by
    delta MorphismProperty.injective
    convert injective_id
    aesop
  comp_mem f g hf
    hg := by
    delta MorphismProperty.injective
    rw [hom_comp]
    exact hg.comp hf

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