Theorems · Definition · commutative algebra

Algebra.Extension.H1Cotangent

{R : Type u} →
  {S : Type v} → [inst : CommRing R] → [inst_1 : CommRing S] → [inst_2 : Algebra R S] → Algebra.Extension R S → Type w

The first homology of the (naive) cotangent complex of S over R, induced by a given presentation 0 → I → P → R → 0, defined as the kernel of I/I² → S ⊗[P] Ω[P⁄R].

Defined in

Mathlib.RingTheory.Extension.Cotangent.Basic

Cited by

49 results in Mathlib

Foundations

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

Assumes

CommRingCommRingAlgebra