From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: <> X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on inbox.vuxu.org X-Spam-Level: X-Spam-Status: No, score=0.3 required=5.0 tests=DKIM_INVALID,DKIM_SIGNED, HTML_MESSAGE,HTTPS_HTTP_MISMATCH,RCVD_IN_DNSWL_NONE autolearn=no autolearn_force=no version=3.4.4 Received: from MEUPR01CU001.outbound.protection.outlook.com (mail-australiasoutheastazlp17010002.outbound.protection.outlook.com [40.93.137.2]) by inbox.vuxu.org (Postfix) with ESMTP id 9468F2E6FB for ; Wed, 13 Nov 2024 10:42:00 +0100 (CET) Received: from SmtpServer.Submit by MEYPR01MB6168 with Microsoft SMTP Server id 15.20.8158.17; Wed, 13 Nov 2024 09:41:57 +0000 Received: from SYBPR01MB5789.ausprd01.prod.outlook.com (2603:10c6:10:e4::5) by MEYPR01MB6168.ausprd01.prod.outlook.com (2603:10c6:220:fb::11) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_ECDHE_RSA_WITH_AES_256_GCM_SHA384) id 15.20.8158.17; Wed, 13 Nov 2024 09:41:51 +0000 Received: from SY4PR01MB8050.ausprd01.prod.outlook.com (2603:10c6:10:1c1::14) by SYBPR01MB5789.ausprd01.prod.outlook.com (2603:10c6:10:e4::5) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_ECDHE_RSA_WITH_AES_256_GCM_SHA384) id 15.20.8158.17; Wed, 13 Nov 2024 09:41:47 +0000 Received: from SY4PR01MB8050.ausprd01.prod.outlook.com ([fe80::c3ce:38df:e603:4779]) by SY4PR01MB8050.ausprd01.prod.outlook.com ([fe80::c3ce:38df:e603:4779%3]) with mapi id 15.20.8158.017; Wed, 13 Nov 2024 09:41:47 +0000 ARC-Seal: i=2; a=rsa-sha256; s=arcselector10001; d=microsoft.com; cv=pass; b=FBUl5JsogS8h2WExiilUYMbmNdH9KA9gpeFn2QpNIPX9yihete5J/0KYtWrmf+1cni0nBMtjfeT41i/8Vb0rgQpeG3csIdKqg4iCAlCm0lV8a0mvv+iDcwloQdjAm3TxkPe98rzVIZ9AULA65c1nMUPn614n2Hwxki8s+y9V6mvqvwsoUVtHkg3NERwoSFOFacVT8y4sMQaI6L7Ce49ZGr6mHiQ+9zSvIqwwYPOOroAmMfbJNgBM7r9e7iQSLUxwpnHGdPXodjDMbWTrDzyg2GIjxvu0YUrl3KySZMwOSc2XRMDk12CQ5GzFwcnJulSpDd58+xUrTaCmQpYZPDwDiA== ARC-Message-Signature: i=2; a=rsa-sha256; c=relaxed/relaxed; d=microsoft.com; s=arcselector10001; h=From:Date:Subject:Message-ID:Content-Type:MIME-Version:X-MS-Exchange-AntiSpam-MessageData-ChunkCount:X-MS-Exchange-AntiSpam-MessageData-0:X-MS-Exchange-AntiSpam-MessageData-1; bh=UWRrAVDPPs+GQ7Wz7YvBVNgp8bxDh1swJD4xpsAD97E=; b=kkdvNNEbL/bU3SFJ8/B4jynL+/5+vAH//KSbnyN2zDL1vN7BgQkOz8o2bXQ/Y5b3Ym+Y2Kybls9ytoLIO+LL5xmW0TaXE2d8Wx/haAaqYkUQn4ezO80iNyvDhsZtqV7M9Oo8fH/o6fmCm453dcYlUcotf8eKYqef20uAgPXKMA+8iZwbqxIitykEQ7TAKFhbWHSxLzSTy98D8wrrfoNqusxnZNvyFlHgEQ8ij78NMSaO7HirGoYGjVUAbR1S6Beo8hTHGEIDC/GBYxCOtkxTq5/v1pNL+wW9sP6KOSgx7ZwhI2//u6bkSbPxqqUePy6VEfdEC8y0tHHDq3Nw8DhPUQ== ARC-Authentication-Results: i=2; mx.microsoft.com 1; spf=pass (sender ip is 209.85.218.65) smtp.rcpttodomain=mq.edu.au smtp.mailfrom=mymail.tstc.edu; dmarc=pass (p=none sp=none pct=100) action=none header.from=mymail.tstc.edu; dkim=fail (signature did not verify) header.d=tstc.edu; arc=pass (0 oda=0 ltdi=0 93) Received: from SY5PR01CA0082.ausprd01.prod.outlook.com (2603:10c6:10:1f5::13) by SYBPR01MB5696.ausprd01.prod.outlook.com (2603:10c6:10:e0::5) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_ECDHE_RSA_WITH_AES_256_GCM_SHA384) id 15.20.8158.17; Wed, 13 Nov 2024 09:39:07 +0000 Received: from SY2PEPF00004FF2.ausprd01.prod.outlook.com (2603:10c6:10:1f5:cafe::55) by SY5PR01CA0082.outlook.office365.com (2603:10c6:10:1f5::13) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_ECDHE_RSA_WITH_AES_256_GCM_SHA384) id 15.20.8158.16 via Frontend Transport; Wed, 13 Nov 2024 09:39:07 +0000 Authentication-Results: spf=pass (sender IP is 209.85.218.65) smtp.mailfrom=mymail.tstc.edu; dkim=fail (signature did not verify) header.d=tstc.edu;dmarc=pass action=none header.from=mymail.tstc.edu; Received-SPF: Pass (protection.outlook.com: domain of mymail.tstc.edu designates 209.85.218.65 as permitted sender) receiver=protection.outlook.com; client-ip=209.85.218.65; helo=mail-ej1-f65.google.com; pr=C Received: from au-smtp-inbound-delivery-1.mimecast.com (103.96.20.101) by SY2PEPF00004FF2.mail.protection.outlook.com (10.167.241.4) with Microsoft SMTP Server (version=TLS1_3, cipher=TLS_AES_256_GCM_SHA384) id 15.20.8158.14 via Frontend Transport; Wed, 13 Nov 2024 09:39:05 +0000 ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=dkim.mimecast.com; s=201903; t=1731490745; h=from:from:reply-to:subject:subject:date:date:message-id:message-id: to:to:cc:mime-version:mime-version:content-type:content-type: dkim-signature; bh=UWRrAVDPPs+GQ7Wz7YvBVNgp8bxDh1swJD4xpsAD97E=; b=JkRFJgpizz/Lbb2mlnrvAijXWqkvmSktKJbjsNvXXn4o2ldK2He7C6QRpq4OmAG1vHldU3 ZLZA8/67p0iotmlNQ+GBfX4UQfCZlDX/lLUOvTvpmg3sAsey2+J8Bmsfi/IpXt3sklufhr g30OWTTWDd1HTYFVVa5BiSJCgIZlG+xUuKP+bJTJ8VRXkSnWeM0dq1bvqksvenMYbBThU2 Ep8moGM0/1MXdi4yC/irrxnIA1PWXadzyZvQ8NxRJCycwt7dn5MiudMRasA8JGP7ozjTBs 4kQnie1Up6kbT4wEXJ+KRPbXRSvyuZU409gVn2AMrtGz0gBWNOi31GFkbb3G9A== ARC-Seal: i=1; s=201903; d=dkim.mimecast.com; t=1731490745; a=rsa-sha256; cv=none; b=TpRnRnKZxx9Vll5cx5liuke2xeRDUy1Roy65WYGZI4HqjEL6nXMDbmYYawZlMBe77J6mjW MgLekUTzu+1w8biJFFwZWHgJtG7SjI+vbPlzx4/2OH6mnHPPqlFFCfXwstCrWPWVZHK9a8 5NBIh03PBzRs1kb7GWb8oYoyIMM7A9A50YcATzykcBbV38CjaIWzdN9zfRGU3/DR9ln4qn jXumOn1cOU2pDMqqHm2u5+3PWazzQ8XvUfVe/UjlnhLP79coxcMpwg9f3R/ledjyXUTJwj r1INCIMC8GKC3xTzLcwnl4IPugbeCHVIbBe157oDJiBYI03jnf67HiDY8cU9mQ== ARC-Authentication-Results: i=1; relay.mimecast.com; dkim=pass header.d=tstc.edu header.s=google header.b=iTbn4lN3; dmarc=pass (policy=none) header.from=mymail.tstc.edu; spf=pass (relay.mimecast.com: domain of aswift@mymail.tstc.edu designates 209.85.218.65 as permitted sender) smtp.mailfrom=aswift@mymail.tstc.edu Authentication-Results-Original: relay.mimecast.com; dkim=pass header.d=tstc.edu header.s=google header.b=iTbn4lN3; dmarc=pass (policy=none) header.from=mymail.tstc.edu; spf=pass (relay.mimecast.com: domain of aswift@mymail.tstc.edu designates 209.85.218.65 as permitted sender) smtp.mailfrom=aswift@mymail.tstc.edu Received: from mail-ej1-f65.google.com (mail-ej1-f65.google.com [209.85.218.65]) by relay.mimecast.com with ESMTP with STARTTLS (version=TLSv1.3, cipher=TLS_AES_256_GCM_SHA384) id au-mta-45-ZdFlWj_zOnKTYSuK00_aaA-1; Wed, 13 Nov 2024 20:39:00 +1100 X-MC-Unique: ZdFlWj_zOnKTYSuK00_aaA-1 X-Mimecast-MFC-AGG-ID: ZdFlWj_zOnKTYSuK00_aaA Received: by mail-ej1-f65.google.com with SMTP id a640c23a62f3a-a99f646ff1bso986251666b.2 for ; Wed, 13 Nov 2024 01:38:59 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=tstc.edu; s=google; t=1731490736; x=1732095536; darn=mq.edu.au; h=content-transfer-encoding:to:subject:message-id:date:from :mime-version:from:to:cc:subject:date:message-id:reply-to; bh=2pvC+xIVmj9alW98WoI2pV1o2wftAeZ/xCyuDtSwEM0=; b=iTbn4lN3hCWmyJGGuY7mz74I5rYXDa4XFsxjd24/uHCqWBoJBwuLdGNVmTf6NPfFIi 74QwfOBQEcPESVpA6N1o5SOajFqPFDAyQFTECdcB+2cXm47LYiv8tMYYTJnFlcXmEEjN WS8MbYs5wX36giHF6Cl3JUHR6BiiPLL5APXU0FozHI/IbnBZZd+0fSwf3iSA65SxdcPN gx35f597XbMsJ2UddEmcwq5/Cw5QejdfmDLrhnoDrPK6KEArt4xUYAar9OLgSJue9S1Y 9pQRb4UiC52DStdul4i2zyykUunhnbau7RCeA6YygmBFjcRQFnST5mZov6B86KrhKtKP RNaw== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20230601; t=1731490736; x=1732095536; h=content-transfer-encoding:to:subject:message-id:date:from :mime-version:x-gm-message-state:from:to:cc:subject:date:message-id :reply-to; bh=2pvC+xIVmj9alW98WoI2pV1o2wftAeZ/xCyuDtSwEM0=; b=I9asMmu0/QV9oPxvCH1HLvORhzRczohGlppSiHgPWSXV5jcNkniMEtK6OMRcP3FV5v 8UAT+IjX0FLYQ0rs1Bw3Vg+oArhjQAClnKakvlKCoiXR0oIT2i7S/r+bLEzbAkYmdMbx PPiDHNWCQ3Iib179bT1tOie9JxoJ0DU5Akt1NuyCAIEvW9CSHNObAU84d5KDyqYhdnM2 Jjsuo7hjRXKRizUbXVycDhqx2I03KDc+t9Tha9QjxTZR0txze5YUe2ApV2aExyD8tUeO pvjdnyuuoa8PWnmcWJGK8c3innTS2uhPlYpfIW2YGc9q0ZL9MEXxP0cWq18r9KjIRD5V KcDw== X-Gm-Message-State: AOJu0YwqPjMef5SccR5FxYkQnHMduGFXtfrQQZEGbNUlq/LmfZlYvuqI Gj8wTSXbgxG0CUhE6eXQkYN41ktEitCFsiWeshhYprSsiXY6aL71ABj2qajgnV3IBzA8YHoU+LD GbRLHnH7yxsH/pFP7/TYH5dFS0jQHP4e+9wqY0AE7BR1VXzj5be/923xsrtm6ElDEFtPP/kF8ix UCeM+gRBI0MkZlo5Rg0Svlpq49oYuE1Kyxu8mgnhGeYw7Fg8QS3aCTS4G4Bb+XPLz0iJtEuf/Mh lnLSQs8tqwD29X7eGCNCjH1ZLxKScBHe5DMhoMP6XaQsdWPYI+Ao4Kh93fff33GYw2gUGvX3guf HqajyvEUnwPPm3O3+6sa X-Google-Smtp-Source: AGHT+IHuUqJv3WB176b7ev0WUpu4EEFemb5EkMCe2tOBy/QGLv/A5Q5HgInYhoEyzywr+YZMmICJNLVMDQW7wMYgJpE= X-Received: by 2002:a17:906:4788:b0:a9e:c446:c284 with SMTP id a640c23a62f3a-aa1c57ef392mr605866566b.55.1731490736185; Wed, 13 Nov 2024 01:38:56 -0800 (PST) MIME-Version: 1.0 From: "aswift@mymail.tstc.edu" Date: Wed, 13 Nov 2024 17:37:00 +0800 Message-ID: Subject: =?UTF-8?Q?Re=3A_=5BCfP=5D_new_proof_assistant_for_schemes_=E2=80=94_The_to?= =?UTF-8?Q?pology_of_critical_processes=2C_II?= To: categories@mq.edu.au X-CLOUD-SEC-AV-Sent: true X-CLOUD-SEC-AV-Info: texasstatetechnicalcollege2,google_mail,monitor X-Gm-Spam: 0 X-Gm-Phishy: 0 X-Mimecast-Spam-Score: 1 X-Mimecast-MFC-PROC-ID: HTetUdD8zRDFbmjGhOERgIIGgUzfaYBIEzFy2ZLtloE_1731490737 X-Mimecast-Impersonation-Protect: Policy=MQ - Tag Header Only on Default Settings;Similar Internal Domain=false;Similar Monitored External Domain=false;Custom External Domain=false;Mimecast External Domain=false;Newly Observed Domain=false;Internal User Name=false;Custom Display Name List=false;Reply-to Address Mismatch=false;Targeted Threat Dictionary=false;Mimecast Threat Dictionary=false;Custom Threat Dictionary=false Content-Type: multipart/alternative; boundary="MCBoundary=_12411132039040511" X-EOPAttributedMessage: 0 X-EOPTenantAttributedMessage: 82c514c1-a717-4087-be06-d40d2070ad52:0 X-MS-Exchange-SkipListedInternetSender: ip=[209.85.218.65];domain=mail-ej1-f65.google.com X-MS-Exchange-ExternalOriginalInternetSender: ip=[209.85.218.65];domain=mail-ej1-f65.google.com X-MS-PublicTrafficType: Email X-MS-TrafficTypeDiagnostic: SY2PEPF00004FF2:EE_|SYBPR01MB5696:EE_|SYBPR01MB5789:EE_|MEYPR01MB6168:EE_ X-MS-Office365-Filtering-Correlation-Id: 52770e41-23db-49c4-ffed-08dd03c70429 X-Moderation-Data: 11/13/2024 9:41:45 AM X-LD-Processed: 82c514c1-a717-4087-be06-d40d2070ad52,ExtAddr,ExtAddr X-Auto-Response-Suppress: DR, RN, NRN, OOF, AutoReply X-MS-Exchange-CrossTenant-Network-Message-Id: 52770e41-23db-49c4-ffed-08dd03c70429 X-MS-Exchange-CrossTenant-Id: 82c514c1-a717-4087-be06-d40d2070ad52 X-MS-Exchange-CrossTenant-AuthSource: SY2PEPF00004FF2.ausprd01.prod.outlook.com X-MS-Exchange-CrossTenant-AuthAs: Anonymous X-MS-Exchange-CrossTenant-FromEntityHeader: Internet X-MS-Exchange-CrossTenant-OriginalArrivalTime: 13 Nov 2024 09:41:47.5505 (UTC) X-MS-Exchange-Transport-CrossTenantHeadersStamped: MEYPR01MB6168 X-MS-Exchange-UnifiedGroup-DisplayName: Categories mailing list X-MS-Exchange-UnifiedGroup-Address: categories@mq.edu.au X-MS-Exchange-UnifiedGroup-MailboxGuid: 9c2f954e-92a7-451b-b723-a07075d7adb5 X-MS-Exchange-UnifiedGroup-CustomizedMessage: RedeemedBusinessGuests X-MS-Exchange-Parent-Message-Id: Auto-Submitted: auto-generated X-MS-Exchange-Generated-Message-Source: Throttled Fork Delivery Agent X-OriginatorOrg: mq.edu.au --MCBoundary=_12411132039040511 Content-Type: text/plain; charset="utf-8" Content-Transfer-Encoding: quoted-printable ---------- Forwarded message --------- From: Christopher Mary CfP: A computational logic (coinductive) interface for schemes in algebraic geometry. [updated] https://github.com/1337777/cartier/blob/master/cartierSolution16.= lp This is the continuation of an ongoing research programme of discovering a truly computational logic (Lambdapi type theory) for categories, profunctors, fibred categories, univalence, polynomial functors, sites, sheaves and schemes, in the style of Kosta Dosen [1]. Firstly, a glue operation for any sheaf `S` over the sheafification modality `mod_smod` is declared: constant symbol glue : =CE=A0 [A B : cat] (A_site : site A) [S : smod A_site B] [I : cat] [G : func I B] (L : mod A I), transf L Id_func (smod_mod S) G =E2=86=92 transf (smod_mod (mod_smod A_site L)) Id_func (smod_mod S) G; >From which a glue operation for any sheaf `S` over the sieve-closure modality `sieve_ssieve` is defined, where `sieve` is the presheaf (profunctor =E2=80=A6) which classifies sieves: symbol glue_sieve_mod_def : =CE=A0 [A B : cat] (A_site : site A) [I : cat] [F : func I A] [S : smod A_site B] [G : func I B] [D : cat] [K : func I D] (ff : hom F (sieve A D) K), transf (sieve_mod ff) Id_func (smod_mod S) G) =E2=86=92 transf (smod_mod (ssieve_smod ((ff '=E2=88=98 (sieve_ssieve A_sit= e _))))) Id_func (smod_mod S) G =E2=89=94 glue =E2=80=A6; Now a transformation (predicate) into the sieves-classifier (truth-values) `sieve` corresponds to a subprofunctor (fibred/dependent profunctor), such as the maximal sieve or the intersection sieve, but also a novel =E2=80=9Csub sieve=E2=80=9D constructi= on. And when the sieve-closure `sieve_ssieve` happens to evaluate to the maximal sieve, then this glue operation is indeed the expected inverse operation of the Yoneda action by sieve-elements. In short: Nicolas Tabareau [2] is only a formalization of the semantics of sheafification, not an actual computational logic; and moreover, its Definition 5.2 causes flaws: instead of =E2=80=9Ca subobject of E is dense = in E if =E2=80=A6=E2=80=9D, it should be =E2=80=9Ca subobject P of E is dense = in another subobject Q of E if =E2=80=A6=E2=80=9D. Next, there are also (substructural) versions of this story in the presence of context: tensor-product context A=E2=8A=97B =E2=8A=A2 C, subtyp= e (sum type) context =CE=A3(a:A),P(a) =E2=8A=A2 C, and dependent-type context (x:A= )|B(x) =E2=8A=A2 C(x). It is not necessary to use multi-categories and hyperdoctrines (categories with families =E2=80=A6) to manage contexts, don=E2=80=99t be indoctrinated by Mikey [3] lol =E2=80=A6 Why? Because a question which is rarely entertained by logicians is: =E2=80=9CWho are my end-users?=E2=80=9D For dependent-type contexts, the answer lies in a (computational) implementation of the (usually semantic) context-extension operation: injective symbol Context_cat : =CE=A0 [X : cat], catd X =E2=86=92 cat; injective symbol Context_proj_func : =CE=A0 [X : cat] (A : catd X), func (Context_cat A) X; injective symbol Context_intro_func : =CE=A0 [Y : cat] [B : catd Y] [X : cat] (xy : func X Y), funcd (Terminal_catd X) xy B =E2=86=92 func X (Context_cat B); injective symbol Context_func : =CE=A0 [X Y : cat] [A : catd X] [B : catd Y] [xy : func X Y], funcd A xy B =E2=86=92 func (Context_cat A) (Context_ca= t B); For subtype contexts, the answer already lies in an implementation of sieves/subobject classifiers/universes as explained in the preceding paragraphs, and in the implementation of the Sigma-sum (along fibrations) and the Pi-product (along opfibrations =E2=80=A6) of fibred categories/profunctors (with beck-chevalley-commutation along fibres): injective symbol Sigma_catd : =CE=A0 [X : cat] (F : catd X) (Z : catd (Context_cat F)), catd X; injective symbol Sigma_elim_funcd : =CE=A0 [X : cat] (F : catd X) [Z : catd (Context_cat F)] [X'] (G : func X X') [C : catd X'], funcd Z ((Context_proj_func F) =E2=88=98> G) C =E2=86=92 funcd (Sigma_catd F Z) G C= ; injective symbol Pi_elim_funcd : =CE=A0 [X : cat] [F : catd X] [Z : catd (Context_cat F)] [X'] [x : func X' X] [E : catd X'], funcd E x (Pi_catd F Z) =E2=86=92 funcd (Fibre_catd E (Context_proj_func (Fibre_catd = F x))) (Context_func (Fibre_elim_funcd F x)) Z; For tensor-product contexts, the answer lies in reformulating the elimination rule for the tensor product in multi-categories which says: if a:A, b:B =E2=8A=A2 C then A=E2=8A=97B =E2=8A=A2 C. Each time that = this rule would be used, instead its intention can be simulated by the Lambdapi end-user by manually (via macros =E2=80=A6) adding a rewrite rule which outputs the intended body content of A=E2=8A=97B =E2=8A=A2 C when applied to a construc= tor =E2=9F=A8a, b=E2=9F=A9. In short: multi-categories are to help the dummy end-user. Next, the presentation of affine schemes is such that it exposes a logical interface/specification which computes; for example the structure sheaf `ascheme_mod_ring_loc` localized away from r : R has restrictions along D(s=E2=8B=85r) =E2=8A=86 D(r) (and, substructurally, alo= ng explicit radicals D(r) =E2=8A=86 D(r^n) =E2=80=A6) which compute (by the usual recas= ting of any sheaf element `f/r^n` as `(s^n)=E2=8B=85f/(s=E2=8B=85r)^n`): rule (@ascheme_mult_hom $Ml $Af _ $U $s $r) '=E2=88=98 (_) _'=E2=88=98> (ring_loc_intro (ascheme_mod_ring_loc $Af $r) $f $n) =E2=86=AA ring_loc_intro (ascheme_mod_ring_loc $Af (ring_mult (mod_loc_ring $Ml $U) $s $r)) (ring_mult (mod_loc_ring $Ml $U) (ring_exp (mod_loc_ring $Ml $U) $s $n) $f) $n; And similar computations have been implemented for formal (colimits) joins D(f)=E2=88=A8D(g) of basic opens. But Joyal=E2=80=99s covering axiom = D(s+r) =E2=8A=86 D(s)=E2=88=AAD(r) of the basic open D(s+r), has been reformulated approximately as a cover by the inclusions D(s=E2=8B=85=E2=88=9A(a=E2=8B=85= s + b=E2=8B=85r)) =E2=8A=86 D(=E2=88=9A(a=E2=8B=85s + b=E2=8B=85r)) (similarly for r) such to simultaneously also handle the unimodular (that is, =E2=9F=A8r, s=E2=9F=A9 =3D 1) cover of a basic open. B= y the way, this functorial double-category framework is justified even for (the limit of) any functor (diagram) of rings, rather than a single ring, because localization is left-exact =E2=80=A6 Then, there is an implementation of locally ringed sites and schemes. But the traditional definition of schemes via isomorphisms to affine schemes won=E2=80=99t work computationally; instead, one has to declare tha= t the slice-category sites of the base site satisfy the interface/specification of an affine scheme. But what is a slice-category site? How does its glue operation relate to the glue operation of the base site? This has required subtle reformulations of a continuous(-and-cocontinuous) morphism of sites with a continuous right adjoint [4] (with =E2=80=9Ctechnical lemma 7.20.4 00XM=E2=80=9D): rule site_morph_mod_adjL $Sm $R (glue $r_) =E2=86=AA glue (adj_mod_adjL (site_morph_adj $Sm) (smod_mod $R) $r_); But then, what is the invertibility-support D(=E2=80=93) for a locally ring= ed site and how does it relate to each affine-scheme=E2=80=99s invertibility-support D(=E2=80=93) in the slice-categories. The author of cartierSolution16.lp claims that D(f) is intended to be the SIEVE (generated by a singleton when restricted to a slice affine-scheme =E2=80= =A6) under U of all opens V where the restriction of the function f: O(U) becomes invertible, together with (a computational reformulation of) the limit condition: lim_{V:D(f)} O(V) =3D O(U)[1/f] In short, some structured data is being transferred from a base scheme to its slice-categories where they are required to satisfy the affine-scheme interface. Moreover, the affine-scheme interface is coinductive (self-reference), meaning that its slice-categories are also required to satisfy the affine-scheme interface. This slice coinduction/self-reference is deeply intrinsic and unavoidable; so that all the constructions are always relativized (in the slice-category under an object). That is, even the affine-scheme invertibility-support D(=E2=80=93) constructors `ascheme_inv_slice_func`, which are the basic objects which generate the topology, are also relativized by-definition: constant symbol ascheme_inv_slice_func : =CE=A0 [Ml : struct_mod_loc] (Af : ascheme Ml), =CE=A0 [I] [U : func I (mod_loc_cat Ml)] (r : hom U (smod_mod (mod_loc_smod Ml)) (Terminal_func _)), func I (slice_cat U); constant symbol scheme_slice_ascheme : =CE=A0 [Ml : struct_mod_loc] [Cs : struct_cov_sieve (mod_loc_site Ml)] (Sc : scheme Ml Cs), =CE=A0 [U : func (cov_sieve_cat Cs) (mod_loc_cat Ml)] (u : hom U (sieve_mod (cov_sieve_hom Cs)) Id_func), ascheme (@Struct_mod_loc (slice_cat U) (slice_site (mod_loc_site Ml) U) (site_morph_pullback_smod (scheme_site_morph Sc U) (mod_loc_smod Ml)) (mod_pullb_mod_ring (mod_loc_mod_ring Ml) (slice_proj_func U)) (mod_pullb_mod_loc (mod_loc_mod_loc Ml) (slice_proj_func U))); A consequence of this formulation is that these various structure sheaves are now canonically related, beyond the mere usual knowledge that for any ring `R`: R[1/fg] =E2=89=85 R[1/f][1/g] MAX [5] recently defended an equivalence between functorial schemes `X` and locally-ringed-lattice schemes `Y`, approximately: LRDL^op( X =E2=87=92 Spec , Y ) =E2=89=85 ( X =E2=87=92 LRDL^op( Spec( =E2= =80=93 ), Y ) ) where ( X =E2=87=92 X' ) =E2=88=B6=3D Fun( CommRing , Set )( X , X' ) and S= pec: Fun( CommRing^op, LRDL^op ). But the author of cartierSolution16.lp claims that their profunctor framework should allow a hybrid handling of schemes as locally ringed sites together with their functor-of-points semantics. And most importantly, it is not necessary to try and express those things using an internal logic (not truly-computational =E2=80=A6) within the Zarisky topos, in the style of Thierry Coquand [6]. Ultimately, it is a conjecture that this new framework could solve the open problem of discovering a (graded) differential linear logic formulation for the algebraic-geometry=E2=80=99s cohomology differentials v= ia the profunctorial semantics of linear logic in the context of sieves as profunctors=E2=80=A6 It is also a conjecture that this new framework could solve the search of a hybrid framework=E2=8B=85 combining polynomial functors (good algebra) =E2=80=9Cdepending=E2=80=9D on analytic functors (good logic) as motivated = by Ehrhard=E2=80=99s [7, section 3.1.1, page 44] outrageous definition of the composition of polynomials by the use of differentials instead of by elementary algebra. Another open question: would such an algebra-independent computational-logical interface for commutative (affine) schemes be able to also specify schemes of (noncommutative) associative algebras; for example, in the sense of Siqveland Arvid [8]? But wait, here is a down-to-Earth-fresh-air sanity-check challenge (=E2=80=9Ccontexte et pr=C3=A9alables d=E2=80=99un d=C3=A9bat=E2=80=9D) for= =E2=88=9E-cosmonauts who may be =E2=80=9Coffended=E2=80=9D/arguing in the vacuum against the preceding para= graphs, lol =E2=80=A6 https://github.com/1337777/cartier/blob/master/cartierSolution14.lp https://github.com/1337777/cartier/blob/master/Kosta_Dosen_2pages.pdf where this author shows that 1+2=3D3 via 3 different methods: the category of natural-numbers as a higher inductive type; the natural-numbers object inside any fixed category; and the colimits inside the category of finite sets/numbers. Indeed, this new functorial programming language, also referred as Dosen=E2=80=99s =C2=AB m=E2=80=94 =C2=BB or =C2=AB emdash =C2=BB or =C2=AB = modos =C2=BB, is able to express the usual logic such as the tensor and internal-hom of profunctors, the sigma-sum and pi-product of fibred categories/profunctors; but is also able to express the concrete and inductively-constructed categories/profunctors, to express the adjunctions such as the product-and-exponential or the constant-diagram-and-limit adjunctions within any fixed category, to express contravariance and duality such as a computational-proof that right-adjoints preserve limits from the dual statement, to express groupoids and univalent universes, to express polynomial functors as bicomodules in the double category of categories, functors, cofunctors and profunctors, etc=E2=80=A6 Such a multi-year research programme requires new tools and frameworks to articulate the speedy circulation of (papers/apps) reviews as a currency; and as for any currency, to articulate the unavoidable questions of =E2=80=9Ctheft=E2=80=9D, =E2=80=9Cfalsification=E2=80=9D, =E2= =80=9Cintoxication=E2=80=9D, =E2=80=9Cassault=E2=80=9D beyond the traditional context of a cash-bank-robbery-by-a-gang =E2=80=A6 An attempt at such a new platform/marketplace is this author=E2=80=99s =C2= =AB re365.net =C2=BB open-source Microsoft 365 app, developed by a community of 3,000+ contributors [9], which is a tiktok-style AI-assisted calendar overlay to standardize the contacting of (VIP) researchers/businesses by reviewers whose side-goals are to co-author or by-product more intelligent (AI) interfaces for their papers/apps API. [1] Kosta Dosen. =E2=80=9CCut-elimination in categories=E2=80=9D [2] Nicolas Tabareau. =E2=80=9CLawvere-Tierney sheafification in homotopy t= ype theory=E2=80=9D [3] Mikey. =E2=80=9CCategorical logic from a categorical point of view (for= dummies)=E2=80=9D [4] The Stacks Project. =E2=80=9CSection 7.22 00XW: Cocontinuous functors which have a right adjoint=E2=80=9D [5] MAX Zeuner. =E2=80=9CUnivalent Foundations of Constructive Algebraic Ge= ometry=E2=80=9D [6] Thierry Coquand. =E2=80=9CA foundation for synthetic algebraic geometry= =E2=80=9D [7] Thomas Ehrhard. =E2=80=9CAn introduction to differential linear logic: proof-nets, models and antiderivatives=E2=80=9D [8] Siqveland Arvid. =E2=80=9CSchemes of Associative algebras=E2=80=9D [9] < https://meetup.com/dubai-ai > < https://dailyReviews.lin= k > You're receiving this message because you're a member of the Categories mai= ling list group from Macquarie University. To take part in this conversatio= n, reply all to this message. View group files | Leave group | = Learn more about Microsoft 365 Groups --MCBoundary=_12411132039040511 Content-Transfer-Encoding: quoted-printable Content-Type: text/html; charset=UTF-8 ---------- Forwarded message ---------
From: Christopher Mary <admin@anthroplogic.onmicrosoft.com>


