toComp_toAlgHom_monomial — Mathlib

English

The image of a renamed constant under the toAlgHom of Q.ofComp P is the constant C of the algebra map induced by the base ring hom.

Русский

Образ константы после применения toAlgHom к renaming эквивалентен константе из соответствующего алгебраического отображения.

LaTeX

$$$ (Q.ofComp P).toAlgHom ((\\mathrm{rename}\\, \\mathrm Sum.inr)\\; p) = C (algebraMap _ _ p)$$$

Lean4

theorem toComp_toAlgHom_monomial (Q : Generators S T ι') (P : Generators R S ι) (j a) :
    (Q.toComp P).toAlgHom (monomial j a) = monomial (Finsupp.sumElim 0 j) a :=
  by
  convert rename_monomial _ _ _
  ext f (i₁ | i₂) <;> simp [Finsupp.mapDomain_notin_range, Finsupp.mapDomain_apply Sum.inr_injective]

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