Theorems · Definition · commutative algebra

Algebra.Extension.H1Cotangent.equivOfFormallySmooth

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

Formally smooth extensions have isomorphic H¹(L_P).

Defined in

Mathlib.RingTheory.Smooth.Basic

Cited by

5 results in Mathlib

Foundations

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

Assumes

CommRingCommRingAlgebraAlgebra.FormallySmoothAlgebra.FormallySmooth