Chern-Weil Theory

Stream: Is there code for X?

[Dean Young]

Hi, all,

I am hoping someone can help me in my exploration of pre-existing code for the topics below that I am interested in.

I am trying to find the code we have for these things, even if it consists of partial progress:

1) Singular homology and cohomology of topological spaces or ``SSet''
2) Cohomology classes and singular cohomology with integral coefficients
3) Derivations, Connections, and the tangent bundle
4) De Rham cohomology
5) Line bundles and divisors for smooth manifolds and complex varieties

It's a lot to ask these together, but a unifying goal is Chern-Weil theory.

[Johan Commelin]

I think 1,2,3 exist for some value of "exist". (Maybe not "connections", though)

[Dean Young]

@Johan Commelin thanks for this. It would be nice if you knew anything about DR cohomology and divisors specifically not being in here... I can be more specific if need-be- I wanted perhaps that DR cohomology matches singular cohomology with coefficients in ℝ for a smooth manifold, and also the definition of Weil and Cartier divisors or something similar, as well as the definition of a bundle or a fiber bundle.

[Yaël Dillies]

I believe Heather and Floris worked on De Rham at Banff, but it was in Lean 3

[Damiano Testa]

Also, from context, I think that the two mentions of de Rham cohomology are different topics.

[Damiano Testa]

Even if you set the bar lower, to say Krull dimension, you still find very little in mathlib...

[Ron Z]

@Damiano Testa (4) just says De Rham cohomology though. What was there besides that DR cohomology matches singular cohomology?

[Damiano Testa]

I think that 4 refers to algebraic de Rham cohomology (for algebraic varieties), while I think that Yaël's comment refers to de Rham cohomology for smooth manifolds.

[Damiano Testa]

But, as I said, I'm going from context alone, so I could very easily be wrong.

[Dean Young]

@Damiano Testa sorry, I should have been more specific here. Smooth manifolds is what I want. I don't know much about algebraic DR cohomology but I do enjoy a certain insight about the "free abelian group object". I'm mostly interested in spaces and manifolds.

[Damiano Testa]

Ok, so I see how I misread the context! Yaël's comment is then very appropriate! My comments would relate more to algebraic de Rham cohomology. In particular, I do not think that a development of Krull dimension would be especially beneficial for the de Rham cohomology pertinent to this thread!

[Patrick Massot]

It’s really funny that there is a world where the default meaning of “de Rham cohomology” is “algebraic de Rham cohomology” instead of “actual de Rham cohomology”.

[Damiano Testa]

Indeed, here is another shocker: for some people "function" does not mean "polynomial".

[Kevin Buzzard]

"Riemann-Roch theorem" is also two different theorems, with the two communities both commonly referring to their one as "the" RR theorem (and the proof that they're related involves GAGA which is harder than the proof of either of the Riemann-Roch theorems)

[Kevin Buzzard]

I've mentioned a "Riemann-Roch race" before, where the algebraic and analytic people both try and prove their version and we see who gets there first. We could also have a de Rham cohomology race; I think that both definitions are close.

[Patrick Massot]

In both cases history of maths has a very clear answer.

[Kevin Buzzard]

Yes, you analytic guys are old and out of date and our modern algebraic definitions specialise to yours and are far more general

[Patrick Massot]

This could even be true now with condensed mathematics, who knows?

[Johan Commelin]

I think it's true. Except that it isn't called algebraic geometry by the authors, but analytic geometry. So I guess that still counts as a win for the analytic guys?

[Adam Topaz]

Are all analytic guys now happy with animated condensed rings?

[Dean Young]

(deleted)