Theorems · Definition · commutative algebra

Algebra.Extension.equivH1CotangentOfFormallySmooth

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

Any formally smooth extension can be used to calculate H¹(L_{A/R}).

Defined in

Mathlib.RingTheory.Smooth.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRingCommRingAlgebraAlgebra.FormallySmooth