feat(CategoryTheory/Topos): Define subobject classifier for sheaf of types#35867

Open

edegeltje wants to merge 4 commits intoleanprover-community:masterfrom

edegeltje:sheaf_classifier

Collaborator

edegeltje commented Feb 27, 2026 •

edited

Loading

This PR defines Sheaf.classifier J : Classifier (Sheaf J (Type (max u v)), which is the last ingredient missing to sheaf categories being elementary topoi.

adapted from:
https://github.com/edegeltje/CwFTT/blob/591d4505390172ae70e1bc97544d293a35cc0b3f/CwFTT/Classifier/Sheaf.lean


          define subobject classifier for sheaf of types

455a179

edegeltje added the t-category-theory label

github-actions bot commented Feb 27, 2026 •

edited

Loading

PR summary bf3d8ad275

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
`Mathlib.CategoryTheory.Topos.Sheaf` (new file)	771

Declarations diff

+ Sheaf.classifier
+ Sheaf.classifier_isPullback
+ Sheaf.terminal
+ Sheaf.terminal.isTerminal
+ Sheaf.truth
+ Sheaf.Ω
+ Sheaf.χ
+ Sheaf.χ_unique
+ instance (J : GrothendieckTopology C) : HasClassifier (Sheaf J (Type (max u v)))

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for scripts/declarations_diff.sh contains some details about this script.

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

edegeltje added 3 commits

February 27, 2026 14:39


          run mk_all

efbf7b7


          fix module doc string

8c8b367


          fix some docs and linter errors

0d2072e

chrisflav reviewed

View reviewed changes

Mathlib/CategoryTheory/Topos/Sheaf.lean

Comment on lines +56 to +64

+              /-- A construction of a terminal object in a sheaf category, given by the constant `PUnit` sheaf. -/
+              @[simps]
+              def Sheaf.terminal (J : GrothendieckTopology C) : Sheaf J (Type w) where
+                val := (CategoryTheory.Functor.const _).obj PUnit
+                cond := Presheaf.isSheaf_of_isTerminal J Types.isTerminalPUnit
+              /-- The constant `PUnit` sheaf is a terminal object in `Sheaf J (Type w)` -/
+              def Sheaf.terminal.isTerminal {J : GrothendieckTopology C} : IsTerminal (Sheaf.terminal.{w} J) :=
+                .ofUniqueHom (fun F => { val := { app X := (fun _ => .unit) } }) (by intros; ext; rfl)

Contributor

chrisflav Feb 27, 2026

This should go in some earlier file.

Mathlib/CategoryTheory/Topos/Sheaf.lean

Comment on lines +217 to +219

+              /-- Sheaf categories have a subobject classifier. -/
+              instance (J : GrothendieckTopology C) : HasClassifier (Sheaf J (Type (max u v))) where
+                exists_classifier := ⟨Sheaf.classifier J⟩

Contributor

chrisflav Feb 27, 2026

Could you please generalize this instance to Sheaf J (Type w) with suitable UnivLE assumptions?

Mathlib/CategoryTheory/Topos/Sheaf.lean

+                simp_rw [← FunctorToTypes.naturality, ← hfst,eq_comm]
+              /--
+              A construction of subobject classifier for sheaf categories. `Ω` is the sheaf of closed sieves,

Contributor

chrisflav Feb 27, 2026

Suggested change

      
            A construction of subobject classifier for sheaf categories. `Ω` is the sheaf of closed sieves,
          
            A construction of a subobject classifier for sheaf categories. `Ω` is the sheaf of closed sieves,

Mathlib/CategoryTheory/Topos/Sheaf.lean

Comment on lines +208 to +215

+                .mkOfTerminalΩ₀
+                  (.terminal J)
+                  (Sheaf.terminal.isTerminal)
+                  (Sheaf.Ω)
+                  (Sheaf.truth)
+                  (Sheaf.χ)
+                  (Sheaf.classifier_isPullback)
+                  (Sheaf.χ_unique)

Contributor

chrisflav Feb 27, 2026

Is this intentionally ungolfed? Could you please also remove the superfluous ( ... )s?

Mathlib/CategoryTheory/Topos/Sheaf.lean

Comment on lines +125 to +128

+              lemma Sheaf.classifier_isPullback {J : GrothendieckTopology C} {F G : Sheaf J (Type (max u v))}
+                  (m : F ⟶ G) [Mono m] :
+                IsPullback m ((Sheaf.terminal.isTerminal).from F) (Sheaf.χ m) (Sheaf.truth) where
+                  w := by

Contributor

chrisflav Feb 27, 2026

I am wondering if it is easier to show that this is a pullback square on all sections? Then this is a square in Type for which you could use something like CategoryTheory.Limits.Types.isPullback_iff.

Mathlib/CategoryTheory/Topos/Sheaf.lean

+                val.app X := fun _ => ⟨⊤,_⟩
+              /--
+              given a monomorphism of sheaves `η : F ⟶ G`, a point X of the site, map an element `x : G(X)`

Contributor

chrisflav Feb 27, 2026

Suggested change

      
            given a monomorphism of sheaves `η : F ⟶ G`, a point X of the site, map an element `x : G(X)`
          
            Given a monomorphism of sheaves `η : F ⟶ G`, an object X of the site, map an element `x : G(X)`

"point" is confusing, given CategoryTheory.GrothendieckTopology.Point exists.

Mathlib/CategoryTheory/Topos/Sheaf.lean

Comment on lines +84 to +87

+              @[simps]
+              def Sheaf.χ {J : GrothendieckTopology C} {F G : Sheaf J (Type (max u v))} (m : F ⟶ G) [Mono m] :
+                  G ⟶ Sheaf.Ω where
+                val.app X := fun x => by

Contributor

chrisflav Feb 27, 2026

Would it make sense to first define this for presheaves (with values in all Sieves) and then show it factors through the closed ones in the case of a sheaf?

chrisflav added the awaiting-author label

chrisflav reviewed

View reviewed changes

Mathlib/CategoryTheory/Topos/Sheaf.lean

Comment on lines +23 to +25

		adapted from:
		https://github.com/edegeltje/CwFTT/blob/591d4505390172ae70e1bc97544d293a35cc0b3f/CwFTT/Classifier/Sheaf.lean

Contributor

chrisflav Feb 27, 2026

You could put this in the PR description, but what is the purpose of having this link here?

Collaborator Author

edegeltje Feb 27, 2026

I just copied the style of Topos/Classifier.lean... i'm fine with removing it though

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

awaiting-author t-category-theory