feat(algebra/category/): minor additions, start on adjunction

library/algebra/category/adjoint.lean

@@ -0,0 +1,31 @@
+-- Copyright (c) 2014 Floris van Doorn. All rights reserved.
+-- Released under Apache 2.0 license as described in the file LICENSE.
+-- Author: Floris van Doorn
+
+import .basic .constructions
+
+open eq eq.ops category functor natural_transformation category.ops prod category.product
+
+namespace adjoint
+--representable functor
+
+  definition foo {obC : Type} (C : category obC) : C ×c C ⇒ C ×c C := functor.id
+
+  definition Hom {obC : Type} (C : category obC) : Cᵒᵖ ×c C ⇒ type :=
+  @functor.mk _ _ _ _ (λ a, hom (pr1 a) (pr2 a))
+	     (λ a b f h, pr2 f ∘ h ∘ pr1 f)
+	     (λ a, funext (λh, !id_left ⬝ !id_right))
+	     (λ a b c g f, funext (λh,
+    show (pr2 g ∘ pr2 f) ∘ h ∘ (pr1 f ∘ pr1 g) = pr2 g ∘ (pr2 f ∘ h ∘ pr1 f) ∘ pr1 g, from sorry))
+  --I'm lazy, waiting for automation to fill this
+
+  section
+  parameters {obC obD : Type} (C : category obC) {D : category obD}
+
+  definition adjoint (F : C ⇒ D) (G : D ⇒ C) :=
+  natural_transformation (Hom D ∘f sorry)
+			 --(Hom C ∘f sorry)
+--product.prod_functor (opposite.opposite_functor F) (functor.ID D)
+
+  end
+end adjoint

library/algebra/category/basic.lean

@@ -32,7 +32,7 @@ namespace category
   definition ID [reducible] : Π (a : ob), hom a a := @id
 
   infixr `∘`:60 := compose
-  infixl `⟶`:25 := hom -- input ⟶ using \-->
+  infixl `⟶`:25 := hom -- input ⟶ using \--> (this is a different arrow than \-> (→))
 
   variables {h : hom c d} {g : hom b c} {f : hom a b} {i : hom a a}
 
@@ -109,11 +109,11 @@ namespace functor
       G (F (g ∘ f)) = G (F g ∘ F f)     : {respect_comp F g f}
                 ... = G (F g) ∘ G (F f) : respect_comp G (F g) (F f))
 
-  infixr `∘∘`:60 := compose
+  infixr `∘f`:60 := compose
 
   protected theorem assoc {obA obB obC obD : Type} {A : category obA} {B : category obB}
       {C : category obC} {D : category obD} (H : C ⇒ D) (G : B ⇒ C) (F : A ⇒ B) :
-      H ∘∘ (G ∘∘ F) = (H ∘∘ G) ∘∘ F :=
+      H ∘f (G ∘f F) = (H ∘f G) ∘f F :=
   rfl
 
   -- later check whether we want implicit or explicit arguments here. For the moment, define both
@@ -123,8 +123,8 @@ namespace functor
   protected definition Id {C : Category} : Functor C C := Functor.mk id
   protected definition iD (C : Category) : Functor C C := Functor.mk id
 
-  protected theorem id_left  (F : C ⇒ D) : id ∘∘ F = F := rec (λ obF homF idF compF, rfl) F
-  protected theorem id_right (F : C ⇒ D) : F ∘∘ id = F := rec (λ obF homF idF compF, rfl) F
+  protected theorem id_left  (F : C ⇒ D) : id ∘f F = F := rec (λ obF homF idF compF, rfl) F
+  protected theorem id_right (F : C ⇒ D) : F ∘f id = F := rec (λ obF homF idF compF, rfl) F
 
   end basic_functor
 
@@ -138,17 +138,17 @@ namespace functor
   Functor.mk (compose (Functor_functor G) (Functor_functor F))
 
 --  namespace Functor
-  infixr `∘∘`:60 := Compose
+  infixr `∘F`:60 := Compose
 --  end Functor
 
   protected definition Assoc (H : Functor C₃ C₄) (G : Functor C₂ C₃) (F : Functor C₁ C₂)
-    :  H ∘∘ (G ∘∘ F) = (H ∘∘ G) ∘∘ F :=
+    :  H ∘F (G ∘F F) = (H ∘F G) ∘F F :=
   rfl
 
-  protected theorem Id_left (F : Functor C₁ C₂) : Id ∘∘ F = F := 
+  protected theorem Id_left (F : Functor C₁ C₂) : Id ∘F F = F := 
   Functor.rec (λ f, subst !id_left rfl) F
 
-  protected theorem Id_right {F : Functor C₁ C₂} : F ∘∘ Id = F :=
+  protected theorem Id_right {F : Functor C₁ C₂} : F ∘F Id = F :=
   Functor.rec (λ f, subst !id_right rfl) F
   end Functor
 

library/algebra/category/constructions.lean

@@ -21,6 +21,7 @@ namespace category
      (λ a b f, !unit.equal)
   end
 
+  namespace opposite
   section
   variables {ob : Type} {C : category ob} {a b c : ob}
   definition opposite (C : category ob) : category ob :=
@@ -43,6 +44,7 @@ namespace category
 
   definition Opposite (C : Category) : Category :=
   Category.mk (objects C) (opposite (category_instance C))
+  end opposite
 
   section
   definition type_category : category Type :=
@@ -93,9 +95,10 @@ namespace category
      (λ a b f, !functor.Id_right)
   end cat_of_cat
 
-  section product
+  namespace product
+  section
   open prod
-  definition product_category {obC obD : Type} (C : category obC) (D : category obD)
+  definition prod_category {obC obD : Type} (C : category obC) (D : category obD)
       : category (obC × obD) :=
   mk (λa b, hom (pr1 a) (pr1 b) × hom (pr2 a) (pr2 b))
      (λ a b c g f, (pr1 g ∘ pr1 f , pr2 g ∘ pr2 f) )
@@ -103,16 +106,47 @@ namespace category
      (λ a b c d h g f, pair_eq    !assoc    !assoc   )
      (λ a b f,         prod.equal !id_left  !id_left )
      (λ a b f,         prod.equal !id_right !id_right)
-
+  end
   end product
 
 namespace ops
   notation `Cat` := category_of_categories
   notation `type` := type_category
   notation 1 := category_one
-  postfix `ᵒᵖ`:max := opposite
-  infixr `×` := product_category
-  instance category_of_categories type_category category_one product_category
+  postfix `ᵒᵖ`:max := opposite.opposite
+  infixr `×c`:30 := product.prod_category
+  instance category_of_categories type_category category_one product.prod_category
+end ops
+  open ops
+  namespace opposite
+  section
+  open ops functor
+  --set_option pp.implicit true
+  definition opposite_functor {obC obD : Type} {C : category obC} {D : category obD} (F : C ⇒ D)
+      : Cᵒᵖ ⇒ Dᵒᵖ :=
+  @functor.mk obC obD (Cᵒᵖ) (Dᵒᵖ)
+	      (λ a, F a)
+	      (λ a b f, F f)
+	      (λ a, !respect_id)
+	      (λ a b c g f, !respect_comp)
+  end
+  end opposite
+
+  namespace product
+  section
+  open ops functor
+  definition prod_functor {obC obC' obD obD' : Type} {C : category obC} {C' : category obC'}
+    {D : category obD} {D' : category obD'} (F : C ⇒ D) (G : C' ⇒ D') : C ×c C' ⇒ D ×c D' :=
+  functor.mk (λ a, pair (F (pr1 a)) (G (pr2 a)))
+	     (λ a b f, pair (F (pr1 f)) (G (pr2 f)))
+	     (λ a, pair_eq !respect_id !respect_id)
+	     (λ a b c g f, pair_eq !respect_comp !respect_comp)
+  end
+  end product
+
+  namespace ops
+  infixr `×f`:30 := product.prod_functor
+  infixr `ᵒᵖᶠ`:max := opposite.opposite_functor
   end ops
 
   section functor_category

library/algebra/category/yoneda.lean

@@ -4,13 +4,27 @@
 
 import .basic .constructions
 
-open eq eq.ops category functor category.ops
+open eq eq.ops category functor category.ops prod
 
 namespace yoneda
 --representable functor
   section
   parameters {ob : Type} {C : category ob}
-  -- definition Hom : Cᵒᵖ × C ⇒ type :=
-  -- sorry
+  set_option pp.universes true
+  check @type_category
+  section
+    parameters {a a' b b' : ob} (f : @hom ob C a' a) (g : @hom ob C b b')
+--    definition Hom_fun_fun :
+  end
+  definition Hom : Cᵒᵖ ×c C ⇒ type :=
+  @functor.mk _ _ _ _ (λ a, hom (pr1 a) (pr2 a))
+	     (λ a b f h, pr2 f ∘ h ∘ pr1 f)
+	     (λ a, funext (λh, !id_left ⬝ !id_right))
+	     (λ a b c g f, funext (λh,
+    show (pr2 g ∘ pr2 f) ∘ h ∘ (pr1 f ∘ pr1 g) = pr2 g ∘ (pr2 f ∘ h ∘ pr1 f) ∘ pr1 g, from sorry))
+  --I'm lazy, waiting for automation to fill this
+
+
+
   end
 end yoneda