lift_lift_assoc — Mathlib

English

The operation lift is associative on morphisms into a monoid object: lift(lift(f,g) ∘ μ) h ∘ μ = lift(f, lift(g,h) ∘ μ) ∘ μ.

Русский

Операция lift ассоциативна на левых отбивках морфизмов в моноидном объекте: lift(lift(f,g) ∘ μ) h ∘ μ = lift(f, lift(g,h) ∘ μ) ∘ μ.

LaTeX

$$$\\mathrm{lift}(\\mathrm{lift}(f,g) \\circ μ) \\, h \\circ μ = \\mathrm{lift}\\big(f, \\mathrm{lift}(g,h) \\circ μ\\big) \\circ μ$$

Lean4

theorem lift_lift_assoc {A : C} {B : C} [MonObj B] (f g h : A ⟶ B) :
    lift (lift f g ≫ μ) h ≫ μ = lift f (lift g h ≫ μ) ≫ μ :=
  by
  have := lift (lift f g) h ≫= mul_assoc B
  rwa [lift_whiskerRight_assoc, lift_lift_associator_hom_assoc, lift_whiskerLeft_assoc] at this

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