English
For any f : α → β, g : β → γ, and x ∈ FreeAbelianGroup α, lift (g ∘ f) x = lift g (map f x).
Русский
Для любых f : α → β, g : β → γ и x ∈ FreeAbelianGroup α выполнено lift (g ∘ f) x = lift g (map f x).
LaTeX
$$$ \forall {\alpha \to \beta} {\beta \to \gamma} (f) (g) (x : FreeAbelianGroup(\alpha)),\; \operatorname{lift}(g \circ f) x = \operatorname{lift} g (\operatorname{map} f x)$$$
Lean4
theorem lift_comp {α} {β} {γ} [AddCommGroup γ] (f : α → β) (g : β → γ) (x : FreeAbelianGroup α) :
lift (g ∘ f) x = lift g (map f x) := by
induction x using FreeAbelianGroup.induction_on with
| C0 => simp only [map_zero]
| C1 => simp only [lift_apply_of, map, Function.comp]
| Cn _ h => simp only [h, AddMonoidHom.map_neg]
| Cp _ _ h₁ h₂ => simp only [h₁, h₂, AddMonoidHom.map_add]
