instIsScalarTowerCotangent — Mathlib

English

There is a natural linear map between cotangent spaces induced by a ring homomorphism f: P → P'.

Русский

Существует естественный линейный отображение между котангентовыми пространствами, индуцированное гомоморфизмом колец f: P → P'.

LaTeX

$$$$ \mathrm{Cotangent}.map f : P.Cotangent \to P'.Cotangent \text{ is linear over } S $$$$

Lean4

instance {R₁ R₂} [CommRing R₁] [CommRing R₂] [Algebra R₁ S] [Algebra R₂ S] [Algebra R₁ R₂] [IsScalarTower R₁ R₂ S] :
    IsScalarTower R₁ R₂ P.Cotangent := by
  constructor
  intro r s m
  change algebraMap R₂ S (r • s) • m = (algebraMap _ S r) • (algebraMap _ S s) • m
  rw [Algebra.smul_def, map_mul, mul_smul, ← IsScalarTower.algebraMap_apply]

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