Pith. sign in

REVIEW 4 major objections 5 minor 1 cited by

Generation of Grothendieck topologies, provability and operations on subtoposes

T0 review · 4 major / 5 minor · reviewed 2026-08-05 · deepseek-v4-flash

Pith's one-line read Pulling back subtoposes along any geometric morphism preserves finite unions, and along locally connected morphisms arbitrary unions; the paper proves this with explicit formulas for generated Grothendieck topologies.

desk verdict A serious systematic monograph with real new formulas, but the headline finite-union preservation theorem depends on a deferred factorization proof that isn't in the visible text. read the letter →

arxiv 2508.21134 v1 pith:KB4PAWK4 submitted 2025-08-28 math.CT math.AGmath.LO

classification math.CTmath.AGmath.LO MSC 18B2518F1003G30
keywords GrothendiecktopologiessubtoposesgenerationofgeometriclogicprovabilitylocallyconnectedmorphismsGaloisconnectionsclassifyingtoposes
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

This monograph builds a systematic calculus for subtoposes, the topos-level analogue of subspaces. The paper's central move is to treat a subtopos as equivalently a Grothendieck topology on any presenting site or a quotient of any presenting geometric theory, and to derive that duality — not assume it — as the fixed points of a Galois connection between sieves and presheaves. This turns provability in first-order geometric logic into a problem of generating topologies, for which the paper gives two explicit formulas. The central new claim is that pulling subtoposes back along any geometric morphism preserves finite unions, and that pullback along locally connected morphisms preserves arbitrary unions, making the lattice of subtoposes behave predictably under all geometric operations. If correct, these results make subtopos computations effective: joins, intersections and differences of subtoposes can be read off from formulas rather than built step by step.

What carries the argument

Three pieces carry the argument. A Galois connection between sieves and presheaves — with an intrinsic version between monomorphisms and objects of a topos — has fixed points that are exactly the Grothendieck topologies and the subtoposes, and generating a topology is the composite of its two adjoints. Two generation formulas compute generated topologies: a closed sieve-closure formula for pullback-stable families, and a multi-cover tree formula whose pullback-stability removes the need for transfinite iteration. For the union theorems: the adjunction f^{-1} ⊣ f_* between subtopos lattices induced by a geometric morphism, the left adjoint f_! ('extraordinary direct image') existing precisely

What would settle it

Test the identity on a small explicit site: take a functor between finite categories (for the locally connected case, a fibration with a Giraud topology) and two topologies on the target; compute the pullback of the intersection of the topologies and the intersection of the pullbacks using the Chapter IV formulas. If they differ, finite-union preservation is false; likewise for an infinite family along a locally connected morphism. Alternatively, test the closed generation formula: for a pullback-stable family of sieves on a small category, a sieve belongs to the generated topology exactly whe

Watch

Extended reading notes

Core claim

A subtopos is equivalently a Grothendieck topology on any presenting site or a quotient of any presenting geometric theory; the paper derives this duality, rather than postulating it, as the fixed points of a Galois connection between sieves and presheaves. Two explicit formulas compute generated topologies: a closed form for pullback-stable families, and a tree-based multi-cover formula avoiding transfinite iteration. The inverse-image operation on subtoposes preserves all intersections, preserves finite unions for every geometric morphism, and preserves arbitrary unions when the morphism is locally connected, via a left adjoint 'extraordinary direct image' and a factorization of any morphi

Load-bearing premise

The whole argument for arbitrary morphisms depends on one factorization theorem: every geometric morphism can be written as an inclusion followed by a locally connected morphism, where the locally connected part itself rests on the stability (Beck–Chevalley) condition built into its definition; without that factorization, finite-union preservation is only proven for the two special cases separately.

Editorial extensions

