coe_lift_symm_apply — Mathlib

English

The inverse of the lift is computed componentwise by composing with the left-inclusion and evaluating at ε.

Русский

Обратное отображение лифта вычисляется по компонентам: композиция с левой инъекцией и значение на ε.

LaTeX

$$$\text{lift}^{-1} : (A[\varepsilon] \to_R B) \to \{ fe : (A \to_R B) × B \;|\; \dots\}$, с $ (\text{lift}^{-1} F).val = (F \circ inlAlgHom, F \varepsilon).$$$

Lean4

@[simp]
theorem coe_lift_symm_apply (F : A[ε] →ₐ[R] B) : (lift.symm F).val = (F.comp (inlAlgHom _ _ _), F ε) :=
  rfl

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