map_hom — Mathlib

English

A deprecated compatibility result: applying a map after lifting equals lifting the composition.

Русский

Устаревшее соответствие: применение отображения после поднятия равно подниманию композиции.

LaTeX

$$$g(\\text{lift } f\\ a) = \\text{lift}(g \\circ f)\\ a$$$

Lean4

@[deprecated lift_comp_apply (since := "2025-07-23")]
theorem map_hom {α β γ} [AddCommGroup β] [AddCommGroup γ] (a : FreeAbelianGroup α) (f : α → β) (g : β →+ γ) :
    g (lift f a) = lift (g ∘ f) a :=
  (lift_comp_apply a f g).symm

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