Library UniMath.CategoryTheory.SubobjectClassifier

Subobject classifiers

Contents


Require Import UniMath.Foundations.PartA.
Require Import UniMath.Foundations.PartB.
Require Import UniMath.Foundations.PartD.

Require Import UniMath.CategoryTheory.Core.Categories.
Require Import UniMath.CategoryTheory.Core.NaturalTransformations.
Require Import UniMath.CategoryTheory.limits.terminal.
Require Import UniMath.CategoryTheory.limits.pullbacks.
Require Import UniMath.CategoryTheory.Monics.
Require Import UniMath.CategoryTheory.Epis.
Require Import UniMath.CategoryTheory.limits.equalizers.

Require Import UniMath.CategoryTheory.Subobjects.
Require Import UniMath.CategoryTheory.categories.HSET.Core.
Require Import UniMath.CategoryTheory.Core.Functors.
Require Import UniMath.Foundations.Sets.
Require Import UniMath.CategoryTheory.Core.Isos.
Require Import UniMath.CategoryTheory.Monics.
Require Import UniMath.CategoryTheory.Subcategory.Core.

Local Open Scope cat.

Definition


Definition subobject_classifier {C : category} (T : Terminal C) : UU :=
  ∑ (O : ob C) (true : C⟦T, O⟧), ∏ (X Y : ob C) (m : Monic _ X Y),
    ∃! chi : C⟦Y, O⟧,
      ∑ (H : m · chi = TerminalArrow _ _ · true), isPullback H.

Definition make_subobject_classifier {C : category} {T : Terminal C}
           (O : ob C) (true : C⟦T, O⟧) :
  (∏ (X Y : ob C) (m : Monic _ X Y),
    iscontr (∑ (chi : C⟦Y, O⟧)
               (H : m · chi = TerminalArrow _ _ · true),
               isPullback H)) -> subobject_classifier T.
Show proof.
  intros.
  use tpair; [exact O|].
  use tpair; [exact true|].
  assumption.

Accessors


Section Accessors.
  Context {C : category} {T : Terminal C} (O : subobject_classifier T).

  Definition subobject_classifier_object : ob C := pr1 O.

