Require Export presheaf_.
Require Export set_cat.
Implicit Arguments On.
Yoneda Embedding |
Construction of Yoneda's Embedding (yoneda, yoneda_embeddig) and proof of Yoneda's Lemma (yoneda_bij, yoneda_bij_inv.
|
Module Yoneda.
Export Presheaf_.
Export Set_Cat.
Definition set := Small_Set.A.
Definition cat := Small_Cat.A.
The presheaf
|
Section Yoneda.
Variable A:Cat.
For each u:A we construct the presheaf (h u) such that (x:A)(h u x)==(mor x u).
|
Section Presheaf_h.
Variable u:A.
Local h_data : (Presheaf_Data A set).
Proof.
Split with [x:A](mor x u); Simpl.
Unfold Morph; Intros x y f g.
Exact (oo g f).
Defined.
Lemma h_theory : (Presheaf_Theory (presh h_data)).
Proof.
Split; Simpl; Unfold morph_comp morph_id; Intros.
Apply nondep_extensionality with A:=(mor 1!A z u) B:=(mor 1!A x u).
Auto.
Apply nondep_extensionality with A:=(!mor A x u) B:=(!mor A x u).
Auto.
Qed.
Definition h : (Presheaf A set).
Proof.
Split with h_data; Exact h_theory.
Defined.
End Presheaf_h.
Natural tranformations for
|
| We show that (h x) is natural in x. |
Section nt_h.
Variable u,v:A; f:(mor u v).
Local nt_data_h [x:A] : (mor (h u x) (h v x)).
Proof.
Intros; Simpl.
Unfold Morph; Intro g.
Exact (oo f g).
Defined.
Remark nt_comm_h : (!NT'_Comm A set (h u) (h v) nt_data_h).
Proof.
Unfold NT'_Comm nt_data_h morph_comp; Simpl; Intros.
Apply nondep_extensionality with A:=(mor 1!A y u) B:=(h v x).
Intro.
Unfold morph_comp; Simpl; Auto.
Qed.
Definition nt_h : (NT' (h u) (h v)).
Proof.
Intros; Split with nt_data_h.
Exact nt_comm_h.
Defined.
End nt_h.
Now we start to build the yoneda functor itself x -> (h x).
|
Definition yoneda_data : (Functor_Data A (Presheaf_Cat A set)) :=
(!Build_Functor_Data A (Presheaf_Cat A set)
h
[x,y:A; f:(mor x y)](nt_h f)).
Remark yoneda_theory : (Functor_Theory (fct yoneda_data)).
Proof.
Simpl; Split; Simpl; Intros.
Apply nt'_extens
with n:=(nt_h (oo g f)) m:=(nt'_comp (nt_h g) (nt_h f)).
Intro; Simpl.
Apply nondep_extensionality with A:=(mor x0 x) B:=(mor x0 z).
Intro.
Unfold morph_comp.
Auto.
Apply nt'_extens with n:=(nt_h (ii x)) m:=(nt'_id (h x)).
Intro.
Simpl.
Unfold morph_id.
Apply nondep_extensionality with A:=(mor 1!A x0 x) B:=(mor 1!A x0 x).
Auto.
Qed.
Definition yoneda : (Functor A (Presheaf_Cat A set)).
Proof.
Split with yoneda_data.
Exact yoneda_theory.
Defined.
Yoneda's lemma |
We construct the bijection yoneda_bij, yoneda_bij_inv.
|
Section Yoneda_Bijection.
Variable F:(Presheaf A set).
Variable x:A.
Definition yoneda_bij [n:(NT' (yoneda x) F)] : (F x) :=
(n x (ii x)).
Section Inverse.
Variable a:(F x).
Local inv_data [u:A] : (mor (yoneda x u) (F u)) :=
[f:(mor 1!A u x)](presh F f a).
Remark inv_nt : (NT'_Comm inv_data).
Proof.
Unfold inv_data NT'_Comm; Simpl; Intros.
Unfold morph_comp.
Apply nondep_extensionality with A:=(mor 1!A y x) B:=(F x0).
Intro; Rewrite presh_oo; Reflexivity.
Qed.
Fact inv : (NT' (yoneda x) F).
Proof.
Intros; Split with inv_data.
Exact inv_nt.
Defined.
End Inverse.
Remark inv_theory : (Inverse_Theory yoneda_bij inv).
Proof.
Split; Simpl; Unfold yoneda_bij inv.
Intro a.
Apply nt'_extens; Simpl; Intro y.
Apply nondep_extensionality with A:=(yoneda x y) B:=(F y).
Simpl.
Intro f.
Change (oo (presh F f) (a x) (ii x))==(a y f).
Rewrite <- nt'_comm; Simpl.
Unfold morph_comp.
Rewrite ii_sx; Reflexivity.
Intro; Simpl.
Rewrite presh_ii.
Reflexivity.
Qed.
Definition yoneda_bij_inv : (inverse yoneda_bij).
Proof.
Split with inv.
Exact inv_theory.
Defined.
End Yoneda_Bijection.
Yoneda's embedding |
Now we prove that yoneda is an embedding of categories. This amount to constructively invert the map (mor x y)->(mor
(yoneda x)
(yoneda y)).
In fact, this is a special case of Yoneda's bijection. We have two options:
We go for the second way. Not necessarely for pratical reason: we want to test reusability of code. |
Section Yoneda_Embedding.
Section Inverse.
Variable x,y:A.
Definition i [f:(mor x y)] : (mor (yoneda x) (yoneda y)) :=
(fct yoneda f).
To prove that yoneda is an embedding we need to find an inverse of i. In fact, the inverse of i is the following map j.
|
Definition j [f:(mor (yoneda x) (yoneda y))] : (mor x y) :=
(yoneda_bij f).
By yoneda_bij_inv we already have the inverse of j.
|
Definition k : (inverse j) := (yoneda_bij_inv (yoneda y) x).
Here we find a difficulty: i and k are not unifiable. That is one would expects to do the proof of the following lemma by Compute; Reflexivity, but it does not work. In fact, they are the same only "up to extensionality".
|
Lemma i_eq_k : i==k.
Proof.
Unfold i k; Simpl.
Apply nondep_extensionality.
Intro f.
Apply nt'_extens with n:=(nt_h f).
Compute; Reflexivity.
Qed.
| Now we can define inv_i using transport. |
Definition inv_i : (inverse i).
Proof.
Apply inverse_transport with f1:=(inverse_map k).
Abstract Symmetry; Apply i_eq_k.
Exact (inverse_inverse k).
Defined.
End Inverse.
Definition yoneda_embedding : (embedding yoneda).
Proof.
Unfold embedding.
Intros.
Apply (!inv_i x y).
Defined.
End Yoneda_Embedding.
End Yoneda.
End Yoneda.