-
-
Save skaslev/9027fca15994de8a57a9f29b35df4e0f to your computer and use it in GitHub Desktop.
Yoneda Lemma
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
namespace cat | |
universes u v | |
@[class] structure category := | |
(obj : Type u) | |
(hom : obj → obj → Type v) | |
(cid : ∀ {x : obj}, hom x x) | |
(comp : ∀ {x y z : obj}, hom y z → hom x y → hom x z) | |
(assoc : ∀ {x y z w} {f : hom x y} {g : hom y z} {h : hom z w}, | |
comp h (comp g f) = comp (comp h g) f) | |
(id_left : ∀ {x y} {f : hom x y}, comp cid f = f) | |
(id_right : ∀ {x y} {f : hom x y}, comp f cid = f) | |
open category | |
notation `∘` := comp | |
infixr `⟶`:25 := hom | |
notation f `∘[` C `]` g:25 := @comp C _ _ _ f g | |
@[instance] def op (C : category) : category := | |
category.mk | |
(@obj C) | |
(λx y, @hom C y x) | |
(@cid C) | |
(λx y z f g, comp g f) | |
(λx y z w f g h, eq.symm assoc) | |
(λx y f, id_right) | |
(λx y f, id_left) | |
structure setmap {S S' : Type u} (A : set S) (B : set S') : Type u := | |
(mapping : S → S') | |
(mapsin : ∀ x, x ∈ A → mapping x ∈ B) | |
open setmap | |
def setmap_comp {A B C : set Type} (g : setmap B C) (f : setmap A B) : setmap A C := | |
setmap.mk | |
(λx, mapping g (mapping f x)) | |
(assume x, assume xin : x ∈ A, g.mapsin (f.mapping x) (f.mapsin x xin)) | |
axiom setmap_eq {A B : set Type} (f g : setmap A B) : (∀ x, mapping f x = mapping g x) → f = g | |
instance Sets : category := | |
category.mk | |
(set Type) | |
(λx y, setmap x y) | |
(λx, setmap.mk (λu, u) (assume x, λp, p)) | |
(λa b c g f, setmap_comp g f) | |
(λa b c d h g f, rfl) | |
(λa b f, begin apply setmap_eq, intro x, apply rfl end) | |
(λa b f, begin apply setmap_eq, intro x, apply rfl end) | |
def homset {C : category} (a b : @obj C) : Type := set (@hom C a b) | |
instance Types : category := | |
category.mk | |
Type | |
(λx y, x → y) | |
(λx u, u) | |
(λa b c g f, λu, g (f u)) | |
(λa b c d h g f, rfl) | |
(λa b f, rfl) | |
(λa b f, rfl) | |
structure iso {C : category} (a b : @obj C) := | |
(mapr : @hom C a b) | |
(mapl : @hom C b a) | |
(isorl : (mapr ∘[C] mapl) = @cid C b) | |
(isolr : (mapl ∘[C] mapr) = @cid C a) | |
notation a `≅` b := @iso _ a b | |
notation a `≅[` C `]` b := @iso C a b | |
structure functor (C : category) (D : category) := | |
(fobj : @obj C → @obj D) | |
(fmap : ∀ {a b : @obj C}, @hom C a b → @hom D (fobj a) (fobj b)) | |
(preserve_id : ∀ {a : @obj C}, @fmap a a (@cid C a) = @cid D (fobj a)) | |
(preserve_comp : ∀ {a b c : @obj C} {g : @hom C b c} {f : @hom C a b}, | |
fmap (g ∘[C] f) = (fmap g ∘[D] fmap f)) | |
open cat.functor | |
def functor_comp {C D E : category} (G : functor D E) (F : functor C D) : functor C E := | |
functor.mk | |
(λx, fobj G (fobj F x)) | |
(λa b f, fmap G (fmap F f)) | |
begin intros, rw [F.preserve_id, G.preserve_id] end | |
begin intros, rw [F.preserve_comp, G.preserve_comp] end | |
notation G `∘f` F := functor_comp G F | |
def functor_id {C : category} : functor C C := | |
functor.mk | |
(λx, x) | |
(λa b f, f) | |
(λa, rfl) | |
(λa b c g f, rfl) | |
-- inductive eqArrow {C : category} {a b : @obj C} (f : @hom C a b) : ∀ {x y : @obj C}, @hom C x y → Type | |
-- | arr : ∀ {g : @hom C a b}, f = g → eqArrow f g | |
-- axiom functor_eq {C D : category} (F G : functor C D) : | |
-- (∀ {a b : @obj C} (f : @hom C a b), eqArrow (fmap F f) (fmap G f)) → F = G | |
-- definition Cat : category := | |
-- category.mk | |
-- category | |
-- functor | |
-- @functor_id | |
-- @functor_comp | |
-- (λa b c d F G H, functor_eq _ _ (λa b f, !eqArrow.arr (calc | |
-- fmap (H ∘f (G ∘f F)) f = fmap H (fmap G (fmap F f)) : rfl | |
-- ... = fmap ((H ∘f G) ∘f F) f : rfl))) | |
-- (λa b F, functor_eq _ _ (λa b f, !eqArrow.arr rfl)) | |
-- (λa b F, functor_eq _ _ (λa b f, !eqArrow.arr rfl)) | |
structure natrans {C D : category} (F G : functor C D) := | |
(component : ∀ (x : @obj C), @hom D (fobj F x) (fobj G x)) | |
(naturality : ∀ {a b : @obj C} {f : @hom C a b}, | |
(component b ∘[D] fmap F f) = (fmap G f ∘[D] component a)) | |
open natrans | |
notation F `⇒` G := natrans F G | |
def natrans_comp {C D : category} {F G H : functor C D} (ε : G ⇒ H) (η : F ⇒ G) : F ⇒ H := | |
natrans.mk | |
(λx, (component ε x ∘[D] component η x)) | |
begin | |
intros, | |
rw [@assoc D, ←naturality ε], | |
rw [←@assoc D, naturality η], | |
rw [@assoc D], | |
end | |
def natrans_id {C D : category} {F : functor C D} : F ⇒ F := | |
natrans.mk | |
(λx, @cid D (fobj F x)) | |
begin intros, rw [@id_right D, @id_left D] end | |
-- axiom natrans_eq {C D : category} {F G : functor C D} (α β : F ⇒ G) : | |
-- (∀ x, eqArrow (component α x) (component β x)) → α = β | |
-- one can define Sets-valued hom functor? | |
-- or Setoids-valued? | |
def homfunctor (C : category) (r : @obj C) : functor (op C) cat.Types := | |
functor.mk | |
(λx, @hom C x r) | |
(λa b f, λu, (u ∘[C] f)) | |
(λa, funext (assume x, id_right)) | |
(λa b c g f, funext (assume u, assoc)) | |
def homnat (C : category) {a b : @obj C} (f : @hom C a b) : (homfunctor C a) ⇒ (homfunctor C b) := | |
natrans.mk | |
(λx, λu, f ∘[C] u) | |
(λx y k, funext (assume u, assoc)) | |
-- def funcat (c d : category) : category := | |
-- category.mk | |
-- (functor c d) | |
-- natrans | |
-- (λx, natrans_id) | |
-- (λa b c, natrans_comp) | |
-- (λa b c d f g h, natrans_eq _ _ (λx, eqarrow.arr assoc)) | |
-- (λa b f, natrans_eq _ _ (λx, eqarrow.arr id_left)) | |
-- (λa b f, natrans_eq _ _ (λx, eqarrow.arr id_right)) | |
-- notation `[` C `,` D `]` := funcat C D | |
-- notation `PSh[` C `]` := [ op C, cat.Types ] | |
-- def yoneda (C : category) : functor C PSh[C] := | |
-- functor.mk | |
-- (λx, homfunctor C x) | |
-- (λa b f, homnat C f) | |
-- (λa, natrans_eq _ _ (λx, !eqArrow.arr (funext (λy, id_left)))) | |
-- (λa b c g f, natrans_eq _ _ (λx, eqArrow.arr (funext (λy, calc _ = _ : assoc)))) | |
-- lemma Yoneda (C : category) (F : functor (op C) Types) (r : @obj C) : | |
-- @hom PSh[C] (fobj (yoneda C) r) F ≅[Types] fobj F r | |
-- := iso.mk | |
-- (λα, component α r (@id C r)) | |
-- (λu, natrans.mk | |
-- (λx f, fmap F f u) | |
-- (λa b f, funext (λ (x : a ⟶ r), calc | |
-- ((λf, fmap F f u) ∘[Types] (fmap (fobj (yoneda C) r) f)) x = fmap F (x ∘[C] f) u : rfl | |
-- ... = (fmap F (f ∘[op C] x)) u : rfl | |
-- ... = (fmap F f ∘[Types] fmap F x) u : congr_fun !preserve_comp | |
-- ... = ((fmap F f) ∘[Types] (λ (f : a ⟶ r), fmap F f u)) x : rfl))) | |
-- (calc | |
-- fmap F (@id C r) = @id Types (fobj F r) : !preserve_id) | |
-- (funext (λα, natrans_eq _ _ (λx, eqArrow.arr (funext (λu, calc | |
-- fmap F u (component α r (@id C r)) = (fmap F u ∘[Types] component α r) (@id C r) : rfl | |
-- ... = (component α x ∘[Types] fmap (fobj (yoneda C) r) u) (@id C r) : congr_fun !naturality | |
-- ... = component α x (@id C r ∘[C] u) : rfl | |
-- ... = component α x u : congr_arg _ id_left))))) | |
end cat |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment