Algebraic De Rham cohomology

Stream: homology

[Joël Riou]

I just would like to mention that I am not very far from being able to construct the algebraic De Rham complex, as a cochain complex of A-modules when B is an A-algebra (PR #18551).
This is based on a series of PR about operations on presentations of modules and presentations of algebras by generators and relations. For example, from a presentation of an algebra, I obtain a presentation of the module of 1-differentials #18440. Then, from a presentation of a module, I obtain a presentation of its exterior powers. Applying this to the obvious presentation of B as an A-algebra (one generator for each element of B, add three types of relations), we may obtain a presentation of ⋀[B]^n (Ω[B⁄A]) as a B-module. The tricky part is to deduce a presentation of the restriction of scalars of this module as an A-module, but using general principles #18389, we can get one for which the generators are b₀ db₁ ∧ db₂ ∧ ... ∧ dbₙ, and then the exterior derivative can be defined on these generators as db₀ ∧ db₁ ∧ db₂ ∧ ... ∧ dbₙ.

[Andrew Yang]

Is the presentation of Ω[B⁄A] the same as file#Mathlib/RingTheory/Kaehler/CotangentComplex?

[Joël Riou]

Andrew Yang said:

Is the presentation of Ω[B⁄A] the same as file#Mathlib/RingTheory/Kaehler/CotangentComplex?

Ah, yes, thank you, it could also be deduced from the code in this file.

[Kevin Buzzard]

This would be great because it will mean that we beat the analysts to de Rham cohomology (like we beat them to the zeta function and will hopefully beat them to finite dimensionality of modular forms)

[Joël Riou]

I have removed the most technical sorries in the main file RingTheory.DeRham.Basic #18551 (it turns out the tautological presentation of ⋀[B]^n (Ω[B⁄A]) as an A-module involves seven types of relations). There are a few other sorries here and there, but they will dissolve when the various parts come together in mathlib. Then, this mostly relies on general constructions of presentations of modules (some PR are ready: #18374, #18359, #18332), and it will also require some progress on exterior powers (@Sophie Morel's PR #10654).

[Joël Riou]

The following definition is now sorry-free:

deRhamComplex.{u_1, u_2} (A : Type u_1) (B : Type u_2) [CommRing A] [CommRing B] [Algebra A B] :
  CochainComplex (ModuleCat A) ℕ