If this is right

  • Provability in geometric logic becomes a closure computation: a sequent is provable from a family of axioms exactly when the associated sieve families are covering for the topology those axioms generate, so the closed generation formula makes the pullback-stable cases explicit and finite.
  • Subtopos joins commute with inverse images: finite joins along every geometric morphism, arbitrary joins along locally connected ones; consequently every action of a topos-theoretic correspondence or chain on subtoposes, being a composite of direct and inverse images, preserves finite unions.
  • The multi-cover tree formula generates topologies without transfinite iteration, settling a point on which the standard treatise had left transfinite induction seemingly unavoidable.
  • Topologies presenting a finite product of sheaf toposes are exactly those generated by the pullbacks of the presenting topologies along the canonical projections; the generation formula therefore computes finite products of toposes, and when the factors are sheaf toposes of locally compact spaces (all but possibly one) the sheaf topos of the product space is the product of the sheaf toposes.
  • Along locally connected morphisms the inverse image of subtoposes acquires a left adjoint, the extraordinary direct image, which preserves arbitrary intersections of subtoposes and adds a new adjoint layer to the calculus of subtopos operations.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • The factorization template — prove a subtopos identity for locally connected morphisms and for inclusions, then extend to all morphisms — could promote further identities, for instance the behaviour of the co-Heyting difference operation under pullback, from the locally connected case to arbitrary geometric morphisms; the paper only applies this template to unions.
  • The paper notes that the closed formula suits sieve presentations (typical of logical contexts such as the dense or De Morgan topologies) while the multi-cover formula suits pre-cover presentations (typical of geometric contexts such as Zariski or étale); a natural testable project is an automated provability checker that switches between the two depending on the site.
  • The preface announces that oriented and fibred products of toposes will be treated in a future version using these methods; if the same generation formulas control those products, the union-preservation theorems should transfer by the same adjunction argument.
  • If data elements are represented as subtoposes rather than vectors, as the preface contemplates, the union-preservation theorems imply that the operation combining data-points commutes with any morphism that changes representation — the topos-level analogue of a linear map commuting with vector addition, and a condition one could test in a concrete representation-learning setting.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

4 major / 5 minor

Summary. The paper develops a systematic account of subtoposes of Grothendieck toposes through Galois connections between sieves and presheaves, monomorphisms and objects, and sieves and subpresheaf embeddings. It claims to derive, as fixed points of these connections, the equivalences between Grothendieck topologies and subtoposes and between topologies and theories, and to obtain explicit formulas for the topology generated by a family of sieves or covering families. It further studies Heyting operations on subtoposes and direct/inverse image operations, and states two preservation theorems: inverse image of subtoposes preserves finite unions along any geometric morphism, and arbitrary unions along locally connected morphisms. The visible text contains the preface, Chapter I and part of Chapter II; the announced Chapter III and Chapter IV are largely not present, and several key statements are only backed by sketches or deferred proofs.

Significance. If the full proofs are supplied, the paper would make a useful contribution: the Galois-connection framework is elegant and likely to clarify structural relationships among topologies, subpresheaves, and subtoposes; the closed formula for generated topologies and the bridge between provability and topology generation have potential applications to logical and geometric computations. The claimed preservation of finite unions by arbitrary inverse image functors is a natural and potentially useful new result. The paper draws on substantial prior work ([TST], [Local fibrations], [Denseness]); the novelty lies mostly in the uniform framework and in the new generation and preservation formulas. However, the present text is not self-contained enough for the main claims to be certified from what is supplied.

