Theorems · Theorem · commutative algebra

Algebra.Generators.repr_CotangentSpaceMap

∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {ι : Type w}
  {P : Algebra.Generators R S ι} {R' : Type u'} {S' : Type v'} {ι' : Type w'} [inst_3 : CommRing R']
  [inst_4 : CommRing S'] [inst_5 : Algebra R' S'] {P' : Algebra.Generators R' S' ι'} [inst_6 : Algebra R R']
  [inst_7 : Algebra S S'] [inst_8 : Algebra R S'] [inst_9 : IsScalarTower R R' S'] [inst_10 : IsScalarTower R S S']
  (f : P.Hom P') (i : ι) (j : ι'),
  (P'.cotangentSpaceBasis.repr ((Algebra.Extension.CotangentSpace.map f.toExtensionHom) (P.cotangentSpaceBasis i))) j =
    (MvPolynomial.aeval P'.val) ((MvPolynomial.pderiv j) (f.val i))

Defined in

Mathlib.RingTheory.Extension.Cotangent.Basic

Cited by

2 results in Mathlib

Foundations

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

Assumes

CommRingCommRingAlgebraCommRingCommRingAlgebraAlgebraAlgebraAlgebraIsScalarTowerIsScalarTower