Theorems · Definition · commutative algebra

Algebra.Extension.h1CotangentEquivCotangent

{R : Type u} →
  {S : Type v} →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] → (P : Algebra.Extension R S) → Algebra.H1Cotangent P.Ring S ≃ₗ[S] P.Cotangent

Given an extension P : Extension R S, this is the linear equivalence between the first homology of the naive cotangent complex of S over P.Ring and the cotangent space of P.

Defined in

Mathlib.RingTheory.Extension.ExtendScalars

Cited by

3 results in Mathlib

Foundations

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

Assumes

CommRingCommRingAlgebra