Documentation

Mathlib.CategoryTheory.Topos.Classifier

Subobject Classifier #

We define what it means for a morphism in a category to be a subobject classifier as CategoryTheory.HasClassifier.

c.f. the following Lean 3 code, where similar work was done: https://github.com/b-mehta/topos/blob/master/src/subobject_classifier.lean

Main definitions #

Let C refer to a category with a terminal object.

Main results #

References #

structure CategoryTheory.Classifier (C : Type u) [Category.{v, u} C] :
Type (max u v)

A monomorphism truth : Ω₀Ω is a subobject classifier if, for every monomorphism m : U ⟶ X in C, there is a unique map χ : X ⟶ Ω such that for some (necessarily unique) χ₀ : U ⟶ Ω₀ the following square is a pullback square:

      U ---------m----------> X
      |                       |
    χ₀ U                     χ m
      |                       |
      v                       v
      Ω₀ ------truth--------> Ω

An equivalent formulation replaces Ω₀ with the terminal object.

  • Ω₀ : C

    The domain of the truth morphism

  • Ω : C

    The codomain of the truth morphism

  • truth : self.Ω₀ self.Ω

    The truth morphism of the subobject classifier

  • mono_truth : Mono self.truth

    The truth morphism is a monomorphism

  • χ₀ (U : C) : U self.Ω₀

    The top arrow in the pullback square

  • χ {U X : C} (m : U X) [Mono m] : X self.Ω

    For any monomorphism U ⟶ X, there is an associated characteristic map X ⟶ Ω.

  • isPullback {U X : C} (m : U X) [Mono m] : IsPullback m (self.χ₀ U) (self.χ m) self.truth

    χ₀ U and χ m form the appropriate pullback square.

  • uniq {U X : C} (m : U X) [Mono m] {χ₀' : U self.Ω₀} {χ' : X self.Ω} (hχ' : IsPullback m χ₀' χ' self.truth) : χ' = self.χ m

    χ m is the only map X ⟶ Ω which forms the appropriate pullback square for any χ₀'.

Instances For
    def CategoryTheory.Classifier.mkOfTerminalΩ₀ {C : Type u} [Category.{v, u} C] (Ω₀ : C) (t : Limits.IsTerminal Ω₀) (Ω : C) (truth : Ω₀ Ω) (χ : {U X : C} → (m : U X) → [Mono m] → X Ω) (isPullback : ∀ {U X : C} (m : U X) [inst : Mono m], IsPullback m (t.from U) (χ m) truth) (uniq : ∀ {U X : C} (m : U X) [inst : Mono m] (χ' : X Ω), IsPullback m (t.from U) χ' truthχ' = χ m) :

    More explicit constructor in case Ω₀ is already known to be a terminal object.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      @[simp]
      theorem CategoryTheory.Classifier.mkOfTerminalΩ₀_truth {C : Type u} [Category.{v, u} C] (Ω₀ : C) (t : Limits.IsTerminal Ω₀) (Ω : C) (truth : Ω₀ Ω) (χ : {U X : C} → (m : U X) → [Mono m] → X Ω) (isPullback : ∀ {U X : C} (m : U X) [inst : Mono m], IsPullback m (t.from U) (χ m) truth) (uniq : ∀ {U X : C} (m : U X) [inst : Mono m] (χ' : X Ω), IsPullback m (t.from U) χ' truthχ' = χ m) :
      (mkOfTerminalΩ₀ Ω₀ t Ω truth χ isPullback uniq).truth = truth
      @[simp]
      theorem CategoryTheory.Classifier.mkOfTerminalΩ₀_Ω {C : Type u} [Category.{v, u} C] (Ω₀ : C) (t : Limits.IsTerminal Ω₀) (Ω : C) (truth : Ω₀ Ω) (χ : {U X : C} → (m : U X) → [Mono m] → X Ω) (isPullback : ∀ {U X : C} (m : U X) [inst : Mono m], IsPullback m (t.from U) (χ m) truth) (uniq : ∀ {U X : C} (m : U X) [inst : Mono m] (χ' : X Ω), IsPullback m (t.from U) χ' truthχ' = χ m) :
      (mkOfTerminalΩ₀ Ω₀ t Ω truth χ isPullback uniq).Ω = Ω
      @[simp]
      theorem CategoryTheory.Classifier.mkOfTerminalΩ₀_χ₀ {C : Type u} [Category.{v, u} C] (Ω₀ : C) (t : Limits.IsTerminal Ω₀) (Ω : C) (truth : Ω₀ Ω) (χ : {U X : C} → (m : U X) → [Mono m] → X Ω) (isPullback : ∀ {U X : C} (m : U X) [inst : Mono m], IsPullback m (t.from U) (χ m) truth) (uniq : ∀ {U X : C} (m : U X) [inst : Mono m] (χ' : X Ω), IsPullback m (t.from U) χ' truthχ' = χ m) (Y : C) :
      (mkOfTerminalΩ₀ Ω₀ t Ω truth χ isPullback uniq).χ₀ Y = t.from Y
      @[simp]
      theorem CategoryTheory.Classifier.mkOfTerminalΩ₀_Ω₀ {C : Type u} [Category.{v, u} C] (Ω₀ : C) (t : Limits.IsTerminal Ω₀) (Ω : C) (truth : Ω₀ Ω) (χ : {U X : C} → (m : U X) → [Mono m] → X Ω) (isPullback : ∀ {U X : C} (m : U X) [inst : Mono m], IsPullback m (t.from U) (χ m) truth) (uniq : ∀ {U X : C} (m : U X) [inst : Mono m] (χ' : X Ω), IsPullback m (t.from U) χ' truthχ' = χ m) :
      (mkOfTerminalΩ₀ Ω₀ t Ω truth χ isPullback uniq).Ω₀ = Ω₀
      @[simp]
      theorem CategoryTheory.Classifier.mkOfTerminalΩ₀_χ {C : Type u} [Category.{v, u} C] (Ω₀ : C) (t : Limits.IsTerminal Ω₀) (Ω : C) (truth : Ω₀ Ω) (χ : {U X : C} → (m : U X) → [Mono m] → X Ω) (isPullback : ∀ {U X : C} (m : U X) [inst : Mono m], IsPullback m (t.from U) (χ m) truth) (uniq : ∀ {U X : C} (m : U X) [inst : Mono m] (χ' : X Ω), IsPullback m (t.from U) χ' truthχ' = χ m) {U✝ X✝ : C} (m : U✝ X✝) (x✝ : Mono m) :
      (mkOfTerminalΩ₀ Ω₀ t Ω truth χ isPullback uniq).χ m = χ m

      A category C has a subobject classifier if there is at least one subobject classifier.

      Instances
        @[reducible, inline]

        Notation for the Ω₀ in an arbitrary choice of a subobject classifier

        Equations
        Instances For
          @[reducible, inline]

          Notation for the Ω in an arbitrary choice of a subobject classifier

          Equations
          Instances For
            @[reducible, inline]

            Notation for the "truth arrow" in an arbitrary choice of a subobject classifier

            Equations
            Instances For
              def CategoryTheory.HasClassifier.χ {C : Type u} [Category.{v, u} C] [HasClassifier C] {U X : C} (m : U X) [Mono m] :
              X Ω C

              returns the characteristic morphism of the subobject (m : U ⟶ X) [Mono m]

              Equations
              Instances For
                theorem CategoryTheory.HasClassifier.isPullback_χ {C : Type u} [Category.{v, u} C] [HasClassifier C] {U X : C} (m : U X) [Mono m] :
                IsPullback m (.some.χ₀ U) (χ m) (truth C)

                The diagram

                      U ---------m----------> X
                      |                       |
                    χ₀ U                     χ m
                      |                       |
                      v                       v
                      Ω₀ ------truth--------> Ω
                

                is a pullback square.

                The diagram

                      U ---------m----------> X
                      |                       |
                    χ₀ U                     χ m
                      |                       |
                      v                       v
                      Ω₀ ------truth--------> Ω
                

                commutes.

                theorem CategoryTheory.HasClassifier.unique {C : Type u} [Category.{v, u} C] [HasClassifier C] {U X : C} (m : U X) [Mono m] (χ' : X Ω C) (hχ' : IsPullback m (.some.χ₀ U) χ' (truth C)) :
                χ' = χ m

                χ m is the only map for which the associated square is a pullback square.

                The following diagram

                      U ---------m----------> X
                      |                       |
                    χ₀ U                     χ m
                      |                       |
                      v                       v
                      Ω₀ ------truth--------> Ω
                

                being a pullback for any monic m means that every monomorphism in C is the pullback of a regular monomorphism; since regularity is stable under base change, every monomorphism is regular. Hence, C is a regular mono category. It also follows that C is a balanced category.

                If the source of a faithful functor has a subobject classifier, the functor reflects isomorphisms. This holds for any balanced category.

                If the source of a faithful functor is the opposite category of one with a subobject classifier, the same holds -- the functor reflects isomorphisms.

                The representability theorem of subobject classifiers #

                From classifiers to representations #

                @[reducible, inline]

                The subobject of 𝒞.Ω corresponding to the truth morphism.

                Equations
                Instances For
                  theorem CategoryTheory.Classifier.surjective_χ {C : Type u} [Category.{v, u} C] [Limits.HasPullbacks C] (𝒞 : Classifier C) {X : C} (φ : X 𝒞.Ω) :
                  ∃ (Z : C) (i : Z X) (x : Mono i), φ = 𝒞.χ i

                  Any subobject classifier Ω represents the subobjects functor Subobject.presheaf.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For

                    From representations to classifiers #

                    @[reducible, inline]

                    Abbreviation to enable dot notation on the hypothesis h stating that the subobjects presheaf is representable by some object Ω.

                    Equations
                    Instances For

                      h.Ω₀ is the subobject of Ω which corresponds to the identity 𝟙 Ω, given h : SubobjectRepresentableBy Ω.

                      Equations
                      Instances For

                        h.homEquiv acts like an "object comprehension" operator: it maps any characteristic map f : X ⟶ Ω to the associated subobject of X, obtained by pulling back h.Ω₀ along f.

                        For any subobject x, the pullback of h.Ω₀ along the characteristic map of x given by h.homEquiv is x itself.

                        h.χ m is the characteristic map of monomorphism m given by the bijection h.homEquiv.

                        Equations
                        Instances For

                          h.iso m is the isomorphism between m and the pullback of Ω₀ along the characteristic map of m.

                          Equations
                          Instances For

                            h.π m is the first projection in the following pullback square:

                            U --h.π m--> (Ω₀ : C)
                            |                |
                            m             Ω₀.arrow
                            |                |
                            v                v
                            X -----h.χ m---> Ω
                            
                            Equations
                            Instances For
                              theorem CategoryTheory.Classifier.SubobjectRepresentableBy.uniq {C : Type u} [Category.{v, u} C] [Limits.HasPullbacks C] {Ω : C} (h : SubobjectRepresentableBy Ω) {U X : C} {m : U X} [Mono m] {χ' : X Ω} {π : U Subobject.underlying.obj h.Ω₀} (sq : IsPullback m π χ' h.Ω₀.arrow) :
                              χ' = h.χ m

                              The unique map to the terminal object.

                              Equations
                              Instances For

                                Any representation Ω of Subobject.presheaf C gives a subobject classifier with truth values object Ω.

                                Equations
                                • One or more equations did not get rendered due to their size.
                                Instances For

                                  A category has a subobject classifier if and only if the subobjects functor is representable.