The Coq mailing list

[Christopher Mary <admin AT AnthropLOGIC.onmicrosoft.com>]

Nicolas “pain au chocolat” Tabareau,

    [ERRATA] 
https://github.com/1337777/cartier/blob/master/cartierSolution16.lp

En effet, merci de ton aide pour l’errata, mais conformément à l’article 6 de 
la loi 2004-575, j’ai un droit de réponse à ton désaveu public… Sonya Massey 
would say “I rebuke you too”, lol #MeToo

-----

Review of Max Zeuner defending “Constructive Algebraic Geometry”.

MAX [1] shows an equivalence between functorial schemes X and 
locally-ringed-lattice schemes Y, approximately:

    LRDL^op( X ⇒ Spec , Y )  ≅   ( X ⇒ LRDL^op( Spec( – ), Y ) )  

Where  ( X ⇒ X' ) ∶= Fun( CommRing , Set )( X , X' ) are abbreviations in the 
category of functors from commutative rings to sets, where LRDL^op is the 
opposite of the category of “locally” ringed distributive lattices, where 
Spec: Fun(  CommRing^op, LRDL^op ) is the functor sending a commutative ring 
to (the underlying set of) its Zarisky lattice, and where “locally” for a 
lattice Y with sheaf of rings O_Y means the existence of an operation 

     D: (u : Y) → O_Y (u) → u↓Y 

where D_u(f) is intended to be the open in the slice lattice under u where 
the function f:  O_Y (u) is invertible.

… But this won’t work; I judge Max’s defense as a “thèse à crédit”.

A prerequisite is a computational logic (type theory) for categories, 
presheaves, sites and locally ringed sites. This requirement is especially 
manifest for the etale topology where the “objects” of the site are etale 
morphisms (adjoint pairs of cocontinuous/continuous functors between sites). 
Note that the existing attempts at “2-dimensional type theory” as in Marcelo 
Fiore [2] have a flaw in that they try to implement the interchange law 
directly  (α ∘_0 β) ∘_1 (γ ∘_0 δ) =  (α ∘_1 γ) ∘_0 (β ∘_1 δ) when in reality 
it hides subtle Yoneda-actions related to the fact that the profunctor 
C[F-,_] is a distinct computer type than the hom-profunctor C[-,_] of the 
category C applied to outer objects of the form F- ...

A draft solution has been implemented in

    https://github.com/1337777/cartier/blob/master/cartierSolution16.lp

as a natural transformation from the structure sheaf to the sieves-classifier 
(“subobject classifier” for the small topos of the scheme Y)

    D: O_Y → Ω 

where D_u(f) is intended to be the SIEVE in Ω(u) under u of all opens where 
the function f: O_Y (u) is invertible. This requires the presence of a 
classifier/universe Ω for sieves, but because of Kosta Dosen 
cut-elimination-in-categories techniques, it is not necessary to work 
“internally” as in Thierry Coquand [3] to get a logic which computes. Now a 
sieve S under the object U can be realized as a (“dependent”) profunctor in 
groupoids over the category of elements of U; that is the sieves need not be 
(-1)-truncated subobjects as in Nicolas Tabareau [4, definition 5.5], because 
checking instead that the cohomology differential is 0 will be an alternative 
way to check for compatibility of a family of sections of the sheaf 
(alternative to “internally” ensuring this compatibility)... Moreover, this 
profunctor framework will allow a hybrid definition of the site and 
functor-of-points approaches to schemes. But all this computational logic 
foundations are still far from your typical birational algebraic geometry 
conference [5], which usually start with blowing up schemes (projective Proj 
bundles) and doing cases analyses with Cartier divisors...

It is a strange coincidence that the formula D: O_Y→Ω resembles the formula 
d:  O_Y→Ω  for Kahler differentials, but the open problem of discovering a 
(graded) differential linear logic formulation for the algebraic-geometry’s 
cohomology differentials will be investigated instead in an upcoming review 
via the profunctorial semantics of linear logic in the context of sieves as 
profunctors… It will also be reviewed how outrageous is Ehrhard’s [6, section 
3.1.1, page 44] definition of the composition of polynomials by the use of 
differentials instead of by elementary concepts, 

     g ∘ f  =  Σ_(i: 0..n) (1/i!) g⋅d’^i⋅f^(⊗i)⋅c^i

and how this motivates the search of a hybrid framework⋅ combining polynomial 
functors (good algebra) “depending” on analytic functors (good logic) …

[1] Max Zeuner “Univalent Foundations of Constructive Algebraic Geometry” 
(defending Oct 4th 2024)
[2] Marcelo Fiore “A type theory for cartesian closed bicategories”
[3] Thierry Coquand “A foundation for synthetic algebraic geometry”
[4] Nicolas Tabareau “Lawvere-Tierney sheafification in homotopy type theory”
[5] SCMS 上海数学中心 “Workshop on Birational Geometry - September 2024”
[6] Thomas Ehrhard “An introduction to differential linear logic: proof-nets, 
models and antiderivatives”

-----

A copy of this review is at https://dailyReviews.link (by re365.net open 
source Microsoft 365 app), the tiktok-style calendar overlay for all your 
research communications!