lift_apply_inr — Mathlib

English

The lift composed with the left-algebra-hom equals f (alternate phrasing).

Русский

Лифт-образование в слое слева эквивалентно f (вариант формулировки).

LaTeX

$$$ (lift\\ f\\ g\\ hg\\ hfg\\ hgf).toLinearMap.comp (inlAlgHom S R M) = f $$$

Lean4

@[simp]
theorem lift_apply_inr (f : R →ₐ[S] A) (g : M →ₗ[S] A) (hg : ∀ x y, g x * g y = 0) (hfg : ∀ r x, g (r •> x) = f r * g x)
    (hgf : ∀ r x, g (x <• r) = g x * f r) (m : M) : lift f g hg hfg hgf (inr m) = g m :=
  show f 0 + g m = g m by rw [map_zero, zero_add]

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