toComp — Mathlib

English

Images of monomials under toComp correspond to renaming, with Elim and monomial structure preserved.

Русский

Образы мономов через toComp сохраняют структуру и переименовываются.

LaTeX

$$$ (Q.toComp P).toAlgHom(\\mathrm{monomial}(j) ) = \\mathrm{monomial}(\\mathrm{sumElim}(0,j)) $$$

Lean4

/-- Given families of generators `X ⊆ T` over `S` and `Y ⊆ S` over `R`,
there is a map of generators `R[Y] → R[X, Y]`. -/
@[simps]
noncomputable def toComp (Q : Generators S T ι') (P : Generators R S ι) : Hom P (Q.comp P)
    where
  val i := X (.inr i)
  aeval_val i := by simp

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