val_smul — Mathlib

English

Let R0 be a commutative ring and S an R0-algebra. For any r in R0 and x in the first homology H1 of the naive cotangent complex, the underlying component satisfies (r · x).1 = r · x.1, i.e. the scalar action commutes with taking the underlying component.

Русский

Пусть R0 — коммутативное кольцо, S — R0-алгебра. Для любого r ∈ R0 и x ∈ H1L_{S/R}, соответствующий первому компоненту выполняется (r · x)1 = r · x1, то есть скалярное действие согласуется с взятием базового компонента.

LaTeX

$$$\\forall r \\in R_0\\, \\forall x \\in P.H1Cotangent:\\ (r \\cdot x).1 = r \\cdot x.1$$$

Lean4

@[simp]
theorem val_smul {R₀} [CommRing R₀] [Algebra R₀ S] [Module R₀ P.Cotangent] [IsScalarTower R₀ S P.Cotangent] (r : R₀)
    (x : P.H1Cotangent) : (r • x).1 = r • x.1 :=
  rfl

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