comap_comp — Mathlib

English

If f: S1 → S2 and g: S2 → R are ring homomorphisms, then pulling back along the composition g ∘ f is the same as pulling back first along g and then along f.

Русский

Если f: S1 → S2 и g: S2 → R — кольцевые гомоморфизмы, то вытяжка по композиции g ∘ f равна последовательной вытяжке по g, затем по f.

LaTeX

$$$$ \\mathrm{comap}_{g \\circ f} v = \\mathrm{comap}_f (\\mathrm{comap}_g v). $$$$

Lean4

theorem comap_comp {S₁ : Type*} {S₂ : Type*} [Ring S₁] [Ring S₂] (f : S₁ →+* S₂) (g : S₂ →+* R) :
    v.comap (g.comp f) = (v.comap g).comap f :=
  Valuation.comap_comp v f g

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