lift_comp_apply — Mathlib

English

Two homomorphisms coincide if they agree on the generators.

Русский

Два гомоморфизма совпадают, если они совпадают на порождающих.

LaTeX

$$$\\forall g,h:\\; FreeAbelianGroup α \\to_+ β,\\ (\\forall x:\\; g(\\text{of} x)=h(\\text{of} x)) \\Rightarrow g=h$$$

Lean4

theorem lift_comp_apply {α β γ} [AddCommGroup β] [AddCommGroup γ] (a : FreeAbelianGroup α) (f : α → β) (g : β →+ γ) :
    lift (g ∘ f) a = g (lift f a) := by
  rw [← AddMonoidHom.comp_apply g (lift f)]
  refine (lift_unique _ _ ?_).symm
  intro a
  change g ((lift f) (of a)) = g (f a)
  simp only [lift_apply_of]

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