New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
feat(category_theory): opposites, and the category of types #249
Changes from 4 commits
3cc4266
4ab4110
ed06add
4c32476
52246b1
cf76212
0d6b7ca
10a03b9
4bd617a
8055b68
670d159
File filter
Filter by extension
Conversations
Jump to
Diff view
Diff view
There are no files selected for viewing
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,55 @@ | ||
-- Copyright (c) 2017 Scott Morrison. All rights reserved. | ||
-- Released under Apache 2.0 license as described in the file LICENSE. | ||
-- Authors: Stephen Morgan, Scott Morrison | ||
|
||
import category_theory.functor | ||
import category_theory.products | ||
import category_theory.types | ||
|
||
namespace category_theory | ||
|
||
universes u₁ v₁ u₂ v₂ | ||
|
||
def op (C : Type u₁) : Type u₁ := C | ||
|
||
notation C `ᵒᵖ` := op C | ||
|
||
variables {C : Type u₁} [𝒞 : category.{u₁ v₁} C] | ||
include 𝒞 | ||
|
||
instance opposite : category.{u₁ v₁} (Cᵒᵖ) := | ||
{ Hom := λ X Y : C, Y ⟶ X, | ||
comp := λ _ _ _ f g, g ≫ f, | ||
id := λ X, 𝟙 X, | ||
id_comp := begin /- `obviously'` says: -/ intros, simp end, | ||
comp_id := begin /- `obviously'` says: -/ intros, simp end, | ||
assoc := begin /- `obviously'` says: -/ intros, simp end } | ||
|
||
namespace functor | ||
|
||
variables {D : Type u₂} [𝒟 : category.{u₂ v₂} D] | ||
include 𝒟 | ||
|
||
definition opposite (F : C ↝ D) : (Cᵒᵖ) ↝ (Dᵒᵖ) := | ||
{ obj := λ X, F X, | ||
map := λ X Y f, F.map f, | ||
map_id := begin /- `obviously'` says: -/ intros, erw [map_id], refl, end, | ||
map_comp := begin /- `obviously'` says: -/ intros, erw [map_comp], refl end } | ||
|
||
@[simp] lemma opposite_obj (F : C ↝ D) (X : C) : (F.opposite) X = F X := rfl | ||
@[simp] lemma opposite_map (F : C ↝ D) {X Y : C} (f : X ⟶ Y) : (F.opposite).map f = F.map f := rfl | ||
|
||
end functor | ||
|
||
variable (C) | ||
|
||
definition hom_pairing : (Cᵒᵖ × C) ↝ (Type v₁) := | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Hm, to me this is not an obvious name. I guess this is the functor mathematicians call There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. This is a fairly common name amongst mathematicians (ha!): the idea is that it is a pairing, like the pairing between a vector space and its dual. I think the common usage is just because "the hom functor for C" doesn't really specify what you mean, but "the hom pairing for C" is unambiguously a "bilinear" thing, i.e. a functor out of I can change it to just There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Another thing: I've been thinking that the field There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Re: I think "hom pairing" sounds more like a way to speak the symbol in a mathematical context without the opportunity for notational or typing disambiguation. In our case, I think this should be called |
||
{ obj := λ p, @category.Hom C _ p.1 p.2, | ||
map := λ X Y f, λ h, f.1 ≫ h ≫ f.2, | ||
map_id := begin /- `obviously'` says: -/ intros, apply funext, intros, cases X, dsimp at *, simp, erw [category.id_comp_lemma] end, | ||
map_comp := begin /- `obviously'` says: -/ intros, apply funext, intros, cases f, cases g, cases X, cases Y, cases Z, dsimp at *, simp, erw [category.assoc] end } | ||
|
||
@[simp] lemma hom_pairing_obj (X : Cᵒᵖ × C) : (hom_pairing C) X = @category.Hom C _ X.1 X.2 := rfl | ||
@[simp] lemma hom_pairing_map {X Y : Cᵒᵖ × C} (f : X ⟶ Y) : (hom_pairing C).map f = λ h, f.1 ≫ h ≫ f.2 := rfl | ||
|
||
end category_theory |
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -8,42 +8,37 @@ namespace category_theory | |
universes u₁ v₁ u₂ v₂ u₃ v₃ u₄ v₄ | ||
|
||
section | ||
variables (C : Type u₁) [category.{u₁ v₁} C] (D : Type u₂) [category.{u₂ v₂} D] | ||
variables (C : Type u₁) [𝒞 : category.{u₁ v₁} C] (D : Type u₂) [𝒟 : category.{u₂ v₂} D] | ||
include 𝒞 𝒟 | ||
|
||
/-- | ||
`prod.category C D` gives the cartesian product of two categories. | ||
-/ | ||
instance prod.category : category.{(max u₁ u₂) (max v₁ v₂)} (C × D) := | ||
instance prod : category.{(max u₁ u₂) (max v₁ v₂)} (C × D) := | ||
{ Hom := λ X Y, ((X.1) ⟶ (Y.1)) × ((X.2) ⟶ (Y.2)), | ||
id := λ X, ⟨ 𝟙 (X.1), 𝟙 (X.2) ⟩, | ||
comp := λ _ _ _ f g, (f.1 ≫ g.1, f.2 ≫ g.2), | ||
id_comp := begin /- `obviously'` says: -/ intros, cases X, cases Y, cases f, dsimp at *, simp end, | ||
id_comp := begin /- `obviously'` says: -/ intros, cases X, cases Y, cases f, dsimp at *, simp end, | ||
comp_id := begin /- `obviously'` says: -/ intros, cases X, cases Y, cases f, dsimp at *, simp end, | ||
assoc := begin /- `obviously'` says: -/ intros, cases W, cases X, cases Y, cases Z, cases f, cases g, cases h, dsimp at *, simp end } | ||
end | ||
|
||
namespace prod.category | ||
|
||
section -- rfl lemmas for prod.category | ||
variables {C : Type u₁} [𝒞 : category.{u₁ v₁} C] {D : Type u₂} [𝒟 : category.{u₂ v₂} D] | ||
include 𝒞 𝒟 | ||
|
||
@[simp, ematch] lemma id (X : C) (Y : D) : 𝟙 (X, Y) = (𝟙 X, 𝟙 Y) := rfl | ||
@[simp, ematch] lemma comp {P Q R : C} {S T U : D} (f : (P, S) ⟶ (Q, T)) (g : (Q, T) ⟶ (R, U)) : f ≫ g = (f.1 ≫ g.1, f.2 ≫ g.2) := rfl | ||
-- rfl lemmas for category.prod | ||
@[simp, ematch] lemma prod_id (X : C) (Y : D) : 𝟙 (X, Y) = (𝟙 X, 𝟙 Y) := rfl | ||
@[simp, ematch] lemma prod_comp {P Q R : C} {S T U : D} (f : (P, S) ⟶ (Q, T)) (g : (Q, T) ⟶ (R, U)) : f ≫ g = (f.1 ≫ g.1, f.2 ≫ g.2) := rfl | ||
end | ||
|
||
section | ||
variables (C : Type u₁) [𝒞 : category.{u₁ v₁} C] (D : Type u₁) [𝒟 : category.{u₁ v₁} D] | ||
include 𝒞 𝒟 | ||
|
||
include 𝒞 𝒟 | ||
/-- | ||
`prod.category.uniform C D` is an additional instance specialised so both factors have the same universe levels. This helps typeclass resolution. | ||
-/ | ||
instance uniform : category (C × D) := prod.category C D | ||
instance uniform_prod : category (C × D) := category_theory.prod C D | ||
end | ||
|
||
-- Next we define the natural functors into and out of product categories. For now this doesn't address the universal properties. | ||
|
||
namespace prod | ||
|
||
/-- `inl C Z` is the functor `X ↦ (X, Z)`. -/ | ||
def inl (C : Type u₁) [category.{u₁ v₁} C] {D : Type u₁} [category.{u₁ v₁} D] (Z : D) : C ↝ (C × D) := | ||
{ obj := λ X, (X, Z), | ||
|
@@ -72,21 +67,21 @@ def snd (C : Type u₁) [category.{u₁ v₁} C] (Z : C) (D : Type u₁) [catego | |
map_id := begin /- `obviously'` says: -/ intros, refl end, | ||
map_comp := begin /- `obviously'` says: -/ intros, refl end } | ||
|
||
end prod.category | ||
end prod | ||
|
||
variables {A : Type u₁} [𝒜 : category.{u₁ v₁} A] {B : Type u₂} [ℬ : category.{u₂ v₂} B] {C : Type u₃} [𝒞 : category.{u₃ v₃} C] {D : Type u₄} [𝒟 : category.{u₄ v₄} D] | ||
include 𝒜 ℬ 𝒞 𝒟 | ||
|
||
namespace functor | ||
/-- The cartesion product of two functors. -/ | ||
/-- The cartesian product of two functors. -/ | ||
def prod (F : A ↝ B) (G : C ↝ D) : (A × C) ↝ (B × D) := | ||
{ obj := λ X, (F X.1, G X.2), | ||
map := λ _ _ f, (F.map f.1, G.map f.2), | ||
map_id := begin /- `obviously'` says: -/ intros, cases X, dsimp, rw map_id_lemma, rw map_id_lemma end, | ||
map_comp := begin /- `obviously'` says: -/ intros, cases Z, cases Y, cases X, cases f, cases g, dsimp at *, rw map_comp_lemma, rw map_comp_lemma end } | ||
|
||
@[simp, ematch] lemma prod_obj (F : A ↝ B) (G : C ↝ D) (a : A) (c : C) : F.prod G (a, c) = (F a, G c) := rfl | ||
@[simp, ematch] lemma prod_map (F : A ↝ B) (G : C ↝ D) {a a' : A} {c c' : C} (f : (a, c) ⟶ (a', c')) : (F.prod G).map f = (F.map f.1, G.map f.2) := rfl | ||
@[simp, ematch] lemma prod_obj (F : A ↝ B) (G : C ↝ D) (a : A) (c : C) : (functor.prod F G) (a, c) = (F a, G c) := rfl | ||
@[simp, ematch] lemma prod_map (F : A ↝ B) (G : C ↝ D) {a a' : A} {c c' : C} (f : (a, c) ⟶ (a', c')) : (functor.prod F G).map f = (F.map f.1, G.map f.2) := rfl | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. What happened here? I liked it better before - did projection stop working? There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Projection is still fine. It just looked awfully lopsided to me, for a very symmetric construction: like There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. I can of course change it back if you say so! There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. I like to think of the projection notation as a poor-man's binary operator, since it puts the word in infix position. For uniformity I also remove unnecessary parentheses in places like this. Part of my "what happened here" reaction was on the inclusion of strange extra spaces, though. |
||
end functor | ||
|
||
namespace nat_trans | ||
|
@@ -96,7 +91,7 @@ def prod {F G : A ↝ B} {H I : C ↝ D} (α : F ⟹ G) (β : H ⟹ I) : F.prod | |
{ app := λ X, (α X.1, β X.2), | ||
naturality := begin /- `obviously'` says: -/ intros, cases f, cases Y, cases X, dsimp at *, simp, split, rw naturality_lemma, rw naturality_lemma end } | ||
|
||
@[simp, ematch] lemma prod_app {F G : A ↝ B} {H I : C ↝ D} (α : F ⟹ G) (β : H ⟹ I) (a : A) (c : C) : α.prod β (a, c) = (α a, β c) := rfl | ||
@[simp, ematch] lemma prod_app {F G : A ↝ B} {H I : C ↝ D} (α : F ⟹ G) (β : H ⟹ I) (a : A) (c : C) : (nat_trans.prod α β) (a, c) = (α a, β c) := rfl | ||
end nat_trans | ||
|
||
end category_theory |
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,51 @@ | ||
-- Copyright (c) 2017 Scott Morrison. All rights reserved. | ||
-- Released under Apache 2.0 license as described in the file LICENSE. | ||
-- Authors: Stephen Morgan, Scott Morrison | ||
|
||
import .functor_category | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. No relative imports There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Fixed. |
||
|
||
namespace category_theory | ||
|
||
universes u v u' v' w | ||
|
||
instance types : large_category (Type u) := | ||
{ Hom := λ a b, (a → b), | ||
id := λ a, id, | ||
comp := λ _ _ _ f g, g ∘ f, | ||
id_comp := begin /- `obviously'` says: -/ intros, refl end, | ||
comp_id := begin /- `obviously'` says: -/ intros, refl end, | ||
assoc := begin /- `obviously'` says: -/ intros, refl end } | ||
|
||
@[simp] lemma types_Hom {α β : Type u} : (α ⟶ β) = (α → β) := rfl | ||
@[simp] lemma types_id {α : Type u} (a : α) : (𝟙 α : α → α) a = a := rfl | ||
@[simp] lemma types_comp {α β γ : Type u} (f : α → β) (g : β → γ) (a : α) : (((f : α ⟶ β) ≫ (g : β ⟶ γ)) : α ⟶ γ) a = g (f a) := rfl | ||
|
||
namespace functor_to_types | ||
variables {C : Type u} [𝒞 : category.{u v} C] (F G H : C ↝ (Type w)) {X Y Z : C} | ||
include 𝒞 | ||
variables (σ : F ⟹ G) (τ : G ⟹ H) | ||
|
||
@[simp,ematch] lemma map_comp (f : X ⟶ Y) (g : Y ⟶ Z) (a : F X) : (F.map (f ≫ g)) a = (F.map g) ((F.map f) a) := | ||
begin /- `obviously'` says: -/ simp end | ||
|
||
@[simp,ematch] lemma map_id (a : F X) : (F.map (𝟙 X)) a = a := | ||
begin /- `obviously'` says: -/ simp end | ||
|
||
@[ematch] lemma naturality (f : X ⟶ Y) (x : F X) : σ Y ((F.map f) x) = (G.map f) (σ X x) := | ||
congr_fun (σ.naturality_lemma f) x | ||
|
||
@[simp] lemma vcomp (x : F X) : (σ ⊟ τ) X x = τ X (σ X x) := rfl | ||
|
||
variables {D : Type u'} [𝒟 : category.{u' v'} D] (I J : D ↝ C) (ρ : I ⟹ J) {W : D} | ||
|
||
@[simp] lemma hcomp (x : (I ⋙ F) W) : (ρ ◫ σ) W x = (G.map (ρ W)) (σ (I W) x) := rfl | ||
|
||
end functor_to_types | ||
|
||
definition type_lift : (Type u) ↝ (Type (max u v)) := | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. I think this should just be called |
||
{ obj := λ X, ulift.{v} X, | ||
map := λ X Y f, λ x : ulift.{v} X, ulift.up (f x.down), | ||
map_id := begin /- `obviously'` says: -/ intros, apply funext, intros, ext, refl end, | ||
map_comp := begin /- `obviously'` says: -/ intros, refl end } | ||
|
||
end category_theory |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
this could be just
op
, protectedThere was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Done.