lift_comp_one_right — Mathlib

English

Same as 75734: the lift operation is associative when combining multiple morphisms into a monoid object.

Русский

Повторение 75734: операция lift ассоциативна при сочетании нескольких морфизмов в моноидном объекте.

LaTeX

$$$\\mathrm{lift}(\\mathrm{lift} f g \\gg μ) h \\gg μ = \\mathrm{lift} f (\\mathrm{lift} g h \\gg μ) \\gg μ$$

Lean4

@[reassoc (attr := simp)]
theorem lift_comp_one_right {A : C} {B : C} [MonObj B] (f : A ⟶ B) (g : A ⟶ 𝟙_ C) : lift f (g ≫ η) ≫ μ = f :=
  by
  have := lift f g ≫= mul_one B
  rwa [lift_whiskerLeft_assoc, lift_rightUnitor_hom] at this

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