Library UniMath.CategoryTheory.PowerObject
**
Following Saunders Mac Lane & Ieke Moerdijk
Sheaves in Geometry and Logic - A First Introduction to Topos theory.
Chapter IV.1
Contents :
- The definition of PowerObject;
- The derivation of PowerObject from Exponentials;
- The definition of PowerObject_functor;
- The derivation of PowerObject_nat_z_iso,
- The derivation of PowerObject_charname_nat_z_iso,
Require Import UniMath.Foundations.PartA.
Require Import UniMath.Foundations.PartD.
Require Import UniMath.CategoryTheory.Core.Categories.
Require Import UniMath.CategoryTheory.Core.Functors.
Require Import UniMath.CategoryTheory.Core.Isos.
Require Import UniMath.CategoryTheory.Core.NaturalTransformations.
Require Import UniMath.CategoryTheory.Limits.Terminal.
Require Import UniMath.CategoryTheory.Limits.BinProducts.
Require Import UniMath.CategoryTheory.SubobjectClassifier.
Require Import UniMath.CategoryTheory.opp_precat.
Require Import UniMath.CategoryTheory.whiskering.
Require Import UniMath.CategoryTheory.PrecategoryBinProduct.
Require Import UniMath.CategoryTheory.OppositeCategory.Core.
Require Import UniMath.CategoryTheory.Categories.HSET.Core.
Require Import UniMath.CategoryTheory.exponentials.
Require Import UniMath.CategoryTheory.Adjunctions.Core.
Local Open Scope cat.
Section PowerObject_def.
Context {C:category} {T:Terminal C} (Prod : BinProducts C) (O : subobject_classifier T).
Local Notation "c 'x' d" :=
(BinProductObject C (Prod c d))(at level 5).
Local Notation "f ⨱ g" :=
(BinProductOfArrows _ (Prod _ _) (Prod _ _) f g) (at level 10).
Definition is_PowerObject
(P : ob C -> ob C)
(inmap : ∏ (b:C), C ⟦b x (P b), O⟧ ):=
∏ (a b:C) (f : C ⟦b x a, O⟧),
∃! g : C ⟦a, P b⟧,
f = identity b ⨱ g·(inmap b).
Definition PowerObject :=
∑ (P : ob C -> ob C)
(inmap : ∏ (b:C), C ⟦b x (P b), O⟧ ),
is_PowerObject P inmap.
Definition make_PowerObject
(P : ob C -> ob C) (inmap : ∏ (b:C), C ⟦b x (P b), O⟧ ) (is : is_PowerObject P inmap)
: PowerObject.
Show proof.
End PowerObject_def.
Section PowerObject_from_exponentials.
Context {C:category} {T:Terminal C} (Prod : BinProducts C) (Ω : subobject_classifier T) (Exp : Exponentials Prod).
Let ExpFun (c:C) := right_adjoint (Exp c).
Let ExpEv (c:C) := counit_from_left_adjoint (Exp c).
Let ExpUnit (c:C) := unit_from_left_adjoint (Exp c).
Let ExpAdj (c:C) := pr2 (Exp c).
Definition PowerObject_from_exponentials : PowerObject Prod Ω.
Show proof.
use make_PowerObject.
+ intro b.
exact (ExpFun b Ω).
+ intro b.
use (ExpEv b).
+
intros c b f.
use make_iscontr.
- split with
(φ_adj (ExpAdj b) f).
use pathsinv0.
use (pathscomp0 (b:=(φ_adj_inv (ExpAdj b) (φ_adj (ExpAdj b) f)))).
* apply idpath.
* use φ_adj_inv_after_φ_adj.
- intros (t,tis).
use subtypePath.
* intro.
use homset_property.
* use (invmaponpathsweq (invweq (adjunction_hom_weq (ExpAdj b) c Ω))).
cbn.
rewrite φ_adj_inv_after_φ_adj.
use pathsinv0.
use tis.
+ intro b.
exact (ExpFun b Ω).
+ intro b.
use (ExpEv b).
+
intros c b f.
use make_iscontr.
- split with
(φ_adj (ExpAdj b) f).
use pathsinv0.
use (pathscomp0 (b:=(φ_adj_inv (ExpAdj b) (φ_adj (ExpAdj b) f)))).
* apply idpath.
* use φ_adj_inv_after_φ_adj.
- intros (t,tis).
use subtypePath.
* intro.
use homset_property.
* use (invmaponpathsweq (invweq (adjunction_hom_weq (ExpAdj b) c Ω))).
cbn.
rewrite φ_adj_inv_after_φ_adj.
use pathsinv0.
use tis.
End PowerObject_from_exponentials.
Section ContextAndNotaions.
Context {C:category} {T:Terminal C} {Prod : BinProducts C} {Ω : subobject_classifier T} (P: PowerObject Prod Ω).
Local Notation "c ⨉ d"
:= (BinProductObject C (Prod c d))(at level 5).
Local Notation "f ⨱ g"
:= (BinProductOfArrows _ (Prod _ _) (Prod _ _) f g) (at level 10).
Section PowerObject_accessor.
Definition PowerObject_on_ob : C -> C := pr1 P.
Definition PowerObject_inPred
: ∏ a : C, C ⟦(a ⨉ (PowerObject_on_ob a)), Ω⟧
:= pr1 (pr2 P).
Definition PowerObject_property {a b : C}
: ∏ f : C ⟦ b ⨉ a, Ω ⟧, ∃! g : C ⟦ a, PowerObject_on_ob b ⟧,
f = (identity b) ⨱ g · PowerObject_inPred b
:= (pr2 (pr2 P)) a b.
Definition PowerObject_transpose {a b : C} (f : C ⟦ b ⨉ a , Ω⟧)
: C ⟦a , (PowerObject_on_ob b)⟧
:= pr1 ( iscontrpr1 ((pr2 (pr2 P)) a b f)).
Definition PowerObject_transpose_tri {a b : C} (f : C ⟦ b ⨉ a , Ω⟧)
: f = (identity b) ⨱ (PowerObject_transpose f)·
PowerObject_inPred b
:= pr2 (iscontrpr1 ((pr2 (pr2 P)) a b f)).
End PowerObject_accessor.
Section PowerObject_transpose_lemma.
Proposition PowerObject_transpose_precomp {a' a b: C} (g : C ⟦a', a⟧)(f : C ⟦(b ⨉ a), Ω⟧ )
: PowerObject_transpose (identity b ⨱ g · f) = g · (PowerObject_transpose f).
Show proof.
apply pathsinv0.
use path_to_ctr.
use pathsinv0.
rewrite <-BinProductOfArrows_idxcomp.
rewrite !assoc'.
use cancel_precomposition.
use pathsinv0.
use (PowerObject_transpose_tri).
use path_to_ctr.
use pathsinv0.
rewrite <-BinProductOfArrows_idxcomp.
rewrite !assoc'.
use cancel_precomposition.
use pathsinv0.
use (PowerObject_transpose_tri).
End PowerObject_transpose_lemma.
Section PowerObject_functor.
Let construction {c b : C} (h : C ⟦b,c⟧):=
h ⨱ (identity (PowerObject_on_ob c))·(PowerObject_inPred c).
Definition PowerObject_functor_data : functor_data C^op C.
Show proof.
use make_functor_data.
- exact (PowerObject_on_ob).
- intros c b h.
use PowerObject_transpose.
exact (construction h).
- exact (PowerObject_on_ob).
- intros c b h.
use PowerObject_transpose.
exact (construction h).
Theorem PowerObject_functor_isfunctor : is_functor PowerObject_functor_data.
Show proof.
split.
+ intro b.
use pathsinv0.
use path_to_ctr.
apply idpath.
+ unfold functor_compax.
intros c b a h h'.
cbn in c, b, a, h, h'.
cbn.
use pathsinv0.
use path_to_ctr.
cbn.
unfold construction.
rewrite
<-BinProductOfArrows_idxcomp,
<-(BinProductOfArrows_compxid), assoc'.
fold (construction h).
rewrite
(PowerObject_transpose_tri (construction h)),
assoc.
rewrite BinProductOfArrows_comp,
(id_right h'), <-(id_left h'),
(id_left (PowerObject_transpose _)),
<-(id_right (PowerObject_transpose _)),
<-BinProductOfArrows_comp,
!assoc', id_left, id_right.
fold (construction h').
rewrite (PowerObject_transpose_tri (construction h')),
!assoc.
rewrite <-(PowerObject_transpose_tri (construction h')), <-(PowerObject_transpose_tri (construction h)).
apply idpath.
+ intro b.
use pathsinv0.
use path_to_ctr.
apply idpath.
+ unfold functor_compax.
intros c b a h h'.
cbn in c, b, a, h, h'.
cbn.
use pathsinv0.
use path_to_ctr.
cbn.
unfold construction.
rewrite
<-BinProductOfArrows_idxcomp,
<-(BinProductOfArrows_compxid), assoc'.
fold (construction h).
rewrite
(PowerObject_transpose_tri (construction h)),
assoc.
rewrite BinProductOfArrows_comp,
(id_right h'), <-(id_left h'),
(id_left (PowerObject_transpose _)),
<-(id_right (PowerObject_transpose _)),
<-BinProductOfArrows_comp,
!assoc', id_left, id_right.
fold (construction h').
rewrite (PowerObject_transpose_tri (construction h')),
!assoc.
rewrite <-(PowerObject_transpose_tri (construction h')), <-(PowerObject_transpose_tri (construction h)).
apply idpath.
Definition PowerObject_functor : functor C^op C.
Show proof.
End PowerObject_functor.
Section PowerObject_nat_z_iso.
Definition HomxO : functor (category_binproduct C^op C^op) hset_category
:=( binswap_pair_functor ∙
category_op_binproduct ∙
(functor_opp (binproduct_functor Prod)) ∙
(contra_homSet_functor Ω)).
Definition HomP : functor (category_binproduct C^op C^op) hset_category
:=( pair_functor (functor_identity C^op) (PowerObject_functor) ∙
homSet_functor).
Definition PowerObject_nt_data : nat_trans_data HomxO HomP.
Show proof.
Theorem PowerObject_nt_is_nat_trans : is_nat_trans HomxO HomP PowerObject_nt_data.
Show proof.
intros (a,b) (a',b') (a'a,b'b).
cbn in a'a, b'b.
use funextfun.
intro f.
apply pathsinv0.
use path_to_ctr.
cbn.
rewrite id_right.
rewrite <-BinProductOfArrows_idxcomp,
!assoc'.
rewrite <-(PowerObject_transpose_tri).
rewrite !assoc,
BinProductOfArrows_comp,
id_left, id_right.
rewrite
(PowerObject_transpose_tri f),
assoc,
BinProductOfArrows_comp,
id_right,
<-(PowerObject_transpose_tri f).
cbn.
apply idpath.
cbn in a'a, b'b.
use funextfun.
intro f.
apply pathsinv0.
use path_to_ctr.
cbn.
rewrite id_right.
rewrite <-BinProductOfArrows_idxcomp,
!assoc'.
rewrite <-(PowerObject_transpose_tri).
rewrite !assoc,
BinProductOfArrows_comp,
id_left, id_right.
rewrite
(PowerObject_transpose_tri f),
assoc,
BinProductOfArrows_comp,
id_right,
<-(PowerObject_transpose_tri f).
cbn.
apply idpath.
Definition PowerObject_nattrans : nat_trans HomxO HomP.
Show proof.
Theorem PowerObject_nt_is_nat_z_iso : is_nat_z_iso PowerObject_nattrans.
Show proof.
intros (a,b).
cbn.
use make_is_z_isomorphism.
+ intro g.
exact ((identity b) ⨱ g · (PowerObject_inPred b)).
+ cbn.
use make_is_inverse_in_precat.
- use funextfun.
intros f.
cbn.
use pathsinv0.
use PowerObject_transpose_tri.
- use funextfun.
intros g.
use pathsinv0.
use path_to_ctr.
apply idpath.
cbn.
use make_is_z_isomorphism.
+ intro g.
exact ((identity b) ⨱ g · (PowerObject_inPred b)).
+ cbn.
use make_is_inverse_in_precat.
- use funextfun.
intros f.
cbn.
use pathsinv0.
use PowerObject_transpose_tri.
- use funextfun.
intros g.
use pathsinv0.
use path_to_ctr.
apply idpath.
Definition PowerObject_nat_z_iso : nat_z_iso HomxO HomP.
Show proof.
Definition idxT_nattrans := binproduct_nat_trans_pr1 C C Prod (functor_identity C) (constant_functor C C T).
Theorem idxT_is_nat_z_iso : is_nat_z_iso idxT_nattrans.
Show proof.
Definition idxT_nat_z_iso := (make_nat_z_iso _ _ (idxT_nattrans) (idxT_is_nat_z_iso)).
Definition idxT_nat_inopp := op_nt idxT_nat_z_iso.
Definition idxT_whiskered_nat := post_whisker (idxT_nat_inopp) (contra_homSet_functor Ω).
Definition PowerObject_nat_z_iso_Tfixed := nat_z_iso_fix_fst_arg C^op C^op hset_category _ _ PowerObject_nat_z_iso T.
Definition PowerObject_charname_nattrans := nat_trans_comp _ _ _ idxT_whiskered_nat PowerObject_nat_z_iso_Tfixed.
Definition PowerObject_charname_is_nat_z_iso : is_nat_z_iso PowerObject_charname_nattrans.
Show proof.
intro c.
use is_z_iso_comp_of_is_z_isos.
+ generalize c.
use post_whisker_z_iso_is_z_iso.
use op_nt_is_z_iso.
use pr2_nat_z_iso.
+ generalize c.
use (pr2_nat_z_iso PowerObject_nat_z_iso_Tfixed).
use is_z_iso_comp_of_is_z_isos.
+ generalize c.
use post_whisker_z_iso_is_z_iso.
use op_nt_is_z_iso.
use pr2_nat_z_iso.
+ generalize c.
use (pr2_nat_z_iso PowerObject_nat_z_iso_Tfixed).
Definition PowerObject_charname_nat_z_iso : nat_z_iso (contra_homSet_functor Ω) (functor_fix_fst_arg C^op C^op hset_category HomP T).
Show proof.
use make_nat_z_iso.
+ exact PowerObject_charname_nattrans.
+ exact PowerObject_charname_is_nat_z_iso.
+ exact PowerObject_charname_nattrans.
+ exact PowerObject_charname_is_nat_z_iso.
Definition PowerObject_charname_nat_z_iso_tri {b : C} (f : C ⟦ b , Ω ⟧)
: (identity b) ⨱ (PowerObject_charname_nat_z_iso b f)·
PowerObject_inPred b
= (BinProductPr1 C (Prod b T) · f).
Show proof.
End PowerObject_nat_z_iso.
End ContextAndNotaions.