liftAlgHom_apply — Mathlib

English

For an algebra hom φ, the lifted RatFunc agrees with the quotient of the mapped numerator and denominator: liftAlgHom φ hφ f = φ f.num / φ f.denom.

Русский

Для алгебра-гомоморфизма φ выполнение полагает, что поднятая функция RatFunc совпадает с отношением образов числителя и знаменателя.

LaTeX

$$$\\operatorname{liftAlgHom}(\\phi, h\\phi)(f) = \\dfrac{\\phi(f\\text{.num})}{\\phi(f\\text{.denom})}$$$

Lean4

theorem liftAlgHom_apply {L S : Type*} [Field L] [CommSemiring S] [Algebra S K[X]] [Algebra S L] (φ : K[X] →ₐ[S] L)
    (hφ : K[X]⁰ ≤ L⁰.comap φ) (f : RatFunc K) : liftAlgHom φ hφ f = φ f.num / φ f.denom :=
  liftMonoidWithZeroHom_apply _ hφ _

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