Theorems · Theorem · commutative algebra

Algebra.Extension.CotangentSpace.map_comp

∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {P : Algebra.Extension R S}
  {R' : Type u'} {S' : Type v'} [inst_3 : CommRing R'] [inst_4 : CommRing S'] [inst_5 : Algebra R' S']
  {P' : Algebra.Extension R' S'} [inst_6 : Algebra R R'] [inst_7 : Algebra S S'] [inst_8 : Algebra R S']
  [inst_9 : IsScalarTower R R' S'] {R'' : Type u''} {S'' : Type v''} [inst_10 : CommRing R''] [inst_11 : CommRing S'']
  [inst_12 : Algebra R'' S''] {P'' : Algebra.Extension R'' S''} [inst_13 : Algebra R R''] [inst_14 : Algebra S S'']
  [inst_15 : Algebra R S''] [inst_16 : IsScalarTower R R'' S''] [inst_17 : Algebra R' R''] [inst_18 : Algebra S' S'']
  [inst_19 : Algebra R' S''] [inst_20 : IsScalarTower R' R'' S''] [inst_21 : IsScalarTower R R' R'']
  [inst_22 : IsScalarTower S S' S''] (f : P.Hom P') (g : P'.Hom P''),
  Algebra.Extension.CotangentSpace.map (g.comp f) =
    ↑S (Algebra.Extension.CotangentSpace.map g) ∘ₗ Algebra.Extension.CotangentSpace.map f

Defined in

Mathlib.RingTheory.Extension.Cotangent.Basic

Cited by

1 results in Mathlib

Foundations

Depth 102 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingCommRingAlgebraCommRingCommRingAlgebraAlgebraAlgebraAlgebraIsScalarTowerCommRingCommRingAlgebraAlgebraAlgebraAlgebraIsScalarTowerAlgebraAlgebraAlgebraIsScalarTowerIsScalarTowerIsScalarTower