lift_inv_comp_right — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[reassoc]
theorem lift_inv_comp_right [GrpObj A] [GrpObj B] (f : A ⟶ B) [IsMonHom f] : lift f (ι ≫ f) ≫ μ = toUnit _ ≫ η :=
  by
  have := right_inv A =≫ f
  rwa [assoc, IsMonHom.mul_hom, assoc, IsMonHom.one_hom, lift_map_assoc, id_comp] at this

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