English
There is a compatible IsScalarTower structure making Cotangent stable under scalar changes along towers of ring homomorphisms.
Русский
Существует совместимая структура IsScalarTower, делающая Cotangent устойчивым при каскадном изменении скаляров через цепочки гомоморфизмов колец.
LaTeX
$$$$ \text{IsScalarTower } R \; R' \; S \; \Rightarrow \text{Cotangent is compatible under towers} $$$$
Lean4
noncomputable instance module : Module S P.Cotangent
where
smul := fun r s ↦ .of (P.σ r • s.val)
smul_zero := fun r ↦ ext (smul_zero (P.σ r))
smul_add := fun r x y ↦ ext (smul_add (P.σ r) x.val y.val)
add_smul := fun r s x ↦
by
have := smul_eq_zero_of_mem (P.σ (r + s) - (P.σ r + P.σ s) : P.Ring) (by simp) x
simpa only [sub_smul, add_smul, sub_eq_zero]
zero_smul := fun x ↦ smul_eq_zero_of_mem (P.σ 0 : P.Ring) (by simp) x
one_smul := fun x ↦ by
have := smul_eq_zero_of_mem (P.σ 1 - 1 : P.Ring) (by simp) x
simpa [sub_eq_zero, sub_smul]
mul_smul := fun r s x ↦
by
have := smul_eq_zero_of_mem (P.σ (r * s) - (P.σ r * P.σ s) : P.Ring) (by simp) x
simpa only [sub_smul, mul_smul, sub_eq_zero] using this
