instIsMultiplicativeBijective — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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