major comments (4)
  1. [Chapter I, Corollary I.3.20] The finite-union preservation claim is proved only by deferral: "On rappellera en effet au chapitre IV que tout morphisme de topos peut s'écrire comme le composé d'un plongement et d'un morphisme localement connexe." This factorization is load-bearing and is not proved in the visible text, nor is a reference given. The standard surjection/embedding factorization does not generally make the first factor locally connected, so this cannot be treated as folklore. The proof of Corollary I.3.20 must either include a complete proof of the factorization or cite a precise theorem with proof in the literature.
  2. [Chapter I, §3.f, Theorem I.3.16] The existence of an extra left adjoint f_! for inverse image of subtoposes along a locally connected morphism, and hence preservation of arbitrary unions, is announced as a Chapter IV result but is not proved in the supplied text. Since this theorem is used for the finite-union claim, it is essential that the manuscript contain a full proof, not merely a sketch or a forward reference.
  3. [Chapters III and IV (not included in the supplied text)] The paper’s central new contributions are the closed generation formula for topologies (Chapter III, §1), the tree/multi-covering formula (Chapter III, §2), and the detailed treatment of inverse images along locally connected morphisms (Chapter IV). None of these chapters appears in the text supplied for review. The abstract and preface cannot substitute for the actual proofs. The manuscript must be re-submitted with the full chapters, or, if this is a partial submission, the missing material must be added or a complete version declared.
  4. [Chapter I, §2.c, Proposition I.2.13] The bridge between quotient theories and topologies, used in the translation of provability into topology generation, is presented with only sketches ("Esquisse de démonstration") for points (i)–(iv). Some of this is based on [TST], but if the presentation is meant to be new, the inference rules of geometric logic must be explicitly matched with the axioms of a topology; a sketch is not enough for a central logical equivalence used in the paper.
minor comments (5)
  1. [General] Several displayed formulas contain typographical artifacts, especially in Definition I.1.1 and the surrounding braces; these should be cleaned up in the final version.
  2. [Chapter I, §3.a] The order convention on ST(E) is stated only implicitly; since union and intersection are order-reversing with respect to the topology inclusion, the direction of the order should be explicitly fixed to avoid confusion.
  3. [Chapter II, §2] The phrase "dualité des cribles et des préfaisceaux" is helpful, but the notation R, F_R, G_R becomes heavy; a small table of notation would improve readability.
  4. [Preface] The preface promises applications to "apprentissage profond topossique" but the visible text does not return to this; if these applications are not developed, the promise should be toned down or the applications deferred explicitly.
  5. [References] The paper cites [Local fibrations], [Denseness], and [TST] for crucial background. Full bibliographic details should be listed and, for the factorization theorem used in Ch. IV, a precise statement with proof should be supplied.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the central derivations are self-contained or rest on independently proved prior theorems; the deferred factorization is a proof-completeness concern, not circular.

full rationale

The paper's load-bearing equivalences (subtoposes ↔ Grothendieck topologies ↔ quotient theories) are either reproved via the Galois connections of Chapter II or cited to [TST], where they are established with proofs; they are not assumed as the conclusions being derived. The generation formula of Chapter III is derived from the closure operator G(F(J)) and from Lemma I.3.5, not identified with its own statement. The provability translation (Cor I.2.15) uses the classifying-topos semantics and the relation between quotient theories and topologies; although the syntactic topology is defined using provability, the corollary concerns arbitrary sites and is not a mere restatement. The finite-union preservation result (Cor I.3.20) is obtained formally from adjunction facts plus a factorization theorem (embedding followed by locally connected morphism) deferred to Chapter IV section 2c. That factorization is not visible in the excerpt and is a genuine prior-work reliance, but it is not an assumption of the conclusion: the conclusion would follow if the factorization holds. Self-citations to [TST], [Denseness] and [Local fibrations] are normal prior-work citations, not circularity, since none reduces the new theorems to the same theorem being proved.

Assumptions & free parameters 0 free parameters · 5 assumptions · 0 invented entities

The central claims rest on standard Grothendieck topos theory plus two domain-specific assumptions: the authors' earlier bridge theory and the factorization theorem for geometric morphisms. No free parameters or invented entities are introduced.

