instIsScalarTowerH1CotangentOfCotangent

English

There is a natural scalar tower structure on H1Cotangent with respect to a tower of rings, i.e. the actions of the intermediate rings are compatible and satisfy (rs) · x = r · (s · x).

Русский

На H1Cotangent имеется естественная структура тензора скаляров в рамках каскадных колец: для скаляров r и s действует (rs)·x = r·(s·x).

LaTeX

$$IsScalarTower R R' P.H1Cotangent$$

Lean4

noncomputable instance {R₁ R₂} [CommRing R₁] [CommRing R₂] [Algebra R₁ R₂] [Algebra R₁ S] [Algebra R₂ S]
    [Module R₁ P.Cotangent] [IsScalarTower R₁ S P.Cotangent] [Module R₂ P.Cotangent] [IsScalarTower R₂ S P.Cotangent]
    [IsScalarTower R₁ R₂ P.Cotangent] : IsScalarTower R₁ R₂ P.H1Cotangent := by delta Extension.H1Cotangent;
  infer_instance

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