preimage_comp — Mathlib

English

For ring homomorphisms f: R → S and g: S → T, the preimage of the composition equals the composition of preimages: Spec.preimage(f ≫ g) = Spec.preimage(g) ≫ Spec.preimage(f).

Русский

Для гомоморфизмов колец f: R → S и g: S → T выполняется: Spec.preimage(f ≫ g) = Spec.preimage(g) ≫ Spec.preimage(f).

LaTeX

$$$\mathrm{Spec.preimage}(f \;\circ\; g) = \mathrm{Spec.preimage}(g) \;\circ\; \mathrm{Spec.preimage}(f).$$$

Lean4

@[simp, reassoc]
theorem preimage_comp {R S T : CommRingCat} (f : Spec R ⟶ Spec S) (g : Spec S ⟶ Spec T) :
    Spec.preimage (f ≫ g) = Spec.preimage g ≫ Spec.preimage f :=
  Spec.map_injective (by simp)

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