Require Export cat_.
Implicit Arguments On.
Presheafs |
| We use the name "presheaf" for contravariant functors. |
Module Presheaf_.
Export Misc_.
Export Cat_.
Section Presheaf_Theory.
Variable A,B:Cat.
Variable F0:A->B; F1:(x,y:A) (mor x y) -> (mor (F0 y) (F0 x)).
Record Presheaf_Theory : Prop := {
ax_presh_oo : (x,y,z:A; g:(mor y z); f:(mor x y))
(F1 (oo g f))==(oo (F1 f) (F1 g));
ax_presh_ii : (x:A) (F1 (ii x))==(ii (F0 x))
}.
End Presheaf_Theory.
Record Presheaf_Data [A,B:Cat] : Type := {
presh_obj :> A->B;
presh : (x,y:A; f:(mor x y)) (mor (presh_obj y) (presh_obj x))
}.
Record Presheaf [A,B:Cat] : Type := {
presheaf_data :> (Presheaf_Data A B);
presheaf_theory :> (Presheaf_Theory (presh presheaf_data))
}.
Section Presheaf_Facts.
Variable A,B:Cat; F:(Presheaf A B).
Lemma presh_oo : (x,y,z:A; g:(mor y z); f:(mor x y))
(presh F (oo g f))==(oo (presh F f) (presh F g)).
Proof.
Intros; Apply (ax_presh_oo F).
Qed.
Lemma presh_ii : (x:A) (presh F (ii x))==(ii (F x)).
Proof.
Intros; Apply (ax_presh_ii F).
Qed.
End Presheaf_Facts.
Hints Resolve presh_oo presh_ii.
Definition Morph [A,B:Cat] : Type := (Presheaf A B).
Section Eq_Presh.
Variable A,B:Cat.
Definition eq_presh [F,G:(Presheaf A B)] : Prop :=
(x,y:A; f:(mor x y)) (eq_mor (presh F f) (presh G f)).
Variable F,G:(Presheaf A B); F_eq_G:(eq_presh F G).
Lemma eq_presh_src : (x,y:A; f:(mor x y))
(src (presh F f))==(src (presh G f)).
Proof.
Intros; NewDestruct (F_eq_G f); Reflexivity.
Qed.
Lemma eq_presh_trg : (x,y:A; f:(mor x y))
(trg (presh F f))==(trg (presh G f)).
Proof.
Intros; NewDestruct (F_eq_G f); Reflexivity.
Qed.
Lemma eq_presh_obj : (x:A)(F x)==(G x).
Proof.
Intros.
Change (src (ii (F x)))==(src (ii (G x))).
Do 2 Rewrite <- presh_ii.
Apply eq_presh_src.
Qed.
Extensionality for presheafs |
We prove that eq_presh implies eqT.
|
Lemma presheaf_extens : F==G.
Proof.
Assert U := eq_presh_obj.
NewDestruct F; NewDestruct G.
NewDestruct presheaf_data0.
NewDestruct presheaf_data1.
Simpl in U.
Assert E : presh_obj0==presh_obj1.
Apply nondep_extensionality.
Apply U.
NewDestruct E.
Clear F G U.
Rename presh_obj0 into FF.
Assert E : presh0==presh1.
Apply extensionality
with T := [x:A](y:A)(mor x y)->(mor (FF y) (FF x)).
Intros.
Apply extensionality
with T := [y:A](mor x y)->(mor (FF y) (FF x)).
Intros.
Apply nondep_extensionality.
Intros.
Unfold eq_presh in F_eq_G.
Simpl in F_eq_G.
Apply eq_mor_eqT.
Apply (F_eq_G x1).
NewDestruct E.
Assert E : presheaf_theory0 == presheaf_theory1.
Apply proof_irrelevance.
NewDestruct E.
Reflexivity.
Qed.
End Eq_Presh.
Morphisms of presheafs. |
| Morphisms of presheafs are natural tranformations between contravariant functors. |
Section NT'.
Variable A,B:Cat; F,G:(Presheaf A B).
Definition NT'_Comm [n:(x:A)(mor (F x) (G x))] : Prop :=
(x,y:A; f:(mor x y))
(oo (n x) (presh F f))==(oo (presh G f) (n y)).
Record NT' : Type := {
nt'_data :> (x:A) (mor (F x) (G x));
ax_nt'_comm :> (NT'_Comm nt'_data)
}.
Lemma nt'_comm : (n:NT'; x,y:A; f:(mor x y))
(oo (n x) (presh F f))==(oo (presh G f) (n y)).
Proof.
Intros; Apply ax_nt'_comm.
Qed.
Lemma nt'_extens : (n,m:NT')
((x:A) (n x)==(m x)) -> n==m.
Proof.
NewDestruct n; NewDestruct m; Simpl; Intros.
Assert nt'_data0==nt'_data1.
Apply extensionality with T := [x:A](mor (F x) (G x)).
Assumption.
NewDestruct H0.
Assert ax_nt'_comm0==ax_nt'_comm1.
Apply proof_irrelevance.
NewDestruct H0.
Reflexivity.
Qed.
End NT'.
Hints Resolve nt'_comm nt'_extens.
Category of functors |
| Presheafs with natural transformations form a category. |
Section Presheaf_Cat.
Variable A,B:Cat.
Definition nt'_id [F:(Presheaf A B)] : (NT' F F).
Proof.
Intros; Split with [x:A](ii (F x)).
Abstract Unfold NT'_Comm; Intros;
Rewrite ii_sx; Rewrite ii_dx; Reflexivity.
Defined.
Implicits nt'_id [1].
Section NT'_Comp.
Variable F,G,H:(Presheaf A B).
Variable m:(NT' G H); n:(NT' F G).
Local p [x:A] : (mor (F x) (H x)) := (oo (m x) (n x)).
Remark p_theory : (NT'_Comm p).
Proof.
Unfold p NT'_Comm; Intros.
Rewrite <- oo_assoc.
Rewrite (nt'_comm n).
Rewrite oo_assoc.
Rewrite (nt'_comm m).
Rewrite oo_assoc.
Reflexivity.
Qed.
Definition nt'_comp : (NT' F H).
Proof.
Split with p; Exact p_theory.
Defined.
End NT'_Comp.
Lemma nt'_comp_assoc : (F,G,H,I:(Presheaf A B))
(n:(NT' F G); m:(NT' G H); p:(NT' H I))
(nt'_comp p (nt'_comp m n))==(nt'_comp (nt'_comp p m) n).
Proof.
Intros; Apply nt'_extens; Simpl; Auto.
Qed.
Lemma nt'_sx_id : (F,G:(Presheaf A B); n:(NT' F G))
(nt'_comp nt'_id n)==n.
Proof.
Intros; Apply nt'_extens; Simpl; Auto.
Qed.
Lemma nt'_dx_id : (F,G:(Presheaf A B); n:(NT' F G))
(nt'_comp n nt'_id)==n.
Proof.
Intros; Apply nt'_extens; Simpl; Auto.
Qed.
Hints Resolve nt'_comp_assoc nt'_sx_id nt'_dx_id.
Definition Presheaf_Cat : Cat.
Proof.
Split with (Build_Cat_Data nt'_comp !nt'_id).
Abstract Split; Simpl; Intros; Auto.
Defined.
End Presheaf_Cat.
Hints Resolve nt'_comp_assoc nt'_sx_id nt'_dx_id.
End Presheaf_.