lift_def — Mathlib

English

The lift composed with the left-algebra-hom equals the original f.

Русский

Сведение lift композицией с left‑алгебра-гомом равняется исходному f.

LaTeX

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

Lean4

theorem lift_def (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 (op r • x) = g x * f r) (x : tsze R M) : lift f g hg hfg hgf x = f x.fst + g x.snd :=
  rfl

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