comap — Mathlib

English

There is a law relating comap across a chain of algebra homomorphisms: comap (g ∘ f) = comap f ∘ comap g.

Русский

Соблюдается тождество перехода по компакам над композицией: comap (g ∘ f) = comap f ∘ comap g.

LaTeX

$$$\\operatorname{comap}(g \\cdot f) = \\operatorname{comap} f \\circ \\operatorname{comap} g$$$

Lean4

/-- Given an algebra hom `f : MvPolynomial σ R →ₐ[R] MvPolynomial τ R`
and a variable evaluation `v : τ → R`,
`comap f v` produces a variable evaluation `σ → R`.
-/
noncomputable def comap (f : MvPolynomial σ R →ₐ[R] MvPolynomial τ R) : (τ → R) → σ → R := fun x i => aeval x (f (X i))

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