lift_comp_of' — Mathlib

English

There is an isomorphism between the space of families (fi) and the space of monoid homomorphisms CoprodI(M) →* N, given by lift and its inverse of.

Русский

Существует изоморфизм между множествами семей fi и множествами гомоморфизм CoprodI(M) →* N, задаваемый lift и обратной величиной.

LaTeX

$$$\\mathrm{lift}: (\\forall i, M_i \\to* N) \\cong (CoprodI(M) \\to* N).$$$

Lean4

@[simp]
theorem lift_comp_of' {N} [Monoid N] (f : CoprodI M →* N) : lift (fun i ↦ f.comp (of (i := i))) = f :=
  lift.apply_symm_apply f

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