instIsMultiplicativeMultiplicativeClosure

English

If W on C^op is multiplicative, then W on C is multiplicative.

Русский

Если W на C^{op} мультипликативно, то W на C мультипликативно.

LaTeX

$$$IsMultiplicative(W^{unop}) \Rightarrow IsMultiplicative(W)$$$

Lean4

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

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