lift_comp_inv_right — Mathlib

English

For a morphism f, the composite lift f (f ∘ ι) followed by μ equals the unit-counit composite: toUnit ∘ η.

Русский

Для морфизма f композиция lift f (f ∘ ι) затем μ равна toUnit ∘ η.

LaTeX

$$$\mathrm{lift}(f, f \circ \iota) \circ \mu = \mathrm{toUnit} \circ \eta$$$

Lean4

@[reassoc (attr := simp)]
theorem lift_comp_inv_right [GrpObj B] (f : A ⟶ B) : lift f (f ≫ ι) ≫ μ = toUnit _ ≫ η :=
  by
  have := f ≫= right_inv B
  rwa [comp_lift_assoc, comp_id, reassoc_of% toUnit_unique (f ≫ toUnit B) (toUnit A)] at this

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