isMonoidal_trans — Mathlib

English

If e: C ≌ D and e': D ≌ E are monoidal equivalences, then their composition e.trans e' (i.e., e followed by e') is a monoidal equivalence.

Русский

Если e: C ≌ D и e': D ≌ E — моноидальные эквивалентности, то их композиция e ∘ e' (то есть объединение через последовательность) является моноидальной эквивалентностью.

LaTeX

$$$IsMonoidal(e \circ e')$$$

Lean4

/-- The composition of two monoidal category equivalences is monoidal. -/
instance isMonoidal_trans [e'.functor.Monoidal] [e'.inverse.Monoidal] [e'.IsMonoidal] : (e.trans e').IsMonoidal :=
  by
  dsimp [Equivalence.IsMonoidal]
  rw [trans_toAdjunction]
  infer_instance

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