baseChange_slope — Mathlib

English

Under base change, the slope function is compatible: slope after base-changing to B and applying f to inputs equals f of the slope over A.

Русский

При базовом изменении наклонная функция совместима: наклон после базового изменения на B и применения f к входам равен f от наклона над A.

LaTeX

$$$ (W'.baseChange K).toAffine.slope (f x_1) (f x_2) (f y_1) (f y_2) = f ((W'.baseChange F).toAffine.slope x_1 x_2 y_1 y_2) $$$

Lean4

theorem baseChange_slope [DecidableEq F] [DecidableEq K] [Algebra R F] [Algebra S F] [IsScalarTower R S F] [Algebra R K]
    [Algebra S K] [IsScalarTower R S K] (f : F →ₐ[S] K) (x₁ x₂ y₁ y₂ : F) :
    (W'.baseChange K).toAffine.slope (f x₁) (f x₂) (f y₁) (f y₂) = f ((W'.baseChange F).toAffine.slope x₁ x₂ y₁ y₂) :=
  by rw [← RingHom.coe_coe, ← map_slope, map_baseChange]

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