true is monic. We only export the accessor for it them as a Monic (rather than the a morphism), as it's strictly more useful.
  Definition true' : C⟦T, subobject_classifier_object⟧ := pr1 (pr2 O).

  Local Lemma true_is_monic : isMonic true'.
  Show proof.
    apply from_terminal_isMonic.

  Definition true : Monic _ T subobject_classifier_object :=
    make_Monic _ true' true_is_monic.

  Definition subobject_classifier_universal_property {X Y} (m : Monic _ X Y) :
    iscontr (∑ (chi : C⟦Y, subobject_classifier_object⟧)
               (H : m · chi = TerminalArrow _ _ · true'),
               isPullback H) := pr2 (pr2 O) X Y m.

  Definition characteristic_morphism {X Y} (m : Monic _ X Y) :
    C⟦Y, subobject_classifier_object⟧ :=
    pr1 (iscontrpr1 (subobject_classifier_universal_property m)).

  Definition subobject_classifier_square_commutes {X Y} (m : Monic _ X Y) :
    m · characteristic_morphism m = TerminalArrow _ _ · true :=
    pr1 (pr2 (iscontrpr1 (subobject_classifier_universal_property m))).

  Definition subobject_classifier_pullback {X Y} (m : Monic _ X Y) :
    Pullback (characteristic_morphism m) true.
  Show proof.
    use make_Pullback.
    - exact X.
    - exact m.
    - apply TerminalArrow.
    - apply subobject_classifier_square_commutes.
    - apply (pr2 (pr2 (iscontrpr1 (subobject_classifier_universal_property m)))).

  Definition subobject_classifier_pullback_sym {X Y} (m : Monic _ X Y) :
    Pullback true (characteristic_morphism m).
  Show proof.
    refine (@switchPullback C _ _ _ _ _ (subobject_classifier_pullback m)).

End Accessors.

Coercion subobject_classifier_object : subobject_classifier >-> ob.
Coercion true : subobject_classifier >-> Monic.

The arrow Goldblatt calls true! := (! : X -> T) · true
Definition const_true {C : category} {T : Terminal C} (X : ob C)
           (O : subobject_classifier T) : X --> subobject_classifier_object O :=
  TerminalArrow T X · true O.

Section balanced.
  Context {C : category} {T : Terminal C} (O : subobject_classifier T)
  {c' c : C} (f : C⟦ c' , c ⟧) (f_isM : isMonic f) (f_isE : isEpi f).

  Local Definition f_asMonic := make_Monic _ f f_isM.

  Local Definition f_asEqualizer : Equalizer (characteristic_morphism O f_asMonic) (TerminalArrow T c · (true O)).
  Show proof.
    use (make_Equalizer _ _ f_asMonic).
    + rewrite
        subobject_classifier_square_commutes,
        assoc.
      use cancel_postcomposition.
      use TerminalArrowEq.
    + use make_isEqualizer.
      intros x h q.
      use unique_exists.
      - assert (p : c' = PullbackObject (subobject_classifier_pullback O f_asMonic)).
        { apply idpath. }
        rewrite p.
        use (PullbackArrow _ _ h (TerminalArrow T x)).
        rewrite q, assoc.
        use cancel_postcomposition.
        use TerminalArrowUnique.
      - simpl.
        assert (p : f =
          PullbackPr1 (subobject_classifier_pullback O f_asMonic)).
        { apply idpath. }
        rewrite p.
        use (PullbackArrow_PullbackPr1
          ((subobject_classifier_pullback O
          f_asMonic))).
      - intro t.
        use homset_property.
      - intros t t_tri.
        simpl.
        use (PullbackArrowUnique' _ _ _ (subobject_classifier_pullback O
        f_asMonic)).
        * exact t_tri.
        * use TerminalArrowUnique.

  Local Lemma path_from_fepi : (characteristic_morphism O f_asMonic) = (TerminalArrow T c · (true O)).
  Show proof.
    use f_isE.
    assert (p : f = f_asMonic). {apply idpath. }
    rewrite p.
    rewrite (subobject_classifier_square_commutes O f_asMonic).
    rewrite assoc.
    use cancel_postcomposition.
    use TerminalArrowEq.

  Theorem subobject_classifier_balanced : (is_z_isomorphism f).
  Show proof.
    assert (p : f = EqualizerArrow (f_asEqualizer)).
    { apply idpath. }
    rewrite p.
    use (z_iso_Equalizer_of_same_map f_asEqualizer).
    exact path_from_fepi.

End balanced.

Section subobject_classifier_natziso.

Context {C:category} {T:Terminal C} (PB : Pullbacks C) (O : subobject_classifier T).

Definition SubobjectClassifier_nt_data : nat_trans_data (SubObj_Functor C PB) (contra_homSet_functor O).
Show proof.
  intros c S.
  cbn in c.
  change (pr1hSet (SubObj c)) in S.
  cbn.
  use (squash_to_set (X:=(pr1setquot (z_iso_eqrel (C:=Subobjectscategory c)) S))).
  + use homset_property.
  + intro m.
    exact (characteristic_morphism O
      (Subobject_Monic (pr1carrier _ m))).
  + intros m m'.
    cbn.
    assert (ej : (z_iso_eqrel (C:=Subobjectscategory c)) (pr1carrier _ m') (pr1carrier _ m)). {
      use (invweq (weqpathsinsetquot _ _ _)).
      use (pathscomp0 (b:=S)).
        * use (setquotl0 (z_iso_eqrel (C:=Subobjectscategory c))).
        * use pathsinv0.
          use (setquotl0 (z_iso_eqrel (C:=Subobjectscategory c))).
    }
    use (squash_to_prop ej).
    - use homset_property.
    - intro j.
      use path_to_ctr.
      cbn.
      transparent assert (pb_aux : (Pullback ((identity c)·(characteristic_morphism O (Subobject_Monic (pr1carrier _ m)))) (true' O))). {
        use (Pullback_z_iso_of_morphisms).
          * exact (subobject_classifier_pullback O (Subobject_Monic (pr1carrier _ m))).
          * exact (Subobject_dom (pr1carrier _ m')).
          * exact (z_iso_from_z_iso_in_Subobjectcategory j).
          * exact (Subobject_mor (pr1carrier _ m')).
          * exact (identity_is_z_iso c).
          * use z_iso_is_z_isomorphism.
          * rewrite id_right.
            use (Subobjectmor_tri j).
      }
      use (isPullback_mor_paths' _ _ _ _ _ (isPullback_Pullback pb_aux)).
      * rewrite id_left.
        apply idpath.
      * apply idpath.
      * apply idpath.
      * use TerminalArrowUnique.
  + exact (eqax0 (SubObj_iseqc S)).

Lemma SubobjectClassifier_nt_is : is_nat_trans (SubObj_Functor C PB) (contra_homSet_functor O) SubobjectClassifier_nt_data.
Show proof.
  intros c c' f.
  cbn in c, c', f.
  use funextfun.
  intro S.
  use (squash_to_prop (X := pr1setquot _ S)).
  + exact (eqax0 (SubObj_iseqc S)).
  + use homset_property.
  + intro m.
    induction (setquotl0 _ _ m).
    cbn.
    rewrite id_right.
    use pathsinv0.
    use path_to_ctr.
    set (pbr := subobject_classifier_pullback O (Subobject_Monic (pr1carrier _ m))).
    cbn.
    set (pbl := PB c c' (Subobject_dom (pr1carrier _ m)) f (Subobject_mor (pr1carrier _ m))).
    transparent assert (pb_glued :
      (Pullback
        (f·(characteristic_morphism O (Subobject_Monic (pr1carrier _ m))))
        O)).
    { use make_Pullback.
    - exact pbl.
    - exact (PullbackPr1 pbl).
    - exact ((PullbackPr2 pbl)·(PullbackPr2 pbr)).
    - use glueSquares.
      * exact (PullbackPr1 pbr).
      * exact (PullbackSqrCommutes pbr).
      * exact (PullbackSqrCommutes pbl).
    - use (isPullbackGluedSquare
      (isPullback_Pullback pbr)
      (isPullback_Pullback pbl)). }
    use (isPullback_mor_paths' _ _ _ _ _ (isPullback_Pullback pb_glued)).
    - apply idpath.
    - apply idpath.
    - apply idpath.
    - use TerminalArrowUnique.

Definition SubobjectClassifier_nat_trans : nat_trans (SubObj_Functor C PB) (contra_homSet_functor O).
Show proof.
  use make_nat_trans.
  + exact SubobjectClassifier_nt_data.
  + exact SubobjectClassifier_nt_is.

Lemma SubobjectClassifier_nt_is_nat_z_iso : is_nat_z_iso SubobjectClassifier_nat_trans.
Show proof.
  intros c.
  use make_is_z_isomorphism.
  + intro phi.
    cbn in c, phi.
    use setquotpr.
    use (PullbackSubobject PB _ phi).
    use (Subobjectscategory_ob (true O)).
    apply from_terminal_isMonic.
  + use make_is_inverse_in_precat.
    - use funextfun.
      intro S.
      use (squash_to_prop (X:= pr1setquot _ S) ((eqax0 (SubObj_iseqc S)))).
      { use isasetsetquot. }
      intro m.
      induction (setquotl0 _ _ m).
      use weqpathsinsetquot.
      use hinhpr.
      cbn.
      set (pbc := subobject_classifier_pullback O ((Subobject_Monic (pr1carrier _ m)))).
      set (PBc := PB _ _ _ (characteristic_morphism O (Subobject_Monic (pr1carrier _ m))) O).

      induction (pullbackiso _ PBc pbc) as (PBpb_z_iso,(PBpb_z_iso1,PBpb_z_iso2)).
      use make_z_iso_in_Subobjectscategory.
      * cbn.
        exact PBpb_z_iso.
      * use z_iso_is_z_isomorphism.
      * apply pathsinv0.
        exact PBpb_z_iso1.
    - use funextfun.
      intro phi.
      cbn.
      apply pathsinv0.
      use path_to_ctr.
      cbn.
      set (pb := PB O c T phi (true' O)).
      use (isPullback_mor_paths' _ _ _ _ _ (isPullback_Pullback pb)).
      * apply idpath.
      * apply idpath.
      * apply idpath.
      * use TerminalArrowUnique.

Definition SubobjectClassifier_nat_z_iso :
  nat_z_iso (SubObj_Functor C PB) (contra_homSet_functor O).
Show proof.
  use make_nat_z_iso.
  + exact SubobjectClassifier_nat_trans.
  + exact SubobjectClassifier_nt_is_nat_z_iso.

End subobject_classifier_natziso.