residueFieldCongr_trans_hom — Mathlib

English

The residue field congruence is stable under transitive composition of equalities; i.e., the hom parts compose as expected.

Русский

Согласование поля остатка устойчиво под композиции равенств; гомоморфные части составляются как и полагается.

LaTeX

$$$$ (X.\mathrm{residueFieldCongr}\ e).\mathrm{hom} \circ (X.\mathrm{residueFieldCongr}\ e').\mathrm{hom} = (X.\mathrm{residueFieldCongr}(e \circ e')).\mathrm{hom}. $$$$

Lean4

@[reassoc (attr := simp)]
theorem residueFieldCongr_trans_hom (X : Scheme) {x y z : X} (e : x = y) (e' : y = z) :
    (X.residueFieldCongr e).hom ≫ (X.residueFieldCongr e').hom = (X.residueFieldCongr (e.trans e')).hom :=
  by
  subst e e'
  rfl

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