assumptions (5)
  • standard math Standard axioms of a Grothendieck topos: small sites, sheafification, local smallness, Giraud's characterization.
    Invoked throughout Chapter I as the background framework for toposes and sites (Definition I.1.3, Theorem I.1.7).
  • standard math Giraud's and Diaconescu's theorems characterizing Grothendieck toposes and geometric morphisms.
    Used to identify toposes with categories of sheaves and to classify geometric morphisms by flat continuous functors (Theorem I.1.23).
  • domain assumption The bridge equivalences from the authors' earlier book [TST] between subtoposes, Grothendieck topologies, and quotient theories.
    Used as the starting point in Chapter I, sections 2 and 3; these equivalences are proved in [TST] (e.g., Theorem I.2.10 here).
  • domain assumption Every geometric morphism factors as an inclusion followed by a locally connected geometric morphism.
    Used to prove finite-union preservation for arbitrary pullbacks from the locally connected case (Chapitre I, Corollary I.3.20 indication; Chapitre IV, section 2c).
  • domain assumption Locally connected geometric morphisms satisfy the Beck-Chevalley condition (left adjoint compatible with base change).
    Part of the definition of local connectedness (Definition I.3.18) needed for the extraordinary direct image theorem (Theorem I.3.16).

how reviews work

0 comments
Cite this review

Pith. "Pith review of Generation of Grothendieck topologies, provability and operations on subtoposes." pith.science (2026). https://pith.science/paper/KB4PAWK4

@misc{pith2026250821134,
  author       = {Pith},
  title        = {Pith review of: Generation of Grothendieck topologies, provability and operations on subtoposes},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/KB4PAWK4}},
  note         = {Machine review of arXiv:2508.21134}
}
read the original abstract

After reviewing the multiple roles of toposes - as generalized topological spaces, as universal invariants, as categorical analogues of the set-theoretic universe, and as semantic environments for first-order theories - we recall the notion of subtopos and its dual expression: both in terms of Grothendieck topologies and in terms of first-order logic. We emphasize the significance of this duality, which enables the translation of provability problems in first-order logic into problems concerning the generation of Grothendieck topologies. We also introduce the natural geometric operations, both inner and outer, on subtoposes. Building on these foundations, we present a new formulation of the duality between Grothendieck topologies and subtoposes, as well as the duality between topologies and closedness properties of subpresheaves. This presentation relies on general categorical principles and aims to clarify the structural relationships involved. We then provide two general formulas for the Grothendieck topology generated by an arbitrary family of sieves or covering families of morphisms. In addition, we refine the constructive procedures that translate logical provability into topology generation, highlighting their role in bridging logic and geometry within the topos-theoretic framework. Finally, we study the inner geometric operations on subtoposes: union, intersection, and difference, along with the outer adjoint operations of pushforward and pullback along topos morphisms. We prove that pullback operations preserve not only arbitrary intersections but also finite unions of subtoposes, and that pullbacks along locally connected morphisms even preserve arbitrary unions.

Discussion (0). Continue with ORCID to comment.

Forward citations

Cited by 1 Pith paper

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score. Full citation record

  1. The Topological Dual of a Dataset: A Logic-to-Topology Encoding for AlphaGeometry-Style Data

    cs.AI 2026-04 unverdicted novelty 6.0 of 10

    The topological dual of a dataset is introduced as a transformation that encodes logical structures into topological ones to expose invariants in neural latent spaces for AlphaGeometry-style reasoning.

Reference graph

Works this paper leans on

