baseChange — Mathlib

English

Given a base-change morphism f that is injective, equations are preserved under base-change.

Русский

При инъективном отображении f уравнения сохраняются при базовом изменении.

LaTeX

$$$$ (W'.baseChange B).\\mathrm{toJacobian}.\\mathrm{Equation}(f \\circ P) \\iff (W'.baseChange A).\\mathrm{toJacobian}.\\mathrm{Equation} P $$$$

Lean4

theorem baseChange (h : (W'.baseChange A).toJacobian.Equation P) : (W'.baseChange B).toJacobian.Equation (f ∘ P) :=
  by
  convert Equation.map f.toRingHom h using 1
  rw [AlgHom.toRingHom_eq_coe, map_baseChange]

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