CfP: A computational logic (coinductive) interface for schemes in
algebraic geometry.

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

This is the continuation of an ongoing research programme of
discovering a truly computational logic (Lambdapi type theory) for
categories, profunctors, fibred categories, univalence, polynomial
functors, sites, sheaves and schemes, in the style of Kosta Dosen [1].

Firstly, a glue operation for any sheaf `S` over the sheafification
modality `mod_smod` is declared:

constant symbol glue : =CE=A0 [A B : cat] (A_site : site A) [S : smod
A_site B] [I : cat] [G : func I B] (L : mod A I),
transf L Id_func (smod_mod S) G
=E2=86=92 transf (smod_mod (mod_smod A_site L)) Id_func (smod_mod S) G;

>From which a glue operation for any sheaf `S` over the sieve-closure
modality `sieve_ssieve` is defined, where `sieve` is the presheaf
(profunctor =E2=80=A6) which classifies sieves:

symbol glue_sieve_mod_def : =CE=A0 [A B : cat] (A_site : site A) [I :
cat] [F : func I A] [S : smod A_site B] [G : func I B] [D : cat] [K
: func I D] (ff : hom F (sieve A D) K),
transf (sieve_mod ff) Id_func (smod_mod S) G)
=E2=86=92 transf (smod_mod (ssieve_smod ((ff '=E2=88=98 (sieve_ssieve A_sit= e _)))))
Id_func (smod_mod S) G =E2=89=94 glue =E2=80=A6;

Now a transformation (predicate) into the sieves-classifier
(truth-values) `sieve` corresponds to a subprofunctor
(fibred/dependent profunctor), such as the maximal sieve or the
intersection sieve, but also a novel =E2=80=9Csub sieve=E2=80=9D constructi= on.

And when the sieve-closure `sieve_ssieve` happens to evaluate to the
maximal sieve, then this glue operation is indeed the expected inverse
operation of the Yoneda action by sieve-elements. In short: Nicolas
Tabareau [2] is only a formalization of the semantics of
sheafification, not an actual computational logic; and moreover, its
Definition 5.2 causes flaws: instead of =E2=80=9Ca subobject of E is dense = in
E if =E2=80=A6=E2=80=9D, it should be =E2=80=9Ca subobject P of E is dense = in another
subobject Q of E if =E2=80=A6=E2=80=9D.

Next, there are also (substructural) versions of this story in the
presence of context: tensor-product context A=E2=8A=97B =E2=8A=A2 C, subtyp= e (sum
type) context =CE=A3(a:A),P(a) =E2=8A=A2 C, and dependent-type context (x:A= )|B(x) =E2=8A=A2
C(x). It is not necessary to use multi-categories and hyperdoctrines
(categories with families =E2=80=A6) to manage contexts, don=E2=80=99t be indoctrinated by Mikey [3] lol =E2=80=A6 Why? Because a question which is rarely entertained by logicians is:

=E2=80=9CWho are my end-users?=E2=80=9D

For dependent-type contexts, the answer lies in a (computational)
implementation of the (usually semantic) context-extension operation:

injective symbol Context_cat : =CE=A0 [X : cat], catd X =E2=86=92 cat;
injective symbol Context_proj_func : =CE=A0 [X : cat] (A : catd X), func (Context_cat A) X;
injective symbol Context_intro_func : =CE=A0 [Y : cat] [B : catd Y] [X : cat] (xy : func X Y), funcd (Terminal_catd X) xy B =E2=86=92 func X
(Context_cat B);
injective symbol Context_func : =CE=A0 [X Y : cat] [A : catd X] [B : catd Y] [xy : func X Y], funcd A xy B =E2=86=92 func (Context_cat A) (Context_ca= t
B);

For subtype contexts, the answer already lies in an implementation of
sieves/subobject classifiers/universes as explained in the preceding
paragraphs, and in the implementation of the Sigma-sum (along
fibrations) and the Pi-product (along opfibrations =E2=80=A6) of fibred
categories/profunctors (with beck-chevalley-commutation along fibres):

injective symbol Sigma_catd : =CE=A0 [X : cat] (F : catd X) (Z : catd
(Context_cat F)), catd X;
injective symbol Sigma_elim_funcd : =CE=A0 [X : cat] (F : catd X) [Z : catd=
(Context_cat F)] [X'] (G : func X X') [C : catd X'], funcd Z
((Context_proj_func F) =E2=88=98> G) C =E2=86=92 funcd (Sigma_catd F Z) = G C;
injective symbol Pi_elim_funcd : =CE=A0 [X : cat] [F : catd X] [Z : catd (Context_cat F)] [X'] [x : func X' X] [E : catd X'], funcd E x
(Pi_catd F Z) =E2=86=92 funcd (Fibre_catd E (Context_proj_func (Fibre_catd = F
x))) (Context_func (Fibre_elim_funcd F x)) Z;

For tensor-product contexts, the answer lies in reformulating the
elimination rule for the tensor product in multi-categories which
says: if a:A, b:B =E2=8A=A2 C then A=E2=8A=97B =E2=8A=A2 C. Each time that = this rule would be
used, instead its intention can be simulated by the Lambdapi end-user
by manually (via macros =E2=80=A6) adding a rewrite rule which outputs the<= br> intended body content of A=E2=8A=97B =E2=8A=A2 C when applied to a construc= tor =E2=9F=A8a, b=E2=9F=A9.
In short: multi-categories are to help the dummy end-user.

Next, the presentation of affine schemes is such that it exposes a
logical interface/specification which computes; for example the
structure sheaf `ascheme_mod_ring_loc` localized away from r : R has
restrictions along D(s=E2=8B=85r) =E2=8A=86 D(r) (and, substructurally, alo= ng explicit
radicals D(r) =E2=8A=86 D(r^n) =E2=80=A6) which compute (by the usual recas= ting of any
sheaf element `f/r^n` as `(s^n)=E2=8B=85f/(s=E2=8B=85r)^n`):

rule (@ascheme_mult_hom $Ml $Af _ $U $s $r) '=E2=88=98 (_) _'=E2=88=98><= br> (ring_loc_intro (ascheme_mod_ring_loc $Af $r) $f $n)
=E2=86=AA ring_loc_intro (ascheme_mod_ring_loc $Af (ring_mult (mod_loc_ring=
$Ml $U) $s $r)) (ring_mult (mod_loc_ring $Ml $U) (ring_exp
(mod_loc_ring $Ml $U) $s $n) $f) $n;

And similar computations have been implemented for formal (colimits)
joins D(f)=E2=88=A8D(g) of basic opens. But Joyal=E2=80=99s covering axiom = D(s+r) =E2=8A=86
D(s)=E2=88=AAD(r) of the basic open D(s+r), has been reformulated
approximately as a cover by the inclusions D(s=E2=8B=85=E2=88=9A(a=E2=8B=85= s + b=E2=8B=85r)) =E2=8A=86 D(=E2=88=9A(a=E2=8B=85s
+ b=E2=8B=85r)) (similarly for r) such to simultaneously also handle the unimodular (that is, =E2=9F=A8r, s=E2=9F=A9 =3D 1) cover of a basic open. B= y the way,
this functorial double-category framework is justified even for (the
limit of) any functor (diagram) of rings, rather than a single ring,
because localization is left-exact =E2=80=A6

Then, there is an implementation of locally ringed sites and schemes.
But the traditional definition of schemes via isomorphisms to affine
schemes won=E2=80=99t work computationally; instead, one has to declare tha= t
the slice-category sites of the base site satisfy the
interface/specification of an affine scheme. But what is a
slice-category site? How does its glue operation relate to the glue
operation of the base site? This has required subtle reformulations of
a continuous(-and-cocontinuous) morphism of sites with a continuous
right adjoint [4] (with =E2=80=9Ctechnical lemma 7.20.4 00XM=E2=80=9D):

rule site_morph_mod_adjL $Sm $R (glue $r_)
=E2=86=AA glue (adj_mod_adjL (site_morph_adj $Sm) (smod_mod $R) $r_);

But then, what is the invertibility-support D(=E2=80=93) for a locally ring= ed
site and how does it relate to each affine-scheme=E2=80=99s
invertibility-support D(=E2=80=93) in the slice-categories. The author of cartierSolution16.lp claims that D(f) is intended to be the SIEVE
(generated by a singleton when restricted to a slice affine-scheme =E2=80= =A6)
under U of all opens V where the restriction of the function f: O(U)
becomes invertible, together with (a computational reformulation of)
the limit condition:

lim_{V:D(f)} O(V) =3D O(U)[1/f]

In short, some structured data is being transferred from a base scheme
to its slice-categories where they are required to satisfy the
affine-scheme interface.

Moreover, the affine-scheme interface is coinductive (self-reference),
meaning that its slice-categories are also required to satisfy the
affine-scheme interface. This slice coinduction/self-reference is
deeply intrinsic and unavoidable; so that all the constructions are
always relativized (in the slice-category under an object). That is,
even the affine-scheme invertibility-support D(=E2=80=93) constructors
`ascheme_inv_slice_func`, which are the basic objects which generate
the topology, are also relativized by-definition:

constant symbol ascheme_inv_slice_func : =CE=A0 [Ml : struct_mod_loc]
(Af : ascheme Ml), =CE=A0 [I] [U : func I (mod_loc_cat Ml)] (r : hom U
(smod_mod (mod_loc_smod Ml)) (Terminal_func _)), func I (slice_cat U);

constant symbol scheme_slice_ascheme : =CE=A0 [Ml : struct_mod_loc] [Cs
: struct_cov_sieve (mod_loc_site Ml)] (Sc : scheme Ml Cs), =CE=A0 [U : func=
(cov_sieve_cat Cs) (mod_loc_cat Ml)] (u : hom U (sieve_mod
(cov_sieve_hom Cs)) Id_func),
ascheme (@Struct_mod_loc (slice_cat U) (slice_site (mod_loc_site Ml) U)
(site_morph_pullback_smod (scheme_site_morph Sc U) (mod_loc_smod Ml))
(mod_pullb_mod_ring (mod_loc_mod_ring Ml) (slice_proj_func U))
(mod_pullb_mod_loc (mod_loc_mod_loc Ml) (slice_proj_func U)));

A consequence of this formulation is that these various structure
sheaves are now canonically related, beyond the mere usual knowledge
that for any ring `R`:

R[1/fg] =E2=89=85 R[1/f][1/g]

MAX [5] recently defended an equivalence between functorial schemes
`X` and locally-ringed-lattice schemes `Y`, approximately:

LRDL^op( X =E2=87=92 Spec , Y ) =E2=89=85 ( X =E2=87=92 LRDL^op( Spec( =E2= =80=93 ), Y ) )

where ( X =E2=87=92 X' ) =E2=88=B6=3D Fun( CommRing , Set )( X , X' ) and S= pec: Fun(
CommRing^op, LRDL^op ). But the author of cartierSolution16.lp claims
that their profunctor framework should allow a hybrid handling of
schemes as locally ringed sites together with their functor-of-points
semantics. And most importantly, it is not necessary to try and
express those things using an internal logic (not truly-computational
=E2=80=A6) within the Zarisky topos, in the style of Thierry Coquand [6].
Ultimately, it is a conjecture that this new framework could solve the
open problem of discovering a (graded) differential linear logic
formulation for the algebraic-geometry=E2=80=99s cohomology differentials v= ia
the profunctorial semantics of linear logic in the context of sieves
as profunctors=E2=80=A6

It is also a conjecture that this new framework could solve the search
of a hybrid framework=E2=8B=85 combining polynomial functors (good algebra)=
=E2=80=9Cdepending=E2=80=9D on analytic functors (good logic) as motivated = by
Ehrhard=E2=80=99s [7, section 3.1.1, page 44] outrageous definition of the<= br> composition of polynomials by the use of differentials instead of by
elementary algebra.

Another open question: would such an algebra-independent
computational-logical interface for commutative (affine) schemes be
able to also specify schemes of (noncommutative) associative algebras;
for example, in the sense of Siqveland Arvid [8]?

But wait, here is a down-to-Earth-fresh-air sanity-check challenge
(=E2=80=9Ccontexte et pr=C3=A9alables d=E2=80=99un d=C3=A9bat=E2=80=9D) for= =E2=88=9E-cosmonauts who may be
=E2=80=9Coffended=E2=80=9D/arguing in the vacuum against the preceding para= graphs, lol
=E2=80=A6

https://github.com/1337777/cartier/blob/master/cartierSolution14.lp
https://github.com/1337777/cartier/blob/master/Kosta_Dosen_2pages.pdf

where this author shows that 1+2=3D3 via 3 different methods: the
category of natural-numbers as a higher inductive type; the
natural-numbers object inside any fixed category; and the colimits
inside the category of finite sets/numbers.

Indeed, this new functorial programming language, also referred as
Dosen=E2=80=99s =C2=AB m=E2=80=94 =C2=BB or =C2=AB emdash =C2=BB or =C2=AB = modos =C2=BB, is able to express the
usual logic such as the tensor and internal-hom of profunctors, the
sigma-sum and pi-product of fibred categories/profunctors; but is also
able to express the concrete and inductively-constructed
categories/profunctors, to express the adjunctions such as the
product-and-exponential or the constant-diagram-and-limit adjunctions
within any fixed category, to express contravariance and duality such
as a computational-proof that right-adjoints preserve limits from the
dual statement, to express groupoids and univalent universes, to
express polynomial functors as bicomodules in the double category of
categories, functors, cofunctors and profunctors, etc=E2=80=A6

Such a multi-year research programme requires new tools and frameworks
to articulate the speedy circulation of (papers/apps) reviews as a
currency; and as for any currency, to articulate the unavoidable
questions of =E2=80=9Ctheft=E2=80=9D, =E2=80=9Cfalsification=E2=80=9D, =E2= =80=9Cintoxication=E2=80=9D, =E2=80=9Cassault=E2=80=9D
beyond the traditional context of a cash-bank-robbery-by-a-gang =E2=80=A6
An attempt at such a new platform/marketplace is this author=E2=80=99s =C2= =AB
re365.net =C2=BB open-source Microsoft 365 app, developed by a community of=
3,000+ contributors [9], which is a tiktok-style AI-assisted calendar
overlay to standardize the contacting of (VIP) researchers/businesses
by reviewers whose side-goals are to co-author or by-product more
intelligent (AI) interfaces for their papers/apps API.


[1] Kosta Dosen. =E2=80=9CCut-elimination in categories=E2=80=9D
[2] Nicolas Tabareau. =E2=80=9CLawvere-Tierney sheafification in homotopy t= ype theory=E2=80=9D
[3] Mikey. =E2=80=9CCategorical logic from a categorical point of view (for= dummies)=E2=80=9D
[4] The Stacks Project. =E2=80=9CSection 7.22 00XW: Cocontinuous functors which have a right adjoint=E2=80=9D
[5] MAX Zeuner. =E2=80=9CUnivalent Foundations of Constructive Algebraic Ge= ometry=E2=80=9D
[6] Thierry Coquand. =E2=80=9CA foundation for synthetic algebraic geometry= =E2=80=9D
[7] Thomas Ehrhard. =E2=80=9CAn introduction to differential linear logic:<= br> proof-nets, models and antiderivatives=E2=80=9D
[8] Siqveland Arvid. =E2=80=9CSchemes of Associative algebras=E2=80=9D
[9] < https://meetup.com/dubai-ai > < https://dailyReviews.link >
 
 
You're receiving this message because you're a member of the Categories mai= ling list group from Macquarie University. To take part in this conversatio= n, reply all to this message.
 
View group files   |   Leav= e group   |&n= bsp;  Learn more about Microsoft 365 Groups
 
--MCBoundary=_12411132039040511--