32 extracted references · 31 canonical work pages · cited by 1 Pith paper

  1. [1]

    horizontal

    FIBRATIONS, TOPOLOGIES DE GIRAUD ET MORPHISMES LOCALEMENT CONNEXES 205 Exemple : Grothendieck Si C est une cat´ egorie localement petite, consid´ erons la cat´ egorie C/C dont les objets sont les morphismes de C X Y et dont les morphismes   X ′ Y ′   − →   X Y   sont les carr´ es commutatifs deC : X ′ // X Y ′ // Y On observe que le fonc...

  2. [2]

    TRADUCTIONS TOPOLOGIQUES DES PROBL `EMES DE D ´EMONTRABILIT ´E 191 Par exemple, si A est la th´ eorie alg´ ebrique (et donc cart´ esienne) des anneaux commutatifs, alors pour tout mod` eleA pr´ esent´ e par des ´ equations polynomiales en des variablesX1, · · ·, Xn Pi(X1, · · ·, Xn) = 0 , 1 ≤ i ≤ m , et tout mod` eleA′, l’ensemble Hom(A, A′) s’identifie `...

  3. [3]

    pr´ esent´ e

    TRADUCTIONS TOPOLOGIQUES DES PROBL `EMES DE D ´EMONTRABILIT ´E 189 (ii) Si e : X → X est un idempotent d’un objet X de C, la cat´ egorie r´ eduite ` aX et ses deux endomorphismes X //e id // X est filtrante, et sa colimite est le foncteur plat ρ : C − →Ens, X ′ 7− → {x ∈ Hom(X, X′) | x ◦ e = x} . Pour tout pr´ efaisceau P : C − →Ens, on a Hom(ρ, P) = {p ∈...

  4. [4]

    TRADUCTIONS TOPOLOGIQUES DES PROBL `EMES DE D ´EMONTRABILIT ´E 193 (ii) Les morphismes de Ccar Σ φ(⃗ x) − →ψ(⃗ y) entre deux formules de Horn φ et ψ en ⃗ x= (xA1 1 , · · ·, xAn n ) et ⃗ y= (yA′ 1 1 , · · ·, y A′ n′ n′ ) qui ont les formes φ(⃗ x) = ^ 1≤j≤m f Bj j (⃗ x) = f ′Bj j (⃗ x) ∧ ^ 1≤k≤ℓ Rk f Bk,1 k,1 (⃗ x), · · ·, f Bk,mk k,mk (⃗ x) , ψ(⃗ y) = ^ 1≤...

  5. [5]

    TRADUCTIONS TOPOLOGIQUES DES PROBL `EMES DE D ´EMONTRABILIT ´E 195 Grothendieck Dans la pratique, calculer des classes d’´ equivalence est difficile. Cependant, les relations d’´ equivalence disparaissent de l’´ enonc´ e de la proposition pr´ ec´ edente dans le cas de signatures Σ qui n’ont pas de symboles de fonctions : Corollaire III.3.16. – Grothendiec...

  6. [6]

    Apr` es un nombre fini de ces r´ eductions, tout tel objetφ(⃗ x) de Ccar Σ se r´ e´ ecrit sous la forme de (i)

    TRADUCTIONS TOPOLOGIQUES DES PROBL `EMES DE D ´EMONTRABILIT ´E 197 Toute formule de Horn en ⃗ x= (xA1 1 , · · ·, xAn n ) dont l’une des composantes atomiques a la forme xAi i = xAj j avec i < j et Ai = Aj c’est-` a-dire s’´ ecrit comme une conjonction φ(⃗ x) = φ1(⃗ x) ∧ (xAi i = xAj j ) est canoniquement isomorphe dans Ccar Σ a la formule en les n − 1 var...

  7. [7]

    TRADUCTIONS TOPOLOGIQUES DES PROBL `EMES DE D ´EMONTRABILIT ´E 199 variables par les relations de (1) Rf (zg1 , · · ·, zgm, zg) associ´ ees aux formules de construction de ces termes g(⃗ x) = f (g1(⃗ x), · · ·, gm(⃗ x)) . On forme alors la conjonction de ces formules en nombre fini et de la formule zB1 g1 = zB1 g2 ou R(zB1 g1 , · · ·, zBn gn ) , et on app...

  8. [8]

    horizontal

    TRADUCTIONS TOPOLOGIQUES DES PROBL `EMES DE D ´EMONTRABILIT ´E 201 De plus, il transforme toute formule de la forme (∃ ⃗ y) (θ1(⃗ x, ⃗ y) ∧ θ2(⃗ y, ⃗ z)) en la formule (∃ ⃗ y) (θr 1(⃗ x, ⃗ y) ∧ θr 2(⃗ x, ⃗ y)) . Ainsi, il d´ efinit un foncteur CT − → CTr . Il r´ esulte de l’interpr´ etation s´ emantique des morphismes entre des objets de topos M f: M A1 ×...

Show all 32 references
  1. [9]

    fibration

    FIBRATIONS, TOPOLOGIES DE GIRAUD ET MORPHISMES LOCALEMENT CONNEXES 207 D´ efinition IV.1.3. –Grothendieck Un foncteur entre deux cat´ egories F : C − → B est appel´ e une “fibration ” si, pour tout objetX de C et tout morphisme de B vers F (X) Y ′ b − − →F (X) , il existe dans...

  2. [10]

    208 CHAPITRE IV

    ∼ // F (x1) $$ Y ′ b F (X ′ 2)∼oo F (x2)zz F (X) alors il r´ esulte de la d´ efinition des morphismes horizontaux que l’isomorphisme compos´ e F (X ′ 1) ∼ − − →F (X ′ 2) se rel` eve en un unique isomorphisme deC X ′ 1 ∼ − − →X ′ 2 qui rende commutatif le triangle : X ′ 1 ∼ // ...

  3. [11]

    D´ emonstration : Grothendieck Supposons d’abord que F soit une fibration et consid´ erons deux morphismes deB de la forme F (X) Y ′ // Y pour un objet X de C

    FIBRATIONS, TOPOLOGIES DE GIRAUD ET MORPHISMES LOCALEMENT CONNEXES 209 Alors le foncteur F : C − → B est une fibration si et seulement si pour tout objet X de C et toute paire de morphisme de B F (X) Y ′ // Y le morphisme naturel F (X ×G(Y ) G(Y ′)) − →F (X) ×Y Y ′ induit par ...

  4. [12]

    essentiel

    FIBRATIONS, TOPOLOGIES DE GIRAUD ET MORPHISMES LOCALEMENT CONNEXES 211 On en d´ eduit que le carr´ e commutatif deC X ′ x // X G ◦ F (X ′) // G ◦ F (X) est cart´ esien, ce qui signifie d’apr` es le lemme IV.1.2 que le morphisme X ′ x − − →X est horizontal. Il rel` eve le morph...

  5. [13]

    p(X) − →Y ], • les morphismes sont les morphismes de C X2 x − − →X1 qui rendent commutatif le triangle p(X2) p(x) Y << "" p(X1) p(X2) p(x)[resp

    FIBRATIONS, TOPOLOGIES DE GIRAUD ET MORPHISMES LOCALEMENT CONNEXES 213    • les objets sont les paires constitu´ ees d’un objetX de C et d’un morphisme de B Y − →p(X) [resp. p(X) − →Y ], • les morphismes sont les morphismes de C X2 ...

  6. [14]

    Cela montre que l’application p!(P ×p∗Q1 p∗Q2) − →p!P (Y ) ×Q1(Y ) Q2(Y ) est une bijection, comme annonc´ e

    // p(X1) Par cons´ equent, le calcul de la limite p!(P ×p∗Q1 p∗Q2)(Y ) = lim − → (X,Y →p(X))∈Y \C P (X) ×Q1(p(X)) Q2(p(X)) peut ˆ etre restreint ` a la sous-cat´ egorie pleine de Y \C constitu´ ee des objets (X, Y− →p(X)) pour lesquels le morphisme de B Y − →p(X) est un isomor...

  7. [15]

    FIBRATIONS, TOPOLOGIES DE GIRAUD ET MORPHISMES LOCALEMENT CONNEXES 215 Th´ eor` eme IV.1.7. – (J. Giraud)Grothendieck Soit un foncteur entre deux cat´ egories essentiellement petites p : C − → B qui est une fibration et induit donc un morphisme localement connexe de topos de p...

  8. [16]

    Comme tout morphisme Y → p(X) se rel` eve en un morphisme horizontal dans C, on voit que pour un tel crible C ′ = p−1C d’un objet X, on a C ′ p = C

    FIBRATIONS, TOPOLOGIES DE GIRAUD ET MORPHISMES LOCALEMENT CONNEXES 217 D’apr` es la remarque (i), la topologieJ ′ de C qui d´ efinit le sous-topos debC image r´ eciproque debBJ ,→ bB est la topologie engendr´ ee par les cribles d’objetsX de C de la forme C ′ = n X ′ x − − →X |...

  9. [17]

    topologies

    FIBRATIONS, TOPOLOGIES DE GIRAUD ET MORPHISMES LOCALEMENT CONNEXES 219 Comme les compos´ es de morphismes horizontaux X ′ i − →Xi avec les morphismes Xi xi − − →X sont des morphismes horizontaux, on obtient que le crible Cp ,− →y(p(X)) est J-couvrant. Donc la condition (3) aus...

  10. [18]

    FIBRATIONS, TOPOLOGIES DE GIRAUD ET MORPHISMES LOCALEMENT CONNEXES 221 (ii) Si f = (f!, f∗, f∗) : E ′ → Eest un morphisme de topos localement connexe, le rel` evement horizontal dans E ′ de tout morphisme de E de la forme Y − →f!X s’identifie ` a f ∗Y ×f ∗f!X X − →X . En effet...

  11. [19]

    (ii) Il y a mˆ eme ´ egalit´ e de sous-objets C ′ f = Cf ×f!X f!X ′ si le morphisme X ′ x − − →X est un ´ epimorphisme

    FIBRATIONS, TOPOLOGIES DE GIRAUD ET MORPHISMES LOCALEMENT CONNEXES 223 Alors, pour tout morphisme de E ′ X ′ x − − →X , tout monomorphisme C ,− →X et son transform´ e par changement de base C ′ = C ×X X ′ ,− →X ′ , on a : (i) Le sous-objet C ′ f ,− →f!X ′ contient le sous-obje...

  12. [20]

    Grothendieck Fin de la d´ emonstration du th´ eor` eme IV.1.8 (ii)

    FIBRATIONS, TOPOLOGIES DE GIRAUD ET MORPHISMES LOCALEMENT CONNEXES 225 Cela termine la d´ emonstration du lemme. Grothendieck Fin de la d´ emonstration du th´ eor` eme IV.1.8 (ii). Il reste ` a v´ erifier les axiomes (2) et (3) des topologies surE ′. Pour (2), consid´ erons un...

  13. [21]

    Comme le morphisme X ′ − →X est un ´ epimorphisme, on obtient d’apr` es le lemme IV.1.9 (ii) la formule C ′ f = Cf ×f!X f!X ′

    FIBRATIONS, TOPOLOGIES DE GIRAUD ET MORPHISMES LOCALEMENT CONNEXES 227 Posant X ′ = a k∈K Xk , on a C ×X X ′ = a k∈K C ×X Xk , f!X ′ = a k∈K f!Xk et, notant C ′ = C ×X X ′, C ′ f = a k∈K (C ×X Xk)f . Comme le morphisme X ′ − →X est un ´ epimorphisme, on obtient d’apr` es le le...

  14. [22]

    D’o` u il r´ esulte comme voulu que l’application Hom(X ′, f∗Y ) − →Hom(C ′, f∗Y ) est une bijection si Y est un objet de EJ j∗ // E

    FIBRATIONS, TOPOLOGIES DE GIRAUD ET MORPHISMES LOCALEMENT CONNEXES 229 Pour tout morphisme X ′ → X, C ′ = C ×X X ′ ,− →X ′ est le rel` evement horizontal de S′ = S ×f!X f!X ′ ,− →f!X ′ si C ,→ X est le rel` evement horizontal deS ,→ f!X, et on a pour tout objet Y de E Hom(X ′,...

  15. [23]

    IMAGES DIRECTES EXTRAORDINAIRES ET IMAGES R ´ECIPROQUES DES R ´EUNIONS 231 (ii) Il poss` ede non seulement un adjoint ` a droite qui est le morphisme d’image directe des sous-topos f∗ : ST(E ′) − →ST(E) mais aussi un adjoint ` a gauche, appel´ e le morphisme d’image directe ex...

  16. [24]

    ⊇ E1 si et seulement si E ′ 1 ⊇ f −1E1 . (iii) Pour tout sous-topos de E ′ E ′ J ′ ,− → E′ qui est d´ efini par une topologie deE ′ engendr´ ee par une famille de monomorphismes (Ci ,− →Xi)i∈I , son image directe extraordinaire par f f!(E ′ J ′) = EJ ,− → E est d´ efinie par l...

  17. [25]

    IMAGES DIRECTES EXTRAORDINAIRES ET IMAGES R ´ECIPROQUES DES R ´EUNIONS 233 Alors : (i) Le morphisme de topos induit (p∗, p∗) : bCJ ′ − →bCJ est localement connexe. (ii) Le morphisme induit d’image r´ eciproque des sous-topos p−1 : (ST( bBJ ), ⊇) − →(ST( bCJ ′), ⊇) respecte les...

  18. [26]

    Grothendieck La conclusion r´ esulte du th´ eor` eme de factorisation suivant : Th´ eor` eme IV.2.4

    IMAGES DIRECTES EXTRAORDINAIRES ET IMAGES R ´ECIPROQUES DES R ´EUNIONS 235 On sait d’autre part d’apr` es la proposition I.3.2 (ii) que si f = j : E ′ ,− → E est un morphisme de plongement d’un sous-topos, l’application d’image r´ eciproque parj, qui n’est autre que l’applicat...

  19. [27]

    IMAGES DIRECTES EXTRAORDINAIRES ET IMAGES R ´ECIPROQUES DES R ´EUNIONS 237 Il suffit de prendre pour B et C n’importe quelles petites cous-cat´ egories pleines deE et E ′ qui contiennent des familles s´ eparantes d’objets pour obtenir des ´ equivalences de topos E ∼ − − →bBJ ,...

  20. [28]

    IMAGES DIRECTES EXTRAORDINAIRES ET IMAGES R ´ECIPROQUES DES R ´EUNIONS 239 D´ emonstration : Grothendieck (i) En effet, pour tous objets (X, Y, X→ ρ(Y )) de C′ = C/B et Y ′ de B , se donner un morphisme de B Y y − − →Y ′ ´ equivaut ` a se donner un morphisme deC′ = C/B (X, Y, ...

  21. [29]

    IMAGES DIRECTES EXTRAORDINAIRES ET IMAGES R ´ECIPROQUES DES R ´EUNIONS 241 (ii) Le foncteur d’oubli de C′ vers C q : C′ = C/B − → C , (X, Y, X→ ρ(Y )) 7− →X d´ efinit deux morphismes de topos bCK − →bC′ K′ et bC′ K′ − →bCK qui sont des ´ equivalences quasi-inverses l’une de l’...

  22. [30]

    Il est aussi K-continu puisque le foncteur r : C → C′ transforme toute famille K-couvrante en une famille K ′-couvrante

    IMAGES DIRECTES EXTRAORDINAIRES ET IMAGES R ´ECIPROQUES DES R ´EUNIONS 243 Comme, d’apr` es le lemme IV.2.6 (iii), le foncteur admet pour adjoint ` a droite le foncteur r : C − → C′ = C/B , X 7− →(X, 1B, X→ ρ(1B)) , on a un carr´ e commutatif de foncteurs : C_ y r // C′ _ y bC...

  23. [31]

    IMAGES DIRECTES EXTRAORDINAIRES ET IMAGES R ´ECIPROQUES DES R ´EUNIONS 245 Ainsi, le foncteur compos´ e B y // bB p∗ // bC′ // bC′ K′ est plat et J-continu. Il d´ efinit un morphisme de topos bC′ K′ − →bBJ qui s’inscrit dans un carr´ e commutatif : bC′ K′ _ // bBJ_ bC′ (p∗, p∗...

  24. [32]

    Th´ eorie des topos

    IMAGES DIRECTES EXTRAORDINAIRES ET IMAGES R ´ECIPROQUES DES R ´EUNIONS 247 L’image r´ eciproque du sous-topos bBJ ,− →bB par le morphisme de topos bC′ (p∗, p∗) − − − − − − →bB est le sous-topos bC′ J ′ ,− →bC′ d´ efini par la topologie de GiraudJ ′ de C′ associ´ ee ` a la topo...

Pith tools

Reviewed August 5, 2026 · model on record in the stance chip above.