instIsMultiplicativeMultiplicativeClosure'

English

The multiplicative closure of a morphism property W is multiplicative.

Русский

Замыкание по умножению свойства морфизмов W является мультипликативным.

LaTeX

$$$IsMultiplicative(W.multiplicativeClosure)$$$

Lean4

/-- `multiplicativeClosure' W` is multiplicative. -/
instance : IsMultiplicative W.multiplicativeClosure'
    where
  id_mem x := .id x
  comp_mem f g hf
    hg := by
    induction hf with
    | of _ h => exact .of_comp _ g h hg
    | id _ => rwa [Category.id_comp]
    | of_comp g' f hg' hf h_rec =>
      rw [Category.assoc]
      exact .of_comp g' (f ≫ g) hg' (h_rec g hg)

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