instIsMultiplicativeSurjective — Mathlib

English

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

Русский

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

LaTeX

$$$ (\\text{MorphismProperty.surjective } C).IsMultiplicative$ with $id\_mem$ and $comp\_mem$.$$

Lean4

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

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