lift_comp_one_left — Mathlib

English

For any f: A → B and g: A → 𝟙_C, the lift satisfies lift(f ∘ η, g) ∘ μ = g; i.e., lifting along η acts as a left identity.

Русский

Для любых f: A → B и g: A → 𝟙, выполнение lift(f ∘ η, g) ∘ μ даёт g; то есть η действует как левый единичный элемент.

LaTeX

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

Lean4

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

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